diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ocaml_backend.ml | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 8 | ||||
| -rw-r--r-- | src/sail.ml | 7 | ||||
| -rw-r--r-- | src/type_check.ml | 1 |
4 files changed, 8 insertions, 9 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 31c3e093..3f34c422 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -128,6 +128,7 @@ let ocaml_typ_id ctx = function | id when Id.compare id (mk_id "list") = 0 -> string "list" | id when Id.compare id (mk_id "bit") = 0 -> string "bit" | id when Id.compare id (mk_id "int") = 0 -> string "Big_int.num" + | id when Id.compare id (mk_id "implicit") = 0 -> string "Big_int.num" | id when Id.compare id (mk_id "nat") = 0 -> string "Big_int.num" | id when Id.compare id (mk_id "bool") = 0 -> string "bool" | id when Id.compare id (mk_id "unit") = 0 -> string "unit" diff --git a/src/rewrites.ml b/src/rewrites.ml index 19294698..4b147aee 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -5147,9 +5147,6 @@ let rewrite_defs_ocaml = [ ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("top_sort_defs", top_sort_defs); - ("constraint", rewrite_constraint); - ("trivial_sizeof", rewrite_trivial_sizeof); - ("sizeof", rewrite_sizeof); ("simple_types", rewrite_simple_types); ("overload_cast", rewrite_overload_cast); (* ("separate_numbs", rewrite_defs_separate_numbs) *) @@ -5184,10 +5181,7 @@ let rewrite_defs_interpreter = [ ("rewrite_undefined", rewrite_undefined_if_gen false); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); - ("simple_assignments", rewrite_simple_assignments); - ("constraint", rewrite_constraint); - ("trivial_sizeof", rewrite_trivial_sizeof); - ("sizeof", rewrite_sizeof); + ("simple_assignments", rewrite_simple_assignments) ] let rewrite_check_annot = diff --git a/src/sail.ml b/src/sail.ml index fdf4f5b9..c63c3d19 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -64,7 +64,7 @@ let opt_print_c = ref false let opt_print_latex = ref false let opt_print_coq = ref false let opt_print_cgen = ref false -let opt_memo_z3 = ref false +let opt_memo_z3 = ref true let opt_sanity = ref false let opt_includes_c = ref ([]:string list) let opt_libs_lem = ref ([]:string list) @@ -202,7 +202,10 @@ let options = Arg.align ([ "<filename>:<line>:<variable> to case split for monomorphisation"); ( "-memo_z3", Arg.Set opt_memo_z3, - " memoize calls to z3, improving performance when typechecking repeatedly"); + " memoize calls to z3, improving performance when typechecking repeatedly (default)"); + ( "-no_memo_z3", + Arg.Clear opt_memo_z3, + " do not memoize calls to z3"); ( "-memo", Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); diff --git a/src/type_check.ml b/src/type_check.ml index 11fed096..82286491 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -473,6 +473,7 @@ end = struct List.fold_left (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) Bindings.empty [ ("range", [K_int; K_int]); ("atom", [K_int]); + ("implicit", [K_int]); ("vector", [K_int; K_order; K_type]); ("register", [K_type]); ("bit", []); |