diff options
| author | Alasdair Armstrong | 2017-10-06 16:53:15 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-10-06 16:53:15 +0100 |
| commit | 6e4573f9a1ace7cba38d0cecb95b4dfe95c73c71 (patch) | |
| tree | 3284c9c20c1c6357894cc950362eec895df4ee36 /src/parser2.mly | |
| parent | 59d7781403f9f92cda4954b75d5116157f98ba84 (diff) | |
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.
Diffstat (limited to 'src/parser2.mly')
| -rw-r--r-- | src/parser2.mly | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/parser2.mly b/src/parser2.mly index 16e93a59..59db84a1 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -46,9 +46,9 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) open Parse_ast -let loc n m = Range (m, n) +let loc n m = Range (n, m) -let mk_id i n m = Id_aux (i, loc m n) +let mk_id i n m = Id_aux (i, loc n m) let mk_kid str n m = Kid_aux (Var str, loc n m) let id_of_kid = function @@ -434,16 +434,19 @@ typ8: | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} | typ9 { $1 } typ8l: | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} | typ9 { $1 } typ8r: | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} | typ9 { $1 } typ9: |