Updates to latex mode for documentation

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);