diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 5 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 5 | ||||
| -rw-r--r-- | src/rewrites.ml | 12 |
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 |