Tweak intermediate language names for loop combinators to allow reparsing

This should produce identical Lem and Coq output, but allow dumped Sail
ASTs from the final stages of rewriting to be reread with -dmagic_hash.

3 files changed, 12 insertions, 10 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 501c610e..c321cb26 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1207,7 +1207,7 @@ let doc_exp, doc_let =
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "None", _) as none -> doc_id_ctor none
-       | Id_aux (Id "foreach", _) ->
+       | Id_aux (Id "foreach#", _) ->
           begin
             match args with
             | [from_exp; to_exp; step_exp; ord_exp; vartuple; body] ->
@@ -1254,7 +1254,8 @@ let doc_exp, doc_let =
           | _ -> raise (Reporting.err_unreachable l __POS__
              "Unexpected number of arguments for loop combinator")
           end
-       | Id_aux (Id (("while" | "until") as combinator), _) ->
+       | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+          let combinator = String.sub combinator 0 (String.length combinator - 1) in
           begin
             match args with
             | [cond; varstuple; body] ->
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index dee0a29f..3e7911fe 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -668,7 +668,7 @@ let doc_exp_lem, doc_let_lem =
           let call = doc_id_lem (append_id f "M") in
           wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
        (* temporary hack to make the loop body a function of the temporary variables *)
-       | Id_aux (Id "foreach", _) ->
+       | Id_aux (Id "foreach#", _) ->
           begin
             match args with
             | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
@@ -713,7 +713,8 @@ let doc_exp_lem, doc_let_lem =
           | _ -> raise (Reporting.err_unreachable l __POS__
             "Unexpected number of arguments for loop combinator")
           end
-       | Id_aux (Id (("while" | "until") as combinator), _) ->
+       | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+          let combinator = String.sub combinator 0 (String.length combinator - 1) in
           begin
             match args with
             | [cond; varstuple; body] ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 31117f33..e40b7387 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3826,7 +3826,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        let v =
          fix_eff_exp (annot_exp (E_let (lb_lower,
            fix_eff_exp (annot_exp (E_let (lb_upper,
-             fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body]))
+             fix_eff_exp (annot_exp (E_app (mk_id "foreach#", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body]))
                el env (typ_of exp4))))
              el env (typ_of exp4))))
            el env (typ_of exp4)) in
@@ -3842,8 +3842,8 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
         let body = rewrite_var_updates (add_vars overwrite body vars) in
         let (E_aux (_,(_,bannot))) = body in
         let fname = match loop with
-          | While -> "while"
-          | Until -> "until" in
+          | While -> "while#"
+          | Until -> "until#" in
         let funcl = Id_aux (Id fname,gen_loc el) in
         let v = E_aux (E_app (funcl,[cond;tuple_exp vars;body]), (gen_loc el, bannot)) in
         Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
@@ -4144,9 +4144,9 @@ let rewrite_defs_remove_superfluous_returns env =
 
 let rewrite_defs_remove_e_assign env (Defs defs) =
   let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
-    [("foreach", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
-     ("while", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
-     ("until", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
+    [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
+     ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
+     ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars")]))) in
   let rewrite_exp _ e =
     replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
   rewrite_defs_base