From 62f7179d0d160439f87d80bc591bddf50bb295fb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 18 Jun 2019 17:06:53 +0100 Subject: Rewriting improvements for monomorphic aarch64_small - allow disjoint_pat to be used on patterns that have just been introduced by the rewrite without rechecking - don't rebuild the matched expression in the generated fallthrough case (or any wildcard fall-through) - it may be dead code and generate badly typed Lem - update the type environment passed to rewrites whenever type checking is performed; stale information broke some rewrites --- src/isail.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/isail.ml') diff --git a/src/isail.ml b/src/isail.ml index 9e9b6236..88408dcd 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -302,7 +302,8 @@ let rec describe_rewrite = | String_rewriter rw -> "" :: describe_rewrite (rw "") | Bool_rewriter rw -> "" :: describe_rewrite (rw false) | Literal_rewriter rw -> "(ocaml|lem|all)" :: describe_rewrite (rw (fun _ -> true)) - | Basic_rewriter rw -> [] + | Basic_rewriter _ + | Checking_rewriter _ -> [] type session = { id : string; @@ -592,7 +593,9 @@ let handle_input' input = failwith "Must provide the name of a rewrite, use :list_rewrites for a list of possible rewrites" end | ":rewrites" -> - Interactive.ast := Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast; + let new_ast, new_env = Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast in + Interactive.ast := new_ast; + Interactive.env := new_env; interactive_state := initial_state !Interactive.ast !Interactive.env Value.primops | ":prover_regstate" -> let env, ast = prover_regstate (Some arg) !Interactive.ast !Interactive.env in -- cgit v1.2.3