Added records to checker

Added the following constructs to the new type checker:

* Added records, and record field accessors

* Added assert statements

* Added nondet blocks

* More simple flow typing tests

17 files changed, 565 insertions, 26 deletions

diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index adbba115..6230f289 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -45,7 +45,7 @@ open Ast
 open Util
 open Big_int
 
-let debug = ref 2
+let debug = ref 1
 let depth = ref 0
 
 let rec indent n = match n with
@@ -81,6 +81,7 @@ and map_exp_annot_aux f = function
   | E_sizeof nexp -> E_sizeof nexp
   | E_exit exp -> E_exit (map_exp_annot f exp)
   | E_return exp -> E_return (map_exp_annot f exp)
+  | E_assert (test, msg) -> E_assert (map_exp_annot f test, map_exp_annot f msg)
   | E_field (exp, id) -> E_field (map_exp_annot f exp, id)
   | E_vector exps -> E_vector (List.map (map_exp_annot f) exps)
   | E_vector_access (exp1, exp2) -> E_vector_access (map_exp_annot f exp1, map_exp_annot f exp2)
@@ -502,18 +503,27 @@ let string_of_index_sort = function
 type flow_typ = typ -> typ
 
 type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
+(*
+type fn = Accessor of typquant * typ | Fn of typquant * typ
 
+let to_bind = function
+  | Accessor (typq, typ) -> typq, typ
+  | Fn (typq, typ) -> typq, typ
+ *)
 module Env : sig
   type t
-  val get_val_spec : id -> t -> typquant * typ
   val add_val_spec : id -> typquant * typ -> t -> t
-  (* val get_local : id -> t -> mut * typ *)
+  val get_val_spec : id -> t -> typquant * typ
+  val add_record : id -> typquant -> (typ * id) list -> t -> t
+  val is_record : id -> t -> bool
+  val get_accessor : id -> t -> typquant * typ
   val add_local : id -> mut * typ -> t -> t
   val add_flow : id -> (typ -> typ) -> t -> t
   val get_flow : id -> t -> typ -> typ
   val get_register : id -> t -> typ
   val add_register : id -> typ -> t -> t
   val add_regtyp : id -> int -> int -> (index_range * id) list -> t -> t
+  val is_regtyp : id -> t -> bool
   val get_regtyp : id -> t -> int * int * (index_range * id) list
   val is_mutable : id -> t -> bool
   val get_constraints : t -> n_constraint list
@@ -534,6 +544,7 @@ module Env : sig
   val allow_casts : t -> bool
   val no_casts : t -> t
   val add_cast : id -> t -> t
+  (* val lookup_fn : id -> t -> fn *)
   val lookup_id : id -> t -> lvar
   val fresh_kid : t -> kid
   val expand_synonyms : t -> typ -> typ
@@ -549,6 +560,8 @@ end = struct
       overloads : (id list) Bindings.t;
       flow : flow_typ Bindings.t;
       enums : IdSet.t Bindings.t;
+      records : (typquant * (typ * id) list) Bindings.t;
+      accessors : (typquant * typ) Bindings.t;
       casts : id list;
       allow_casts : bool;
       constraints : n_constraint list;
@@ -566,6 +579,8 @@ end = struct
       overloads = Bindings.empty;
       flow = Bindings.empty;
       enums = Bindings.empty;
+      records = Bindings.empty;
+      accessors = Bindings.empty;
       casts = [];
       allow_casts = true;
       constraints = [];
@@ -609,6 +624,7 @@ end = struct
   (* FIXME: Add an IdSet for builtin types *)
   let bound_typ_id env id =
     Bindings.mem id env.typ_synonyms
+    || Bindings.mem id env.records
     || Bindings.mem id env.regtyps
     || Bindings.mem id env.enums
     || Id.compare id (mk_id "range") = 0
@@ -685,6 +701,29 @@ end = struct
         { env with enums = Bindings.add id (IdSet.of_list ids) env.enums }
       end
 
+  let is_record id env = Bindings.mem id env.records
+
+  let add_record id typq fields env =
+    if bound_typ_id env id
+    then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
+    else
+      begin
+        typ_print ("Adding record " ^ string_of_id id);
+        let fold_accessors accs (typ, fid) =
+          let acc_typ = mk_typ (Typ_fn (mk_id_typ id, typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          typ_print (indent 1 ^ "Adding accessor " ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ));
+          Bindings.add fid (typq, acc_typ) accs
+        in
+        { env with records = Bindings.add id (typq, fields) env.records;
+                   accessors = List.fold_left fold_accessors env.accessors fields }
+      end
+
+  let get_accessor id env =
+    let freshen_bind bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in
+    try freshen_bind (Bindings.find id env.accessors)
+    with
+    | Not_found -> typ_error (id_loc id) ("No accessor found for " ^ string_of_id id)
+
   let is_mutable id env =
     try
       let (mut, _) = Bindings.find id env.locals in
@@ -773,6 +812,8 @@ end = struct
         { env with regtyps = Bindings.add id (base, top, ranges) env.regtyps }
       end
 
+  let is_regtyp id env = Bindings.mem id env.regtyps
+
   let get_regtyp id env =
     try Bindings.find id env.regtyps with
     | Not_found -> typ_error (id_loc id) (string_of_id id ^ " is not a register type")
@@ -795,8 +836,19 @@ end = struct
               | Not_found -> Unbound
             end
        end
-
-   let add_typ_var kid k env =
+(*
+  let lookup_fn id env =
+    let freshen_bind bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in
+    try let typq, typ = freshen_bind (Bindings.find id env.top_val_specs) in Fn (typq, typ)
+    with
+    | Not_found ->
+       begin
+         try let typq, typ = freshen_bind (Bindings.find id env.accessors) in Accessor (typq, typ)
+         with
+         | Not_found -> typ_error (id_loc id) ("No function found for " ^ string_of_id id)
+       end
+ *)
+  let add_typ_var kid k env =
     if KBindings.mem kid env.typ_vars
     then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
     else
@@ -839,7 +891,7 @@ end = struct
     then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
     else
       begin
-        typ_debug ("Adding typ synonym " ^ string_of_id id);
+        typ_debug ("Adding type synonym " ^ string_of_id id);
         { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms }
       end
 
@@ -946,14 +998,6 @@ and string_of_tnf_arg = function
   | Tnf_arg_order o -> string_of_order o
   | Tnf_arg_effect eff -> string_of_effect eff
 
-let index_sort_intersect is1 is2 =
-  match is1, is2 with
-  | IS_int, _ -> is2
-  | _, IS_int -> is1
-  | IS_prop (kid1, cs1), IS_prop (kid2, cs2) ->
-     let cs2 = props_subst kid2 (Nexp_var kid1) cs2 in
-     IS_prop (kid1, cs1 @ cs2)
-
 let rec normalize_typ env (Typ_aux (typ, l)) =
   match typ with
   | Typ_wild -> Tnf_wild
@@ -1417,10 +1461,11 @@ let restrict_range_lower c1 (Typ_aux (typ_aux, l) as typ) =
 
 type flow_constraint =
   | Flow_lteq of int
-(* | Flow_gteq of int *)
+  | Flow_gteq of int
 
 let apply_flow_constraint = function
   | Flow_lteq c -> (restrict_range_upper c, restrict_range_lower (c + 1))
+  | Flow_gteq c -> (restrict_range_lower c, restrict_range_upper (c - 1))
 
 let rec infer_flow env (E_aux (exp_aux, (l, _))) =
   match exp_aux with
@@ -1428,6 +1473,22 @@ let rec infer_flow env (E_aux (exp_aux, (l, _))) =
      let kid = Env.fresh_kid env in
      let c = destructure_atom (typ_of y) in
      [(v, Flow_lteq (c - 1))]
+  | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" ->
+     let kid = Env.fresh_kid env in
+     let c = destructure_atom (typ_of y) in
+     [(v, Flow_lteq c)]
+  | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gt_range_atom" ->
+     let kid = Env.fresh_kid env in
+     let c = destructure_atom (typ_of y) in
+     [(v, Flow_gteq (c + 1))]
+  | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" ->
+     let kid = Env.fresh_kid env in
+     let c = destructure_atom (typ_of y) in
+     [(v, Flow_gteq c)]
+       (*
+  | E_app (f, [exp1; exp2]) when string_of_id f = "bool_and" ->
+     infer_flow env exp1 @ infer_flow env exp2
+        *)
   | _ -> []
 
 let rec add_flows b flows env =
@@ -1668,7 +1729,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
          | _ -> typ_error l "l-expression field is not a register"
        in
        match Env.expand_synonyms env regtyp with
-       | Typ_aux (Typ_id regtyp_id, _) ->
+       | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env ->
           let base, top, ranges = Env.get_regtyp regtyp_id env in
           let range, _ =
             try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
@@ -1764,6 +1825,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
 and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
   match exp_aux with
+  | E_nondet exps ->
+     annot_exp (E_nondet (List.map (fun exp -> check_exp env exp unit_typ) exps)) unit_typ
   | E_id v ->
      begin
        match Env.lookup_id v env with
@@ -1782,7 +1845,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      begin
        let inferred_exp = infer_exp env exp in
        match Env.expand_synonyms env (typ_of inferred_exp) with
-       | Typ_aux (Typ_id regtyp, _) ->
+       (* Accessing a (bit) field of a register *)
+       | Typ_aux (Typ_id regtyp, _) when Env.is_regtyp regtyp env ->
           let base, top, ranges = Env.get_regtyp regtyp env in
           let range, _ =
             try List.find (fun (_, id) -> Id.compare id field = 0) ranges with
@@ -1796,9 +1860,17 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
             | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) ->
                let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) (mk_typ (Typ_id (mk_id "bit"))) in
                annot_exp (E_field (inferred_exp, field)) vec_typ
-            | _, _ -> typ_error l "Not implemented this register field type yet..."
+            | _, _ -> typ_error l "Not implemented this register field type yet..." (* FIXME *)
+          end
+       (* Accessing a field of a record *)
+       | Typ_aux (Typ_id rectyp, _) as typ when Env.is_record rectyp env ->
+          begin
+            let inferred_acc = infer_funapp' l (Env.no_casts env) field (Env.get_accessor field env) [strip_exp inferred_exp] None in
+            match inferred_acc with
+            | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc)
+            | _ -> assert false (* Unreachable *)
           end
-       | _ ->  typ_error l ("Field expression " ^ string_of_exp exp ^ " :: " ^ string_of_typ (typ_of inferred_exp) ^ " is not a register type")
+       | _ ->  typ_error l ("Field expression " ^ string_of_exp exp ^ " :: " ^ string_of_typ (typ_of inferred_exp) ^ " is not valid")
      end
   | E_tuple exps ->
      let inferred_exps = List.map (irule infer_exp env) exps in
@@ -1822,8 +1894,9 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
   | E_app (f, xs) -> infer_funapp l env f xs None
   | E_if (cond, then_branch, else_branch) ->
      let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
-     let then_branch' = irule infer_exp env then_branch in
-     let else_branch' = crule check_exp env else_branch (typ_of then_branch') in
+     let flows = infer_flow env cond' in
+     let then_branch' = irule infer_exp (add_flows true flows env) then_branch in
+     let else_branch' = crule check_exp (add_flows false flows env) else_branch (typ_of then_branch') in
      annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch')
   | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ())))
   | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "vector_append", [v1; v2]), (l, ())))
@@ -1847,9 +1920,16 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
                             mk_typ_arg (Typ_arg_typ (typ_of inferred_item))]))
      in
      annot_exp (E_vector (inferred_item :: checked_items)) vec_typ
+  | E_assert (test, msg) ->
+     let checked_test = check_exp env test bool_typ in
+     let checked_msg = check_exp env msg string_typ in
+     annot_exp (E_assert (checked_test, checked_msg)) unit_typ
   | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp)
 
-and infer_funapp l env f xs ret_ctx_typ =
+and infer_funapp l env f xs ret_ctx_typ = infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ
+
+and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
+
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
   let rec number n = function
     | [] -> []
@@ -1869,7 +1949,7 @@ and infer_funapp l env f xs ret_ctx_typ =
            let iuargs = List.map2 (fun utyp (n, uarg) -> (n, crule check_exp env uarg utyp)) utyps uargs in
            (iuargs, ret_typ)
          else typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
-                           ^ " not resolved during function application of " ^ string_of_id f)
+                           ^ " not resolved during application of " ^ string_of_id f)
        end
     | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args)) ->
        begin
@@ -1906,7 +1986,6 @@ and infer_funapp l env f xs ret_ctx_typ =
          (quants', typs', ret_typ')
        end
   in
-  let (typq, f_typ) = Env.get_val_spec f env in
   match f_typ with
   | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, effs), _) ->
      let (quants, typ_args, typ_ret) = instantiate_ret (quant_items typq) typ_args typ_ret in
@@ -1918,7 +1997,7 @@ and infer_funapp l env f xs ret_ctx_typ =
      let (xs_instantiated, typ_ret) = instantiate quants ([], typ_args) typ_ret ([], number 0 xs) in
      let xs_reordered = List.map snd (List.sort (fun (n, _) (m, _) -> compare n m) xs_instantiated) in
      annot_exp (E_app (f, xs_reordered)) typ_ret
-  | _ -> typ_error l (string_of_id f ^ " is not a function")
+  | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type")
 
 let check_letdef env (LB_aux (letbind, (l, _))) =
   begin
@@ -2025,7 +2104,8 @@ let check_typedef env (TD_aux (tdef, (l, _))) =
   match tdef with
   | TD_abbrev(id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
      DEF_type (TD_aux (tdef, (l, None))), Env.add_typ_synonym id (fun _ -> typ) env
-  | TD_record(id, nmscm, typq, fields, _) -> td_err ()
+  | TD_record(id, nmscm, typq, fields, _) ->
+     DEF_type (TD_aux (tdef, (l, None))), Env.add_record id typq fields env
   | TD_variant(id, nmscm, typq, arms, _) -> td_err ()
   | TD_enum(id, nmscm, ids, _) ->
      DEF_type (TD_aux (tdef, (l, None))), Env.add_enum id ids env
diff --git a/test/typecheck/fail/flow_gt1.sail b/test/typecheck/fail/flow_gt1.sail
new file mode 100644
index 00000000..917793cd
--- /dev/null
+++ b/test/typecheck/fail/flow_gt1.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x > 31)
+  then x - 33
+  else x + 32
+}
diff --git a/test/typecheck/fail/flow_gt2.sail b/test/typecheck/fail/flow_gt2.sail
new file mode 100644
index 00000000..f5ea4978
--- /dev/null
+++ b/test/typecheck/fail/flow_gt2.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x > 31)
+  then x - 32
+  else x + 33
+}
diff --git a/test/typecheck/fail/flow_gteq1.sail b/test/typecheck/fail/flow_gteq1.sail
new file mode 100644
index 00000000..b55647d3
--- /dev/null
+++ b/test/typecheck/fail/flow_gteq1.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x >= 32)
+  then x - 33
+  else x + 32
+}
diff --git a/test/typecheck/fail/flow_gteq2.sail b/test/typecheck/fail/flow_gteq2.sail
new file mode 100644
index 00000000..9d0a6201
--- /dev/null
+++ b/test/typecheck/fail/flow_gteq2.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x >= 32)
+  then x - 32
+  else x + 33
+}
diff --git a/test/typecheck/fail/flow_lteq1.sail b/test/typecheck/fail/flow_lteq1.sail
new file mode 100644
index 00000000..3bebcc97
--- /dev/null
+++ b/test/typecheck/fail/flow_lteq1.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x <= 32)
+  then x + 32
+  else x - 33
+}
diff --git a/test/typecheck/fail/flow_lteq2.sail b/test/typecheck/fail/flow_lteq2.sail
new file mode 100644
index 00000000..c3ee9c0a
--- /dev/null
+++ b/test/typecheck/fail/flow_lteq2.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x <= 32)
+  then x + 31
+  else x - 34
+}
diff --git a/test/typecheck/fail/nondet.sail b/test/typecheck/fail/nondet.sail
new file mode 100644
index 00000000..bce110c6
--- /dev/null
+++ b/test/typecheck/fail/nondet.sail
@@ -0,0 +1,10 @@
+
+register int z
+
+function int test () = {
+  nondet {
+    z := 0;
+    z := 1;
+    z
+  }
+}
diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail
new file mode 100644
index 00000000..be897021
--- /dev/null
+++ b/test/typecheck/pass/add_vec_lit.sail
@@ -0,0 +1,10 @@
+default Order inc
+
+val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec"
+val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add_range"
+
+val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure cast_vec_range
+
+overload (deinfix +) [add_vec; add_range]
+
+let (range<0,30>) x = 0xF + 0x2
diff --git a/test/typecheck/pass/arm_types.sail b/test/typecheck/pass/arm_types.sail
new file mode 100644
index 00000000..d7244beb
--- /dev/null
+++ b/test/typecheck/pass/arm_types.sail
@@ -0,0 +1,140 @@
+
+typedef boolean = enumerate {FALSE; TRUE}
+
+typedef signal = enumerate {LOW; HIGH}
+
+typedef __RetCode =
+  enumerate {__RC_OK;
+  __RC_UNDEFINED;
+  __RC_UNPREDICTABLE;
+  __RC_SEE;
+  __RC_IMPLEMENTATION_DEFINED;
+  __RC_SUBARCHITECTURE_DEFINED;
+  __RC_EXCEPTION_TAKEN;
+  __RC_ASSERT_FAILED;
+  __RC_UNMATCHED_CASE}
+
+typedef TUBE_Type = bit[32]
+
+typedef ScheduleIRQ_Type = bit[32]
+
+typedef ClearIRQ_Type = bit[32]
+
+typedef ScheduleFIQ_Type = bit[32]
+
+typedef ClearFIQ_Type = bit[32]
+
+typedef TargetCPU_Type = bit[32]
+
+typedef AbortRgn64Lo1_Type = bit[32]
+
+typedef AbortRgn64Lo1_Hi_Type = bit[32]
+
+typedef AbortRgn64Hi1_Type = bit[32]
+
+typedef AbortRgn64Hi1_Hi_Type = bit[32]
+
+typedef AbortRgn64Lo2_Type = bit[32]
+
+typedef AbortRgn64Lo2_Hi_Type = bit[32]
+
+typedef AbortRgn64Hi2_Type = bit[32]
+
+typedef AbortRgn64Hi2_Hi_Type = bit[32]
+
+typedef AXIAbortCtl_Type = bit[32]
+
+typedef GTE_API_Type = bit[32]
+
+typedef GTE_API_PARAM_Type = bit[32]
+
+typedef GTE_API_STATUS_Type = bit[32]
+
+typedef PPURBAR_Type = bit[32]
+
+typedef PPURSER_Type = bit[32]
+
+typedef PPURACR_Type = bit[32]
+
+typedef GTE_API_STATUS_64_Type = bit[32]
+
+typedef GTE_API_STATUS_64_HI_Type = bit[32]
+
+typedef GTE_API_PARAM_64_Type = bit[32]
+
+typedef GTE_API_PARAM_64_HI_Type = bit[32]
+
+typedef MemAtomicOp =
+  enumerate {MemAtomicOp_ADD;
+  MemAtomicOp_BIC;
+  MemAtomicOp_EOR;
+  MemAtomicOp_ORR;
+  MemAtomicOp_SMAX;
+  MemAtomicOp_SMIN;
+  MemAtomicOp_UMAX;
+  MemAtomicOp_UMIN;
+  MemAtomicOp_SWP}
+
+typedef SCRType = bit[32]
+
+typedef SCTLRType = bit[32]
+
+typedef MAIRType = bit[64]
+
+typedef ESRType = bit[32]
+
+typedef FPCRType = bit[32]
+
+typedef FPSRType = bit[32]
+
+typedef FPSCRType = bit[32]
+
+typedef CPSRType = bit[32]
+
+typedef APSRType = bit[32]
+
+typedef ITSTATEType = bit[8]
+
+typedef CPACRType = bit[32]
+
+typedef CNTKCTLType = bit[32]
+
+typedef GTEParamType = enumerate {GTEParam_WORD; GTEParam_LIST; GTEParam_EOACCESS}
+
+typedef GTE_PPU_SizeEn_Type = bit[32]
+
+typedef GTEExtObsAccess_Type = bit[16]
+
+typedef GTEASAccess_Type = bit[32]
+
+typedef GTEASRecordedAccess_Type = bit[32]
+
+typedef AccType =
+  enumerate {AccType_NORMAL;
+  AccType_VEC;
+  AccType_STREAM;
+  AccType_VECSTREAM;
+  AccType_ATOMIC;
+  AccType_ORDERED;
+  AccType_UNPRIV;
+  AccType_IFETCH;
+  AccType_PTW;
+  AccType_DC;
+  AccType_IC;
+  AccType_DCZVA;
+  AccType_AT}
+
+typedef MemType = enumerate {MemType_Normal; MemType_Device}
+
+typedef DeviceType =
+  enumerate {DeviceType_GRE; DeviceType_nGRE; DeviceType_nGnRE; DeviceType_nGnRnE}
+
+typedef MemAttrHints = const struct {bit[2] attrs; bit[2] hints; bool transient;}
+
+typedef MemoryAttributes =
+  const struct {MemType type;
+  DeviceType device;
+  MemAttrHints inner;
+  MemAttrHints outer;
+  bool shareable;
+  bool outershareable;}
diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail
new file mode 100644
index 00000000..acfbab68
--- /dev/null
+++ b/test/typecheck/pass/flow_gt1.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x > 31)
+  then x - 32
+  else x + 32
+}
diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail
new file mode 100644
index 00000000..8918438c
--- /dev/null
+++ b/test/typecheck/pass/flow_gteq1.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x >= 32)
+  then x - 32
+  else x + 32
+}
diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail
new file mode 100644
index 00000000..d32831a2
--- /dev/null
+++ b/test/typecheck/pass/flow_lteq1.sail
@@ -0,0 +1,28 @@
+default Order inc
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
+
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
+val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
+
+overload (deinfix +) [add_range]
+overload (deinfix -) [sub_range]
+overload (deinfix <) [lt_atom_range; lt_range_atom]
+overload (deinfix <=) [lteq_atom_range; lteq_range_atom]
+overload (deinfix >) [gt_atom_range; gt_range_atom]
+overload (deinfix >=) [gteq_atom_range; gteq_range_atom]
+
+function ([|63|]) branch (([|63|]) x) =
+{
+  if (x <= 32)
+  then x + 31
+  else x - 33
+}
diff --git a/test/typecheck/pass/nondet.sail b/test/typecheck/pass/nondet.sail
new file mode 100644
index 00000000..3c5db152
--- /dev/null
+++ b/test/typecheck/pass/nondet.sail
@@ -0,0 +1,10 @@
+
+register int z
+
+function unit test () = {
+  nondet {
+    z := 0;
+    z := 1;
+    z := 2;
+  }
+}
diff --git a/test/typecheck/pass/nondet_assert.sail b/test/typecheck/pass/nondet_assert.sail
new file mode 100644
index 00000000..1486c8d4
--- /dev/null
+++ b/test/typecheck/pass/nondet_assert.sail
@@ -0,0 +1,12 @@
+
+register int z
+
+function int test () = {
+  nondet {
+    z := 0;
+    assert(false, "Nondeterministic assert");
+    return z;
+    z := 1;
+  };
+  z
+}
diff --git a/test/typecheck/pass/nondet_return.sail b/test/typecheck/pass/nondet_return.sail
new file mode 100644
index 00000000..2a559e19
--- /dev/null
+++ b/test/typecheck/pass/nondet_return.sail
@@ -0,0 +1,11 @@
+
+register int z
+
+function int test () = {
+  nondet {
+    z := 0;
+    return z;
+    z := 1;
+  };
+  z
+}
diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail
new file mode 100644
index 00000000..a31dfa83
--- /dev/null
+++ b/test/typecheck/pass/simple_record_access.sail
@@ -0,0 +1,14 @@
+typedef signal = enumerate {LOW; HIGH}
+
+typedef Bit32 = bit[32]
+
+typedef Record =
+  const struct {signal rsig;
+  Bit32 bitfield;}
+
+register bit[32] R0
+
+function unit test ((Record) r) =
+{
+  R0 := r.bitfield;
+}