X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=1242a1cded879cb24a21c7d3be344f34a8228d1b;hb=2a79430fa706179258b3a9c5e68e3e268063aa65;hp=bb978a4cce3b2eef43b4a389ff0243e31d8ffbac;hpb=3695c4b811d7e0d731724ea3fdcdd1fa68b76006;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index bb978a4cc..1242a1cde 100644 --- a/components/cic_unification/cicRefine.ml +++ b/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");