fix various bugs exposed by armv8

2 files changed, 95 insertions, 46 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 4023f021..005cd70b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -207,12 +207,20 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 			       [TA_nexp{nexp = Nconst (big_int_of_int i)};TA_nexp{nexp= Nconst zero};])},lit
 	      | _ -> {t = Tapp("range",
 			       [TA_nexp{nexp = Nconst (big_int_of_int i)};TA_nexp{nexp= Nconst zero};])},lit)
-	  | L_hex s -> {t = Tapp("vector",
-				 [TA_nexp{nexp = Nconst zero};TA_nexp{nexp = Nconst (big_int_of_int ((String.length s)*4))};
-				  TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])},lit
-	  | L_bin s -> {t = Tapp("vector",
-				 [TA_nexp{nexp = Nconst zero};TA_nexp{nexp = Nconst(big_int_of_int (String.length s))};
-				  TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])},lit
+	  | L_hex s -> 
+	    let size = big_int_of_int ((String.length s) * 4) in
+	    let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in
+	    {t = Tapp("vector",
+		      [TA_nexp (if is_inc then {nexp = Nconst zero} else {nexp = Nconst (sub_big_int size one)});
+		       TA_nexp {nexp = Nconst size};
+		       TA_ord d_env.default_o; TA_typ{t=Tid "bit"}])},lit
+	  | L_bin s -> 
+	    let size = big_int_of_int (String.length s) in
+	    let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in
+	    {t = Tapp("vector",
+		      [TA_nexp(if is_inc then {nexp = Nconst zero} else {nexp = Nconst (sub_big_int size one)});
+		       TA_nexp{nexp = Nconst size};
+		       TA_ord d_env.default_o;TA_typ{t = Tid"bit"}])},lit
 	  | L_string s -> {t = Tid "string"},lit
 	  | L_undef -> typ_error l' "Cannot pattern match on undefined") in
       let t',cs' = type_consistent (Patt l) d_env t expect_t in
@@ -363,7 +371,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	match expect_t.t with 
 	  | Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])
 	  | Tabbrev(_,{t=Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])}) -> item,b,r,o
-	  | _ -> new_t (),new_n (), new_n (), new_o () in
+	  | _ -> new_t (),new_n (), new_n (), d_env.default_o in
       let vec_ti _ = {t= Tapp("vector",[TA_nexp (new_n ());TA_nexp (new_n ());TA_ord order;TA_typ item_t])} in
       let (pats',ts,envs,constraints) = 
 	List.fold_right 
@@ -382,7 +390,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	  match t.t with
 	    | Tapp("vector",[(TA_nexp b);(TA_nexp r);(TA_ord o);(TA_typ u)]) -> {nexp = Nadd(r,rn)}
 	    | _ -> raise (Reporting_basic.err_unreachable l "vector concat pattern impossibility") ) (List.tl ts) r1 in
-      let cs = [Eq((Patt l),base,base_c);Eq((Patt l),rise,range_c)]@cs in
+      let cs = [Eq((Patt l),rise,range_c)]@cs in
       (P_aux(P_vector_concat(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
     | P_list(pats) -> 
       let item_t = match expect_actual.t with
@@ -539,10 +547,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
           | (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs)
           | _ -> raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) 
       in
-      let check_result ret imp tag cs ef parms =           
+      let check_result ret imp tag cs ef parms =    
 	(*TODO How do I want to pass the information about start along?*)
 	match (imp,imp_param) with
 	  | (IP_length,None) | (IP_var _,None) ->
+	    (*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",_),_ -> 
 		E_aux (E_internal_exp (l,Base(([],expect_t),Emp_local,[],pure_e)), (l,Base(([],nat_t),Emp_local,[],pure_e)))
@@ -551,6 +560,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
               | _ -> typ_error l (i ^ " expected either the return type or the expected type to be a vector") in
             type_coerce (Expr l) d_env false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef))))) expect_t
 	  | (IP_length,Some ne) | (IP_var _,Some ne) ->
+	    (*let _ = Printf.printf "implicit length or var required with imp_param\n" in*)
 	    let internal_exp = (match expect_t.t,ret.t with
 	      | Tapp("vector",[_;TA_nexp len;_;_]),_ ->
 		if nexp_eq ne len 
@@ -568,6 +578,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 			    (l,Base(([],nat_t), Emp_local,[],pure_e))) (*TODO as above*)) in
 	    type_coerce (Expr l) d_env false ret (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef))))) expect_t
           | (IP_none,_) -> 
+	    (*let _ = Printf.printf "no implicit length or var required\n" in*)
             type_coerce (Expr l) d_env false ret (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef))))) expect_t 
       in
       (match Envmap.apply t_env i with
@@ -579,8 +590,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         let t,cs,ef = subst params t cs ef in
         (match t.t with
         | Tfn(arg,ret,imp,ef') ->
+	  (*let _ = Printf.printf "Checking funcation call of %s\n" i in*)
           let parms,arg_t,cs_p,ef_p = check_parms arg parms in
+	  (*let _ = Printf.printf "Checked parms of %s\n" i in*)
           let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' parms in
+	  (*let _ = Printf.printf "Checked result of %s\n" i in*)
           (e',ret_t,t_env,cs@cs_p@cs_r, union_effects ef' (union_effects ef_p ef_r))
         | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
       | Some(Overload(Base((params,t),tag,cs,ef),overload_return,variants)) ->
@@ -1460,21 +1474,23 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
 	    let franges = 
 	      List.map 
 		(fun ((BF_aux(idx,l)),id) ->
-		  let (base,climb) =
-		    match idx with
-		      | BF_single i -> 
-			if (ge_big_int b (big_int_of_int i)) && (ge_big_int (big_int_of_int i) t) 
-			then {nexp=Nconst (big_int_of_int i)},{nexp=Nconst zero}
-			else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
-		      | BF_range(i1,i2) -> 
-			if i1>i2 
-			then if (ge_big_int b (big_int_of_int i1)) && (ge_big_int (big_int_of_int i2) t) 
-			  then {nexp=Nconst (big_int_of_int i1)},{nexp=Nconst (big_int_of_int (i1 - i2))}
-			  else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
-			else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing")
-		      | BF_concat _ -> assert false (* What is this supposed to imply again?*) in
 		  ((id_to_string id),
-		   Base(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp_global,[],pure_e)))
+		   Base(([],
+			 match idx with
+			   | BF_single i -> 
+			     if (ge_big_int b (big_int_of_int i)) && (ge_big_int (big_int_of_int i) t) 
+			     then {t = Tid "bit"}
+			     else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+			   | BF_range(i1,i2) -> 
+			     if i1>i2 
+			     then if (ge_big_int b (big_int_of_int i1)) && (ge_big_int (big_int_of_int i2) t) 
+			       then {t = Tapp("vector",[TA_nexp {nexp=Nconst (big_int_of_int i1)};
+							TA_nexp {nexp=Nconst (big_int_of_int (i1 - i2))};
+							TA_ord({order = Odec}); TA_typ({t = Tid "bit"})])}
+			       else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+			     else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing")
+			   | BF_concat _ -> assert false (* What is this supposed to imply again?*)),
+			Emp_global,[],pure_e)))
 		ranges 
 	    in
 	    let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e)) in
@@ -1510,6 +1526,7 @@ let check_default envs (DT_aux(ds,l)) =
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
 let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) =
+  (*let _ = Printf.printf "checking fundef\n" in*)
   let Env(d_env,t_env) = envs in
   let _ = reset_fresh () in
   let is_rec = match recopt with
@@ -1535,11 +1552,10 @@ 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.eprintf "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.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
-      (*let _ = (Pretty_print.pp_exp Format.std_formatter) 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*)
 	let cs = [CondCons(Fun l,cs_p,cs_e)] in
 	(FCL_aux((FCL_Funcl(id,pat',exp')),l),(cs,ef))) funcls) in
   let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),l)) = 
@@ -1551,10 +1567,10 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   in
   match (in_env,tannot) with
     | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') ->
-      (*let _ = Printf.eprintf "Function %s is in env\n" id in*)
+      (*let _ = Printf.printf "Function %s is in env\n" id in*)
       let u,constraints,eft = subst params u constraints eft in
       let _,cs = type_consistent (Specc l) d_env t u in
-      (*let _ = Printf.eprintf "valspec consistent with declared type for %s\n" id in*)
+      (*let _ = Printf.printf "valspec consistent with declared type for %s\n" id in*)
       let imp_param = match u.t with 
 	| Tfn(_,_,IP_var n,_) -> Some n
 	| _ -> None in
@@ -1564,10 +1580,11 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
 	(List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
       let cs' = resolve_constraints cs@constraints in
       let tannot = check_tannot l tannot cs' ef in
-      (*let _ = Printf.eprintf "check_tannot ok for %s\n" id in*)
+      (*let _ = Printf.printf "check_tannot ok for %s\n" id in*)
       let funcls = match imp_param with
 	| None | Some {nexp = Nconst _} -> funcls
 	| Some {nexp = Nvar i} -> List.map (update_pattern i) funcls in
+      (*let _ = Printf.printf "done funcheck case 1\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,Envmap.insert t_env (id,tannot))
     | _ , _-> 
@@ -1576,6 +1593,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
       let cs' = resolve_constraints cs in
       let tannot = check_tannot l tannot cs' ef in
+      (*let _ = Printf.printf "done funcheck case2\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)))
 
@@ -1662,29 +1680,47 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 let check_def envs def = 
   let (Env(d_env,t_env)) = envs in
   match def with
-  | DEF_type tdef -> let td,envs = check_type_def envs tdef in
-		     (DEF_type td,envs)
-  | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in
-		       (DEF_fundef fd,envs)
-  | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs None true Emp_global letdef in
-                      (DEF_val letbind,Env(d_env,Envmap.union t_env t_env_let))
-  | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
-		     (DEF_spec vs, envs)
+  | DEF_type tdef ->
+(*    let _ = Printf.printf "checking type def\n" in*)
+    let td,envs = check_type_def envs tdef in
+(*    let _ = Printf.printf "checked type def\n" in*)
+    (DEF_type td,envs)
+  | DEF_fundef fdef -> 
+(*    let _ = Printf.printf "checking fun def\n" in*)
+    let fd,envs = check_fundef envs fdef in
+(*    let _ = Printf.printf "checked fun def\n" in*)
+    (DEF_fundef fd,envs)
+  | DEF_val letdef -> 
+(*    let _ = Printf.printf "checking letdef\n" in*)
+    let (letbind,t_env_let,_,eft) = check_lbind envs None true Emp_global letdef in
+(*    let _ = Printf.printf "checked letdef\n" in*)
+    (DEF_val letbind,Env(d_env,Envmap.union t_env t_env_let))
+  | DEF_spec spec -> 
+(*    let _ = Printf.printf "checking spec\n" in*)
+    let vs,envs = check_val_spec envs spec in
+  (*  let _ = Printf.printf "checked spec\n" in*)
+    (DEF_spec vs, envs)
   | DEF_default default -> let ds,envs = check_default envs default in
 			   (DEF_default ds,envs)
   | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> 
+(*    let _ = Printf.printf "checking reg dec\n" in *)
     let t = (typ_to_t false typ) in
     let i = id_to_string id in
     let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e)) in
+(*    let _ = Printf.printf "done checking reg dec\n" in*)
     (DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
   | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> 
+(*    let _ = Printf.printf "checking reg dec b\n" in*)
     let i = id_to_string id in
     let (aspec,tannot,d_env) = check_alias_spec envs i aspec None in
+  (*  let _ = Printf.printf "done checking reg dec b\n" in *)
     (DEF_reg_dec(DEC_aux(DEC_alias(id,aspec),(l,tannot))),(Env(d_env, Envmap.insert t_env (i,tannot))))
   | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) ->
+(*    let _ = Printf.printf "checking reg dec c\n" in*)
     let i = id_to_string id in
     let t = typ_to_t false typ in
     let (aspec,tannot,d_env) = check_alias_spec envs i aspec (Some t) in
+(*    let _ = Printf.printf "done checking reg dec c\n" in*)
     (DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 72f3b30d..63cb5fd0 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -24,7 +24,7 @@ and k_aux =
   | K_Lam of kind list * kind
   | K_infer
 
-type t = { mutable t : t_aux }
+ type t = { mutable t : t_aux }
 and t_aux =
   | Tvar of string
   | Tid of string
@@ -133,6 +133,12 @@ let rec string_of_list sep string_of = function
 
 let debug_mode = ref true;;
 
+let co_to_string = function
+  | Patt l -> "Pattern " 
+  | Expr l -> "Expression " 
+  | Fun l -> "Function def " 
+  | Specc l -> "Specification " 
+
 let rec t_to_string t = 
   match t.t with
     | Tid i -> i
@@ -378,6 +384,9 @@ let rec normalize_nexp n =
   | Nadd(n1,n2) ->
     let n1',n2' = normalize_nexp n1, normalize_nexp n2 in
     (match n1'.nexp,n2'.nexp with
+    | Nneg_inf, Npos_inf | Npos_inf, Nneg_inf -> {nexp = Nconst zero }
+    | Npos_inf, _ | _, Npos_inf -> { nexp = Npos_inf }
+    | Nneg_inf, _ | _, Nneg_inf -> { nexp = Nneg_inf } 
     | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some i2) | N2n(_,Some i2), Nconst i1 -> {nexp = Nconst (add_big_int i1 i2)}
     | Nadd(n11,n12), Nconst _ -> {nexp = Nadd(n11,normalize_nexp {nexp = Nadd(n12,n2')})}
     | Nconst _, Nadd(n21,n22) -> {nexp = Nadd(n21,normalize_nexp {nexp = Nadd(n22,n1')})}
@@ -998,7 +1007,7 @@ let initial_typ_env =
            External (Some "eq_vec_range"),
            [Eq(Specc(Parse_ast.Int("==",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
       Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "eq"),[],pure_e)]));
-    ("!=",Base((["a",{k=K_Typ}], (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "neq"),[],pure_e));
+    ("!=",Base((["a",{k=K_Typ}; "b",{k=K_Typ}], (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),External (Some "neq"),[],pure_e));
     ("<",
      Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "lt"),[],pure_e),
 	      false,
@@ -1461,11 +1470,12 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
     if tl1=tl2 then 
       let ids = List.map (fun _ -> Id_aux(Id (new_id ()),l)) t1s in
       let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Base(([],t),Emp_local,[],pure_e)))) ids t1s in
-      let (coerced_ts,cs,efs,coerced_vars) = 
-        List.fold_right2 (fun v (t1,t2) (ts,cs,efs,es) -> let (t',c',ef,e') = type_coerce co d_env is_explicit t1 v t2 in
-							  ((t'::ts),c'@cs,union_effects ef efs,(e'::es)))
-          vars (List.combine t1s t2s) ([],[],pure_e,[]) in
-      if vars = coerced_vars then (t2,cs,pure_e,e)
+      let (coerced_ts,cs,efs,coerced_vars,any_coerced) = 
+        List.fold_right2 (fun v (t1,t2) (ts,cs,efs,es,coerced) ->
+	  let (t',c',ef,e') = type_coerce co d_env is_explicit t1 v t2 in
+	  ((t'::ts),c'@cs,union_effects ef efs,(e'::es), coerced || (v == e')))
+          vars (List.combine t1s t2s) ([],[],pure_e,[],false) in
+      if (not any_coerced) then (t2,cs,pure_e,e)
       else let e' = E_aux(E_case(e,[(Pat_aux(Pat_exp(P_aux(P_tup (List.map2 
 								    (fun i t -> P_aux(P_id i,(l,(Base(([],t),Emp_local,[],pure_e)))))
 								    ids t1s),(l,Base(([],t1),Emp_local,[],pure_e))),
@@ -1672,9 +1682,9 @@ let rec simple_constraint_check in_env cs =
   | [] -> []
   | Eq(co,n1,n2)::cs -> 
     let check_eq ok_to_set n1 n2 = 
-      (*let _ = Printf.printf "eq check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
+(*      let _ = Printf.printf "eq check, about to normalize_nexp of %s, %s arising from %s \n" (n_to_string n1) (n_to_string n2) (co_to_string co) in *)
       let n1',n2' = normalize_nexp n1,normalize_nexp n2 in
-      (*let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string 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
       | Npos_inf,Npos_inf | Nneg_inf, Nneg_inf -> None
       | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst(i2) -> 
@@ -1772,6 +1782,7 @@ let check_tannot l annot constraints efs =
     | Overload _ -> raise (Reporting_basic.err_unreachable l "check_tannot given overload")
 
 let tannot_merge co denv t_older t_newer = 
+  (*let _ = Printf.printf "tannot_merge called\n" in*)
   match t_older,t_newer with
     | NoTyp,NoTyp -> NoTyp
     | NoTyp,_ -> t_newer
@@ -1785,7 +1796,9 @@ let tannot_merge co denv t_older t_newer =
 			 Base(([],t),tag_n,cs_o,ef_o)
 	    | _ -> t_newer)
 	| Emp_local, Emp_local -> 
+	  (*let _ = Printf.printf "local-local case\n" in*) (*TODO Check conforms to first; if true check consistent, if false replace with t_newer *)
 	  let t,cs_b = type_consistent co denv t_n t_o in
+	  (*let _ = Printf.printf "types consistent\n" in*)
 	  Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n)
 	| _,_ -> t_newer)
     | _ -> t_newer