Various improvements to menhir parser, and performance improvments for Z3 calls

New option -memo_z3 memoizes calls to the Z3 solver, and saves these
results between calls to sail. This greatly increases the performance
of sail when re-checking large specifications by about an order of
magnitude. For example:

time sail -no_effects prelude.sail aarch64_no_vector.sail

real	0m4.391s
user	0m0.856s
sys	0m0.464s

After running with -memo_z3 once, running again gives:

time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail

real	0m0.457s
user	0m0.448s
sys	0m0.008s

Both the old and the new parser should now have better error messages
where the location of the parse error is displayed visually in the
error message and highlighted.

1 files changed, 15 insertions, 8 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 0f789c9d..1749bc03 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -82,13 +82,16 @@ let parse_file (f : string) : Parse_ast.defs =
       in
       close_in in_chan; ast
     with
-      | Parsing.Parse_error ->
-          let pos = Lexing.lexeme_start_p lexbuf in
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
-      | Parse_ast.Parse_error_locn(l,m) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
-      | Lexer.LexError(s,p) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
+    | Parser2.Error ->
+       let pos = Lexing.lexeme_start_p lexbuf in
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information")))
+    | Parsing.Parse_error ->
+       let pos = Lexing.lexeme_start_p lexbuf in
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
+    | Parse_ast.Parse_error_locn(l,m) ->
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
+    | Lexer.LexError(s,p) ->
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
 let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs
 
@@ -237,7 +240,11 @@ let rewrite_step defs rewriter =
     | _ -> () in
   defs
 
-let rewrite rewriters defs = List.fold_left rewrite_step defs rewriters
+let rewrite rewriters defs =
+  try List.fold_left rewrite_step defs rewriters with
+  | Type_check.Type_error (_, err) ->
+     prerr_endline (Type_check.string_of_type_error err);
+     exit 1
 
 let rewrite_ast = rewrite [Rewriter.rewrite_defs]
 let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem