Steps towards solving constraints

6 files changed, 139 insertions, 68 deletions

diff --git a/src/parser.mly b/src/parser.mly
index 52b8a8ae..ada8365a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -91,10 +91,10 @@ let mk_eannot e i = Effect_opt_aux((Effect_opt_effect(e)),(locn i i))
 let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown)
 let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
 
-let make_enum_sugar_bounded typ1 typ2 =
-  ATyp_app(Id_aux(Id("enum"),Unknown),[typ1; typ2;])
-let make_enum_sugar typ1 =
-  make_enum_sugar_bounded typ1 (ATyp_aux(ATyp_constant(0), Unknown))
+let make_range_sugar_bounded typ1 typ2 =
+  ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;])
+let make_range_sugar typ1 =
+  make_range_sugar_bounded typ1 (ATyp_aux(ATyp_constant(0), Unknown))
 
 let make_r bot top =
   match bot,top with
@@ -320,9 +320,9 @@ atomic_typ:
   | Dec
     { tloc (ATyp_dec) } 
   | SquareBar nexp_typ BarSquare
-      { tloc (make_enum_sugar $2) }
+      { tloc (make_range_sugar $2) }
   | SquareBar nexp_typ Colon nexp_typ BarSquare
-      { tloc (make_enum_sugar_bounded $2 $4) }
+      { tloc (make_range_sugar_bounded $2 $4) }
   | Lparen typ Rparen
     { $2 }
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index ab6e0539..b47f808a 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -580,7 +580,11 @@ let pp_format_nes nes =
        | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
        | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
        | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
-       | In(_,i,ns) -> "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])")
+       | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) |InOpen(_,{nexp=Nvar i},ns)-> 
+	 "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])"
+       | InS(_,{nexp = Nuvar _},ns) | InOpen(_,{nexp = Nuvar _},ns) ->  
+	 "(Nec_in (Kid_aux (Var \"fresh\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])"
+     )
      nes) ^ "]"
 
 let pp_format_annot = function
diff --git a/src/process_file.ml b/src/process_file.ml
index 592c8cf5..57024bb4 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -62,7 +62,7 @@ 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";"enum";"list";"bit";"nat"] in
+  let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"] in
   let type_names = 
     try
       Pre_parser.file Pre_lexer.token scanbuf
diff --git a/src/type_check.ml b/src/type_check.ml
index dbf55a1a..0c3f25af 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -171,9 +171,9 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	      | Tid "bit" -> 
 		if i = 0 then bit_t,L_zero 
 		else if i = 1 then bit_t,L_one
-		else {t = Tapp("enum",
+		else {t = Tapp("range",
 			       [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])},lit
-	      | _ -> {t = Tapp("enum",
+	      | _ -> {t = Tapp("range",
 			       [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])},lit)
 	  | L_hex s -> {t = Tapp("vector",
 				 [TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst ((String.length s)*4)};
@@ -430,7 +430,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
             else 
               if i = 1 then bool_t,L_true,pure_e
               else typ_error l "Expected bool, found a number that cannot be used as a bit and converted to bool"
-          | _ -> {t = Tapp("enum",
+          | _ -> {t = Tapp("range",
 			   [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])},lit,pure_e)
 	| L_hex s -> {t = Tapp("vector",
 			       [TA_nexp{nexp = Nconst 0};
@@ -524,18 +524,18 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
        union_effects ef1 (union_effects then_ef else_ef))
     | E_for(id,from,to_,step,order,block) -> 
       let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in
-      let ft,tt,st = {t=Tapp("enum",[TA_nexp fb;TA_nexp fr])},
-	{t=Tapp("enum",[TA_nexp tb;TA_nexp tr])},{t=Tapp("enum",[TA_nexp sb;TA_nexp sr])} in     
+      let ft,tt,st = {t=Tapp("range",[TA_nexp fb;TA_nexp fr])},
+	{t=Tapp("range",[TA_nexp tb;TA_nexp tr])},{t=Tapp("range",[TA_nexp sb;TA_nexp sr])} in     
       let from',from_t,_,from_c,from_ef = check_exp envs ft from in
       let to_',to_t,_,to_c,to_ef = check_exp envs tt to_ in
       let step',step_t,_,step_c,step_ef = check_exp envs st step in
       let new_annot,local_cs = 
 	match (aorder_to_ord order).order with
 	  | Oinc ->
-	    (Some(([],{t=Tapp("enum",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp_local,[],pure_e),
+	    (Some(([],{t=Tapp("range",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp_local,[],pure_e),
 	     [LtEq(l,{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});LtEq(l,fb,tb)])
 	  | Odec ->
-	    (Some(([],{t=Tapp("enum",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp_local,[],pure_e),
+	    (Some(([],{t=Tapp("range",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp_local,[],pure_e),
 	     [GtEq(l,{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});GtEq(l,fb,tb)])
 	  | _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic")
       in
@@ -545,7 +545,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
     | E_vector(es) ->
       let item_t = match expect_t.t with
         | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
-          (* TODO: Consider whether an enum should be looked for here*)
+          (* TODO: Consider whether an range should be looked for here*)
         | _ -> new_t () in
       let es,cs,effect = (List.fold_right 
 			    (fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect)
@@ -556,7 +556,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
     | E_vector_indexed eis ->
       let item_t = match expect_t.t with
         | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
-          (* TODO: Consider whether an enum should be looked for here*)
+          (* TODO: Consider whether an range should be looked for here*)
         | _ -> new_t () in
       let first,last = fst (List.hd eis), fst (List.hd (List.rev eis)) in
       let is_increasing = first <= last in
@@ -579,7 +579,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let item_t = new_t () in
       let vt = {t= Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord; TA_typ item_t])} in
       let (vec',t',_,cs,ef) = check_exp envs vt vec in
-      let it = {t= Tapp("enum",[TA_nexp min;TA_nexp m_rise])} in
+      let it = {t= Tapp("range",[TA_nexp min;TA_nexp m_rise])} in
       let (i',ti',_,cs_i,ef_i) = check_exp envs it i in
       let cs_loc = 
 	match ord.order with
@@ -600,9 +600,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	| _ -> new_n(),new_n(),new_o(),new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
       let (vec',t',_,cs,ef) = check_exp envs vt vec in
-      let i1t = {t=Tapp("enum",[TA_nexp min1;TA_nexp m_rise1])} in
+      let i1t = {t=Tapp("range",[TA_nexp min1;TA_nexp m_rise1])} in
       let (i1', ti1, _,cs_i1,ef_i1) = check_exp envs i1t i1 in
-      let i2t = {t=Tapp("enum",[TA_nexp min2;TA_nexp m_rise2])} in
+      let i2t = {t=Tapp("range",[TA_nexp min2;TA_nexp m_rise2])} in
       let (i2', ti2, _,cs_i2,ef_i2) = check_exp envs i2t i2 in
       let cs_loc =
 	match ord.order with
@@ -629,7 +629,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	| _ -> new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
       let (vec',t',_,cs,ef) = check_exp envs vt vec in
-      let it = {t=Tapp("enum",[TA_nexp min;TA_nexp m_rise])} in
+      let it = {t=Tapp("range",[TA_nexp min;TA_nexp m_rise])} in
       let (i', ti, _,cs_i,ef_i) = check_exp envs it i in
       let (e', te, _,cs_e,ef_e) = check_exp envs item_t e in
       let cs_loc = 
@@ -653,9 +653,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	| _ -> new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
       let (vec',t',_,cs,ef) = check_exp envs vt vec in
-      let i1t = {t=Tapp("enum",[TA_nexp min1;TA_nexp m_rise1])} in
+      let i1t = {t=Tapp("range",[TA_nexp min1;TA_nexp m_rise1])} in
       let (i1', ti1, _,cs_i1,ef_i1) = check_exp envs i1t i1 in
-      let i2t = {t=Tapp("enum",[TA_nexp min2;TA_nexp m_rise2])} in
+      let i2t = {t=Tapp("range",[TA_nexp min2;TA_nexp m_rise2])} in
       let (i2', ti2, _,cs_i2,ef_i2) = check_exp envs i2t i2 in
       let (e',item_t',_,cs_e,ef_e) =
 	try check_exp envs item_t e with
@@ -985,8 +985,8 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
       (match item_actual.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
 	  let acc_t = match ord.order with
-	    | Oinc -> {t = Tapp("enum",[TA_nexp base;TA_nexp rise])} 
-	    | Odec -> {t = Tapp("enum",[TA_nexp {nexp = Nadd(base,{nexp=Nneg rise})};TA_nexp base])} 
+	    | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp rise])} 
+	    | Odec -> {t = Tapp("range",[TA_nexp {nexp = Nadd(base,{nexp=Nneg rise})};TA_nexp base])} 
 	    | _ -> typ_error l ("Assignment to one vector element requires either inc or dec order")
 	  in
 	  let (e,t',_,cs',ef_e) = check_exp envs acc_t acc in
@@ -1011,8 +1011,8 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
       (match item_actual.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
 	  let base_e1,range_e1,base_e2,range_e2 = new_n(),new_n(),new_n(),new_n() in
-	  let base_t = {t=Tapp("enum",[TA_nexp base_e1;TA_nexp range_e1])} in
-	  let range_t = {t=Tapp("enum",[TA_nexp base_e2;TA_nexp range_e2])} in
+	  let base_t = {t=Tapp("range",[TA_nexp base_e1;TA_nexp range_e1])} in
+	  let range_t = {t=Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])} in
 	  let cs_t,res_t = match ord.order with
 	    | Oinc ->  ([LtEq(l,base,base_e1);
 			 LtEq(l,{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)});
@@ -1113,8 +1113,8 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
       (TD_aux(td,(l,ty)),Env({d_env with enum_env = enum_env;},t_env))
     | TD_register(id,base,top,ranges) -> 
       let id' = id_to_string id in
-      let basei = eval_to_nexp_const(anexp_to_nexp base) in
-      let topi = eval_to_nexp_const(anexp_to_nexp top) in
+      let basei = eval_nexp(anexp_to_nexp base) in
+      let topi = eval_nexp(anexp_to_nexp top) in
       match basei.nexp,topi.nexp with
 	| Nconst b, Nconst t -> 
 	  if b <= t then (
@@ -1170,6 +1170,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
 	    (TD_aux(td,(l,tannot)),
 	     Env({d_env with rec_env = (id',Register,franges)::d_env.rec_env;
 	       abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
+	| _,_ -> raise (Reporting_basic.err_unreachable l "Nexps in register declaration do not evaluate to constants")
 
 let check_val_spec envs (VS_aux(vs,(l,annot))) = 
   let (Env(d_env,t_env)) = envs in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 3f7ca294..5eb2b85a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -74,6 +74,7 @@ type nexp_range =
   | GtEq of Parse_ast.l * nexp * nexp
   | In of Parse_ast.l * string * int list
   | InS of Parse_ast.l * nexp * int list
+  | InOpen of Parse_ast.l * nexp * int list
 
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list * effect) option
@@ -205,26 +206,37 @@ let rec eval_nexp n =
   match n.nexp with
     | Nconst i -> n
     | Nmult(n1,n2) ->
-      (match (eval_nexp n1).nexp,(eval_nexp n2).nexp with
+      let n1',n2' = (eval_nexp n1),(eval_nexp n2) in
+      (match n1'.nexp,n2'.nexp with
 	| Nconst i1, Nconst i2 -> {nexp=Nconst (i1*i2)}
-	| _,_ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+	| (Nconst _ as c),Nmult(nl,nr) | Nmult(nl,nr),(Nconst _ as c) -> 
+	  {nexp = Nmult(eval_nexp {nexp = Nmult({nexp = c},nl)},eval_nexp {nexp = Nmult({nexp=c},nr)})}
+	| (Nconst _ as c),Nadd(nl,nr) | Nadd(nl,nr),(Nconst _ as c) ->
+	  {nexp = Nadd(eval_nexp {nexp =Nmult({nexp=c},nl)},eval_nexp {nexp = Nmult({nexp=c},nr)})}
+	| N2n n1, N2n n2 -> {nexp = N2n( eval_nexp {nexp = Nadd(n1,n2)} ) }
+	| _,_ -> {nexp = Nmult(n1',n2') })
     | Nadd(n1,n2) ->
-      (match (eval_nexp n1).nexp,(eval_nexp n2).nexp with
+      let n1',n2' = (eval_nexp n1),(eval_nexp n2) in      
+      (match n1'.nexp,n2'.nexp with
 	| Nconst i1, Nconst i2 -> {nexp=Nconst (i1+i2)}
-	| _,_ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+	| (Nconst _ as c),Nadd(nl,nr) | Nadd(nl,nr),(Nconst _ as c) ->
+	  {nexp = Nadd(eval_nexp {nexp =Nadd({nexp=c},nl)},eval_nexp {nexp = Nadd({nexp=c},nr)})}
+	| _,_ -> {nexp = Nadd(n1',n2') })
     | Nneg n1 ->
-      (match (eval_nexp n1).nexp with
-	| Nconst i -> {nexp = Nconst(- i)}
-	| _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+      let n1' = eval_nexp n1 in
+      (match n1'.nexp with
+	| Nconst i -> {nexp = Nconst(i * -1)}
+	| _ -> {nexp = Nneg n1'})
     | N2n n1 ->
-      (match (eval_nexp n1).nexp with
+      let n1' = eval_nexp n1 in
+      (match n1'.nexp with
 	| Nconst i ->
 	  let rec two_pow = function
 	    | 0 -> 1;
 	    | n -> 2* (two_pow n-1) in
 	  {nexp = Nconst(two_pow i)}
-	| _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
-    | Nvar _ | Nuvar _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const")
+	| _ -> {nexp = N2n n1'})
+    | Nvar _ | Nuvar _ -> n
 
 
 let v_count = ref 0
@@ -443,10 +455,19 @@ let rec fresh_evar bindings e =
       None
     | _ -> None
 
-let nat_t = {t = Tapp("enum",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};])}
+let nat_t = {t = Tapp("range",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};])}
 let unit_t = { t = Tid "unit" }
 let bit_t = {t = Tid "bit" }
 let bool_t = {t = Tid "bool" }
+let nat_typ = {t=Tid "nat"}
+let pure_e = {effect=Eset []}
+
+let is_nat_typ t =
+  if t == nat_typ || t == nat_t then true
+  else match t.t with
+    | Tid "nat" -> true
+    | Tapp("range",[TA_nexp{nexp = Nconst 0};TA_nexp{nexp = Nconst i}]) -> i == max_int
+    | _ -> false
 
 let initial_kind_env = 
   Envmap.from_list [ 
@@ -457,12 +478,10 @@ let initial_kind_env =
     ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})});
     ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
     ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})});
-    ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) });
+    ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) });
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
   ]
 
-let nat_typ = {t=Tid "nat"}
-let pure_e = {effect=Eset []}
 let initial_typ_env =
   Envmap.from_list [
     ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External None,[],pure_e));
@@ -608,6 +627,7 @@ let rec cs_subst t_env cs =
     | LtEq(l,n1,n2)::cs -> LtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs)
     | In(l,s,ns)::cs -> InS(l,n_subst t_env {nexp=Nvar s},ns)::(cs_subst t_env cs)
     | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
+    | InOpen(l,n,ns)::cs -> InOpen(l,n_subst t_env n,ns)::(cs_subst t_env cs)
 
 let subst k_env t cs e =
   let subst_env = Envmap.from_list
@@ -733,20 +753,22 @@ let effects_eq l e1 e2 =
   | Evar v1, Eset _ -> eq_error l ("Effect variable " ^ v1 ^ " cannot be used where a concrete set of effects is specified")
 
 (* Is checking for structural equality only, other forms of equality will be handeled by constraints *)
-let rec nexp_eq n1 n2 =
+let rec nexp_eq_check n1 n2 =
   match n1.nexp,n2.nexp with
   | Nvar v1,Nvar v2 -> v1=v2
   | Nconst n1,Nconst n2 -> n1=n2
-  | Nadd(nl1,nl2), Nadd(nr1,nr2) -> nexp_eq nl1 nr1 && nexp_eq nl2 nr2
-  | Nmult(nl1,nl2), Nmult(nr1,nr2) -> nexp_eq nl1 nr1 && nexp_eq nl2 nr2
-  | N2n n,N2n n2 -> nexp_eq n n2
-  | Nneg n,Nneg n2 -> nexp_eq n n2
-  | Nuvar _, n -> equate_n n1 n2; true
-  | n,Nuvar _ -> equate_n n2 n1; true
+  | Nadd(nl1,nl2), Nadd(nr1,nr2) | Nmult(nl1,nl2), Nmult(nr1,nr2) -> nexp_eq_check nl1 nr1 && nexp_eq_check nl2 nr2
+  | N2n n,N2n n2 -> nexp_eq_check n n2
+  | Nneg n,Nneg n2 -> nexp_eq_check n n2
+  | Nuvar {nindex =i1},Nuvar {nindex = i2} -> i1 = i2
   | _,_ -> false
 
+let nexp_eq n1 n2 =
+  nexp_eq_check (eval_nexp n1) (eval_nexp n2)
+
 (*Is checking for structural equality amongst the types, building constraints for kind Nat. 
-  When considering two enum type applications, will check for consistency instead of equality*)
+  When considering two range type applications, will check for consistency instead of equality*)
+(*TODOTODO when t1 range and t2 a tuvar or t2 an range with nuvars, need to not copy directly but issue bound (not eq) constraints for pattern matching against multiple constants ... possibly an in constraint for constants, and then when considering constraints, merge various in statements for same variable *)
 let rec type_consistent_internal l d_env t1 cs1 t2 cs2 = 
   let t1,cs1',_ = get_abbrev d_env t1 in
   let t2,cs2',_ = get_abbrev d_env t2 in
@@ -761,7 +783,7 @@ let rec type_consistent_internal l d_env t1 cs1 t2 cs2 =
   | Tid v1,Tid v2 -> 
     if v1 = v2 then (t2,cs1@cs2) 
     else eq_error l ("Types " ^ v1 ^ " and " ^ v2 ^ " do not match")
-  | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tapp("enum",[TA_nexp b2;TA_nexp r2;]) -> 
+  | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tapp("range",[TA_nexp b2;TA_nexp r2;]) -> 
     if (nexp_eq b1 b2)&&(nexp_eq r1 r2) then (t2,[])
     else (t2, cs1@cs2@[GtEq(l,b1,b2);LtEq(l,r1,r2)])
   | Tapp(id1,args1), Tapp(id2,args2) ->
@@ -776,6 +798,14 @@ let rec type_consistent_internal l d_env t1 cs1 t2 cs2 =
   | Ttup t1s, Ttup t2s ->
     (t2,cs1@cs2@(List.flatten (List.map snd (List.map2 (type_consistent l d_env) t1s t2s))))
   | Tuvar _, t -> equate_t t1 t2; (t1,cs1@cs2)
+  | Tapp("range",[TA_nexp b;TA_nexp r]),Tuvar _ ->
+    if is_nat_typ t1 then
+      begin equate_t t2 t1; (t2,cs1@cs2) end
+    else 
+      let b2,r2 = new_n (), new_n () in
+      let t2' = {t=Tapp("range",[TA_nexp b2;TA_nexp r2])} in
+      equate_t t2 t2';
+      (t2,cs1@cs2@[GtEq(l,b,b2);LtEq(l,r,r2)]) (*This and above should maybe be In constraints when constants and nuvars/vars*)
   | t,Tuvar _ -> equate_t t2 t1; (t2,cs1@cs2)
   | _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2))
 
@@ -820,7 +850,7 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
     if id1=id2 
     then let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e)
     else (match id1,id2 with
-    | "vector","enum" -> 
+    | "vector","range" -> 
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
@@ -831,11 +861,11 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
 	let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd({nexp=Nneg b1},r1)})})] in
 	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
-	eq_error l "Cannot convert a vector to an enum without an order"
+	eq_error l "Cannot convert a vector to an range without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
-        eq_error l "Cannot convert non-bit vector into an enum"
-      | _,_ -> raise (Reporting_basic.err_unreachable l "vector or enum is not properly kinded"))
-    | "enum","vector" -> 
+        eq_error l "Cannot convert non-bit vector into an range"
+      | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+    | "range","vector" -> 
       (match args2,args1 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
@@ -847,10 +877,10 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
 		  Eq(l,r1,b1)] in
 	(t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
-	eq_error l "Cannot convert an enum to a vector without an order"
+	eq_error l "Cannot convert an range to a vector without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
-        eq_error l "Cannot convert an enum into a non-bit vector"
-      | _,_ -> raise (Reporting_basic.err_unreachable l "vector or enum is not properly kinded"))
+        eq_error l "Cannot convert an range into a non-bit vector"
+      | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
     | "register",_ ->
       (match args1 with
 	| [TA_typ t] ->
@@ -865,10 +895,10 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
   | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
     let cs = [Eq(l,r1,{nexp = Nconst 1})] in
     (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)),
-					   (l,Some(([],{t=Tapp("enum",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp_local,cs,pure_e)))))),
+					   (l,Some(([],{t=Tapp("range",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp_local,cs,pure_e)))))),
                  (l,Some(([],t2),Emp_local,cs,pure_e))))
-  | Tid("bit"),Tapp("enum",[TA_nexp b1;TA_nexp r1]) ->
-    let t',cs'= type_consistent l d_env {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} t2 in
+  | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) ->
+    let t',cs'= type_consistent l d_env {t=Tapp("range",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} t2 in
     (t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Some(([],t1),Emp_local,[],pure_e))),
 					     E_aux(E_lit(L_aux(L_num 0,l)),(l,Some(([],t2),Emp_local,[],pure_e)))),
 				     (l,Some(([],t2),Emp_local,[],pure_e)));
@@ -876,13 +906,13 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
 					     E_aux(E_lit(L_aux(L_num 1,l)),(l,Some(([],t2),Emp_local,[],pure_e)))),
 				     (l,Some(([],t2),Emp_local,[],pure_e)));]),
 		  (l,Some(([],t2),Emp_local,[],pure_e))))    
-  | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
-    let t',cs'= type_consistent l d_env t1 {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} 
+  | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
+    let t',cs'= type_consistent l d_env t1 {t=Tapp("range",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} 
     in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_one",l),[e]),(l,Some(([],bool_t),External None,[],pure_e))),
 			  E_aux(E_lit(L_aux(L_one,l)),(l,Some(([],bit_t),Emp_local,[],pure_e))),
 			  E_aux(E_lit(L_aux(L_zero,l)),(l,Some(([],bit_t),Emp_local,[],pure_e)))),
 		     (l,Some(([],bit_t),Emp_local,cs',pure_e))))
-  | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> 
+  | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> 
     (match Envmap.apply d_env.enum_env i with
     | Some(enums) -> 
       (t2,[Eq(l,b1,{nexp=Nconst 0});LtEq(l,r1,{nexp=Nconst (List.length enums)})],
@@ -897,7 +927,7 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
   | Tid("bit"),Tid("bool") ->
     let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External None,[],pure_e))) in
     (t2,[],e')
-  | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> 
+  | Tid(i),Tapp("range",[TA_nexp b1;TA_nexp r1;]) -> 
     (match Envmap.apply d_env.enum_env i with
     | Some(enums) -> 
       (t2,[Eq(l,b1,{nexp=Nconst 0});GtEq(l,r1,{nexp=Nconst (List.length enums)})],
@@ -913,7 +943,40 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
 
 and type_coerce l d_env t1 e t2 = type_coerce_internal l d_env t1 [] e t2 []
 
-let resolve_constraints a = a
+let rec simple_constraint_check = function
+  | [] -> []
+  | Eq(l,n1,n2)::cs -> 
+    let n1',n2' = eval_nexp n1,eval_nexp n2 in
+    (match n1'.nexp,n2.nexp with
+      | Nconst i1, Nconst i2 -> 
+	if i1==i2 
+	then simple_constraint_check cs
+	else eq_error l ("Type constraint mismatch: constraint arising from here requires " 
+			 ^ string_of_int i1 ^ " to equal " ^ string_of_int i2)
+      | _,_ -> Eq(l,n1',n2')::(simple_constraint_check cs))
+  | GtEq(l,n1,n2)::cs -> 
+    let n1',n2' = eval_nexp n1,eval_nexp n2 in
+    (match n1'.nexp,n2.nexp with
+      | Nconst i1, Nconst i2 -> 
+	if i1>=i2 
+	then simple_constraint_check cs
+	else eq_error l ("Type constraint mismatch: constraint arising from here requires " 
+			 ^ string_of_int i1 ^ " to be greater than or equal to " ^ string_of_int i2)
+      | _,_ -> GtEq(l,n1',n2')::(simple_constraint_check cs))
+  | LtEq(l,n1,n2)::cs -> 
+    let n1',n2' = eval_nexp n1,eval_nexp n2 in
+    (match n1'.nexp,n2.nexp with
+      | Nconst i1, Nconst i2 -> 
+	if i1<=i2 
+	then simple_constraint_check cs
+	else eq_error l ("Type constraint mismatch: constraint arising from here requires " 
+			 ^ string_of_int i1 ^ " to be less than or equal to " ^ string_of_int i2)
+      | _,_ -> LtEq(l,n1',n2')::(simple_constraint_check cs))
+  | x::cs -> x::(simple_constraint_check cs)
+    
+let resolve_constraints cs = 
+  (*let complex_constraints = simple_constraint_check cs in
+  complex_constraints*) cs
 
 
 let check_tannot l annot constraints efs = 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 8184c36f..496db9df 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -69,6 +69,7 @@ type nexp_range =
   | GtEq of Parse_ast.l * nexp * nexp
   | In of Parse_ast.l * string * int list
   | InS of Parse_ast.l * nexp * int list (* This holds the given value for string after a substitution *)
+  | InOpen of Parse_ast.l * nexp * int list (* This holds a non-exhaustive value/s for a var or nuvar during constraint gathering *)
 
 type t_params = (string * kind) list
 type tannot = ((t_params * t) * tag * nexp_range list * effect) option
@@ -115,6 +116,8 @@ val new_e : unit -> effect
 val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect
 val get_abbrev : def_envs -> t -> (t * nexp_range list * effect)
 
+val eval_nexp : nexp -> nexp
+
 (*May raise an exception if a contradiction is found*)
 val resolve_constraints : nexp_range list -> nexp_range list