diff options
| author | Brian Campbell | 2019-02-15 18:09:33 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-02-15 18:21:09 +0000 |
| commit | a62061fd64d3fb8a31f115a3d059da4346a13d85 (patch) | |
| tree | 82875760d773a5a8ff13317340834021ef6ee3f2 /src/pretty_print_coq.ml | |
| parent | 18b38f6495ea8836f332e9b5da8525caac338e28 (diff) | |
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.
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 5 |
1 files changed, 3 insertions, 2 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] -> |