diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 19 | ||||
| -rw-r--r-- | src/type_internal.ml | 38 |
2 files changed, 35 insertions, 22 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 2f3cb6c6..c27e5cd6 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -187,7 +187,9 @@ let into_register d_env (t : tannot) : tannot = let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * bounds_env * t) = let (Env(d_env,t_env,b_env,tp_env)) = envs in +(* let _ = Printf.printf "checking pattern with expected type %s\n" (t_to_string expect_t) in*) let expect_t,cs = get_abbrev d_env expect_t in +(* let _ = Printf.printf "check pattern expect_t after abbrev %s\n" (t_to_string expect_t) in*) let expect_actual = match expect_t.t with | Tabbrev(_,t) -> t | _ -> expect_t in match p with | P_lit (L_aux(lit,l')) -> @@ -223,6 +225,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 t',cs' = type_consistent (Patt l) d_env 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) @@ -1702,14 +1705,14 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let check t_env tp_env imp_param = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> - (*let _ = Printf.eprintf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) +(* let _ = Printf.printf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_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 t', _ = type_consistent (Patt l) d_env false param_t t' in let exp',_,_,cs_e,_,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', merge_bounds b_env b_env',tp_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 _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) (*let _ = Printf.eprintf "effects were %s\n" (e_to_string ef) in*) let cs = [CondCons(Fun l,cs_p,cs_e)] in (FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef,nob)))),(cs,ef))) funcls) in @@ -1722,10 +1725,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.printf "Function %s is in env\n" id in*) +(* let _ = Printf.printf "Function %s is in env\n" id in*) let u,constraints,eft,t_param_env = subst params u constraints eft in let _,cs_decs = type_consistent (Specc l) d_env false t u in - (*let _ = Printf.printf "valspec consistent with declared type for %s, %s ~< %s with %i constraints \n" id (t_to_string t) (t_to_string u) (List.length cs_decs) in*) +(* let _ = Printf.printf "valspec consistent with declared type for %s, %s ~< %s with %i constraints \n" id (t_to_string t) (t_to_string u) (List.length cs_decs) in*) let imp_param = match u.t with | Tfn(_,_,IP_user n,_) -> Some n | _ -> None in @@ -1734,13 +1737,13 @@ 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@cs_decs@constraints) in - (*let _ = Printf.printf "checking tannot for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*) +(* let _ = Printf.printf "checking tannot for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*) let tannot = check_tannot l tannot imp_param cs' ef in - (*let _ = Printf.printf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*) +(* let _ = Printf.printf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) 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*) + 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),b_env,tp_env) | _ , _-> diff --git a/src/type_internal.ml b/src/type_internal.ml index 812b96d0..84d84460 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2273,22 +2273,21 @@ let freshen n = let rec simple_constraint_check in_env cs = let check = simple_constraint_check in_env in -(* let _ = Printf.printf "simple_constraint_check\n" in *) + (*let _ = Printf.printf "simple_constraint_check\n" in *) match cs with | [] -> [] | 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 arising from %s \n" (n_to_string n1) (n_to_string n2) (co_to_string co) 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 | Ninexact,nok | nok,Ninexact -> eq_error (get_c_loc co) ("Type constraint arising from here requires " ^ n_to_string {nexp = nok} ^ " to be equal to +inf + -inf") | Npos_inf,Npos_inf | Nneg_inf, Nneg_inf -> None | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst(i2) -> if eq_big_int i1 i2 then None - else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires (" ^ n_to_string n1 ^ "=" - ^ string_of_big_int i1 ^ ") to equal (" ^ n_to_string n2 ^ " = " ^ string_of_big_int i2) + else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string n1 ^ " to equal " ^ n_to_string n2 ) | Nconst i, Nuvar u -> if not(u.nin) && ok_to_set then begin equate_n n2' n1'; None end @@ -2298,7 +2297,7 @@ let rec simple_constraint_check in_env cs = then begin equate_n n1' n2'; None end else Some (Eq(co,n1',n2')) | Nuvar u1, Nuvar u2 -> -(* let _ = Printf.printf "setting two nuvars, %s and %s, it is ok_to_set %b\n" (n_to_string n1) (n_to_string n2) ok_to_set in*) + (*let _ = Printf.printf "setting two nuvars, %s and %s, it is ok_to_set %b\n" (n_to_string n1) (n_to_string n2) ok_to_set in*) if ok_to_set then begin ignore(resolve_nsubst n1); ignore(resolve_nsubst n2); equate_n n1' n2'; None end else Some(Eq(co,n1',n2')) @@ -2328,9 +2327,9 @@ let rec simple_constraint_check in_env cs = | Some(c) -> c::(check cs)) | _ -> (Eq(co,n1,n2)::(check cs))) | GtEq(co,n1,n2)::cs -> -(* let _ = Printf.printf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + (*let _ = Printf.printf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) 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 | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst i2 -> if ge_big_int i1 i2 @@ -2351,9 +2350,9 @@ let rec simple_constraint_check in_env cs = ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) | _ -> GtEq(co,n1',n2')::(check cs))) | LtEq(co,n1,n2)::cs -> -(* let _ = Printf.printf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) + (*let _ = Printf.printf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) 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 | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst i2 -> if le_big_int i1 i2 @@ -2365,13 +2364,15 @@ let rec simple_constraint_check in_env cs = ^ (n_to_string n2')) | _,_ -> LtEq(co,n1',n2')::(check cs)) | CondCons(co,pats,exps):: cs -> + (*let _ = Printf.printf "Condcons check length pats %i, length exps %i\n" (List.length pats) (List.length exps) in*) let pats' = check pats in let exps' = check exps in + (*let _ = Printf.printf "Condcons after check length pats' %i, length exps' %i\n" (List.length pats') (List.length exps') in*) (match pats',exps' with | [],[] -> check cs - | _,[] -> check cs | _ -> CondCons(co,pats',exps')::(check cs)) | BranchCons(co,branches)::cs -> +(* let _ = Printf.printf "Branchcons check length branches %i\n" (List.length branches) in*) let b' = check branches in if [] = b' then check cs @@ -2379,20 +2380,29 @@ let rec simple_constraint_check in_env cs = | x::cs -> x::(check cs) let rec resolve_in_constraints cs = cs + +let rec constraint_size = function + | [] -> 0 + | c::cs -> + match c with + | CondCons(_,ps,es) -> constraint_size ps + constraint_size es + | BranchCons(_,bs) -> constraint_size bs + | _ -> 1 let do_resolve_constraints = ref true let resolve_constraints cs = -(* let _ = Printf.printf "called resolve constraints with %i constraints\n" (List.length cs) in*) +(* let _ = Printf.printf "called resolve constraints with %i constraints\n" (constraint_size cs) in*) if not !do_resolve_constraints then cs 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 (in_constraint_env cs) cs in - if len > (List.length cs') then fix (List.length cs') cs' + let len' = constraint_size cs' in + if len > len' then fix len' cs' else cs' in - let complex_constraints = fix (List.length cs) cs in + let complex_constraints = fix (constraint_size cs) cs in complex_constraints |