diff options
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 17 | ||||
| -rw-r--r-- | src/type_check.ml | 14 | ||||
| -rw-r--r-- | src/type_internal.ml | 31 |
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 |