From 5f18d404d23d75d47b018631cc05221ccd2d2b1b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 8 Sep 2007 23:50:41 +0000 Subject: [PATCH] huge commit regarding coercions to funclass and eat_prods. before there was a so broken behaviour that is impossible to describe the changes. now: eat_prods he hety args starts checking if hety is metaclosed, if it is does nothing, if not unifies it with ?->?-> ... ->? s.t. there is a Pi for every args. if this unification fails, does nothing (all coercions are in the second phase. continues eating prods in hety and args in parallel, if there is an arg and no more prods, tries to fix the arity of (he already_processed_args). fix_arity gives a range of possible coercions to funclass s.t. (c (he ..)) : FunType. The eat prods and args continues, eting the remaining args toghether with FunType. If it fails, it continues with another c to another FunType. This recursively (yes, it backtracks. no strong opinion here, but there is no sane heuristinc to chose one FunType). the code is reduced to 1/3, but Localization of errors probably need fixing. --- .../components/cic_unification/cicRefine.ml | 244 +++++++----------- 1 file changed, 92 insertions(+), 152 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index bb978a4cc..1242a1cde 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1197,148 +1197,84 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il and eat_prods allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph = - (* aux function to add coercions to funclass *) - let rec fix_arity metasenv context subst he hetype eaten args_bo_and_ty ugraph = - (* {{{ body *) - let pristinemenv = metasenv in - let metasenv,hetype' = - mk_prod_of_metas metasenv context subst args_bo_and_ty - in - try - let subst,metasenv,ugraph = - fo_unif_subst_eat_prods - subst context metasenv hetype hetype' ugraph - in - subst,metasenv,ugraph,hetype',he,args_bo_and_ty - with RefineFailure s | Uncertain s as exn - when allow_coercions && !insert_coercions -> - (* {{{ we search a coercion of the head (saturated) to funclass *) - let metasenv = pristinemenv in - debug_print (lazy - ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^ - " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype' - (* ^ " cause: " ^ Lazy.force s *))); - let how_many_args_are_needed = - let rec aux n = function - | Cic.Prod(_,_,t) -> aux (n+1) t - | _ -> n - in - aux 0 (CicMetaSubst.apply_subst subst hetype) - in - let args, remainder = - HExtlib.split_nth how_many_args_are_needed args_bo_and_ty - in - let args = List.map fst (eaten@args) in - let x = - if args <> [] then - match he with - | Cic.Appl l -> Cic.Appl (l@args) - | _ -> Cic.Appl (he::args) - else - he - in - let x,xty,subst,metasenv,ugraph = - (*CSC: here unsharing is necessary to avoid an unwanted - relocalization. However, this also shows a great source of - inefficiency: "x" is refined twice (once now and once in the - subsequent eat_prods_and_args). Morevoer, how is divergence avoided? - *) - type_of_aux subst metasenv context (Unshare.unshare x) ugraph - in - let carr_src = - CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) - in - let carr_tgt = CoercDb.Fun 0 in - match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with - | CoercGraph.NoCoercion - | CoercGraph.NotMetaClosed - | CoercGraph.NotHandled _ -> raise exn - | CoercGraph.SomeCoercionToTgt candidates - | CoercGraph.SomeCoercion candidates -> - match - HExtlib.list_findopt - (fun (metasenv,last,coerc) -> - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc)); - debug_print (lazy ("Last " ^ CicMetaSubst.ppterm ~metasenv subst last)); - debug_print (lazy ("x " ^ CicMetaSubst.ppterm ~metasenv subst x)); - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last x ugraph in - try - (* we want this to be available in the error handler fo the - * following (so it has its own try. *) - let t,tty,subst,metasenv,ugraph = - type_of_aux subst metasenv context coerc ugraph - in - try - let metasenv, hetype' = - mk_prod_of_metas metasenv context subst remainder - in - debug_print (lazy - (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^ - CicMetaSubst.ppterm ~metasenv subst hetype')); - let subst,metasenv,ugraph = - fo_unif_subst_eat_prods - subst context metasenv tty hetype' ugraph - in - debug_print (lazy " success!"); - Some (subst,metasenv,ugraph,tty,t,remainder) - with - | Uncertain _ | RefineFailure _ -> - try - let subst,metasenv,ugraph,hetype',he,args_bo_and_ty = - fix_arity - metasenv context subst t tty [] remainder ugraph - in - Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) - with Uncertain _ | RefineFailure _ -> None - with - Uncertain _ - | RefineFailure _ - | HExtlib.Localized (_,Uncertain _) - | HExtlib.Localized (_,RefineFailure _) -> None - | exn -> assert false) (* ritornare None, e' un localized *) - candidates - with - | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> - subst,metasenv,ugraph,hetype',he,args_bo_and_ty - | None -> - more_args_than_expected localization_tbl metasenv - subst he context hetype args_bo_and_ty exn - (* }}} end coercion to funclass stuff *) - (* }}} end fix_arity *) + (* given he:hety, gives beack all (c he) such that (c e):?->? *) + let fix_arity exn metasenv context subst he hetype ugraph = + let hetype = CicMetaSubst.apply_subst subst hetype in + let src = CoercDb.coerc_carr_of_term hetype in + let tgt = CoercDb.Fun 0 in + match CoercGraph.look_for_coercion' metasenv subst context src tgt with + | CoercGraph.NoCoercion + | CoercGraph.NotMetaClosed + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercionToTgt candidates + | CoercGraph.SomeCoercion candidates -> + HExtlib.filter_map + (fun (metasenv,last,coerc) -> + let pp t = + CicMetaSubst.ppterm_in_context ~metasenv subst t context in + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last he ugraph in + debug_print (lazy ("New head: "^ pp coerc)); + try + let t,tty,subst,metasenv,ugraph = + type_of_aux subst metasenv context coerc ugraph in + (*{{{*)debug_print (lazy (" refined: "^ pp t)); + debug_print (lazy (" has type: "^ pp tty));(*}}}*) + Some (t,tty,subst,metasenv,ugraph) + with + | Uncertain _ | RefineFailure _ + | HExtlib.Localized (_,Uncertain _) + | HExtlib.Localized (_,RefineFailure _) -> None + | exn -> assert false) + candidates in (* aux function to process the type of the head and the args in parallel *) - let rec eat_prods_and_args - pristinemenv metasenv subst context pristinehe he hetype ugraph newargs - = - (* {{{ body *) + let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs = function - | [] -> newargs,subst,metasenv,he,hetype,ugraph - | (hete, hety)::tl as rest -> - match (CicReduction.whd ~subst context hetype) with - | Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph = - coerce_to_something allow_coercions localization_tbl - hete hety s subst metasenv context ugraph in - eat_prods_and_args - pristinemenv metasenv subst context pristinehe he - (CicSubstitution.subst (fst arg) t) - ugraph (newargs@[arg]) tl - | _ -> - try - let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = - fix_arity - pristinemenv context subst he hetype - newargs rest ugraph - in - eat_prods_and_args metasenv - metasenv subst context pristinehe he hetype' - ugraph [] args_bo_and_ty - with RefineFailure _ | Uncertain _ as exn -> - (* unable to fix arity *) - more_args_than_expected localization_tbl metasenv - subst he context hetype args_bo_and_ty exn - (* }}} *) + | [] -> newargs,subst,metasenv,he,hetype,ugraph + | (hete, hety)::tl as args -> + match (CicReduction.whd ~subst context hetype) with + | Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph = + coerce_to_something allow_coercions localization_tbl + hete hety s subst metasenv context ugraph in + eat_prods_and_args + metasenv subst context he (CicSubstitution.subst (fst arg) t) + ugraph (newargs@[arg]) tl + | _ -> + let he = + match he, newargs with + | _, [] -> he + | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs) + | _ -> Cic.Appl (he::List.map fst newargs) + in + (*{{{*) debug_print (lazy + let pp x = + CicMetaSubst.ppterm_in_context ~metasenv subst x context in + "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^ + "\n but is applyed to: " ^ String.concat ";" + (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*) + let exn = RefineFailure (lazy ("more args than expected")) in + let possible_fixes = + fix_arity exn metasenv context subst he hetype ugraph in + match + HExtlib.list_findopt + (fun (he,hetype,subst,metasenv,ugraph) -> + (* {{{ *)debug_print (lazy ("Try fix: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context)); + debug_print (lazy (" of type: "^ + CicMetaSubst.ppterm_in_context + ~metasenv subst hetype context)); (* }}} *) + try + Some (eat_prods_and_args + metasenv subst context he hetype ugraph [] args) + with RefineFailure _ | Uncertain _ -> None) + possible_fixes + with + | Some x -> x + | None -> + more_args_than_expected localization_tbl metasenv + subst he context hetype args_bo_and_ty exn in (* first we check if we are in the simple case of a meta closed term *) let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = @@ -1347,16 +1283,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il subst,metasenv,ugraph,hetype,he,args_bo_and_ty else (* this (says CSC) is also useful to infer dependent types *) - try - fix_arity metasenv context subst he hetype [] args_bo_and_ty ugraph - with RefineFailure _ | Uncertain _ as exn -> - (* unable to fix arity *) - more_args_than_expected localization_tbl metasenv - subst he context hetype args_bo_and_ty exn + let pristinemenv = metasenv in + let metasenv,hetype' = + mk_prod_of_metas metasenv context subst args_bo_and_ty + in + try + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph + in + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + with RefineFailure _ | Uncertain _ -> + subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty in let coerced_args,subst,metasenv,he,t,ugraph = eat_prods_and_args - metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty + metasenv subst context he hetype' ugraph1 [] args_bo_and_ty in he,(List.map fst coerced_args),t,subst,metasenv,ugraph @@ -1382,17 +1323,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il candidates found")); let uncertain = ref false in let selected = -(* HExtlib.list_findopt *) let posibilities = HExtlib.filter_map (fun (metasenv,last,c) -> try - debug_print (lazy ("FO_UNIF_SUBST: " ^ + (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context)); debug_print (lazy ("FO_UNIF_SUBST: " ^ - CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); + CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *) let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last t ugraph in @@ -1440,10 +1380,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let infty = clean infty subst context in let expty = clean expty subst context in let t = clean t subst context in - debug_print (lazy ("COERCE_TO_SOMETHING: " ^ + (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^ " ==> " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expty 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"); -- 2.39.2