let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
+ let rec count_prods context ty =
+ match CicReduction.whd context ~subst:subst'' ty with
+ | Cic.Prod (n,s,t) ->
+ 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+ in
+ let exp_prods = count_prods context ty' in
+ let inf_prods = count_prods context inferredty in
+ let te', inferredty, metasenv'', subst'', ugraph2 =
+ let rec aux t m s ug it = function
+ | 0 -> t,it,m,s,ug
+ | n ->
+ match CicReduction.whd context ~subst:s it with
+ | Cic.Prod (_,src,tgt) ->
+ let newmeta, metaty, s, m, ug =
+ type_of_aux s m context (Cic.Implicit None) ug
+ in
+ let s,m,ug =
+ fo_unif_subst s context m metaty src ug
+ in
+ let t =
+ match t with
+ | Cic.Appl l -> Cic.Appl (l @ [newmeta])
+ | _ -> Cic.Appl [t;newmeta]
+ in
+ aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
+ | _ -> t,it,m,s,ug
+ in
+ aux te' metasenv'' subst'' ugraph2 inferredty
+ (max 0 (inf_prods - exp_prods))
+ in
let (te', ty'), subst''',metasenv''',ugraph3 =
coerce_to_something true localization_tbl te' inferredty ty'
subst'' metasenv'' context ugraph2
| (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() in
(try
- let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
C.Sort (C.Type t'),subst,metasenv,ugraph2
with
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (function (metasenv,last,c) ->
+ (fun (metasenv,last,c) _ ->
match c with
| c when not (CoercGraph.is_composite c) ->
debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
"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 error = ref None in
let possible_fixes =
fix_arity (List.length args) metasenv context subst he hetype
ugraph in
match
HExtlib.list_findopt
- (fun (he,hetype,subst,metasenv,ugraph) ->
+ (fun (he,hetype,subst,metasenv,ugraph) _ ->
(* {{{ *)debug_print (lazy ("Try fix: "^
CicMetaSubst.ppterm_in_context ~metasenv subst he context));
debug_print (lazy (" of type: "^
with
| RefineFailure _ | Uncertain _
| HExtlib.Localized (_,RefineFailure _)
- | HExtlib.Localized (_,Uncertain _) -> None)
+ | HExtlib.Localized (_,Uncertain _) as exn ->
+ error := Some exn; None)
possible_fixes
with
| Some x -> x
| None ->
- raise
- (MoreArgsThanExpected
- (List.length args, RefineFailure (lazy "")))
+ match !error with
+ None ->
+ raise
+ (MoreArgsThanExpected
+ (List.length args, RefineFailure (lazy "")))
+ | Some exn -> raise 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 =
let newt,newhety,subst,metasenv,ugraph =
type_of_aux subst metasenv context c ugraph in
let newt, newty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph newt expty
+ avoid_double_coercion context subst metasenv ugraph newt
+ expty
in
let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv newhety expty ugraph in
- Some ((newt,newty), subst, metasenv, ugraph)
+ fo_unif_subst subst context metasenv newhety expty ugraph
+ in
+ let b, ugraph =
+ CicReduction.are_convertible ~subst context infty expty ugraph
+ in
+ if b then
+ Some ((t,infty), subst, metasenv, ugraph)
+ else
+ Some ((newt,newty), subst, metasenv, ugraph)
with
| Uncertain _ -> uncertain := true; None
| RefineFailure _ -> None)
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
| Cic.Constant (name,None,ty,args,attrs) ->
- let ty',_,metasenv,ugraph =
+ let ty',sort,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph
in
- Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+ (match CicReduction.whd [] sort with
+ Cic.Sort _
+ | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+ | _ -> raise (RefineFailure (lazy "")))
| Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
assert (metasenv' = metasenv);
(* Here we do not check the metasenv for correctness *)
let ty',sort,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph in
begin
- match sort with
+ match CicReduction.whd ~delta:true [] sort with
Cic.Sort _
(* instead of raising Uncertain, let's hope that the meta will become
a sort *)