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 =
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
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
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");
projects / helm.git / blobdiff