Fix error in building register values

	(make one function to do it instead of almost the same function multiple times)

Fix lost nexp variable in constraints, removing another undefined

3 files changed, 31 insertions, 31 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 0fa5730b..d2684553 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -882,9 +882,9 @@ let concretizable_bytls = List.all concretizable_bytl
 
 (* constructing values *)
 
-val register_value : bit_lifted -> direction -> nat -> nat -> register_value
-let register_value b dir width start_index = 
-  <| rv_bits = List.replicate width b;
+val build_register_value : list bit_lifted -> direction -> nat -> nat -> register_value
+let build_register_value bs dir width start_index =
+  <| rv_bits = bs;
      rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
      rv_start_internal = start_index; 
      rv_start = if dir = D_increasing 
@@ -892,6 +892,10 @@ let register_value b dir width start_index =
        else (start_index+1) - width; (* Smaller index, as in Power, for external interaction *)
   |>
 
+val register_value : bit_lifted -> direction -> nat -> nat -> register_value
+let register_value b dir width start_index = 
+  build_register_value (List.replicate width b) dir width start_index
+
 val register_value_zeros : direction -> nat -> nat -> register_value
 let register_value_zeros dir width start_index = 
   register_value Bitl_zero dir width start_index
@@ -1080,12 +1084,7 @@ let integer_of_register_value (rv:register_value):maybe integer =
 val register_value_of_integer : nat -> nat -> direction -> integer -> register_value 
 let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):register_value =
   let bs = bit_list_of_integer len i in
-  <| 
-  rv_bits = List.map bit_lifted_of_bit bs;
-  rv_dir = dir;
-  rv_start = start;
-  rv_start_internal = if dir = D_increasing then start else start + (List.length bs) - 1
-|> 
+  build_register_value (List.map bit_lifted_of_bit bs) dir len start
 
 (* *)
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 105748a3..92e42641 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -227,7 +227,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 		       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 _ = Printf.printf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*)
+(*      let _ = Printf.eprintf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*)
       let t',cs' = type_consistent (Patt l) d_env Require true t expect_t in
       let cs_l = cs@cs' in
       (P_aux(P_lit(L_aux(lit,l')),(l,cons_tag_annot t emp_tag cs_l)),Envmap.empty,cs_l,nob,t)
@@ -499,7 +499,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
           | Tabbrev(_,t),_ -> t,expect_t 
           | _,Tabbrev(_,e) -> t,e
           | _,_ -> t,expect_t in
-	(*let _ = Printf.printf "On general id check, expect_t %s, t %s, tactual %s, expect_actual %s\n" (t_to_string expect_t) (t_to_string t) (t_to_string t_actual) (t_to_string expect_actual) in*)
+	(*let _ = Printf.eprintf "On general id check, expect_t %s, t %s, tactual %s, expect_actual %s\n" (t_to_string expect_t) (t_to_string t) (t_to_string t_actual) (t_to_string expect_actual) in*)
         (match t_actual.t,expect_actual.t with 
         | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
         | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
@@ -1870,7 +1870,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
 		  let tannot = Base(([],et),Alias,[],pure_e,nob) in
 		  let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
 		  (AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env)))
-	| _ -> let _ = Printf.printf "%s\n" (t_to_string reg_t) in assert false)
+	| _ -> let _ = Printf.eprintf "%s\n" (t_to_string reg_t) in assert false)
     | AL_bit(reg_a,bit) -> 
       let (reg,reg_a,reg_t,t) = check_reg reg_a in
       let (E_aux(bit,(le,eannot)),_,_,_,_,_) = check_exp envs None (new_t ()) bit in
@@ -1920,14 +1920,14 @@ let check_def envs def =
   let (Env(d_env,t_env,b_env,tp_env)) = envs in
   match def with
   | DEF_type tdef ->
-    (*let _ = Printf.printf "checking type def\n" in*)
+    (*let _ = Printf.eprintf "checking type def\n" in*)
     let td,envs = check_type_def envs tdef in
-    (*let _ = Printf.printf "checked type def\n" in*)
+    (*let _ = Printf.eprintf "checked type def\n" in*)
     (DEF_type td,envs)
   | DEF_fundef fdef -> 
-    (*let _ = Printf.printf "checking fun def\n" in*)
+    (*let _ = Printf.eprintf "checking fun def\n" in*)
     let fd,envs = check_fundef envs fdef in
-    (*let _ = Printf.printf "checked fun def\n" in*)
+    (*let _ = Printf.eprintf "checked fun def\n" in*)
     (DEF_fundef fd,envs)
   | DEF_val letdef -> 
     (*let _ = Printf.eprintf "checking letdef\n" in*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index fb5e3489..eae11d6e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -625,7 +625,7 @@ let rec normalize_nexp n =
 	    | _ -> {nexp = Nmult(n2',n1')})
 	| _ -> {nexp = Nmult(normalize_nexp {nexp = Nmult(n1',n21)},n22)})
     | Nmult _ ,Nmult(n21,n22) -> {nexp = Nmult({nexp = Nmult(n21,n1')},{nexp = Nmult(n22,n1')})}
-    | Nneg _,_ | _,Nneg _ -> let _ = Printf.printf "neg case still around %s\n" (n_to_string n) in assert false (* If things are normal, neg should be gone. *)
+    | Nneg _,_ | _,Nneg _ -> let _ = Printf.eprintf "neg case still around %s\n" (n_to_string n) in assert false (* If things are normal, neg should be gone. *)
     )
     
 let int_to_nexp i = {nexp = Nconst (big_int_of_int i)}
@@ -685,7 +685,7 @@ let new_e _ =
 
 exception Occurs_exn of t_arg
 let rec resolve_tsubst (t : t) : t = 
-  (*let _ = Printf.printf "resolve_tsubst on %s\n" (t_to_string t) in*)
+  (*let _ = Printf.eprintf "resolve_tsubst on %s\n" (t_to_string t) in*)
   match t.t with
   | Tuvar({ subst=Some(t') } as u) ->
     let t'' = resolve_tsubst t' in
@@ -772,9 +772,9 @@ let rec nexp_eq_check n1 n2 =
   | _,_ -> false
 
 let nexp_eq n1 n2 =
-(*  let _ = Printf.printf "comparing nexps %s and %s\n" (n_to_string n1) (n_to_string n2) in*)
+(*  let _ = Printf.eprintf "comparing nexps %s and %s\n" (n_to_string n1) (n_to_string n2) in*)
   let b = nexp_eq_check (normalize_nexp n1) (normalize_nexp n2) in
-(*  let _ = Printf.printf "compared nexps %s\n" (string_of_bool b) in*)
+(*  let _ = Printf.eprintf "compared nexps %s\n" (string_of_bool b) in*)
   b
 
 let nexp_one_more_than n1 n2 =
@@ -912,7 +912,8 @@ let rec fresh_nvar bindings n =
   (*let _ = Printf.eprintf "fresh_nvar for %s\n" (n_to_string n) in*)
   match n.nexp with
     | Nuvar { nindex = i;nsubst = None } -> 
-      fresh_var "nv" i (fun v add -> n.nexp <- (Nvar v); (*(Printf.eprintf "fresh nvar set %i to %s : %s\n" i v (n_to_string n));*) if add then Some(v,{k=K_Nat}) else None) bindings
+      fresh_var "nv" i (fun v add -> n.nexp <- (Nvar v); 
+(*(Printf.eprintf "fresh nvar set %i to %s : %s\n" i v (n_to_string n));*) if add then Some(v,{k=K_Nat}) else None) bindings
     | Nuvar { nindex = i; nsubst = Some({nexp=Nuvar _} as n')} ->
       let kv = fresh_nvar bindings n' in
       n.nexp <- n'.nexp;
@@ -2182,7 +2183,7 @@ and conforms_to_e loosely spec actual =
   When considering two atom type applications, will expand into a range encompasing both when widen is true
 *)
 let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 = 
-(*  let _ = Printf.printf "type_consistent_internal called with %s and %s\n" (t_to_string t1) (t_to_string t2) in*)
+(*  let _ = Printf.eprintf "type_consistent_internal called with %s and %s\n" (t_to_string t1) (t_to_string t2) in*)
   let l = get_c_loc co in
   let t1,cs1' = get_abbrev d_env t1 in
   let t2,cs2' = get_abbrev d_env t2 in
@@ -2219,7 +2220,7 @@ let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 =
 	     ({t=Tapp("range",[TA_nexp nu1;TA_nexp nu2])},
 	      csp@[LtEq(co,enforce,nu1,a1);LtEq(co,enforce,nu1,a2);LtEq(co,enforce,a1,nu2);LtEq(co,enforce,a2,nu2)]))
   | Tapp(id1,args1), Tapp(id2,args2) ->
-    (*let _ = Printf.printf "checking consistency of %s and %s\n" id1 id2 in*)
+    (*let _ = Printf.eprintf "checking consistency of %s and %s\n" id1 id2 in*)
     let la1,la2 = List.length args1, List.length args2 in
     if id1=id2 && la1 = la2 
     then (t2,csp@(List.flatten (List.map2 (type_arg_eq co d_env enforce widen) args1 args2)))
@@ -2491,9 +2492,9 @@ let rec select_overload_variant d_env params_check get_all variants actual_type
     | NoTyp::variants | Overload _::variants ->
       select_overload_variant d_env params_check get_all variants actual_type
     | Base((parms,t_orig),tag,cs,ef,bindings)::variants ->
-      (*let _ = Printf.printf "About to check a variant %s\n" (t_to_string t_orig) in*)
+      (*let _ = Printf.eprintf "About to check a variant %s\n" (t_to_string t_orig) in*)
       let t,cs,ef,_ = if parms=[] then t_orig,cs,ef,Envmap.empty else subst parms false t_orig cs ef in
-      (*let _ = Printf.printf "And after substitution %s\n" (t_to_string t) in*)
+      (*let _ = Printf.eprintf "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
@@ -2505,7 +2506,7 @@ let rec select_overload_variant d_env params_check get_all variants actual_type
 		(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*)
+	  (*let _ = Printf.eprintf "Checked a variant, matching? %b\n" is_matching in*)
 	  if is_matching 
 	  then (Base(([],t),tag,cs@cs',ef,bindings))::(if get_all then (recur ()) else [])
 	  else recur ()
@@ -2657,7 +2658,7 @@ let rec simple_constraint_check in_env cs =
 	let occurs = occurs_in_nexp n1' n2' in
 	let leave = leave_nu_as_var n2' in
 	(*let _ = Printf.eprintf "occurs? %b, leave? %b n1' %s in n2' %s\n" occurs leave (n_to_string n1') (n_to_string n2') in*)
-        if not(u.nin) && ok_to_set && not(occurs) && not(leave)
+        if (*not(u.nin) &&*) ok_to_set && not(occurs) && not(leave)
         then if (equate_n n2' n1') then  None else (Some (Eq(co,n1',n2')))
         else if occurs 
 	then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end
@@ -2667,7 +2668,7 @@ let rec simple_constraint_check in_env cs =
 	let occurs = occurs_in_nexp n2' n1' in
 	let leave = leave_nu_as_var n1' in
 	(*let _ = Printf.eprintf "occurs? %b, leave? %b n2' %s in n1' %s\n" occurs leave (n_to_string n2') (n_to_string n1') in*)
-        if not(u.nin) && ok_to_set && not(occurs) && not(leave)
+        if (*not(u.nin) && *)ok_to_set && not(occurs) && not(leave)
         then if equate_n n1' n2' then None else (Some (Eq(co,n1',n2')))
         else if occurs
 	then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end
@@ -2808,7 +2809,7 @@ let check_tannot l annot imp_param constraints efs =
     | Overload _ -> raise (Reporting_basic.err_unreachable l "check_tannot given overload")
 
 let tannot_merge co denv widen t_older t_newer = 
-  (*let _ = Printf.printf "tannot_merge called\n" in*)
+  (*let _ = Printf.eprintf "tannot_merge called\n" in*)
   match t_older,t_newer with
     | NoTyp,NoTyp -> NoTyp
     | NoTyp,_ -> t_newer
@@ -2822,10 +2823,10 @@ let tannot_merge co denv widen t_older t_newer =
 			 Base(([],t),tag_n,cs_o,ef_o,bounds_o)
 	    | _ -> t_newer)
 	| Emp_local, Emp_local -> 
-	  (*let _ = Printf.printf "local-local case\n" in*) 
+	  (*let _ = Printf.eprintf "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 Guarantee widen t_n t_o in
-	  (*let _ = Printf.printf "types consistent\n" in*)
+	  (*let _ = Printf.eprintf "types consistent\n" in*)
 	  Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n, merge_bounds bounds_o bounds_n)
 	| _,_ -> t_newer)
     | _ -> t_newer