Add overflow checking arithmetic operations. Fix various bugs that this exposed

Of note: Interp_lib.to_num now takes an Unsigned or a Signed constructor, rather than a boolean

8 files changed, 154 insertions, 67 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 50e37cf2..085e2fe2 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -334,9 +334,10 @@ val list_length : forall 'a . list 'a -> integer
 let list_length l = integerFromNat (List.length l)
 
 val taint: value -> list reg_form -> value
-let taint value regs = 
+let rec taint value regs = 
   match value with 
   | V_track value rs -> V_track value (regs ++ rs)
+  | V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
   | _ -> V_track value regs
 end
 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 58a92cef..90d162e7 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -58,7 +58,7 @@ end
 
 let integer_of_byte_list bytes =
   let intv = intern_value (Bytevector bytes) in
-  match Interp_lib.to_num false intv with
+  match Interp_lib.to_num Interp_lib.Unsigned intv with
     | Interp.V_lit (L_aux (L_num n) _) -> n
   end
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 823e358b..6c0d5b31 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -115,6 +115,8 @@ let rec bitwise_binop op (V_tuple [v1;v2]) =
   | (_,V_unknown) -> V_unknown
 end ;;
 
+type signed = Unsigned | Signed
+
 (* BitSeq expects LSB first.
  * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
  * hence MSB first.
@@ -123,14 +125,9 @@ let rec to_num signed v =
   match v with
   | (V_vector idx inc l) ->
   (* Word library in Lem expects bitseq with LSB first *)
-(*TODO: Kathy think more
-  We thought a reverse was needed due to above comments only in inc case.
-  However, we seem to be interpresting bit vectors such that reverse is always needed
-  and despite numbering MSB is on the left.
-*)
-  let l = (*if inc then reverse l else l*) reverse l in
+  let l = reverse l in
   (* Make sure the last bit is a zero to force unsigned numbers *)
-  let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
+  let l = match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end in
   V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
   | V_unknown -> V_unknown
   | V_track v r -> taint (to_num signed v) r
@@ -166,7 +163,7 @@ let to_vec ord len n =
 
 let rec exts (V_tuple[v1;v]) = match v1 with
   | V_lit(L_aux (L_num len) _) -> (match v with
-      | V_vector _ inc _  -> to_vec inc (natFromInteger len) (to_num true v)
+      | V_vector _ inc _  -> to_vec inc (natFromInteger len) (to_num Signed v)
       | V_unknown -> V_unknown
       | V_track v r2 -> taint (exts (V_tuple[v1;v])) r2 end)
   | V_unknown -> v1
@@ -176,8 +173,8 @@ end
 
 let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
 (* XXX interpret vectors as unsigned numbers for equality *)
-let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num false v; r]) ;;
-let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num false v]) ;;
+let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num Unsigned v; r]) ;;
+let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num Unsigned v]) ;;
 
 let rec neg v = match v with
   | V_lit (L_aux arg la) -> 
@@ -202,7 +199,7 @@ let rec arith_op op (V_tuple args) = match args with
   end ;;
 let rec arith_op_vec op size (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num false l1,to_num false l2) in
+    let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
     let n = arith_op op (V_tuple [l1';l2']) in
     to_vec ord ((List.length cs) * size) n
   | [V_track v1 r1;V_track v2 r2] ->
@@ -214,6 +211,36 @@ let rec arith_op_vec op size (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
 end ;;
+let rec arith_op_vec_vec_range op (V_tuple args) = match args with
+  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
+    let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+    arith_op op (V_tuple [l1';l2'])
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] ->
+    taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] ->
+    taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
+end ;;
+let rec arith_op_overflow_vec op size (V_tuple args) = match args with
+  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
+    let (l1',l2') = (to_num Signed l1,to_num Signed l2) in
+    let n = arith_op op (V_tuple [l1';l2']) in
+    let correct_size_num = to_vec ord ((List.length cs) * size) n in
+    let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
+    let overflow =  neq (V_tuple [correct_size_num;one_larger]) in
+    V_tuple [correct_size_num;overflow]
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] ->
+    taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] ->
+    taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown]
+  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown]
+end ;;
 let rec arith_op_range_vec op size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
     taint (arith_op_range_vec op size (V_tuple [v1;v2])) (r1++r2)
@@ -248,7 +275,7 @@ let rec arith_op_range_vec_range op (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [n;(V_vector _ ord _ as l2)] ->
-    arith_op op (V_tuple [n;(to_num false l2)])
+    arith_op op (V_tuple [n;(to_num Unsigned l2)])
 end ;;
 let rec arith_op_vec_range_range op (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
@@ -260,7 +287,7 @@ let rec arith_op_vec_range_range op (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord _ as l1);n] ->
-    arith_op op (V_tuple [(to_num false l1);n])
+    arith_op op (V_tuple [(to_num Unsigned l1);n])
 end ;;
 
 let rec compare_op op (V_tuple args) = match args with
@@ -287,7 +314,7 @@ let rec compare_op_vec op (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
-    let (l1',l2') = (to_num true l1, to_num true l2) in
+    let (l1',l2') = (to_num Signed l1, to_num Signed l2) in
     compare_op op (V_tuple[l1';l2'])
 end ;;
 
@@ -330,16 +357,20 @@ let function_map = [
   ("add_vec_range_range", arith_op_vec_range_range (+));
   ("add_range_vec", arith_op_range_vec (+) 1);
   ("add_range_vec_range", arith_op_range_vec_range (+));
+  ("add_vec_vec_range", arith_op_vec_vec_range (+));
+  ("add_overload_vec", arith_op_overflow_vec (+) 1);
   ("minus", arith_op (-));
   ("minus_vec", arith_op_vec (-) 1);
   ("minus_vec_range", arith_op_vec_range (-) 1);
   ("minus_range_vec", arith_op_range_vec (-) 1);
   ("minus_vec_range_range", arith_op_vec_range_range (-));
   ("minus_range_vec_range", arith_op_range_vec_range (-));
+  ("minus_overload_vec", arith_op_overflow_vec (-) 1);
   ("multiply", arith_op ( * ));
   ("multiply_vec", arith_op_vec ( * ) 2);
   ("mult_range_vec", arith_op_range_vec ( * ) 2);
   ("mult_vec_range", arith_op_vec_range ( * ) 2);
+  ("mult_overload_vec", arith_op_overflow_vec ( * ) 2);
   ("mod", arith_op (mod));
   ("mod_vec", arith_op_vec (mod) 1);
   ("mod_vec_range", arith_op_vec_range (mod) 1);
@@ -349,8 +380,8 @@ let function_map = [
   ("neq", neq);
   ("vec_concat", vec_concat);
   ("is_one", is_one);
-  ("to_num_inc", to_num false);
-  ("to_num_dec", to_num false);
+  ("to_num_inc", to_num Unsigned);
+  ("to_num_dec", to_num Unsigned);
   ("EXTS", exts);
   ("to_vec_inc", to_vec_inc);
   ("to_vec_dec", to_vec_dec);
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index d47a87b4..99b1f974 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -259,7 +259,7 @@ let instr_parm_to_string (name, typ, value) =
     | Other,_ -> "Unrepresentable external value"
     | _, Unknown0 -> "Unknown"
     | _, v -> let intern_v = (Interp_inter_imp.intern_value value) in
-	      match Interp_lib.to_num false intern_v with
+	      match Interp_lib.to_num Interp_lib.Unsigned intern_v with
 		| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
 		| _ -> val_to_string value
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 98b6f0d8..48855e64 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -241,8 +241,8 @@ let rec pp_format_t t =
     | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
     | 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(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
-    | Toptions _ -> "(T_var \"fresh_v\" Unknown)"
+    | Tuvar(_) -> "(T_var \"fresh_v\")"
+    | Toptions _ -> "(T_var \"fresh_v\")"
 and pp_format_targ = function
   | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
   | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
@@ -291,7 +291,7 @@ let pp_format_tag = function
 
 let rec pp_format_nes nes = 
   "[" ^ 
-  (*(list_format "; "
+  (list_format "; "
      (fun ne -> match ne with
        | 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 ^ ")"
@@ -305,7 +305,7 @@ let rec pp_format_nes nes =
        | BranchCons(_,nes_b) ->
          "(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"
      )
-     nes) ^*) "]"
+     nes) ^ "]"
 
 let pp_format_annot = function
   | NoTyp -> "Nothing"
@@ -986,11 +986,11 @@ let doc_exp, doc_let =
   | LB_val_explicit(ts,pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals])
-        (exp e)
+        (atomic_exp e)
   | LB_val_implicit(pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_atomic_pat pat; equals])
-        (exp e)
+        (atomic_exp e)
 
   and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e)
 
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 8ae00d78..8143bf5d 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -45,7 +45,7 @@ typedef colors = enumerate { red; green; blue }
 
 let (colors) rgb = red
 
-function bit enu (red) = 0
+function bit enu ((colors) red) = let (one, two) = (1,2) in 0
 
 function bit main _ = {ignore(sw(0)); ignore((nat) v2); ignore(enu(0)); v1[0] }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 884e90c6..0d9a245d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -558,7 +558,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       in
       let coerce_parms arg_t parms expect_arg_t =
 	(match parms with
-	| [parm] -> let _,cs,ef,parm' = type_coerce (Expr l) d_env false arg_t parm expect_arg_t in [parm'],ef,cs
+	| [parm] -> 
+	  let _,cs,ef,parm' = type_coerce (Expr l) d_env false arg_t parm expect_arg_t in [parm'],ef,cs
 	| parms ->
           (match type_coerce (Expr l) d_env false arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t with
           | (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs)
@@ -571,6 +572,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	    (*let _ = Printf.printf "implicit length or var required, no imp_param\n!" in*)
             let internal_exp =  match expect_t.t,ret.t with 
               | Tapp("vector",_),_ -> 
+		(*let _ = Printf.printf "adding internal exp on expext_t: %s %s \n" (t_to_string expect_t) (t_to_string ret) in*)
 		E_aux (E_internal_exp (l,Base(([],expect_t),Emp_local,[],pure_e)), (l,Base(([],nat_t),Emp_local,[],pure_e)))
               | _,Tapp("vector",_) -> 
 		E_aux (E_internal_exp (l,Base(([],ret),Emp_local,[],pure_e)), (l,Base(([],nat_t),Emp_local,[],pure_e)))
@@ -619,9 +621,13 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	let args,arg_t,arg_cs,arg_ef = 
 	  (match t_p.t with
 	  | Tfn(arg,ret,_,ef') -> check_parms arg parms 
-	  | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
+	  | _ -> 
+	    typ_error l ("Expected a function or constructor, found identifier " ^ i
+			 ^ " bound to type " ^ (t_to_string t))) in
 	(match (select_overload_variant d_env true overload_return variants arg_t) with
-	  | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+	  | [] -> typ_error l 
+	    ("No matching function found with name " ^ i ^ " that expects parameters " ^ 
+		(t_to_string arg_t))
 	  | [Base((params,t),tag,cs,ef)] ->
 	    (match t.t with
 	      | Tfn(arg,ret,imp,ef') ->
@@ -632,7 +638,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	      | _ -> raise (Reporting_basic.err_unreachable l "Overloaded variant not a function"))
 	  | variants' ->
 	    (match select_overload_variant d_env false true variants' expect_t with
-	      | [] -> typ_error l ("No matching function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
+	      | [] ->
+		typ_error l ("No matching function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
 	      | [Base((params,t),tag,cs,ef)] ->
 		(match t.t with
 		  |Tfn(arg,ret,imp,ef') ->
@@ -679,36 +686,47 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	let lft',rht',arg_t,arg_cs,arg_ef =  
 	  (match t_p.t with
 	  | Tfn(arg,ret,_,ef') -> check_parms arg lft rht
-	  | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
+	  | _ -> typ_error l ("Expected a function or constructor, found identifier " ^
+				 i ^ " bound to type " ^ (t_to_string t))) in
         (*let _ = Printf.printf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" i (t_to_string t_p) (t_to_string arg_t) in*)
 	(match (select_overload_variant d_env true overload_return variants arg_t) with
-	| [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+	| [] -> 
+	  typ_error l ("No matching function found with name " ^ i ^
+			  " that expects parameters " ^ (t_to_string arg_t))
 	| [Base((params,t),tag,cs,ef)] ->
-          (*let _ = Printf.printf "Selected an overloaded function for %s, variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
+          (*let _ = Printf.printf "Selected an overloaded function for %s,
+	    variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
 	  (match t.t with
 	  | Tfn(arg,ret,imp,ef') ->
             (match arg.t,arg_t.t with
             | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) ->
-              let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
-              let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in
+	      let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in
+              (*let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
+		let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in*)
 	      let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in
-	      (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,
-	       union_effects ef_r (union_effects ef_p (union_effects (union_effects (union_effects ef_lft ef_rght) arg_ef) ef')))
+	      (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,
+	       union_effects ef_r (union_effects ef_p (union_effects arg_ef ef')))
             |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type"))
 	  | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function"))
 	| variants ->
+	  (*let _ = Printf.printf "Number of variants found before looking at return value %i\n%!" (List.length variants) in*)
 	  (match (select_overload_variant d_env false true variants expect_t) with
-	    | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t))
+	    | [] -> 
+	      typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^
+			      (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t))
 	    | [Base((params,t),tag,cs,ef)] -> 
+              (*let _ = Printf.printf "Selected an overloaded function for %s,
+	    variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
 	      (match t.t with
 		| Tfn(arg,ret,imp,ef') ->
 		  (match arg.t,arg_t.t with
 		    | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) ->
-		      let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
+		      let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in
+		      (*let (_,cs_lft,ef_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
 		      let (_,cs_rght,ef_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in
-		      let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in
-		      (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,
-		       union_effects ef_r (union_effects ef_p (union_effects (union_effects (union_effects ef_lft ef_rght) arg_ef) ef')))
+		      *)let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef lft' rht' in
+		      (e',ret_t,t_env,cs_p@arg_cs@cs@cs_r,
+		       union_effects ef_r (union_effects ef_p (union_effects arg_ef ef')))
 		    |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type"))
 		| _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function"))
 	    | _ -> 
@@ -1444,17 +1462,23 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
       let t,cs,ef = subst params t cs ef in
       let (pat',env,cs1,u) = check_pattern envs emp_tag t pat in
       let (e,t,_,cs2,ef2) = check_exp envs imp_param t e in
-      let cs = resolve_constraints cs@cs1@cs2 in
+      let cs = if is_top_level then resolve_constraints cs@cs1@cs2 else cs@cs1@cs2 in
       let ef = union_effects ef ef2 in
-      let tannot = check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) in
+      let tannot = if is_top_level 
+	then check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) 
+	else (Base ((params,t),tag,cs,ef))
+      in
       (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,ef)
     | NoTyp | Overload _ -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Base"))
   | LB_val_implicit(pat,e) -> 
     let t = new_t () in
     let (pat',env,cs1,u) = check_pattern envs emp_tag (new_t ()) pat in
     let (e,t',_,cs2,ef) = check_exp envs imp_param u e in
-    let cs = resolve_constraints cs1@cs2 in
-    let tannot = check_tannot l (Base(([],t'),emp_tag,cs,ef)) cs ef (* see above *) in
+    let cs = if is_top_level then resolve_constraints cs1@cs2 else cs1@cs2 in
+    let tannot = 
+      if is_top_level then check_tannot l (Base(([],t'),emp_tag,cs,ef)) cs ef (* see above *)
+      else (Base (([],t'),emp_tag,cs,ef))
+    in
     (LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,ef)
 
 (*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
@@ -1613,7 +1637,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
 	let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
-	(*let _ = Printf.printf "about to check that %s and %s are consistent\n!" (t_to_string t') (t_to_string param_t) in*)
+	(*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
 	let exp',_,_,cs_e,ef = 
 	  check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) imp_param ret_t exp in
 	(*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 0b0a2646..83d40e64 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -143,7 +143,7 @@ let co_to_string = function
 let rec t_to_string t = 
   match t.t with
     | Tid i -> i
-    | Tvar i -> "'" ^ i
+    | Tvar i -> i
     | Tfn(t1,t2,_,e) -> (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e
     | Ttup(tups) -> "(" ^ string_of_list ", " t_to_string tups ^ ")"
     | Tapp(i,args) -> i ^ "<" ^  string_of_list ", " targ_to_string args ^ ">"
@@ -866,13 +866,25 @@ let initial_typ_env =
                    Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
                          (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
                                                mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
-                                      (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")))), External (Some "add_vec"),[],pure_e);
+                                      (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")))),
+			External (Some "add_vec"),[],pure_e);
+		   Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]),
+                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+                                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                                      (mk_range (mk_nv "q") {nexp = N2n (mk_nv "n",None)}))),
+			External (Some "add_vec_vec_range"),[],pure_e);
+                   
                    Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
                                               mk_range (mk_nv "o") (mk_nv "p")])
                                      (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
                         External (Some "add_vec_range"),
                         [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+                   Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
+                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+                                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                                      (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")); bit_t]))),
+			External (Some "add_overload_vec"),[],pure_e);
 		   Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]),
 			 (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
 					       mk_range (mk_nv "o") (mk_nv "p")])
@@ -1102,10 +1114,11 @@ let rec t_subst s_env t =
   match t.t with
   | Tvar i -> (match Envmap.apply s_env i with
                | Some(TA_typ t1) -> t1
-               | _ -> t)
+               | _ -> { t = Tvar i})
   | Tuvar _  -> new_t()
-  | Tid _ -> t
-  | Tfn(t1,t2,imp,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(ip_subst s_env imp),(e_subst s_env e)) }
+  | Tid i -> { t = Tid i}
+  | Tfn(t1,t2,imp,e) -> 
+    {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(ip_subst s_env imp),(e_subst s_env e)) }
   | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
   | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
   | Tabbrev(ti,ta) -> {t = Tabbrev(t_subst s_env ti,t_subst s_env ta) }
@@ -1125,7 +1138,7 @@ and n_subst s_env n =
   match n.nexp with
   | Nvar i -> (match Envmap.apply s_env i with
                | Some(TA_nexp n1) -> n1
-               | _ -> n)
+               | _ -> { nexp = Nvar i })
   | Nuvar _ -> new_n()
   | Nconst _ | Npos_inf | Nneg_inf -> n
   | N2n(n1,i) -> { nexp = N2n (n_subst s_env n1,i) }
@@ -1137,14 +1150,14 @@ and o_subst s_env o =
   match o.order with
   | Ovar i -> (match Envmap.apply s_env i with
                | Some(TA_ord o1) -> o1
-               | _ -> o)
+               | _ -> { order = Ovar i })
   | Ouvar _ -> new_o ()
   | _ -> o
 and e_subst s_env e =
   match e.effect with
   | Evar i -> (match Envmap.apply s_env i with
                | Some(TA_eft e1) -> e1
-               | _ -> e)
+               | _ -> {effect = Evar i})
   | Euvar _ -> new_e ()
   | _ -> e
 
@@ -1179,9 +1192,13 @@ let subst k_env t cs e =
 let rec t_remove_unifications s_env t =
   match t.t with
   | Tvar _ | Tid _-> s_env
-  | Tuvar _ -> (match fresh_tvar s_env t with
-      | Some ks -> Envmap.insert s_env ks
-      | None -> s_env)
+  | Tuvar tu -> 
+    (match tu.subst with
+      | None ->
+	(match fresh_tvar s_env t with
+	  | Some ks -> Envmap.insert s_env ks
+	  | None -> s_env)
+      | _ -> resolve_tsubst t; s_env)
   | Tfn(t1,t2,_,e) -> e_remove_unifications (t_remove_unifications (t_remove_unifications s_env t1) t2) e
   | Ttup(ts) -> List.fold_right (fun t s_env -> t_remove_unifications s_env t) ts s_env
   | Tapp(i,args) -> List.fold_right (fun t s_env -> ta_remove_unifications s_env t) args s_env
@@ -1196,9 +1213,16 @@ and ta_remove_unifications s_env ta =
 and n_remove_unifications s_env n =
   match n.nexp with
   | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env
-  | Nuvar _ -> (match fresh_nvar s_env n with
-      | Some ks -> Envmap.insert s_env ks
-      | None -> s_env)
+  | Nuvar nu -> 
+    let n' = match nu.nsubst with
+      | None -> n
+      | _ -> resolve_nsubst n; n in
+    (match n.nexp with
+      | Nuvar _ -> 
+	(match fresh_nvar s_env n with
+	  | Some ks -> Envmap.insert s_env ks
+	  | None -> s_env)
+      | _ -> s_env)
   | N2n(n1,_) | Npow(n1,_) | Nneg n1 -> (n_remove_unifications s_env n1)
   | Nadd(n1,n2) | Nmult(n1,n2) -> (n_remove_unifications (n_remove_unifications s_env n1) n2)
 and o_remove_unifications s_env o =
@@ -1479,7 +1503,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 =
       let t2' = {t=Tapp("range",[TA_nexp b2;TA_nexp r2])} in
       equate_t t2 t2';
       (t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)])
-  | t,Tuvar _ -> equate_t t2 t1; (t1,csp)
+  | t,Tuvar _ -> equate_t t2 t1; (t2,csp)
   | _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2))
 
 and type_arg_eq co d_env ta1 ta2 = 
@@ -1546,6 +1570,10 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
         | Oinc,Ouvar _ | Odec,Ouvar _ -> equate_o o2 o1;
         | Ouvar _,Oinc | Ouvar _, Odec -> equate_o o1 o2;
         | _,_ -> equate_o o1 o2); 
+        (*(match r1.nexp,r2.nexp with
+	  | Nuvar _,_ -> ignore(resolve_nsubst(r1)); equate_n r1 r2;
+	  | _,Nuvar _ -> ignore(resolve_nsubst(r2)); equate_n r2 r1;
+	  | _ -> ());*)
         let cs = csp@[Eq(co,r1,r2)] in
         let t',cs' = type_consistent co d_env t1i t2i in
         let tannot = Base(([],t2),Emp_local,cs@cs',pure_e) in
@@ -1659,18 +1687,21 @@ and type_coerce co d_env is_explicit t1 e t2 = type_coerce_internal co d_env is_
 let rec select_overload_variant d_env params_check get_all variants actual_type =
   match variants with
     | [] -> []
-    | NoTyp::variants | Overload _::variants -> select_overload_variant d_env params_check get_all variants actual_type
-    | Base((parms,t),tag,cs,ef)::variants ->
-      let t,cs,ef = subst parms t cs ef in
+    | NoTyp::variants | Overload _::variants ->
+      select_overload_variant d_env params_check get_all variants actual_type
+    | Base((parms,t_orig),tag,cs,ef)::variants ->
+      (*let _ = Printf.printf "About to check a variant %s\n" (t_to_string t_orig) in*)
+      let t,cs,ef = if parms=[] then t_orig,cs,ef else subst parms t_orig cs ef in
+      (*let _ = Printf.printf "And after substitution %s\n" (t_to_string t) in*)
       let t,cs' = get_abbrev d_env t in
       let recur _ = select_overload_variant d_env params_check get_all variants actual_type in
       (match t.t with
 	| Tfn(a,r,_,e) ->
-	  (*let _ = Printf.printf "About to check a variant\n" in*)
 	  let is_matching = 
 	    if params_check then conforms_to_t d_env true false a actual_type 
 	    else match actual_type.t with
-	      | Toptions(at1,Some at2) -> (conforms_to_t d_env false true at1 r || conforms_to_t d_env false true at2 r)
+	      | Toptions(at1,Some at2) -> 
+		(conforms_to_t d_env false true at1 r || conforms_to_t d_env false true at2 r)
 	      | Toptions(at1,None) -> conforms_to_t d_env false true at1 r
 	      | _ -> conforms_to_t d_env true true actual_type r in
 	  (*let _ = Printf.printf "Checked a variant, matching? %b\n" is_matching in*)