let insert_coercions = ref true
let pack_coercions = ref true
-let debug_print = fun _ -> ()
-(* let debug_print x = prerr_endline (Lazy.force x);; *)
+let debug_print = fun _ -> ();;
+(*let debug_print x = prerr_endline (Lazy.force x);;*)
let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
match exn with
RefineFailure msg -> RefineFailure (f msg)
| Uncertain msg -> Uncertain (f msg)
+ | Sys.Break -> raise exn
| _ -> assert false in
let loc =
try
| sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
let sib2,head = last_of tl2 in
true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
- (c2::sib2@[Cic.Implicit None])])
+ (c2::sib2@[imp])])
| _ -> dummyres)
| _ -> dummyres
-let more_args_than_expected subst he context hetype' tlbody_and_type =
- 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")
+let more_args_than_expected
+ localization_tbl metasenv subst he context hetype' tlbody_and_type exn
+=
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
+ " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
+ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+ " arguments that are more than expected")
+ in
+ enrich localization_tbl he ~f:(fun _-> msg) exn
;;
let mk_prod_of_metas metasenv context' subst args =
ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module U = UriManager in
let try_coercion t subst metasenv context ugraph coercion_tgt c =
- let coerced = Cic.Appl[c;t] in
+ let coerced =
+ match c with
+ C.Appl l2 -> C.Appl (l2@[t])
+ | _ -> C.Appl [c;t]
+ in
try
let newt,_,subst,metasenv,ugraph =
type_of_aux subst metasenv context coerced ugraph
with
| RefineFailure _ | Uncertain _ -> None
in
- let module C = Cic in
- let module S = CicSubstitution in
- let module U = UriManager in
let (t',_,_,_,_) as res =
match t with
(* function *)
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
with
- _ ->
+ Failure _ ->
enrich localization_tbl t
- (RefineFailure (lazy "Not a close term")))
+ (RefineFailure (lazy "Not a closed term")))
| C.Var (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst
subst', metasenv',ugraph1)
| C.Sort (C.Type tno) ->
let tno' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ (try
+ let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+ t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| C.Sort _ ->
t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
| C.Implicit infos ->
enrich localization_tbl te'
~f:(fun _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst'' te'
+ CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst'' inferredty
+ CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
+ CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
)
| C.Prod (name,s,t) ->
let carr t subst context = CicMetaSubst.apply_subst subst t in
enrich localization_tbl t
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst t context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.NotMetaClosed ->
enrich localization_tbl t
(Uncertain
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst t context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.SomeCoercion candidates ->
let selected =
enrich localization_tbl t
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst t context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^
" that is not a sort"))))
in
t' sort2 subst'' context_for_t metasenv'' ugraph2
in
let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
+ sort_of_prod localization_tbl subst'' metasenv''
+ context (name,s') t' (sort1,sort2) ugraph2
in
C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
| C.Lambda (n,s,t) ->
enrich localization_tbl s'
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.NotMetaClosed ->
enrich localization_tbl s'
(Uncertain
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.SomeCoercion candidates ->
let selected =
enrich localization_tbl s'
(RefineFailure
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
+ CicMetaSubst.ppterm_in_context ~metasenv
subst coercion_src context ^
" that is not a sort")))
in
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
- subst'',metasenv'',ugraph2
+ C.LetIn (n,s',t'),
+ CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
+ subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
let he',hetype,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context he ugraph
enrich localization_tbl term' exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst term'
+ CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst actual_type
+ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_type' context))
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
in
let rec instantiate_prod t =
function
enrich localization_tbl p exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst p
+ CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst instance'
+ CicMetaSubst.ppterm_in_context ~metasenv subst instance'
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst instance
+ CicMetaSubst.ppterm_in_context ~metasenv subst instance
context)))
(subst,metasenv,ugraph5) pl' outtypeinstances
in
enrich localization_tbl bo exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst ty_of_bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_ty
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
context))
in
fl @ [bo'] , subst',metasenv',ugraph'
enrich localization_tbl bo exn
~f:(function _ ->
lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst ty_of_bo
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_ty
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
context))
in
fl @ [bo'],subst',metasenv',ugraph'
| Some t,Some (_,C.Def (ct,_)) ->
let subst',metasenv',ugraph' =
(try
+prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
fo_unif_subst subst context metasenv t ct ugraph
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
(try
fo_unif_subst
subst' context metasenv' inferredty ct ugraph1
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t'], subst'',metasenv'',ugraph2
| None, Some _ ->
- raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
+ raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
with
Invalid_argument _ ->
raise
(RefineFailure
(lazy (sprintf
"Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
- (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
- (CicMetaSubst.ppcontext subst canonical_context))))
+ (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
and check_exp_named_subst metasubst metasenv context tl ugraph =
let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
with _ ->
raise (RefineFailure (lazy
("Wrong Explicit Named Substitution: " ^
- CicMetaSubst.ppterm metasubst' typeoft ^
+ CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
" not unifiable with " ^
- CicMetaSubst.ppterm metasubst' typeofvar)))
+ CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
in
(* FIXME: no mere tail recursive! *)
let exp_name_subst, metasubst''', metasenv''', ugraph4 =
check_exp_named_subst_aux metasubst metasenv [] tl ugraph
- and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
+ and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
+ ugraph
+ =
let module C = Cic in
let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicReduction.whd ~subst context t1 in
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() 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
+ (try
+ 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
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) ->
C.Sort (C.Type t1),subst,metasenv,ugraph
| (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
with _ -> assert false (* unification against a metavariable *)
in
t2'',subst,metasenv,ugraph1
+ | (C.Sort _,_)
+ | (C.Meta _,_) ->
+ enrich localization_tbl s
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
| _,_ ->
- raise
- (RefineFailure
- (lazy
- (sprintf
- ("Two sorts were expected, found %s " ^^
- "(that reduces to %s) and %s (that reduces to %s)")
- (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
- (CicPp.ppterm t2''))))
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
and avoid_double_coercion context subst metasenv ugraph t ty =
+ if not !pack_coercions then
+ t,ty,subst,metasenv,ugraph
+ else
let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
if b then
let source_carr = CoercGraph.source_of c2 in
| RefineFailure s | Uncertain s ->
debug_print s;debug_print (lazy "goon\n");
try
+ let old_pack_coercions = !pack_coercions in
pack_coercions := false; (* to avoid diverging *)
let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
type_of_aux subst metasenv context c1_c2_implicit ugraph
in
- pack_coercions := true;
+ pack_coercions := old_pack_coercions;
let b, _, _, _, _ =
is_a_double_coercion refined_c1_c2_implicit
in
debug_print
(lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
t, ty, subst, metasenv, ugraph)
- | _ -> assert false) (* the composite coercion must exist *)
+ | _ -> t, ty, subst, metasenv, ugraph)
else
t, ty, subst, metasenv, ugraph
(* {{{ 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));
+ ("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
HExtlib.list_findopt
(fun coerc ->
let t = Cic.Appl [coerc;x] in
- debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t));
try
(* we want this to be available in the error handler fo the
* following (so it has its own try. *)
mk_prod_of_metas metasenv context subst remainder
in
debug_print (lazy
- (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
- CicMetaSubst.ppterm subst hetype'));
+ (" 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
metasenv context subst t tty remainder ugraph
in
Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
- with exn -> None
- with exn -> None)
+ with Uncertain _ | RefineFailure _ -> None
+ with Uncertain _ | 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 ->
- enrich localization_tbl he
- ~f:(fun _-> more_args_than_expected subst he context hetype
- args_bo_and_ty) exn
+ more_args_than_expected localization_tbl metasenv
+ subst he context hetype args_bo_and_ty exn
(* }}} end coercion to funclass stuff *)
(* }}} end fix_arity *)
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 he hetype ugraph newargs
+ pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
=
(* {{{ body *)
function
(match coer with
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
- enrich localization_tbl hete
- (RefineFailure
+ enrich localization_tbl hete exn
+ ~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.NotMetaClosed ->
- enrich localization_tbl hete
- (Uncertain
+ enrich localization_tbl hete exn
+ ~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.SomeCoercion candidates ->
let selected =
enrich localization_tbl hete
~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
(* "\nReason: " ^ Lazy.force e*)))) exn))
| exn ->
enrich localization_tbl hete
~f:(fun _ ->
(lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
+ CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
+ CicMetaSubst.ppterm_in_context ~metasenv subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context ^
- "\nReason: " ^ Printexc.to_string exn))) exn
+ CicMetaSubst.ppterm_in_context ~metasenv subst s context
+ (* "\nReason: " ^ Printexc.to_string exn*)))) exn
(* }}} end coercion stuff *)
in
- eat_prods_and_args pristinemenv metasenv subst context he
+ eat_prods_and_args pristinemenv metasenv subst context pristinehe he
(CicSubstitution.subst (fst arg) t)
ugraph1 (newargs@[arg]) tl
| _ ->
(newargs@[hete,hety]@tl) ugraph
in
eat_prods_and_args metasenv
- metasenv subst context he hetype' ugraph [] args_bo_and_ty
- with RefineFailure s | Uncertain s ->
+ metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
+ with RefineFailure _ | Uncertain _ as exn ->
(* unable to fix arity *)
- let msg =
- more_args_than_expected
- subst he context hetype args_bo_and_ty
- in
- raise (RefineFailure msg)
+ 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 =
- if CicUtil.is_meta_closed hetype then
+ if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
(* this optimization is to postpone fix_arity (the most common case)*)
subst,metasenv,ugraph,hetype,he,args_bo_and_ty
else
(* this (says CSC) is also useful to infer dependent types *)
- fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+ 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
in
let coerced_args,subst,metasenv,he,t,ugraph =
eat_prods_and_args
- metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
+ metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
in
he,(List.map fst coerced_args),t,subst,metasenv,ugraph
in
let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
| C.LetIn (name,so,dest) ->
- let ctx' = Some (name,(C.Def (so,None)))::ctx in
+ let _,ty,metasenv,ugraph =
+ pack_coercions := false;
+ type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+ pack_coercions := true;
+ let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in
try
type_of_aux' metasenv ctx t ugraph
with RefineFailure _ | Uncertain _ ->
- prerr_endline (CicPp.ppterm t);
t, t, [], ugraph
in
insert_coercions := old_insert_coercions;
merge_coercions ctx t
;;
+let pack_coercion_metasenv conjectures =
+ let module C = Cic in
+ List.map
+ (fun (i, ctx, ty) ->
+ let ctx =
+ List.fold_right
+ (fun item ctx ->
+ let item' =
+ match item with
+ Some (name, C.Decl t) ->
+ Some (name, C.Decl (pack_coercion conjectures ctx t))
+ | Some (name, C.Def (t,None)) ->
+ Some (name,C.Def (pack_coercion conjectures ctx t,None))
+ | Some (name, C.Def (t,Some ty)) ->
+ Some (name, C.Def (pack_coercion conjectures ctx t,
+ Some (pack_coercion conjectures ctx ty)))
+ | None -> None
+ in
+ item'::ctx
+ ) ctx []
+ in
+ ((i,ctx,pack_coercion conjectures ctx ty))
+ ) conjectures
+;;
+
let pack_coercion_obj obj =
let module C = Cic in
match obj with
let ty = pack_coercion [] [] ty in
C.Variable (name, body, ty, params, attrs)
| C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
- let conjectures =
- List.map
- (fun (i, ctx, ty) ->
- let ctx =
- List.fold_right
- (fun item ctx ->
- let item' =
- match item with
- Some (name, C.Decl t) ->
- Some (name, C.Decl (pack_coercion conjectures ctx t))
- | Some (name, C.Def (t,None)) ->
- Some (name,C.Def (pack_coercion conjectures ctx t,None))
- | Some (name, C.Def (t,Some ty)) ->
- Some (name, C.Def (pack_coercion conjectures ctx t,
- Some (pack_coercion conjectures ctx ty)))
- | None -> None
- in
- item'::ctx
- ) ctx []
- in
- ((i,ctx,pack_coercion conjectures ctx ty))
- ) conjectures
- in
+ let conjectures = pack_coercion_metasenv conjectures in
let body = pack_coercion conjectures [] body in
let ty = pack_coercion conjectures [] ty in
C.CurrentProof (name, conjectures, body, ty, params, attrs)
projects / helm.git / blobdiff