diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_sail2.ml | 4 | ||||
| -rw-r--r-- | src/process_file.ml | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index e354fe58..8c8b5661 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -194,6 +194,8 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = separate space [string "match"; doc_exp exp; doc_pexps pexps] | E_let (LB_aux (LB_val (pat, binding), _), exp) -> separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp] + | E_internal_let (lexp, binding, exp) -> + separate space [string "var"; doc_lexp lexp; equals; doc_exp binding; string "in"; doc_exp exp] | E_assign (lexp, exp) -> separate space [doc_lexp lexp; equals; doc_exp exp] | E_for (id, exp1, exp2, exp3, order, exp4) -> @@ -247,6 +249,8 @@ and doc_block = function | [] -> string "()" | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] -> separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps + | [E_aux (E_internal_let (lexp, binding, E_aux (E_block exps, _)), _)] -> + separate space [string "var"; doc_lexp lexp; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps | [exp] -> doc_exp exp | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps and doc_lexp (LEXP_aux (l_aux, _) as lexp) = diff --git a/src/process_file.ml b/src/process_file.ml index e4518837..92b3f328 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -210,7 +210,7 @@ let rewrite_step defs (name,rewriter) = | Some (f, i) -> begin let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in - output "" Lem_ast_out [filename, defs]; + (* output "" Lem_ast_out [filename, defs]; *) let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in Pretty_print_sail2.pp_defs ot defs; close_output_with_check ext_ot; |