Solve more constraints; fix up test suite bugs uncovered by solving more constraints. Clean up Lem output a little for readability while debugging.

7 files changed, 106 insertions, 90 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a033285e..20f4a948 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -325,34 +325,34 @@ let id_of_string s = (Id_aux (Id s) Unknown)
 
 let rec combine_typs ts =
   match ts with
-  | [] -> T_var (Kid_aux (Var "fresh") Unknown)
+  | [] -> T_var "fresh"
   | [t] -> t
   | t::ts ->
     let t' = combine_typs ts in
     match (t,t') with 
       | (_,T_var _) -> t
-      | ((T_app (Id_aux (Id "enum") _) (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
-	 (T_app (Id_aux (Id "enum") _) (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
+      | ((T_app "enum" (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
+	 (T_app "enum" (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
 	let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
 	let r = (larger + larger_r) - smaller in
-	T_app (id_of_string "enum") (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
-      | ((T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); 
-						  T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
-	 (T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); 
-						  T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
+	T_app "enum" (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
+      | ((T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); 
+				   T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
+	 (T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); 
+				  T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
 	let t = combine_typs [t1;t2] in
 	match (o1,o2) with
 	  | (Ord_inc,Ord_inc) ->
 	    let larger_start = if b1 < b2 then b2 else b1 in
 	    let smaller_rise = if r1 < r2 then r1 else r2 in
-	    (T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
-						    (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+	    (T_app "vector" (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
+				     (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
 	  | (Ord_dec,Ord_dec) ->
 	    let smaller_start = if b1 < b2 then b1 else b2 in
 	    let smaller_fall = if r1 < r2 then r2 else r2 in
-	    (T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
-						    (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
-	  | _ -> T_var (Kid_aux (Var "fresh") Unknown)
+	    (T_app "vector" (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
+				     (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+	  | _ -> T_var "fresh"
 	 end 
       | _ -> t'
      end 
@@ -361,35 +361,35 @@ let rec combine_typs ts =
 let reg_to_t r =
   match r with
     | Reg id (Just (t,_,_,_)) -> t
-    | _ -> T_var (Kid_aux (Var "fresh") Unknown)
+    | _ -> T_var "fresh"
  end
 
 let rec val_typ v =
   match v with
-    | V_boxref n t -> T_app (id_of_string "reg") (T_args [T_arg_typ t])
+    | V_boxref n t -> T_app "reg" (T_args [T_arg_typ t])
     | V_lit (L_aux lit _) ->
       match lit with
-	| L_unit -> T_id (id_of_string "unit")
-	| L_true -> T_id (id_of_string "bool")
-	| L_false -> T_id (id_of_string "bool")
-	| L_one -> T_id (id_of_string "bit")
-	| L_zero -> T_id (id_of_string "bit")
-	| L_string _ -> T_id (id_of_string "string")
-	| L_num n -> T_app (id_of_string "enum") (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
-	| L_undef -> T_var (Kid_aux (Var "fresh") Unknown)
+	| L_unit -> T_id "unit"
+	| L_true -> T_id "bool"
+	| L_false -> T_id "bool"
+	| L_one -> T_id "bit"
+	| L_zero -> T_id "bit"
+	| L_string _ -> T_id "string"
+	| L_num n -> T_app "enum" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
+	| L_undef -> T_var "fresh"
       end 
     | V_tuple vals -> T_tup (List.map val_typ vals)
     | V_vector n inc vals -> 
       let ts = List.map val_typ vals in
       let t = combine_typs ts in
-      T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const (list_length vals));
-					     T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
-					     T_arg_typ t])
+      T_app "vector" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const (list_length vals));
+			      T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
+			      T_arg_typ t])
     | V_record t ivals -> t
     | V_list vals -> 
       let ts = List.map val_typ vals in
       let t = combine_typs ts in
-      T_app (id_of_string "list") (T_args [T_arg_typ t])
+      T_app "list" (T_args [T_arg_typ t])
     | V_ctor id t vals -> t
     | V_register reg -> reg_to_t reg
   end
@@ -614,8 +614,7 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps =
 and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
   let (Env defs lets regs ctors subregs) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
-    | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown),
-		  Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
+    | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
   match exp with
     | E_lit lit -> 
@@ -638,7 +637,6 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 			    | _ -> (Value v tag,lm,le) end) 
                         | _ -> (Value v Tag_empty,lm,le) end)
 	              (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast ctyp e) (l,annot)))))
- (* TODO introduce coercions to change offset of vectors *)
     | E_id id -> 
       let name = get_id id in
       match tag with
@@ -792,7 +790,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 			match (exp,a) with
 			  | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
 			     (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_))) as regf) Nothing) s)) ->
-			    match in_env subregs id' with
+			    match in_env subregs (Id_aux (Id id') Unknown) with
 			      | Just(indexes) ->
 				match in_env indexes id with
 				  | Just ir -> 
@@ -802,7 +800,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                               | Nothing -> Error l "Internal error, unrecognized read, no reg" end
                          | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
                             (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_))) as regf) Nothing) s))->
-			    match in_env subregs id' with
+			    match in_env subregs (Id_aux (Id id') Unknown) with
 			      | Just(indexes) ->
 				match in_env indexes id with
 				  | Just ir -> 
@@ -917,7 +915,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_vector_indexed(iexps) ->
       let (indexes,exps) = List.unzip iexps in
       let is_inc = match typ with
-        | T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
+        | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
         | _ -> false end in
       exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot))) 
                        (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
@@ -1054,7 +1052,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
    let (Env defs lets regs ctors subregs) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
-    | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
+    | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
    match lexp with
     | LEXP_id id -> 
@@ -1226,7 +1224,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
        | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | Write_reg ((Reg _ (Just(T_id id',_,_,_))) as regf) Nothing value -> 
-	 match in_env subregs id' with
+	 match in_env subregs (Id_aux (Id id') Unknown) with
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
@@ -1236,7 +1234,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
 		 end 
             | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
        | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_))) as regf) Nothing value -> 
-	 match in_env subregs id' with
+	 match in_env subregs (Id_aux (Id id') Unknown) with
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index dd7a1cf0..45ced731 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -6,6 +6,8 @@ open import Num
 open import List
 open import Word
 
+let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;
+
 let compose f g x = f (V_tuple [g x]) ;;
 
 let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
@@ -58,6 +60,7 @@ let rec vec_concat (V_tuple args) = match args with
   end ;;
 
 let function_map = [
+  ("ignore", ignore_sail);            
   ("add", add);
   ("eq", eq);
   ("vec_concat", vec_concat);
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 8ae6d1ee..7100a197 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -24,7 +24,7 @@ let id_to_string = function
 
 let loc_to_string = function
   | Unknown -> "Unknown"
-  | Trans(s,_) -> s
+  | Int(s,_) -> s
   | Range(s,fline,fchar,tline,tchar) -> 
     "in " ^ s ^ " from line " ^  (string_of_int fline) ^ " character " ^ (string_of_int fchar) ^ 
       " to line " ^ (string_of_int tline) ^ " character " ^ (string_of_int tchar)
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index e78f3a09..d863c2b2 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -366,8 +366,8 @@ let pp_defs ppf (Defs(defs)) =
 
 let rec pp_format_l_lem = function
   | Parse_ast.Unknown -> "Unknown"
-  | Parse_ast.Trans(s,None) -> "(Trans \"" ^ s ^ "\" Nothing)"
-  | Parse_ast.Trans(s,(Some l)) -> "(Trans \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
+  | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
+  | Parse_ast.Int(s,(Some l)) -> "(Int \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
   | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
                                (string_of_int p1.Lexing.pos_lnum) ^ " " ^ 
                                (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
@@ -535,11 +535,11 @@ let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
 
 let rec pp_format_t t =
   match t.t with
-    | Tid i -> "(T_id (Id_aux (Id \"" ^ i ^ "\") Unknown))"
-    | Tvar i -> "(T_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+    | Tid i -> "(T_id \"" ^ i ^ "\")"
+    | Tvar i -> "(T_var \"" ^ i ^ "\")"
     | Tfn(t1,t2,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")"
     | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
-    | Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
+    | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
     | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")"
     | Tuvar(_) -> assert false (*"(T_var (Kid_aux (Var \"fresh_v\") Unknown))"*)
 and pp_format_targ = function
@@ -549,13 +549,13 @@ and pp_format_targ = function
   | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")"
 and pp_format_n n =
   match n.nexp with
-    | Nvar i -> "(Ne_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+    | Nvar i -> "(Ne_var \"" ^ i ^ "\")"
     | Nconst i -> "(Ne_const " ^ string_of_int i ^ ")"
     | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
     | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
     | N2n n -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
     | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
-    | Nuvar _ -> "(Ne_var (Kid_aux (Var \"fresh_v_" ^ string_of_int (get_index n) ^ "\") Unknown))"
+    | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
 and pp_format_e e = 
   "(Effect_aux " ^
   (match e.effect with
@@ -590,9 +590,9 @@ let pp_format_nes nes =
        | 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) | InS(_,{nexp=Nvar i},ns) |InOpen(_,{nexp=Nvar i},ns)-> 
-	 "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])"
+	 "(Nec_in \"" ^ i ^ "\" [" ^ (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)^ "])"
+	 "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"
      )
      nes) ^ "]"
 
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index b3880598..3d211d82 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -76,11 +76,11 @@ let read_from_file_pos2 p1 p2 =
   let _ = close_in ic in
   (buf, not (multi = None))
 
-(* Destruct a location by splitting all the Trans strings except possibly the
+(* Destruct a location by splitting all the Internal strings except possibly the
    last one into a string list and keeping only the last location *)
 let dest_loc (l : Parse_ast.l) : (Parse_ast.l * string list) = 
   let rec aux acc l = match l with
-    | Parse_ast.Trans(s, Some l') -> aux (s::acc) l'
+    | Parse_ast.Int(s, Some l') -> aux (s::acc) l'
     | _ -> (l, acc)
   in
   aux [] l
@@ -90,7 +90,7 @@ let rec format_loc_aux ff l =
   let _ = match l_org with
     | Parse_ast.Unknown -> Format.fprintf ff "no location information available"
     | Parse_ast.Range(p1,p2) -> format_pos2 ff p1 p2
-    | Parse_ast.Trans(s,_) -> Format.fprintf ff "code generated by: %s" s
+    | Parse_ast.Int(s,_) -> Format.fprintf ff "code generated by: %s" s
   in
   ()
 
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 78d60513..06086dd7 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -1,5 +1,5 @@
 (* a register containing nat numbers *)
-register nat dummy_reg
+register [|0:256|] dummy_reg
 (* and one containing a byte *)
 register (bit[8]) dummy_reg2
 (* a function to read from memory; wmem serves no purpose currently,
@@ -9,18 +9,6 @@ val extern nat -> nat effect { wmem , rmem }  MEM_GPU
 val extern forall Nat 'n . ( nat, [|'n|] ) -> (bit['n * 8]) effect { wmem , rmem }  MEM_SIZE
 val extern nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
 
-(* XXX types are wrong *)
-val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc"
-val extern forall Type 'a . 'a -> nat effect pure to_num_dec = "to_num_dec"
-val extern forall Type 'a . nat -> 'a effect pure to_vec_inc = "to_vec_inc"
-val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec"
-
-function unit ignore(x) = ()
-
-(* extern functions *)
-val extern ( nat, nat ) -> nat effect pure add = "add"
-val extern ( nat, nat ) -> nat effect pure (deinfix + ) = "add"   (* infix plus *)
-
 function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
 function nat main _ = {
@@ -57,10 +45,10 @@ function nat main _ = {
 
   (* extern calls *)
   dummy_reg := 3 + 39;
-  dummy_reg := add(5, 37);
+  dummy_reg := (deinfix +)(5, 37);
   (* casts and external calls *)
   dummy_reg := 0b01 + 0b01;
-  dummy_reg2 := dummy_reg;               (* cast from nat to bit[8] *)
+  dummy_reg2 := dummy_reg;               (* cast from [|256|] to bit[8] *)
   dummy_reg2 := dummy_reg2 + dummy_reg2; (* cast to nat for add call *)
   dummy_reg2;                            (* cast again and return 4 *)
 }
diff --git a/src/type_internal.ml b/src/type_internal.ml
index b6b58d75..e406e976 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -249,7 +249,7 @@ let rec eval_nexp n =
 	  let rec two_pow n =
 	    match n with 
 	    | 0 -> 1
-	    | n -> (two_pow (n-1)) in
+	    | n -> 2*(two_pow (n-1)) in
 	  {nexp = Nconst(two_pow i)}
 	| _ -> {nexp = N2n n1'})
     | Nvar _ | Nuvar _ -> n
@@ -303,7 +303,7 @@ let rec resolve_nsubst (n : nexp) : nexp = match n.nexp with
   | Nuvar({ nsubst=Some(n') } as u) ->
     let n'' = resolve_nsubst n' in
     (match n''.nexp with
-    | Nuvar(_) -> u.nsubst <- Some(n''); n''
+    | Nuvar(m) -> if u.nin then m.nin <- true else (); u.nsubst <- Some(n''); n''
     | x -> n.nexp <- x; n)
   | _ -> n
 let rec resolve_osubst (o : order) : order = match o.order with
@@ -498,15 +498,23 @@ let initial_kind_env =
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
   ]
 
-let mk_range n = {t=Tapp("range",[TA_nexp {nexp=n};TA_nexp {nexp=Nconst 0}])}
+let mk_range n1 n2 = {t=Tapp("range",[TA_nexp {nexp=n1};TA_nexp {nexp=n2}])}
 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));
-    ("+",Some(([("n",{k=K_Nat});("m",{k=K_Nat})],{t= Tfn({t=Ttup([mk_range (Nvar "n");mk_range (Nvar "m")])},
-							 (mk_range (Nadd({nexp=Nvar "n"},{nexp=Nvar "m"}))),
-							 pure_e)}),External (Some "add"),[],pure_e));
+    ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,pure_e)}),External None,[],pure_e));
+    ("+",Some(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+               {t= Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");
+                                mk_range (Nvar "o") (Nvar "p")])},
+		       (mk_range (Nadd({nexp=Nvar "n"},{nexp=Nvar "o"})) (Nadd({nexp=Nvar "m"},{nexp=Nvar "p"}))),
+		       pure_e)}),External (Some "add"),[],pure_e));
     ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e));
-    ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e));
+    ("-",Some(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
+               {t= Tfn({t=Ttup([mk_range (Nvar "n") (Nvar "m");
+                                mk_range (Nvar "o") (Nvar "p")])},
+		       (mk_range (Nadd ({nexp=(Nvar "n")},{ nexp = Nneg({nexp=Nvar "o"})})) (Nadd({nexp=Nvar "m"},{nexp =Nneg {nexp=Nvar "p"}}))),
+		       pure_e)}),External (Some "minus"),
+              [GtEq(Spec(Parse_ast.Int("-",None)),{nexp=Nvar "n"},{nexp=Nvar "o"});
+               GtEq(Spec(Parse_ast.Int("-",None)),{nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nvar "o"})],pure_e));
     ("mod",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e));
     ("quot",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "quot"),[],pure_e));
     (*Type incomplete*)
@@ -527,10 +535,11 @@ let initial_typ_env =
     ("|",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_or"),[],pure_e));
     ("^",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_xor"),[],pure_e));
     ("&",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_and"),[],pure_e));
-    ("^^",Some((["n",{k=K_Nat}],{t= Tfn ({t=Ttup([bit_t;mk_range (Nvar "n")])},
-					  {t=Tapp("vector",[TA_nexp {nexp=Nconst 0}; TA_nexp {nexp=Nvar "n"};
-							    TA_ord {order = Oinc}; TA_typ bit_t])},
-					  pure_e)}),External (Some "duplicate"),[],pure_e));
+    ("^^",Some(([("n",{k=K_Nat});("m",{k=K_Nat})],
+                {t= Tfn ({t=Ttup([bit_t;mk_range (Nvar "n") (Nvar "m")])},
+			 {t=Tapp("vector",[TA_nexp {nexp=Nconst 0}; TA_nexp {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})};
+					   TA_ord {order = Oinc}; TA_typ bit_t])},
+			 pure_e)}),External (Some "duplicate"),[],pure_e));
     ("<<<",Some((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};nat_typ])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_leftshift"),[],pure_e));
   ]
 
@@ -540,7 +549,6 @@ let initial_abbrev_env =
   ]
 
 let rec t_subst s_env t =
-  (*let _ = Printf.printf "Calling t_subst on %s\n" (t_to_string t) in*)
   match t.t with
   | Tvar i -> (match Envmap.apply s_env i with
                | Some(TA_typ t1) -> t1
@@ -589,7 +597,12 @@ let rec cs_subst t_env cs =
     | Eq(l,n1,n2)::cs -> Eq(l,n_subst t_env n1,n_subst t_env n2)::(cs_subst t_env cs)
     | GtEq(l,n1,n2)::cs -> GtEq(l,n_subst t_env n1, n_subst t_env n2)::(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)
+    | In(l,s,ns)::cs -> 
+      let nexp = n_subst t_env {nexp=Nvar s} in
+      (match nexp.nexp with
+      | Nuvar urec -> urec.nin <- true
+      | _ -> ()); 
+      InS(l,nexp,ns)::(cs_subst t_env cs)
     | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
 
 let subst k_env t cs e =
@@ -993,19 +1006,29 @@ let rec simple_constraint_check cs =
   | Eq(co,n1,n2)::cs -> 
 (*    let _ = Printf.printf "eq check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
-(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
-    (match n1'.nexp,n2.nexp with
+(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
+    (match n1'.nexp,n2'.nexp with
     | Nconst i1, Nconst i2 -> 
       if i1==i2 
       then simple_constraint_check cs
       else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " 
 			            ^ string_of_int i1 ^ " to equal " ^ string_of_int i2)
+    | Nconst i, Nuvar u ->
+      if u.nin
+      then Eq(co,n1',n2')::(simple_constraint_check cs)
+      else begin equate_n n2' n1'; (simple_constraint_check cs) end
+    | Nuvar u, Nconst i ->
+      if u.nin
+      then Eq(co,n1',n2')::(simple_constraint_check cs)
+      else begin equate_n n1' n2'; (simple_constraint_check cs) end
+    | Nuvar u1, Nuvar u2 ->
+      resolve_nsubst n1; resolve_nsubst n2; equate_n n1' n2'; (simple_constraint_check cs)
     | _,_ -> Eq(co,n1',n2')::(simple_constraint_check cs))
   | GtEq(co,n1,n2)::cs -> 
-(*    let _ = Printf.printf ">= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in*)
+(*    let _ = Printf.printf ">= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
-(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
-    (match n1'.nexp,n2.nexp with
+(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
+    (match n1'.nexp,n2'.nexp with
     | Nconst i1, Nconst i2 -> 
       if i1>=i2 
       then simple_constraint_check cs
@@ -1013,10 +1036,10 @@ let rec simple_constraint_check cs =
 			            ^ string_of_int i1 ^ " to be greater than or equal to " ^ string_of_int i2)
     | _,_ -> GtEq(co,n1',n2')::(simple_constraint_check cs))
   | LtEq(co,n1,n2)::cs -> 
-    (*    let _ = Printf.printf "<= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
+(*    let _ = Printf.printf "<= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
-    (*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
-    (match n1'.nexp,n2.nexp with
+(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
+    (match n1'.nexp,n2'.nexp with
     | Nconst i1, Nconst i2 -> 
       if i1<=i2 
       then simple_constraint_check cs
@@ -1030,10 +1053,14 @@ let do_resolve_constraints = ref true
 let resolve_constraints cs = 
   if not !do_resolve_constraints
   then cs
-  else begin
-    let complex_constraints = simple_constraint_check cs in
-    complex_constraints (*cs*)
-  end
+  else
+    let rec fix len cs =
+(*      let _ = Printf.printf "Calling simple constraint check, fix check point is %i\n" len in *)
+      let cs' = simple_constraint_check cs in
+      if len > (List.length cs') then fix (List.length cs') cs'
+      else cs' in
+    let complex_constraints = fix (List.length cs) cs in
+    complex_constraints
 
 
 let check_tannot l annot constraints efs =