From: Enrico Tassi Date: Sun, 9 Sep 2007 15:16:46 +0000 (+0000) Subject: in the case of coerce_to_sort the whd was done with delta:true, that caused an incred... X-Git-Tag: make_still_working~6032 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99de9c457e6aaac40a64a44433d6163ad0d17263;p=helm.git in the case of coerce_to_sort the whd was done with delta:true, that caused an incredible slowdown in dama/ more debug printings added and some comments for vim folding mechanism --- diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 1242a1cde..9fb3548d6 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -328,21 +328,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let module C = Cic in let module S = CicSubstitution in let module U = UriManager in -(* - let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) = - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last t ugraph - in - try - let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph coerced - coercion_tgt - in - Some (newt, tty, subst, metasenv, ugraph) - with - | RefineFailure _ | Uncertain _ -> None - in -*) let (t',_,_,_,_) as res = match t with (* function *) @@ -1308,6 +1293,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let module CR = CicReduction in let cs_subst = CS.subst ~avoid_beta_redexes:true in let coerce_atom_to_something t infty expty subst metasenv context ugraph = + debug_print (lazy ("COERCE_ATOM_TO_SOMETHING")); let coer = CoercGraph.look_for_coercion metasenv subst context infty expty in @@ -1319,8 +1305,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy "coerce_atom_to_something fails since no coercions found")) | CoercGraph.SomeCoercion candidates -> - debug_print (lazy (string_of_int (List.length candidates) ^ " - candidates found")); + debug_print (lazy (string_of_int (List.length candidates) ^ + " candidates found")); let uncertain = ref false in let selected = let posibilities = @@ -1336,7 +1322,6 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last t ugraph in - let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context c ugraph in let newt, newty, subst, metasenv, ugraph = @@ -1384,280 +1369,284 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^ CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*) - match infty, expty, t with - | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) -> - debug_print (lazy "FIX"); - (match fl with - [name,i,_(* infty *),bo] -> - let context_bo = - Some (Cic.Name name,Cic.Decl expty)::context in - let (rel1, _), subst, metasenv, ugraph = - coerce_to_something_aux (Cic.Rel 1) - (CS.lift 1 expty) (CS.lift 1 infty) subst - metasenv context_bo ugraph in - let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in - let (bo,_), subst, metasenv, ugraph = - coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1 - expty) subst - metasenv context_bo ugraph - in - (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph - | _ -> assert false (* not implemented yet *)) - | _,_, Cic.MutCase (uri,tyno,outty,m,pl) -> - debug_print (lazy "CASE"); - (* {{{ helper functions *) - let get_cl_and_left_p uri tyno outty ugraph = - match CicEnvironment.get_obj ugraph uri with - | Cic.InductiveDefinition (tl, _, leftno, _),ugraph -> - let count_pis t = - let rec aux ctx t = - match CicReduction.whd ~delta:false ctx t with - | Cic.Prod (name,src,tgt) -> - let ctx = Some (name, Cic.Decl src) :: ctx in - 1 + aux ctx tgt - | _ -> 0 - in - aux [] t - in - let rec skip_lambda_delifting t n = - match t,n with - | _,0 -> t - | Cic.Lambda (_,_,t),n -> - skip_lambda_delifting - (CS.subst (Cic.Implicit None) t) (n - 1) - | _ -> assert false - in - let get_l_r_p n = function - | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] - | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> - HExtlib.split_nth n args - | _ -> assert false + let (coerced,_),subst,metasenv,_ as result = + match infty, expty, t with + | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) -> + (*{{{*) debug_print (lazy "FIX"); + (match fl with + [name,i,_(* infty *),bo] -> + let context_bo = + Some (Cic.Name name,Cic.Decl expty)::context in + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux (Cic.Rel 1) + (CS.lift 1 expty) (CS.lift 1 infty) subst + metasenv context_bo ugraph in + let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in + let (bo,_), subst, metasenv, ugraph = + coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1 + expty) subst + metasenv context_bo ugraph in - let _, _, ty, cl = List.nth tl tyno in - let pis = count_pis ty in - let rno = pis - leftno in - let t = skip_lambda_delifting outty rno in - let left_p, _ = get_l_r_p leftno t in - let instantiale_with_left cl = - List.map - (fun ty -> - List.fold_left - (fun t p -> match t with - | Cic.Prod (_,_,t) -> - cs_subst p t - | _-> assert false) - ty left_p) - cl - in - let cl = instantiale_with_left (List.map snd cl) in - cl, left_p, leftno, rno, ugraph - | _ -> raise exn - in - let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = - match t,n with - | _,0 -> - let rec mkr n = function - | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl - in - let bo = - CicReplace.replace_lifting - ~equality:(fun _ -> CicUtil.alpha_equivalence) - ~context:ctx - ~what:(matched::right_p) - ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p)) - ~where:bo - in - bo - | Cic.Lambda (name, src, tgt),_ -> - Cic.Lambda (name, src, + (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph + | _ -> assert false (* not implemented yet *)) (*}}}*) + | _,_, Cic.MutCase (uri,tyno,outty,m,pl) -> + (*{{{*) debug_print (lazy "CASE"); + (* {{{ helper functions *) + let get_cl_and_left_p uri tyno outty ugraph = + match CicEnvironment.get_obj ugraph uri with + | Cic.InductiveDefinition (tl, _, leftno, _),ugraph -> + let count_pis t = + let rec aux ctx t = + match CicReduction.whd ~delta:false ctx t with + | Cic.Prod (name,src,tgt) -> + let ctx = Some (name, Cic.Decl src) :: ctx in + 1 + aux ctx tgt + | _ -> 0 + in + aux [] t + in + let rec skip_lambda_delifting t n = + match t,n with + | _,0 -> t + | Cic.Lambda (_,_,t),n -> + skip_lambda_delifting + (CS.subst (Cic.Implicit None) t) (n - 1) + | _ -> assert false + in + let get_l_r_p n = function + | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] + | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> + HExtlib.split_nth n args + | _ -> assert false + in + let _, _, ty, cl = List.nth tl tyno in + let pis = count_pis ty in + let rno = pis - leftno in + let t = skip_lambda_delifting outty rno in + let left_p, _ = get_l_r_p leftno t in + let instantiale_with_left cl = + List.map + (fun ty -> + List.fold_left + (fun t p -> match t with + | Cic.Prod (_,_,t) -> + cs_subst p t + | _-> assert false) + ty left_p) + cl + in + let cl = instantiale_with_left (List.map snd cl) in + cl, left_p, leftno, rno, ugraph + | _ -> raise exn + in + let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = + match t,n with + | _,0 -> + let rec mkr n = function + | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl + in + let bo = + CicReplace.replace_lifting + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:ctx + ~what:(matched::right_p) + ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p)) + ~where:bo + in + bo + | Cic.Lambda (name, src, tgt),_ -> + Cic.Lambda (name, src, keep_lambdas_and_put_expty (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo) (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1)) - | _ -> assert false - in - let eq_uri, eq, eq_refl = - match LibraryObjects.eq_URI () with - | None -> HLog.warn "no default equality"; raise exn - | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[]) - in - let add_params - metasenv subst context uri tyno cty outty mty m leftno i - = - let rec aux context outty par k mty m = function - | Cic.Prod (name, src, tgt) -> - let t,k = - aux - (Some (name, Cic.Decl src) :: context) - (CS.lift 1 outty) (Cic.Rel k::par) (k+1) - (CS.lift 1 mty) (CS.lift 1 m) tgt - in - Cic.Prod (name, src, t), k - | Cic.MutInd _ -> - let k = - let k = Cic.MutConstruct (uri,tyno,i,[]) in - if par <> [] then Cic.Appl (k::par) else k - in - Cic.Prod (Cic.Name "p", - Cic.Appl [eq; mty; m; k], - (CS.lift 1 - (CR.head_beta_reduce ~delta:false - (Cic.Appl [outty;k])))),k - | Cic.Appl (Cic.MutInd _::pl) -> - let left_p,right_p = HExtlib.split_nth leftno pl in - let has_rights = right_p <> [] in - let k = - let k = Cic.MutConstruct (uri,tyno,i,[]) in - Cic.Appl (k::left_p@par) - in - let right_p = - try match - CicTypeChecker.type_of_aux' ~subst metasenv context k - CicUniv.oblivion_ugraph - with - | Cic.Appl (Cic.MutInd _::args),_ -> - snd (HExtlib.split_nth leftno args) - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> assert false - in - if has_rights then - CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k])),k - else - Cic.Prod (Cic.Name "p", - Cic.Appl [eq; mty; m; k], - (CS.lift 1 - (CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k]))))),k - | _ -> assert false - in - aux context outty [] 1 mty m cty - in - let add_lambda_for_refl_m pbo rno mty m k cty = - (* k lives in the right context *) - if rno <> 0 then pbo else - let rec aux mty m = function - | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) -> - Cic.Lambda (name,src, - (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty))) - | t,_ -> - Cic.Lambda (Cic.Name "p", - Cic.Appl [eq; mty; m; k],CS.lift 1 t) - in - aux mty m (pbo,cty) - in - let add_pi_for_refl_m new_outty mty m rno = - if rno <> 0 then new_outty else - let rec aux m mty = function - | Cic.Lambda (name, src, tgt) -> - Cic.Lambda (name, src, - aux (CS.lift 1 m) (CS.lift 1 mty) tgt) - | t -> - Cic.Prod - (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1], - CS.lift 1 t) - in - aux m mty new_outty - in (* }}} end helper functions *) - (* constructors types with left params already instantiated *) - let outty = CicMetaSubst.apply_subst subst outty in - let cl, left_p, leftno,rno,ugraph = - get_cl_and_left_p uri tyno outty ugraph - in - let right_p, mty = - try - match - CicTypeChecker.type_of_aux' ~subst metasenv context m - CicUniv.oblivion_ugraph - with - | Cic.MutInd _ as mty,_ -> [], mty - | Cic.Appl (Cic.MutInd _::args) as mty,_ -> - snd (HExtlib.split_nth leftno args), mty - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> assert false - in - let new_outty = + | _ -> assert false + in + let eq_uri, eq, eq_refl = + match LibraryObjects.eq_URI () with + | None -> HLog.warn "no default equality"; raise exn + | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[]) + in + let add_params + metasenv subst context uri tyno cty outty mty m leftno i + = + let rec aux context outty par k mty m = function + | Cic.Prod (name, src, tgt) -> + let t,k = + aux + (Some (name, Cic.Decl src) :: context) + (CS.lift 1 outty) (Cic.Rel k::par) (k+1) + (CS.lift 1 mty) (CS.lift 1 m) tgt + in + Cic.Prod (name, src, t), k + | Cic.MutInd _ -> + let k = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + if par <> [] then Cic.Appl (k::par) else k + in + Cic.Prod (Cic.Name "p", + Cic.Appl [eq; mty; m; k], + (CS.lift 1 + (CR.head_beta_reduce ~delta:false + (Cic.Appl [outty;k])))),k + | Cic.Appl (Cic.MutInd _::pl) -> + let left_p,right_p = HExtlib.split_nth leftno pl in + let has_rights = right_p <> [] in + let k = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + Cic.Appl (k::left_p@par) + in + let right_p = + try match + CicTypeChecker.type_of_aux' ~subst metasenv context k + CicUniv.oblivion_ugraph + with + | Cic.Appl (Cic.MutInd _::args),_ -> + snd (HExtlib.split_nth leftno args) + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _-> assert false + in + if has_rights then + CR.head_beta_reduce ~delta:false + (Cic.Appl (outty ::right_p @ [k])),k + else + Cic.Prod (Cic.Name "p", + Cic.Appl [eq; mty; m; k], + (CS.lift 1 + (CR.head_beta_reduce ~delta:false + (Cic.Appl (outty ::right_p @ [k]))))),k + | _ -> assert false + in + aux context outty [] 1 mty m cty + in + let add_lambda_for_refl_m pbo rno mty m k cty = + (* k lives in the right context *) + if rno <> 0 then pbo else + let rec aux mty m = function + | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) -> + Cic.Lambda (name,src, + (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty))) + | t,_ -> + Cic.Lambda (Cic.Name "p", + Cic.Appl [eq; mty; m; k],CS.lift 1 t) + in + aux mty m (pbo,cty) + in + let add_pi_for_refl_m new_outty mty m rno = + if rno <> 0 then new_outty else + let rec aux m mty = function + | Cic.Lambda (name, src, tgt) -> + Cic.Lambda (name, src, + aux (CS.lift 1 m) (CS.lift 1 mty) tgt) + | t -> + Cic.Prod + (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1], + CS.lift 1 t) + in + aux m mty new_outty + in (* }}} end helper functions *) + (* constructors types with left params already instantiated *) + let outty = CicMetaSubst.apply_subst subst outty in + let cl, left_p, leftno,rno,ugraph = + get_cl_and_left_p uri tyno outty ugraph + in + let right_p, mty = + try + match + CicTypeChecker.type_of_aux' ~subst metasenv context m + CicUniv.oblivion_ugraph + with + | Cic.MutInd _ as mty,_ -> [], mty + | Cic.Appl (Cic.MutInd _::args) as mty,_ -> + snd (HExtlib.split_nth leftno args), mty + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _ -> assert false + in + let new_outty = keep_lambdas_and_put_expty context outty expty right_p m (rno+1) - in - debug_print - (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst new_outty context)); - let _,pl,subst,metasenv,ugraph = - List.fold_right2 - (fun cty pbo (i, acc, s, menv, ugraph) -> - (* Pi k_par, (Pi H:m=(K_i left_par k_par)), - * (new_)outty right_par (K_i left_par k_par) *) - let infty_pbo, _ = - add_params menv s context uri tyno - cty outty mty m leftno i in - debug_print + in + debug_print + (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst new_outty context)); + let _,pl,subst,metasenv,ugraph = + List.fold_right2 + (fun cty pbo (i, acc, s, menv, ugraph) -> + (* Pi k_par, (Pi H:m=(K_i left_par k_par)), + * (new_)outty right_par (K_i left_par k_par) *) + let infty_pbo, _ = + add_params menv s context uri tyno + cty outty mty m leftno i in + debug_print (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context - ~metasenv subst infty_pbo context)); - let expty_pbo, k = (* k is (K_i left_par k_par) *) - add_params menv s context uri tyno - cty new_outty mty m leftno i in - debug_print + ~metasenv subst infty_pbo context)); + let expty_pbo, k = (* k is (K_i left_par k_par) *) + add_params menv s context uri tyno + cty new_outty mty m leftno i in + debug_print (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context - ~metasenv subst expty_pbo context)); - let pbo = add_lambda_for_refl_m pbo rno mty m k cty in - debug_print - (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst pbo context)); - let (pbo, _), subst, metasenv, ugraph = - coerce_to_something_aux pbo infty_pbo expty_pbo - s menv context ugraph - in - debug_print - (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst pbo context)); - (i-1, pbo::acc, subst, metasenv, ugraph)) - cl pl (List.length pl, [], subst, metasenv, ugraph) - in - let new_outty = add_pi_for_refl_m new_outty mty m rno in - debug_print - (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst new_outty context)); - let t = - if rno = 0 then - let refl_m=Cic.Appl[eq_refl;mty;m]in - Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] - else - Cic.MutCase(uri,tyno,new_outty,m,pl) - in - (t, expty), subst, metasenv, ugraph - | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> - debug_print (lazy "LAM"); - let name_con = - FreshNamesGenerator.mk_fresh_name - ~subst metasenv context ~typ:src2 Cic.Anonymous - in - let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in - (* contravariant part: the argument of f:src->ty *) - let (rel1, _), subst, metasenv, ugraph = - coerce_to_something_aux - (Cic.Rel 1) (CS.lift 1 src2) - (CS.lift 1 src) subst metasenv context_src2 ugraph - in - (* covariant part: the result of f(c x); x:src2; (c x):src *) - let name_t, bo = - match t with - | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo) - | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1] - in - (* we fix the possible dependency problem in the source ty *) - let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in - let (bo, _), subst, metasenv, ugraph = - coerce_to_something_aux - bo ty ty2 subst metasenv context_src2 ugraph - in - let coerced = Cic.Lambda (name_t,src2, bo) in - debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context - ~metasenv subst coerced context)); - (coerced, expty), subst, metasenv, ugraph - | _ -> - debug_print (lazy ("ATOM: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst infty context ^ " ==> " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); - coerce_atom_to_something t infty expty subst metasenv context ugraph + ~metasenv subst expty_pbo context)); + let pbo = add_lambda_for_refl_m pbo rno mty m k cty in + debug_print + (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst pbo context)); + let (pbo, _), subst, metasenv, ugraph = + coerce_to_something_aux pbo infty_pbo expty_pbo + s menv context ugraph + in + debug_print + (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst pbo context)); + (i-1, pbo::acc, subst, metasenv, ugraph)) + cl pl (List.length pl, [], subst, metasenv, ugraph) + in + let new_outty = add_pi_for_refl_m new_outty mty m rno in + debug_print + (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst new_outty context)); + let t = + if rno = 0 then + let refl_m=Cic.Appl[eq_refl;mty;m]in + Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] + else + Cic.MutCase(uri,tyno,new_outty,m,pl) + in + (t, expty), subst, metasenv, ugraph (*}}}*) + | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> + (*{{{*) debug_print (lazy "LAM"); + let name_con = + FreshNamesGenerator.mk_fresh_name + ~subst metasenv context ~typ:src2 Cic.Anonymous + in + let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in + (* contravariant part: the argument of f:src->ty *) + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux + (Cic.Rel 1) (CS.lift 1 src2) + (CS.lift 1 src) subst metasenv context_src2 ugraph + in + (* covariant part: the result of f(c x); x:src2; (c x):src *) + let name_t, bo = + match t with + | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo) + | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1] + in + (* we fix the possible dependency problem in the source ty *) + let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in + let (bo, _), subst, metasenv, ugraph = + coerce_to_something_aux + bo ty ty2 subst metasenv context_src2 ugraph + in + let coerced = Cic.Lambda (name_t,src2, bo) in + (coerced, expty), subst, metasenv, ugraph (*}}}*) + | _ -> + (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context + ~metasenv subst infty context ^ " ==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); + coerce_atom_to_something + t infty expty subst metasenv context ugraph (*}}}*) + in + debug_print (lazy ("COERCE TO SOMETHING END: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst coerced context)); + result in try coerce_to_something_aux t infty expty subst metasenv context ugraph @@ -1672,16 +1661,20 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il enrich localization_tbl ~f t exn and coerce_to_sort localization_tbl t infty subst context metasenv uragph = - match CicReduction.whd ~subst:subst context infty with + match CicReduction.whd ~delta:false ~subst context infty with | Cic.Meta _ | Cic.Sort _ -> t,infty, subst, metasenv, ugraph | src -> + debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context + ~metasenv subst src context)); let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in try let (t, ty_t), subst, metasenv, ugraph = coerce_to_something true localization_tbl t src tgt subst metasenv context ugraph in + debug_print (lazy ("COERCE TO SORT END: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context)); t, ty_t, subst, metasenv, ugraph with HExtlib.Localized (_, exn) -> let f _ =