diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 44 | ||||
| -rw-r--r-- | src/type_internal.ml | 52 |
2 files changed, 48 insertions, 48 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 9723fd09..d858cbf0 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -268,7 +268,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) | _ -> default) | P_app(id,pats) -> let i = id_to_string id in - let _ = Printf.eprintf "checking constructor pattern %s\n" i in + (*let _ = Printf.eprintf "checking constructor pattern %s\n" i in*) (match Envmap.apply t_env i with | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined") | Some(Base((params,t),Constructor,constraints,eft,bounds)) -> @@ -578,11 +578,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let cast_t = typ_subst tp_env cast_t in let ct = {t = Toptions(cast_t,None)} in let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param ct e in - let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" (t_to_string cast_t) (constraints_to_string cs) in + (*let _ = Printf.eprintf "Type checking cast: cast_t is %s constraints after checking e are %s\n" (t_to_string cast_t) (constraints_to_string cs) in*) let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false u e' cast_t in - let _ = Printf.eprintf "Type checking cast: after first coerce t' %s is and constraints are %s\n" (t_to_string t') (constraints_to_string cs2) in + (*let _ = Printf.eprintf "Type checking cast: after first coerce t' %s is and constraints are %s\n" (t_to_string t') (constraints_to_string cs2) in*) let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false cast_t e' expect_t in - let _ = Printf.eprintf "Type checking cast: after second coerce t' %s is and constraints are %s\n" (t_to_string t') (constraints_to_string cs3) in + (*let _ = Printf.eprintf "Type checking cast: after second coerce t' %s is and constraints are %s\n" (t_to_string t') (constraints_to_string cs3) in*) (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef)) | E_app(id,parms) -> let i = id_to_string id in @@ -609,7 +609,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let check_result ret imp tag cs ef parms = match (imp,imp_param) with | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) -> - let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in + (*let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in*) let internal_exp = let implicit = {t= Tapp("implicit",[TA_nexp n])} in let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in @@ -617,8 +617,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): type_coerce (Expr l) d_env Guarantee false false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) -> - let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in - let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in + (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in + let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in*) let internal_exp = let implicit_user = {t = Tapp("implicit",[TA_nexp ne])} in let implicit = {t= Tapp("implicit",[TA_nexp n])} in @@ -639,16 +639,16 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Some(Base(tp,Default,_,_,_)) -> typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use") | Some(Base((params,t),tag,cs,ef,bounds)) -> - let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in + (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*) let t,cs,ef,_ = subst params t cs ef in (match t.t with | Tfn(arg,ret,imp,ef') -> - let _ = Printf.eprintf "Checking funcation call of %s\n" i in - let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in + (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in + let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in*) let parms,arg_t,cs_p,ef_p = check_parms arg parms in - let _ = Printf.eprintf "Checked parms of %s\n" i in + (*let _ = Printf.eprintf "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.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in + (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*) (e',ret_t,t_env,cs@cs_p@cs_r, bounds,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)) -> @@ -1735,14 +1735,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.eprintf "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 t', _ = type_consistent (Patt l) d_env Require 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.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) 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.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) 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 let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = @@ -1754,11 +1754,11 @@ 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.eprintf "Function %s is in env\n" id in*) let u,constraints,eft,t_param_env_spec = subst params u constraints eft in let t_param_cs = type_param_consistent l t_param_env_spec t_param_env in let _,cs_decs = type_consistent (Specc l) d_env Require false t u in - let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in + (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in*) let imp_param = match u.t with | Tfn(_,_,IP_user n,_) -> Some n | _ -> None in @@ -1767,14 +1767,14 @@ 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@c'@t_param_cs) in - let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in + (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in*) let tannot = check_tannot l tannot imp_param cs' ef in - let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in + (*let _ = Printf.eprintf "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 | Some {nexp = Nvar i} -> List.map (update_pattern i) funcls | _ -> funcls in - let _ = Printf.eprintf "done funcheck case 1\n" in + (*let _ = Printf.eprintf "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) | _ , _-> @@ -1782,9 +1782,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let funcls,cs_ef = check t_env t_param_env None in 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 _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" id (constraints_to_string cs') in + (*let _ = Printf.eprintf "checking tannot for %s 2 remaining constraints are %s\n" id (constraints_to_string cs') in*) let tannot = check_tannot l tannot None cs' ef in - let _ = Printf.eprintf "done funcheck case2\n" in + (*let _ = Printf.eprintf "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)),b_env,tp_env) diff --git a/src/type_internal.ml b/src/type_internal.ml index 0e309d82..cee2a64d 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -522,7 +522,7 @@ let rec normalize_nexp n = | Npos_inf, _ | _,Nneg_inf -> { nexp = Npos_inf } | Nneg_inf, _ | _,Npos_inf -> { nexp = Nneg_inf } | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some i2) | N2n(_,Some i1), Nconst i2 -> - let _ = Printf.eprintf "constant subtraction of %s - %s gives %s" (Big_int.string_of_big_int i1) (Big_int.string_of_big_int i2) (Big_int.string_of_big_int (sub_big_int i1 i2)) in + (*let _ = Printf.eprintf "constant subtraction of %s - %s gives %s" (Big_int.string_of_big_int i1) (Big_int.string_of_big_int i2) (Big_int.string_of_big_int (sub_big_int i1 i2)) in*) {nexp = Nconst (sub_big_int i1 i2)} | Nadd(n11,n12), Nconst _ -> {nexp = Nadd(n11,normalize_nexp {nexp = Nsub(n12,n2')})} | Nconst _, Nadd(n21,n22) -> {nexp = Nadd(n21,normalize_nexp {nexp = Nsub(n22,n1')})} @@ -791,7 +791,7 @@ let rec occurs_in_pending_subst n_box n : bool = | _ -> occurs_in_nexp n_box n and occurs_in_nexp n_box nuvar : bool = - let _ = Printf.eprintf "occurs_in_nexp given n_box %s nuvar %s eq? %b\n" (n_to_string n_box) (n_to_string nuvar) (n_box.nexp == nuvar.nexp) in + (*let _ = Printf.eprintf "occurs_in_nexp given n_box %s nuvar %s eq? %b\n" (n_to_string n_box) (n_to_string nuvar) (n_box.nexp == nuvar.nexp) in*) if n_box.nexp == nuvar.nexp then true else match n_box.nexp with | Nuvar _ -> occurs_in_pending_subst n_box nuvar @@ -800,7 +800,7 @@ and occurs_in_nexp n_box nuvar : bool = | _ -> false let rec reduce_n_unifications n = - let _ = Printf.eprintf "reduce_n_unifications %s\n" (n_to_string n) in + (*let _ = Printf.eprintf "reduce_n_unifications %s\n" (n_to_string n) in*) (match n.nexp with | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> () | N2n(n1,_) | Npow(n1,_) | Nneg n1 -> reduce_n_unifications n1 @@ -810,7 +810,7 @@ let rec reduce_n_unifications n = | None -> () | Some(nexp) -> reduce_n_unifications(nexp); if nu.leave_var then ignore(leave_nuvar(nexp)) else (); n.nexp <- nexp.nexp)); - let _ = Printf.eprintf "n reduced to %s\n" (n_to_string n) in () + (*let _ = Printf.eprintf "n reduced to %s\n" (n_to_string n) in*) () let rec leave_nu_as_var n = match n.nexp with @@ -888,10 +888,10 @@ let rec fresh_tvar bindings t = None | _ -> None let rec fresh_nvar bindings n = - let _ = Printf.eprintf "fresh_nvar for %s\n" (n_to_string n) in + (*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; @@ -1705,7 +1705,7 @@ and ta_remove_unifications s_env ta = | TA_eft e -> (e_remove_unifications s_env e) | TA_ord o -> (o_remove_unifications s_env o) and n_remove_unifications s_env n = - let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in + (*let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in*) match n.nexp with | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env | Nuvar nu -> @@ -1714,7 +1714,7 @@ and n_remove_unifications s_env n = | _ -> resolve_nsubst n; n in (match n'.nexp with | Nuvar _ -> - let _ = Printf.eprintf "nuvar is before turning into var %s\n" (n_to_string n') in + (*let _ = Printf.eprintf "nuvar is before turning into var %s\n" (n_to_string n') in*) (match fresh_nvar s_env n with | Some ks -> Envmap.insert s_env ks | None -> s_env) @@ -2392,14 +2392,14 @@ let freshen n = let rec equate_nuvars in_env cs = - let _ = Printf.eprintf "equate_nuvars\n" in + (*let _ = Printf.eprintf "equate_nuvars\n" in*) let equate = equate_nuvars in_env in match cs with | [] -> [] | (Eq(co,n1,n2) as c)::cs -> (match (n1.nexp,n2.nexp) with | Nuvar u1, Nuvar u2 -> - let _ = Printf.eprintf "setting two nuvars, %s and %s in equate\n" (n_to_string n1) (n_to_string n2) in + (*let _ = Printf.eprintf "setting two nuvars, %s and %s in equate\n" (n_to_string n1) (n_to_string n2) in*) let occurs = (occurs_in_nexp n1 n2) || (occurs_in_nexp n2 n1) in if not(occurs) then begin ignore(resolve_nsubst n1); ignore(resolve_nsubst n2); @@ -2422,12 +2422,12 @@ let rec equate_nuvars in_env cs = let rec simple_constraint_check in_env cs = let check = simple_constraint_check in_env in - let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in + (*let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in *) match cs with | [] -> [] | Eq(co,n1,n2)::cs -> let eq_to_zero ok_to_set n1 n2 = - let _ = Printf.eprintf "eq_to_zero called with n1 %s and n2%s\n" (n_to_string n1) (n_to_string n2) in + (*let _ = Printf.eprintf "eq_to_zero called with n1 %s and n2%s\n" (n_to_string n1) (n_to_string n2) in*) let new_n = normalize_nexp (mk_sub n1 n2) in (match new_n.nexp with | Nconst i -> @@ -2445,16 +2445,16 @@ let rec simple_constraint_check in_env cs = | _ -> Some(Eq(co,n1,n2))) | _ -> Some(Eq(co,n1,n2))) in let check_eq ok_to_set n1 n2 = - let _ = Printf.eprintf "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.eprintf "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.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in + (*let _ = Printf.eprintf "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 ^ " to equal " ^ n_to_string n2 ) | Nuvar u1, Nuvar u2 -> - let _ = Printf.eprintf "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.eprintf "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 occurs = (occurs_in_nexp n1' n2') || (occurs_in_nexp n2' n1') in if ok_to_set && not(occurs) then begin ignore(resolve_nsubst n1'); ignore(resolve_nsubst n2'); @@ -2462,20 +2462,20 @@ let rec simple_constraint_check in_env cs = else if occurs then eq_to_zero ok_to_set n1' n2' else Some(Eq(co,n1',n2')) | _, Nuvar u -> - let _ = Printf.eprintf "setting right nuvar\n" in + (*let _ = Printf.eprintf "setting right nuvar\n" in*) 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 + (*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) 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 else Some (Eq(co,n1',n2')) | Nuvar u, _ -> - let _ = Printf.eprintf "setting left nuvar\n" in + (*let _ = Printf.eprintf "setting left nuvar\n" in*) 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 + (*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) then if equate_n n1' n2' then None else (Some (Eq(co,n1',n2'))) else if occurs @@ -2494,9 +2494,9 @@ let rec simple_constraint_check in_env cs = | Some(c) -> c::(check cs)) | _ -> (Eq(co,n1,n2)::(check cs))) | GtEq(co,enforce,n1,n2)::cs -> - let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in + (*let _ = Printf.eprintf ">= 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.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in + (*let _ = Printf.eprintf "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 @@ -2517,9 +2517,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,enforce,n1',n2')::(check cs))) | LtEq(co,enforce,n1,n2)::cs -> - let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in + (*let _ = Printf.eprintf "<= 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.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in + (*let _ = Printf.eprintf "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 @@ -2581,11 +2581,11 @@ let check_tannot l annot imp_param constraints efs = ignore(effects_eq (Specc l) efs e); let s_env = (t_remove_unifications (Envmap.from_list params) t) in let params = Envmap.to_list s_env in - let _ = Printf.eprintf "parameters going to save are " in + (*let _ = Printf.eprintf "parameters going to save are " in let _ = List.iter (fun (s,_) -> Printf.eprintf "%s " s) params in - let _ = Printf.eprintf "\n" in + let _ = Printf.eprintf "\n" in*) ignore (remove_internal_unifications s_env); - let _ = Printf.eprintf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in + (*let _ = Printf.eprintf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in*) let t' = match (t.t,imp_param) with | Tfn(p,r,_,e),Some x -> {t = Tfn(p,r,IP_user x,e) } | _ -> t in |