Improvements to sail n_constraints

1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.

For example we could have something like:

default Order dec

val bit[64] -> unit effect pure test64

val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test

function forall 'n. unit test addr =
{
  if constraint('n = 32) then {
    ()
  } else {
    assert(constraint('n = 64), "64-bit mode");
    test64(addr)
  }
}

2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.

3) Added != to the n_constraint language

4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:

val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test

This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.

12 files changed, 155 insertions, 60 deletions

diff --git a/src/ast.ml b/src/ast.ml
index f26bcba8..3830388a 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -171,21 +171,19 @@ n_constraint_aux =  (* constraint over kind $_$ *)
    NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
+ | NC_not_equal of nexp * nexp
  | NC_nat_set_bounded of kid * (int) list
- (* We need this for the new typechecker when as nexp is substituted for an id *)
- | NC_set_subst of nexp * int list
+ | NC_or of n_constraint * n_constraint
+ | NC_and of n_constraint * n_constraint
 
+and
+n_constraint =
+   NC_aux of n_constraint_aux * l
 
 type
 kinded_id =
    KOpt_aux of kinded_id_aux * l
 
-
-type
-n_constraint =
-   NC_aux of n_constraint_aux * l
-
-
 type
 quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
    QI_id of kinded_id (* An optionally kinded identifier *)
@@ -316,6 +314,7 @@ type
  | E_let of 'a letbind * 'a exp (* let expression *)
  | E_assign of 'a lexp * 'a exp (* imperative assignment *)
  | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
+ | E_constraint of n_constraint (* Expression to evaluate the n_constraint at run time *)
  | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
  | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
  | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 3eb5ddf0..898c65c4 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -46,6 +46,10 @@ open Ast
 open Util
 open Big_int
 
+let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
+
+let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown)
+
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
@@ -76,6 +80,7 @@ and map_exp_annot_aux f = function
   | E_let (letbind, exp) -> E_let (map_letbind_annot f letbind, map_exp_annot f exp)
   | E_assign (lexp, exp) -> E_assign (map_lexp_annot f lexp, map_exp_annot f exp)
   | E_sizeof nexp -> E_sizeof nexp
+  | E_constraint nc -> E_constraint nc
   | 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)
@@ -214,12 +219,15 @@ and string_of_typ_arg_aux = function
   | Typ_arg_order o -> string_of_order o
   | Typ_arg_effect eff -> string_of_effect eff
 
-let string_of_n_constraint = function
+let rec string_of_n_constraint = function
   | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
+  | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
   | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2
   | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2
-  | NC_aux (NC_set_subst (nexp, ns), _) ->
-     string_of_nexp nexp ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
+  | NC_aux (NC_or (nc1, nc2), _) ->
+     "(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
+  | NC_aux (NC_and (nc1, nc2), _) ->
+     "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_nat_set_bounded (kid, ns), _) ->
      string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
 
@@ -259,6 +267,7 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_block exps -> "{ " ^ string_of_list "; " string_of_exp exps ^ " }"
   | E_id v -> string_of_id v
   | E_sizeof nexp -> "sizeof " ^ string_of_nexp nexp
+  | E_constraint nc -> "constraint(" ^ string_of_n_constraint nc ^ ")"
   | E_lit lit -> string_of_lit lit
   | E_return exp -> "return " ^ string_of_exp exp
   | E_app (f, args) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp args ^ ")"
@@ -282,6 +291,7 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ " by " ^ string_of_exp u ^ " order " ^ string_of_order ord
      ^ ") { "
      ^ string_of_exp body
+  | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | _ -> "INTERNAL"
 and string_of_pexp (Pat_aux (pexp, _)) =
   match pexp with
@@ -337,6 +347,11 @@ module Id = struct
     | Id_aux (DeIid _, _), Id_aux (Id _, _) -> 1
 end
 
+module Bindings = Map.Make(Id)
+module IdSet = Set.Make(Id)
+module KBindings = Map.Make(Kid)
+module KidSet = Set.Make(Kid)
+
 let rec is_number (Typ_aux (t,_)) =
   match t with
   | Typ_app (Id_aux (Id "range", _),_)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 8902c39c..0adda3ef 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,6 +44,9 @@
 
 open Ast
 
+val mk_nc : n_constraint_aux -> n_constraint
+val mk_nexp : nexp_aux -> nexp
+
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
 val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
@@ -96,6 +99,22 @@ module BE : sig
   val compare : base_effect -> base_effect -> int
 end
 
+module IdSet : sig
+  include Set.S with type elt = id
+end
+
+module KidSet : sig
+  include Set.S with type elt = kid
+end
+
+module KBindings : sig
+  include Map.S with type key = kid
+end
+
+module Bindings : sig
+  include Map.S with type key = id
+end
+
 val is_number : typ -> bool
 val is_vector_typ : typ -> bool
 val is_bit_typ : typ -> bool
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 528a1526..39454049 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -303,14 +303,18 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg
     | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")),
     l)
 
-let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint =
-  match c with 
+let rec to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint =
+  match c with
   | Parse_ast.NC_aux(nc,l) ->
     NC_aux( (match nc with
              | Parse_ast.NC_fixed(t1,t2) -> 
                let n1 = to_ast_nexp k_env t1 in
                let n2 = to_ast_nexp k_env t2 in
                NC_fixed(n1,n2)
+             | Parse_ast.NC_not_equal(t1,t2) ->
+                let n1 = to_ast_nexp k_env t1 in
+                let n2 = to_ast_nexp k_env t2 in
+                NC_not_equal(n1,n2)
              | Parse_ast.NC_bounded_ge(t1,t2) ->
                let n1 = to_ast_nexp k_env t1 in
                let n2 = to_ast_nexp k_env t2 in
@@ -320,8 +324,12 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
                let n2 = to_ast_nexp k_env t2 in
                NC_bounded_le(n1,n2)
              | Parse_ast.NC_nat_set_bounded(id,bounds) ->
-               NC_nat_set_bounded(to_ast_var id, bounds)
-    ), l)               
+                NC_nat_set_bounded(to_ast_var id, bounds)
+             | Parse_ast.NC_or (nc1, nc2) ->
+                NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
+             | Parse_ast.NC_and (nc1, nc2) ->
+                NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
+    ), l)
 
 (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *)
 let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t * kind Envmap.t =
@@ -488,6 +496,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp)
+    | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc)
     | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp)
     | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg)
diff --git a/src/lexer.mll b/src/lexer.mll
index 34fd56f9..45d8b3c2 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -97,6 +97,7 @@ let kw_table =
      ("return",                  (fun x -> Return));
      ("scattered",               (fun x -> Scattered));
      ("sizeof",                  (fun x -> Sizeof));
+     ("constraint",              (fun x -> Constraint));
      ("struct",                  (fun x -> Struct));
      ("switch",			 (fun x -> Switch));
      ("then",                    (fun x -> Then));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index e020e0d5..767bd8dd 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -160,20 +160,20 @@ n_constraint_aux =  (* constraint over kind $_$ *)
    NC_fixed of atyp * atyp
  | NC_bounded_ge of atyp * atyp
  | NC_bounded_le of atyp * atyp
+ | NC_not_equal of atyp * atyp
  | NC_nat_set_bounded of kid * (int) list
+ | NC_or of n_constraint * n_constraint
+ | NC_and of n_constraint * n_constraint
 
+and
+n_constraint = 
+   NC_aux of n_constraint_aux * l
 
 type 
 kinded_id = 
    KOpt_aux of kinded_id_aux * l
 
-
-type 
-n_constraint = 
-   NC_aux of n_constraint_aux * l
-
-
-type 
+type
 quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
    QI_id of kinded_id (* An optionally kinded identifier *)
  | QI_const of n_constraint (* A constraint for this type *)
@@ -277,6 +277,7 @@ exp_aux =  (* Expression *)
  | E_let of letbind * exp (* let expression *)
  | E_assign of exp * exp (* imperative assignment *)
  | E_sizeof of atyp
+ | E_constraint of n_constraint
  | E_exit of exp
  | E_return of exp
  | E_assert of exp * exp
diff --git a/src/parser.mly b/src/parser.mly
index 6a76cec9..ef56934e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -131,7 +131,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
 %token Enumerate Else Exit Extern False Forall Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
-%token Undefined Union With When Val
+%token Undefined Union With When Val Constraint
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 
@@ -593,6 +593,8 @@ atomic_exp:
     { eloc (E_case($2,$4)) }
   | Sizeof atomic_typ
     { eloc (E_sizeof($2)) }
+  | Constraint Lparen nexp_constraint Rparen
+    { eloc (E_constraint $3) }
   | Exit atomic_exp
       { eloc (E_exit $2) }
   | Return atomic_exp
@@ -1053,14 +1055,32 @@ nums:
     { $1::$3 }
 
 nexp_constraint:
+  | nexp_constraint1
+    { $1 }
+  | nexp_constraint1 Bar nexp_constraint
+    { NC_aux (NC_or ($1, $3), loc ()) }
+
+nexp_constraint1:
+  | nexp_constraint2
+    { $1 }
+  | nexp_constraint2 Amp nexp_constraint1
+    { NC_aux (NC_and ($1, $3), loc ()) }
+
+nexp_constraint2:
   | nexp_typ Eq nexp_typ
     { NC_aux(NC_fixed($1,$3), loc () ) }
+  | nexp_typ ExclEq nexp_typ
+    { NC_aux (NC_not_equal ($1, $3), loc ()) }
   | nexp_typ GtEq nexp_typ
     { NC_aux(NC_bounded_ge($1,$3), loc () ) }
   | nexp_typ LtEq nexp_typ
     { NC_aux(NC_bounded_le($1,$3), loc () ) }
+  | tyvar In Lcurly nums Rcurly
+    { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
   | tyvar IN Lcurly nums Rcurly
     { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+  | Lparen nexp_constraint Rparen
+    { $2 }
 
 id_constraint:
   | nexp_constraint
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d4278b56..c674735d 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -49,9 +49,6 @@ open Pretty_print_common
  * PPrint-based source-to-source pretty printer
 ****************************************************************************)
 
-
-
-
 let doc_bkind (BK_aux(k,_)) =
   string (match k with
   | BK_type -> "Type"
@@ -62,13 +59,18 @@ let doc_bkind (BK_aux(k,_)) =
 let doc_kind (K_aux(K_kind(klst),_)) =
   separate_map (spaces arrow) doc_bkind klst
 
-let doc_nexp_constraint (NC_aux(nc,_)) = match nc with
+let rec doc_nexp_constraint (NC_aux(nc,_)) = match nc with
   | NC_fixed(n1,n2) -> doc_op equals (doc_nexp n1) (doc_nexp n2)
+  | NC_not_equal (n1, n2) -> doc_op (string "!=") (doc_nexp n1) (doc_nexp n2)
   | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (doc_nexp n1) (doc_nexp n2)
   | NC_bounded_le(n1,n2) -> doc_op (string "<=") (doc_nexp n1) (doc_nexp n2)
   | NC_nat_set_bounded(v,bounds) ->
       doc_op (string "IN") (doc_var v)
-        (braces (separate_map comma_sp doc_int bounds))
+             (braces (separate_map comma_sp doc_int bounds))
+  | NC_or (nc1, nc2) ->
+     parens (separate space [doc_nexp_constraint nc1; string "|"; doc_nexp_constraint nc2])
+  | NC_and (nc1, nc2) ->
+     separate space [doc_nexp_constraint nc1; string "&"; doc_nexp_constraint nc2]
 
 let doc_qi (QI_aux(qi,_)) = match qi with
   | QI_const n_const -> doc_nexp_constraint n_const
@@ -293,7 +295,9 @@ let doc_exp, doc_let =
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rbrace
   | E_sizeof n ->
-    separate space [string "sizeof"; doc_nexp n]
+     separate space [string "sizeof"; doc_nexp n]
+  | E_constraint nc ->
+     string "constraint" ^^ parens (doc_nexp_constraint nc)
   | E_exit e ->
     separate space [string "exit"; atomic_exp e;]
   | E_return e ->
diff --git a/src/process_file.ml b/src/process_file.ml
index efa2ec55..b2054f40 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -81,10 +81,16 @@ let parse_file (f : string) : Parse_ast.defs =
       | Lexer.LexError(s,p) ->
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
+
 (*Should add a flag to say whether we want to consider Oinc or Odec the default order *)
 let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
 
+let load_file env f =
+  let ast = parse_file f in
+  let (ast, _, _) = convert_ast ast in
+  Type_check_new.check env ast
+
 let opt_new_typecheck = ref false
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
diff --git a/src/process_file.mli b/src/process_file.mli
index 9620712a..b3748145 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -46,6 +46,7 @@ val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal
 val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_lem : Type_check.envs -> Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
+val load_file : Type_check_new.Env.t -> string -> Type_check_new.tannot Ast.defs * Type_check_new.Env.t
 
 val opt_new_typecheck : bool ref
 val opt_just_check : bool ref
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 69994797..634b043c 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -116,6 +116,8 @@ let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown)
 let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
 let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
 
+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)
 let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
 let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1))
@@ -123,11 +125,19 @@ let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1))
 
 let mk_lit l = E_aux (E_lit (L_aux (l, Parse_ast.Unknown)), (Parse_ast.Unknown, ()))
 
-let nc_negate (NC_aux (nc, _)) =
+(* FIXME: Can now negate all n_constraints *)
+let rec nc_negate (NC_aux (nc, _)) =
   match nc with
-  | NC_bounded_ge (n1, n2) -> Some (nc_lt n1 n2)
-  | NC_bounded_le (n1, n2) -> Some (nc_gt n1 n2)
-  | _ -> None
+  | NC_bounded_ge (n1, n2) -> nc_lt n1 n2
+  | NC_bounded_le (n1, n2) -> nc_gt n1 n2
+  | NC_fixed (n1, n2) -> nc_neq n1 n2
+  | NC_not_equal (n1, n2) -> nc_eq n1 n2
+  | NC_and (n1, n2) -> mk_nc (NC_or (nc_negate n1, nc_negate n2))
+  | NC_or (n1, n2) -> mk_nc (NC_and (nc_negate n1, nc_negate n2))
+  | NC_nat_set_bounded (kid, []) -> typ_error Parse_ast.Unknown "Cannot negate empty nexp set"
+  | NC_nat_set_bounded (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
+  | NC_nat_set_bounded (kid, int :: ints) ->
+     mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_nat_set_bounded (kid, ints)))))
 
 (* Utilities for constructing effect sets *)
 
@@ -151,13 +161,6 @@ let equal_effects e1 e2 =
      BESet.compare (BESet.of_list base_effs1) (BESet.of_list base_effs2) = 0
   | _, _ -> assert false (* We don't do Effect variables *)
 
-(* Sets and maps for identifiers and kind identifiers *)
-
-module Bindings = Map.Make(Id)
-module IdSet = Set.Make(Id)
-module KBindings = Map.Make(Kid)
-module KidSet = Set.Make(Kid)
-
 (* An index_sort is a more general form of range type: it can either
    be IS_int, which represents every natural number, or some set of
    natural numbers given by an IS_prop expression of the form
@@ -188,6 +191,11 @@ and nexp_subst_aux sv subst = function
   | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp)
   | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
 
+let rec nexp_set_to_or l subst = function
+  | [] -> typ_error l "Cannot substitute into empty nexp set"
+  | [int] -> NC_fixed (subst, nconstant int)
+  | (int :: ints) -> NC_or (mk_nc (NC_fixed (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
+
 let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
 and nc_subst_nexp_aux l sv subst = function
   | NC_fixed (n1, n2) -> NC_fixed (nexp_subst sv subst n1, nexp_subst sv subst n2)
@@ -195,9 +203,10 @@ and nc_subst_nexp_aux l sv subst = function
   | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
   | NC_nat_set_bounded (kid, ints) as set_nc ->
      if Kid.compare kid sv = 0
-     then NC_set_subst (Nexp_aux (subst, Parse_ast.Unknown), ints)
+     then nexp_set_to_or l (mk_nexp subst) ints
      else set_nc
-  | NC_set_subst (nexp, ints) -> NC_set_subst (nexp_subst sv subst nexp, ints)
+  | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
 
 let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l)
 and typ_subst_nexp_aux sv subst = function
@@ -341,6 +350,7 @@ module Env : sig
   val get_constraints : t -> n_constraint list
   val add_constraint : n_constraint -> t -> t
   val get_typ_var : kid -> t -> base_kind_aux
+  val get_typ_vars : t -> base_kind_aux KBindings.t
   val add_typ_var : kid -> base_kind_aux -> t -> t
   val get_ret_typ : t -> typ option
   val add_ret_typ : typ -> t -> t
@@ -450,6 +460,8 @@ end = struct
     try KBindings.find kid env.typ_vars with
     | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
 
+  let get_typ_vars env = env.typ_vars
+
   (* FIXME: Add an IdSet for builtin types *)
   let bound_typ_id env id =
     Bindings.mem id env.typ_synonyms
@@ -695,13 +707,15 @@ end = struct
         { env with typ_vars = KBindings.add kid k env.typ_vars }
       end
 
-  let wf_constraint env (NC_aux (nc, _)) =
+  let rec wf_constraint env (NC_aux (nc, _)) =
     match nc with
     | NC_fixed (n1, n2) -> wf_nexp env n1; wf_nexp env n2
+    | NC_not_equal (n1, n2) -> wf_nexp env n1; wf_nexp env n2
     | NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2
     | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2
     | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
-    | NC_set_subst (nexp, ints) -> wf_nexp env nexp
+    | NC_or (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2
+    | NC_and (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2
 
   let get_constraints env = env.constraints
 
@@ -917,14 +931,16 @@ let rec nexp_constraint var_of (Nexp_aux (nexp, l)) =
 let rec nc_constraint var_of (NC_aux (nc, l)) =
   match nc with
   | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
+  | NC_not_equal (nexp1, nexp2) -> Constraint.neq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
   | NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
   | NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
-  | NC_nat_set_bounded (kid, ints) -> nc_constraint var_of (NC_aux (NC_set_subst (nvar kid, ints), l))
-  | NC_set_subst (_, []) -> Constraint.literal false
-  | NC_set_subst (nexp, (int :: ints)) ->
+  | NC_nat_set_bounded (_, []) -> Constraint.literal false
+  | NC_nat_set_bounded (kid, (int :: ints)) ->
      List.fold_left Constraint.disj
-                    (Constraint.eq (nexp_constraint var_of nexp) (Constraint.constant (big_int_of_int int)))
-                    (List.map (fun i -> Constraint.eq (nexp_constraint var_of nexp) (Constraint.constant (big_int_of_int i))) ints)
+                    (Constraint.eq (nexp_constraint var_of (nvar kid)) (Constraint.constant (big_int_of_int int)))
+                    (List.map (fun i -> Constraint.eq (nexp_constraint var_of (nvar kid)) (Constraint.constant (big_int_of_int i))) ints)
+  | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint var_of nc1) (nc_constraint var_of nc2)
+  | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint var_of nc1) (nc_constraint var_of nc2)
 
 let rec nc_constraints var_of ncs =
   match ncs with
@@ -1471,15 +1487,6 @@ let rec add_flows b flows env =
   | (id, flow) :: flows when b -> add_flows true flows (Env.add_flow id (fst (apply_flow_constraint flow)) env)
   | (id, flow) :: flows -> add_flows false flows (Env.add_flow id (snd (apply_flow_constraint flow)) env)
 
-let neg_constraints = function
-  | [constr] ->
-     begin
-       match nc_negate constr with
-       | Some constr -> [constr]
-       | None -> []
-     end
-  | _ -> []
-
 let rec add_constraints constrs env =
   List.fold_left (fun env constr -> Env.add_constraint constr env) env constrs
 
@@ -1560,6 +1567,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
          | (E_aux (E_assign (lexp, bind), _) :: exps) ->
             let texp, env = bind_assignment env lexp bind in
             texp :: check_block l env exps typ
+         | ((E_aux (E_assert (E_aux (E_constraint nc, _), assert_msg), _) as exp) :: exps) ->
+            typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert");
+            let inferred_exp = irule infer_exp env exp in
+            inferred_exp :: check_block l (Env.add_constraint nc env) exps typ
          | (exp :: exps) ->
             let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
             texp :: check_block l env exps typ
@@ -1610,7 +1621,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
      let flows, constrs = infer_flow env cond' in
      let then_branch' = crule check_exp (add_constraints constrs (add_flows true flows env)) then_branch typ in
-     let else_branch' = crule check_exp (add_constraints (neg_constraints constrs) (add_flows false flows env)) else_branch typ in
+     let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch typ in
      annot_exp (E_if (cond', then_branch', else_branch')) typ
   | E_exit exp, _ ->
      let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
@@ -1992,6 +2003,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      end
   | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
   | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])))
+  | E_constraint nc ->
+     annot_exp (E_constraint nc) bool_typ
   | E_return exp ->
      begin
        match Env.get_ret_typ env with
@@ -2076,7 +2089,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
      let flows, constrs = infer_flow env cond' in
      let then_branch' = irule infer_exp (add_constraints constrs (add_flows true flows env)) then_branch in
-     let else_branch' = crule check_exp (add_constraints (neg_constraints constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in
+     let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (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, ())))
@@ -2278,6 +2291,7 @@ and propagate_exp_effect_aux = function
      let propagated_exp = propagate_exp_effect exp in
      E_assign (propagated_lexp, propagated_exp), union_effects (effect_of propagated_exp) (effect_of_lexp propagated_lexp)
   | E_sizeof nexp -> E_sizeof nexp, no_effect
+  | E_constraint nc -> E_constraint nc, no_effect
   | E_exit exp ->
      let propagated_exp = propagate_exp_effect exp in
      E_exit propagated_exp, effect_of propagated_exp
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index a8a1378d..c3f0360a 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -42,6 +42,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_util
 
 val opt_tc_debug : int ref
 
@@ -81,6 +82,8 @@ module Env : sig
 
   val get_typ_var : kid -> t -> base_kind_aux
 
+  val get_typ_vars : t -> base_kind_aux KBindings.t
+
   val is_record : id -> t -> bool
 
   val get_accessor : id -> t -> typquant * typ
@@ -117,8 +120,11 @@ module Env : sig
   val allow_casts : t -> bool
 
   val empty : t
+
 end
 
+val add_typquant : typquant -> Env.t -> Env.t
+
 (* Some handy utility functions for constructing types. *)
 val mk_typ : typ_aux -> typ
 val mk_typ_arg : typ_arg_aux -> typ_arg