diff options
| -rw-r--r-- | editors/sail-mode.el | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 2 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 5 |
4 files changed, 7 insertions, 3 deletions
diff --git a/editors/sail-mode.el b/editors/sail-mode.el index 0d70b51e..5c1d1e07 100644 --- a/editors/sail-mode.el +++ b/editors/sail-mode.el @@ -46,7 +46,7 @@ (defconst sail2-special '("_prove" "_not_prove" "create" "kill" "convert" "undefined" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" - "$latex" "$property" "$counterexample" "$suppress_warnings")) + "$latex" "$property" "$counterexample" "$suppress_warnings" "$assert")) (defconst sail2-font-lock-keywords `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) diff --git a/src/process_file.ml b/src/process_file.ml index d2a86595..116788b9 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -108,6 +108,8 @@ let have_symbol symbol = let clear_symbols () = symbols := default_symbols +let add_symbol str = symbols := StringSet.add str !symbols + let cond_pragma l defs = let depth = ref 0 in let in_then = ref true in diff --git a/src/process_file.mli b/src/process_file.mli index d1fa2cb8..c9eb5e9e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -54,6 +54,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val clear_symbols : unit -> unit val have_symbol : string -> bool +val add_symbol : string -> unit val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/rewrites.ml b/src/rewrites.ml index 863f8115..e622d620 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2114,8 +2114,7 @@ let rewrite_tuple_assignments env defs = let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in let block = mk_exp (E_block (List.mapi block_assign lexps)) in - let letbind = mk_letbind (mk_pat (P_typ (Type_check.typ_of exp, - mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))))) + let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in let let_exp = mk_exp (E_let (letbind, block)) in @@ -5033,6 +5032,8 @@ let rewrites_c = [ ("pattern_literals", [Literal_arg "all"]); ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); + ("tuple_assignments", []); ("simple_assignments", []); ("exp_lift_assign", []); ("merge_function_clauses", []); |