- let rec mk_prod metasenv context' =
- function
- [] ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- metasenv,Cic.Meta (idx, irl)
- | (_,argty)::tl ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- let meta = Cic.Meta (idx,irl) in
- let name =
- (* The name must be fresh for context. *)
- (* Nevertheless, argty is well-typed only in context. *)
- (* Thus I generate a name (name_hint) in context and *)
- (* then I generate a name --- using the hint name_hint *)
- (* --- that is fresh in context'. *)
- let name_hint =
- (* Cic.Name "pippo" *)
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- ~typ:(CicMetaSubst.apply_subst subst argty)
- in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
- FreshNamesGenerator.mk_fresh_name ~subst
- [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
- in
- let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
- in
- metasenv,Cic.Prod (name,meta,target)
- in
- let ((subst,metasenv,ugraph1),hetype') =
- if CicUtil.is_meta_closed hetype then
- (subst,metasenv,ugraph),hetype
- else
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- try
- fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
- with exn ->
- enrich localization_tbl he
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he
- context ^ " (that has type " ^
- CicMetaSubst.ppterm_in_context subst hetype
- context ^ ") is here applied to " ^
- string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected"
- (* "\nReason: " ^ Lazy.force exn*)))) exn
+ (* aux function to add coercions to funclass *)
+ let rec fix_arity metasenv context subst he hetype 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 subst hetype ^
+ " since unif failed with: " ^ CicMetaSubst.ppterm 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 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 =
+ type_of_aux subst metasenv context 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' carr_src carr_tgt with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotMetaClosed
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ match
+ HExtlib.list_findopt
+ (fun coerc ->
+ let t = Cic.Appl [coerc;x] in
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+ 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 t ugraph
+ in
+ try
+ let metasenv, hetype' =
+ mk_prod_of_metas metasenv context subst remainder
+ in
+ debug_print (lazy
+ (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
+ CicMetaSubst.ppterm 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 _
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ 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 exn -> None
+ with exn -> None)
+ candidates
+ with
+ | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
+ subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+ | None ->
+ enrich localization_tbl he
+ ~f:(fun _-> more_args_than_expected subst he context hetype
+ args_bo_and_ty) exn
+ (* }}} end coercion to funclass stuff *)
+ (* }}} end fix_arity *)