add for loops and rust ranges (1..=7)

src/mlw/rust_printer.ml

@@ -31,17 +31,23 @@ module Rust = struct
 
   type var = ident * ty (* ref? mut? *)
 
+  type rs_or_syntax =
+    | RSrs of rsymbol
+    | RSsyn of string
+
   type expr =
     | Econst of string option * BigInt.t
     | Evar of pvsymbol
     | Eblock of expr list
-    | Ecall of string option * rsymbol * expr list
+    | Ecall of rs_or_syntax * expr list
     (* optional syntax, r(e1, ...) *)
     | Elet of pat * expr * expr (* let p = e1; e2 *)
     | Ematch of expr * branch list
     | Eif of expr * expr * expr
     | Eclosure of var list * expr
     | Ewhile of expr * expr
+    | Efor of pvsymbol * expr * expr (* for p in e1 {e2} *)
+    | Erange_inc of expr * expr (* inclusive range lo..=hi *)
     | Eunreachable
 
   and branch = pat * expr
@@ -80,7 +86,7 @@ module Rust = struct
         (match List.map clean_expr el with
         | [Eblock el'] -> clean_expr (Eblock el')
         | _ -> Eblock (List.map clean_expr el))
-    | Ecall (s, rs, el) -> Ecall (s, rs, (List.map clean_expr el))
+    | Ecall (s, el) -> Ecall (s, (List.map clean_expr el))
     | Elet (p, e1, e2) -> Elet (p, clean_expr e1, clean_expr e2)
     | Ematch (e, bl) ->
         let clean_bl = List.map (fun (p, e) -> (p, clean_expr e)) bl in
@@ -88,6 +94,8 @@ module Rust = struct
     | Eif (a, b, c) -> Eif (clean_expr a, clean_expr b, clean_expr c)
     | Eclosure (vl, e) -> Eclosure (vl, clean_expr e)
     | Ewhile (c, b) -> Ewhile (clean_expr c, clean_expr b)
+    | Efor (i, e1, e2) -> Efor (i, clean_expr e1, clean_expr e2)
+    | Erange_inc (l, h) -> Erange_inc (clean_expr l, clean_expr h)
 end
 
 type info = {
@@ -166,6 +174,13 @@ module MLToRust = struct
     | Pas (p, vs) -> Rust.Pat (vs, translate_pat info p)
     (* TODO pattern bindings are not allowed after @: l @ (a, b) *)
 
+  let is_mapped_to_bigint info ity =
+    match ity.ity_node with
+    | Ity.Ityapp ({ its_ts = ts }, _, _) ->
+        query_syntax info.syntax ts.ts_name = Some ("num::BigInt")
+        (* TODO use the same string as the driver *)
+    | _ -> false
+
   exception MissingSyntaxLiteral
 
   let rec translate_expr (info:info) (e:expr) : Rust.expr =
@@ -180,8 +195,11 @@ module MLToRust = struct
          | None -> raise MissingSyntaxLiteral) (* TODO exception with info *)
     | Evar pvs -> Rust.Evar pvs
     | Eapp (rs, el) ->
-        let s_opt = query_syntax info.syntax rs.rs_name in
-        Rust.Ecall (s_opt, rs, List.map (translate_expr info) el)
+        let el = List.map (translate_expr info) el in
+        (match query_syntax info.syntax rs.rs_name with
+        | Some (s) -> Rust.Ecall (RSsyn s, el)
+        | None -> Rust.Ecall (RSrs rs, el)
+        )
         (* TODO other cases, like struct constructors *)
     | Efun (argl, e) ->
         Rust.Eclosure (translate_vars info argl, translate_expr info e)
@@ -206,7 +224,16 @@ module MLToRust = struct
     | Eblock el -> Rust.Eblock (List.map (translate_expr info) el)
     | Ewhile (test, body) ->
         Rust.Ewhile (translate_expr info test, Rust.Eblock [(translate_expr info body)])
-    | Mltree.Efor (_, _, _, _, _) -> raise (TODO "Efor")
+    | Efor (pv1, pv2, dir, pv3, e) ->
+        let b = translate_expr info e in
+        let r = (match dir with
+        | Mltree.To -> Rust.Erange_inc (Rust.Evar pv2, Rust.Evar pv3)
+        | Mltree.DownTo ->
+            (* (pv3..pv2).rev() *)
+            let range = Rust.Erange_inc (Rust.Evar pv3, Rust.Evar pv2) in
+            Rust.Ecall(RSsyn "(%1).rev()", [range])
+        ) in
+        Rust.Efor (pv1, r, Rust.Eblock [b])
     | Mltree.Eraise (_, _) -> raise (TODO "Eraise")
     | Mltree.Eexn (_, _, _) -> raise (TODO "Eexn")
     | Mltree.Eignore _ -> raise (TODO "Eignore")
@@ -242,13 +269,15 @@ module MLToRust = struct
 (*     let map_and_union el = union_stv_list (List.map discover_lts_tvs_expr el) in *)
     (match e with
     | Rust.Econst _ | Rust.Evar _ | Rust.Eunreachable -> Slt.empty, Stv.empty
-    | Rust.Ecall (_, _, el) | Rust.Eblock el -> map_and_union el
+    | Rust.Ecall (_, el) | Rust.Eblock el -> map_and_union el
     | Rust.Elet (_, e1, e2) -> map_and_union [e1;e2]
     | Rust.Ematch (e, bl) ->
         let bel = List.map (fun (_, e) -> e) bl in
         map_and_union (e :: bel)
     | Rust.Eif (a, b, c) -> map_and_union [a;b;c]
     | Rust.Ewhile (t, b) -> map_and_union [t;b]
+    | Rust.Efor (i, r, b) -> map_and_union [r;b] (* FIXME what about i? *)
+    | Rust.Erange_inc (l, h) -> map_and_union [l;h]
     | Rust.Eclosure (vl, e) ->
 (*         let v_stv = union_stv_list (List.map (fun (_, t) -> discover_lts_tvs_ty t) vl) in *)
         let sl = List.map (fun (_, t) -> discover_lts_tvs_ty t) vl in
@@ -469,6 +498,7 @@ module Print = struct
         end
     | Ttuple tl -> fprintf fmt "(%a)" (print_list comma (print_ty info)) tl
     | Tfn (argl, res) ->
+        (* FIXME bad output when args or result is Tfn *)
         fprintf fmt "impl FnMut(%a) -> %a"
           (print_list comma (print_ty info)) argl
           (print_ty info) res
@@ -510,10 +540,10 @@ module Print = struct
     | Evar pv -> print_pv info fmt pv
     | Eblock el ->
         fprintf fmt "@[<hov 2>{@\n%a@]@\n}" (print_list semi (print_expr info)) el
-    | Ecall (s_opt, rs, el) ->
-        (match s_opt with
-        | Some s -> syntax_arguments s (print_expr info) fmt el
-        | None -> fprintf fmt "%a(@[%a@])" (print_rs info) rs
+    | Ecall (rs_or_syn, el) ->
+        (match rs_or_syn with
+        | RSsyn s -> syntax_arguments s (print_expr info) fmt el
+        | RSrs rs -> fprintf fmt "%a(@[%a@])" (print_rs info) rs
           (print_list comma (print_expr info)) el)
     | Elet (pat, e, e_after) ->
         fprintf fmt "let@ %a@ =@ @[%a@];@\n%a" (print_pat info) pat
@@ -534,8 +564,16 @@ module Print = struct
         fprintf fmt "@[<hov 2>if %a {@\n%a@]@\n@[<hov 2>} else {@\n%a@]@\n}@\n"
           (print_expr info) c (print_expr info) e1 (print_expr info) e2
     | Ewhile (t, b) ->
-        fprintf fmt "while %a@ %a"
-          (print_expr info) t (print_expr info) b
+        fprintf fmt "while %a@ %a" (print_expr info) t (print_expr info) b
+    | Efor (p, r, b) ->
+(*      TODO special case when p is a bigint:
+        if is_mapped_to_bigint info p.pv_ity then ?? else ??
+*)
+        fprintf fmt "for %a in %a@ %a" (print_pv info) p
+          (print_expr info) r (print_expr info) b
+    | Erange_inc (lo, hi) ->
+        (* TODO special case for bigint *)
+        fprintf fmt "%a..%a" (print_expr info) lo (print_expr info) hi
     | Eclosure (args, e) ->
         fprintf fmt "@[<hov 2>|%a| {@\n%a@]@\n}\n"
           (print_list comma (print_arg info)) args