diff options
| -rw-r--r-- | editors/sail2-mode.el | 6 | ||||
| -rw-r--r-- | src/initial_check.ml | 8 | ||||
| -rw-r--r-- | src/latex.ml | 2 | ||||
| -rw-r--r-- | src/value.ml | 15 |
4 files changed, 25 insertions, 6 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index 0a0bbc8a..9eefa654 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -4,10 +4,10 @@ (add-to-list 'auto-mode-alist '("\\.sail\\'" . sail2-mode)) (defconst sail2-keywords - '("val" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" + '("val" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by" "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" - "overload" "cast" "sizeof" "constraint" "default" "assert" "newtype" - "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" + "overload" "cast" "sizeof" "constraint" "default" "assert" "newtype" "from" + "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield")) (defconst sail2-kinds diff --git a/src/initial_check.ml b/src/initial_check.ml index 06ee1f65..b8c70e57 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -220,7 +220,9 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown); Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown); Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);]) + Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);]) + | Parse_ast.ATyp_app (Parse_ast.Id_aux (Parse_ast.Id "int", il), [n]) -> + Typ_app(Id_aux(Id "atom", il), [Typ_arg_aux (Typ_arg_nexp (to_ast_nexp k_env n), Parse_ast.Unknown)]) | Parse_ast.ATyp_app(pid,typs) -> let id = to_ast_id pid in let k = Envmap.apply k_env (id_to_string id) in @@ -436,10 +438,12 @@ let rec to_ast_typ_pat (Parse_ast.ATyp_aux (typ_aux, l)) = match typ_aux with | Parse_ast.ATyp_wild -> TP_aux (TP_wild, l) | Parse_ast.ATyp_var kid -> TP_aux (TP_var (to_ast_var kid), l) + | Parse_ast.ATyp_app (Parse_ast.Id_aux (Parse_ast.Id "int", il), typs) -> + TP_aux (TP_app (Id_aux (Id "atom", il), List.map to_ast_typ_pat typs), l) | Parse_ast.ATyp_app (f, typs) -> TP_aux (TP_app (to_ast_id f, List.map to_ast_typ_pat typs), l) | _ -> typ_error l "Unexpected type in type pattern" None None None - + let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : unit pat = P_aux( (match pat with diff --git a/src/latex.ml b/src/latex.ml index f6aed63c..0375757c 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -86,7 +86,7 @@ let add_links str = let module StringSet = Set.Make(String) in let keywords = StringSet.of_list [ "function"; "forall"; "if"; "then"; "else"; "exit"; "return"; "match"; "vector"; - "assert"; "constraint"; "let"; "in"; "atom"; "range"; "throw"; "sizeof" ] + "assert"; "constraint"; "let"; "in"; "atom"; "range"; "throw"; "sizeof"; "foreach" ] in let fn = Str.matched_group 1 s in let spacing = Str.matched_group 2 s in diff --git a/src/value.ml b/src/value.ml index 2f8144b9..4b4f0865 100644 --- a/src/value.ml +++ b/src/value.ml @@ -340,6 +340,18 @@ let value_zero_extend = function | [v1; v2] -> mk_vector (Sail_lib.zero_extend (coerce_bv v1, coerce_int v2)) | _ -> failwith "value zero_extend" +let value_zeros = function + | [v] -> mk_vector (Sail_lib.zeros (coerce_int v)) + | _ -> failwith "value zeros" + +let value_shiftl = function + | [v1; v2] -> mk_vector (Sail_lib.shiftl (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value shiftl" + +let value_shiftr = function + | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2)) + | _ -> failwith "value shiftr" + let eq_value v1 v2 = string_of_value v1 = string_of_value v2 let value_eq_anything = function @@ -425,6 +437,9 @@ let primops = ("hex_slice", value_hex_slice); ("zero_extend", value_zero_extend); ("sign_extend", value_sign_extend); + ("zeros", value_zeros); + ("shiftr", value_shiftr); + ("shiftl", value_shiftl); ("add_int", value_add_int); ("sub_int", value_sub_int); ("mult", value_mult); |