Introduce a Sail library

Used by the Power XML extraction tool.

6 files changed, 42 insertions, 7 deletions

diff --git a/src/Makefile b/src/Makefile
index 8d3c1b9c..ce31ca6c 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -3,7 +3,7 @@
 all: sail lib power doc test
 
 sail:
-	ocamlbuild sail.native
+	ocamlbuild sail.native sail_lib.cma sail_lib.cmxa
 
 test: sail
 	ocamlbuild test/run_tests.native
diff --git a/src/initial_check.mli b/src/initial_check.mli
index fd9444da..feed37b8 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -8,3 +8,4 @@ type envs = Nameset.t * kind Envmap.t * tannot Envmap.t
 type 'a envs_out = 'a * envs
 
 val to_ast : Nameset.t -> kind Envmap.t -> tannot Envmap.t -> Parse_ast.defs -> tannot defs * kind Envmap.t
+val to_ast_exp : kind Envmap.t -> Parse_ast.exp -> Type_internal.tannot Ast.exp
diff --git a/src/lexer.mll b/src/lexer.mll
index 206df359..b53577c5 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -119,7 +119,8 @@ let kw_table =
 
 ]
 
-let type_names : string list ref = ref []
+let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "uint8";"uint16";"uint32";"uint64"]
+let custom_type_names : string list ref = ref []
 
 }
 
@@ -228,7 +229,9 @@ rule token = parse
   | tyvar_start startident ident* as i  { TyVar(r i) }
   | startident ident* as i              { if M.mem i kw_table then
                                             (M.find i kw_table) ()
-                                          else if List.mem i !type_names then
+                                          else if
+                                            List.mem i default_type_names ||
+                                            List.mem i !custom_type_names then
 					    TyId(r i)
                                           else Id(r i) }
   | "&" oper_char+ as i                 { (AmpI(r i)) }
diff --git a/src/parser.mly b/src/parser.mly
index e1647642..2ab911ee 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -163,7 +163,7 @@ let make_vector_sugar typ typ1 =
 %token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
 %token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
 
-%start file
+%start file exp
 %type <Parse_ast.defs> defs
 %type <Parse_ast.atyp> typ
 %type <Parse_ast.pat> pat
diff --git a/src/process_file.ml b/src/process_file.ml
index c2a977da..6d1729a5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -62,8 +62,6 @@ let get_lexbuf fn =
 
 let parse_file (f : string) : Parse_ast.defs =
   let scanbuf = get_lexbuf f in
-  let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat";
-  "uint8";"uint16";"uint32";"uint64"] in
   let type_names = 
     try
       Pre_parser.file Pre_lexer.token scanbuf
@@ -75,7 +73,7 @@ let parse_file (f : string) : Parse_ast.defs =
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
       | Lexer.LexError(s,p) ->
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in
-  let _ = Lexer.type_names := (default_type_names@type_names) in
+  let () = Lexer.custom_type_names := type_names in
   let lexbuf = get_lexbuf f in
     try
       Parser.file Lexer.token lexbuf
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
new file mode 100644
index 00000000..a0ef6a06
--- /dev/null
+++ b/src/sail_lib.ml
@@ -0,0 +1,33 @@
+(** A Sail library *)
+
+(* This library is not well-thought. It has grown driven by the need to
+ * reuse some components of Sail in the Power XML extraction tool. It
+ * should by no means by considered stable (hence the lack of mli
+ * interface file), and is not intended for general consumption. Use at
+ * your own risks. *)
+
+module Pretty = Pretty_print
+
+let parse_exp s =
+  let lexbuf = Lexing.from_string s in
+  try
+  let pre_exp = Parser.exp Lexer.token lexbuf in
+  Initial_check.to_ast_exp Type_internal.initial_kind_env pre_exp
+  with
+    | Parsing.Parse_error ->
+        let pos = Lexing.lexeme_start_p lexbuf in
+        let msg = Printf.sprintf "syntax error on character %d" pos.Lexing.pos_cnum in
+        failwith msg
+    | Parse_ast.Parse_error_locn(l,m) ->
+        let loc = match l with
+        | Parse_ast.Unknown -> "???"
+        | Parse_ast.Range(p1,p2) -> Printf.sprintf "%d:%d" p1.Lexing.pos_cnum p2.Lexing.pos_cnum
+        | Parse_ast.Int(s,_) -> Printf.sprintf "code generated by: %s" s in
+        let msg = Printf.sprintf "syntax error: %s %s" loc m in
+        failwith msg
+    | Lexer.LexError(s,p) ->
+        let msg = Printf.sprintf "lexing error: %s %d" s p.Lexing.pos_cnum in
+        failwith msg
+        
+
+