Added additional utility functions in ast_util

Also fixed basic ocaml test suite

4 files changed, 37 insertions, 2 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2f630021..46c79764 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -70,6 +70,14 @@ let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
 
 let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, pat, body), no_annot)
 
+let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown)
+
+let mk_qi_id bk kid =
+  let kopt =
+    KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (bk, Parse_ast.Unknown)], Parse_ast.Unknown), kid), Parse_ast.Unknown)
+  in
+  QI_aux (QI_id kopt, Parse_ast.Unknown)
+
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
   let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
@@ -155,6 +163,8 @@ let range_typ nexp1 nexp2 =
 let bool_typ = mk_id_typ (mk_id "bool")
 let string_typ = mk_id_typ (mk_id "string")
 let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
+let tuple_typ typs = mk_typ (Typ_tup typs)
+let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff))
 
 let vector_typ n m ord typ =
   mk_typ (Typ_app (mk_id "vector",
@@ -173,6 +183,7 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
 let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
 let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
 
+let nc_set kid ints = mk_nc (NC_nat_set_bounded (kid, ints))
 let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
 let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
 let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
@@ -297,6 +308,10 @@ let string_of_id = function
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
+let kid_of_id = function
+  | Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l)
+  | Id_aux (DeIid v, _) -> assert false
+
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 246e0ebd..33d65ede 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -60,6 +60,8 @@ val mk_funcl : id -> unit pat -> unit exp -> unit funcl
 val mk_fundef : (unit funcl) list -> unit def
 val mk_val_spec : val_spec_aux -> unit def
 val mk_typschm : typquant -> typ -> typschm
+val mk_qi_id : base_kind_aux -> kid -> quant_item
+val mk_qi_nc : n_constraint -> quant_item
 val mk_fexp : id -> unit exp -> unit fexp
 val mk_fexps : (unit fexp) list -> unit fexps
 val mk_letbind : unit pat -> unit exp -> unit letbind
@@ -94,6 +96,8 @@ val real_typ : typ
 val vector_typ : nexp -> nexp -> order -> typ -> typ
 val list_typ : typ -> typ
 val exc_typ : typ
+val tuple_typ : typ list -> typ
+val function_typ : typ -> typ -> effect -> typ
 
 val no_effect : effect
 val mk_effect : base_effect_aux list -> effect
@@ -120,6 +124,7 @@ val nc_and : n_constraint -> n_constraint -> n_constraint
 val nc_or : n_constraint -> n_constraint -> n_constraint
 val nc_true : n_constraint
 val nc_false : n_constraint
+val nc_set : kid -> int list -> n_constraint
 
 val quant_items : typquant -> quant_item list
 
@@ -164,6 +169,7 @@ val string_of_index_range : index_range -> string
 val id_of_fundef : 'a fundef -> id
 
 val id_of_kid : kid -> id
+val kid_of_id : id -> kid
 
 val prepend_id : string -> id -> id
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 0e1928dd..f89ff0d3 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -72,6 +72,7 @@ type type_error =
   | Err_no_casts of type_error * type_error list
   | Err_unresolved_quants of id * quant_item list
   | Err_subtype of typ * typ * n_constraint list
+  | Err_no_num_ident of id
   | Err_other of string
 
 let pp_type_error err =
@@ -92,6 +93,8 @@ let pp_type_error err =
                         string (string_of_typ typ2) ]
        ^/^ string "in context"
        ^//^ string (string_of_list ", " string_of_n_constraint constrs)
+    | Err_no_num_ident id ->
+       string "No num identifier" ^^ space ^^ string (string_of_id id)
     | Err_other str -> string str
   in
   pp_err err
@@ -770,7 +773,7 @@ end = struct
 
   let get_num_def id env =
     try Bindings.find id env.num_defs with
-    | Not_found -> typ_error (id_loc id) ("No Num identifier " ^ string_of_id id)
+    | Not_found -> typ_raise (id_loc id) (Err_no_num_ident id)
 
   let rec wf_constraint env (NC_aux (nc, _)) =
     match nc with
diff --git a/src/type_check.mli b/src/type_check.mli
index ca2fb90c..6073913b 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -47,10 +47,17 @@ open Ast_util
 val opt_tc_debug : int ref
 val opt_no_effects : bool ref
 
-type type_error
+type type_error =
+  | Err_no_casts of type_error * type_error list
+  | Err_unresolved_quants of id * quant_item list
+  | Err_subtype of typ * typ * n_constraint list
+  | Err_no_num_ident of id
+  | Err_other of string
 
 exception Type_error of l * type_error;;
 
+val string_of_type_error : type_error -> string
+
 type mut = Immutable | Mutable
 
 type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
@@ -249,4 +256,8 @@ Some invariants that will hold of a fully checked AST are:
    for them to have type annotations. *)
 val check : Env.t -> 'a defs -> tannot defs * Env.t
 
+(* Like check but throws type_errors rather than Sail generic errors
+   from Reporting_basic. *)
+val check' : Env.t -> 'a defs -> tannot defs * Env.t
+
 val initial_env : Env.t