let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
- (try
- let subst''',metasenv''',ugraph3 =
- fo_unif_subst subst'' context metasenv''
- inferredty ty' ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- | Uncertain _ | RefineFailure _ ->
- let exn =
- RefineFailure (lazy ("(3)The term " ^
- CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context metasenv''
- subst'' inferredty context ^
- " but is here used with type " ^
- CicMetaSubst.ppterm_in_context
- metasenv'' subst'' ty' context))
- in
- try
- let (te, ty), subst, metasenv, ugraph =
- coerce_to_something te' inferredty ty'
- subst'' metasenv'' context exn ugraph2
- in
- C.Cast (te, ty'), ty', subst, metasenv, ugraph
- with exn -> enrich localization_tbl te' exn)
+ let (te', ty'), subst''',metasenv''',ugraph3 =
+ coerce_to_something true localization_tbl te' inferredty ty'
+ subst'' metasenv'' context ugraph2
+ in
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
| C.Prod (name,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
let s',sort1,subst', metasenv',ugraph1 =
- coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+ coerce_to_sort localization_tbl
s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (name,(C.Decl s')))::context) in
context_for_t t ugraph1
in
let t',sort2,subst'',metasenv'',ugraph2 =
- coerce_to_sort false (Cic.Type(CicUniv.fresh()))
+ coerce_to_sort localization_tbl
t' sort2 subst'' context_for_t metasenv'' ugraph2
in
let sop,subst''',metasenv''',ugraph3 =
type_of_aux subst metasenv context s ugraph
in
let s',sort1,subst',metasenv',ugraph1 =
- coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+ coerce_to_sort localization_tbl
s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
| (hete, hety)::tl ->
match (CicReduction.whd ~subst context hetype) with
| Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph1 =
- try
- (try
- let subst,metasenv,ugraph1 =
- fo_unif_subst_eat_prods2
- subst context metasenv hety s ugraph
- in
- (hete,hety),subst,metasenv,ugraph1
- with RefineFailure _ | Uncertain _ as exn
- when allow_coercions && !insert_coercions ->
- coerce_to_something
- hete hety s subst metasenv context exn ugraph)
- with exn ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("(2)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context
- ~metasenv subst s context
- (* "\nReason: " ^ Printexc.to_string exn*)))) exn
- in
- eat_prods_and_args pristinemenv metasenv subst context pristinehe he
- (CicSubstitution.subst (fst arg) t)
- ugraph1 (newargs@[arg]) tl
+ 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 =
(newargs@[hete,hety]@tl) ugraph
in
eat_prods_and_args metasenv
- metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
+ 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
in
he,(List.map fst coerced_args),t,subst,metasenv,ugraph
- and coerce_to_something t infty expty subst metasenv context exn ugraph =
- if not !insert_coercions then
- raise exn
- else
- let clean t subst context =
- CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t)
- in
- let infty = clean infty subst context in
- let expty = clean expty subst context in
- match infty, expty with
- | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
- (* covariant part *)
- let name_con = Cic.Name "name_con" in
- let name_t, ty_s_bo, bo =
- match t with
- | Cic.Lambda (name, src, bo) -> name, src, bo
- | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1]
- in
- let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
- let (bo, _), subst, metasenv, ugraph =
- coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph
- in
- (* contravariant part *)
- let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
- let (rel1, _), subst, metasenv, ugraph =
- coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2)
- (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn
- ugraph
- in
- let coerced =
- Cic.Lambda (name_t,src2,
- CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
- in
- (coerced, expty), subst, metasenv, ugraph
- | _ ->
- coerce_atom_to_something t infty expty subst metasenv context exn ugraph
-
- and coerce_atom_to_something t infty expty subst metasenv context exn ugraph =
- let coer =
- CoercGraph.look_for_coercion metasenv subst context infty expty
- in
+ and coerce_to_something
+ allow_coercions localization_tbl t infty expty subst metasenv context ugraph
+ =
+ let coerce_atom_to_something t infty expty subst metasenv context ugraph =
+ let coer =
+ CoercGraph.look_for_coercion metasenv subst context infty expty
+ in
match coer with
- | CoercGraph.NotMetaClosed ->
- (match exn with
- | RefineFailure s -> raise (Uncertain s)
- | HExtlib.Localized _ -> assert false
- | _ -> raise exn)
+ | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
+ "coerce_atom_to_something fails since not meta closed"))
| CoercGraph.NoCoercion
| CoercGraph.SomeCoercionToTgt _
- | CoercGraph.NotHandled _ ->
- raise exn
+ | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+ "coerce_atom_to_something fails since no coercions found"))
| CoercGraph.SomeCoercion candidates ->
+ let uncertain = ref false in
let selected =
HExtlib.list_findopt
(fun (metasenv,last,c) ->
try
let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last t
- ugraph in
+ fo_unif_subst subst context metasenv last t ugraph in
let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context
- c ugraph
- in
+ 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,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety expty ugraph
- in
+ fo_unif_subst subst context metasenv newhety expty ugraph in
Some ((newt,newty), subst, metasenv, ugraph)
- with Uncertain _ | RefineFailure _ -> None)
+ with
+ | Uncertain _ -> uncertain := true; None
+ | RefineFailure _ -> None)
candidates
in
match selected with
| Some x -> x
- | None -> raise exn
+ | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
+ | None -> raise (RefineFailure (lazy "coerce_atom fails"))
+ in
+ let rec coerce_to_something_aux
+ t infty expty subst metasenv context ugraph
+ =
+ try
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv infty expty ugraph
+ in
+ (t, expty), subst, metasenv, ugraph
+ with Uncertain _ | RefineFailure _ as exn ->
+ if not allow_coercions || not !insert_coercions then
+ enrich localization_tbl t exn
+ else
+ let clean t subst context =
+ CicReduction.whd
+ ~delta:false context (CicMetaSubst.apply_subst subst t)
+ in
+ let infty = clean infty subst context in
+ let expty = clean expty subst context in
+ match infty, expty with
+ | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
+ (* covariant part *)
+ let name_con = Cic.Name "name_con" in
+ let name_t, ty_s_bo, bo =
+ match t with
+ | Cic.Lambda (name, src, bo) -> name, src, bo
+ | _ -> name_con,src,Cic.Appl[CicSubstitution.lift 1 t;Cic.Rel 1]
+ in
+ let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
+ let (bo, _), subst, metasenv, ugraph =
+ coerce_to_something_aux
+ bo ty ty2 subst metasenv context_bo ugraph
+ in
+ (* contravariant part *)
+ let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something_aux
+ (Cic.Rel 1) (CicSubstitution.lift 1 src2)
+ (CicSubstitution.lift 1 src) subst metasenv context_rel1 ugraph
+ in
+ let coerced =
+ Cic.Lambda (name_t,src2,
+ CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
+ in
+ (coerced, expty), subst, metasenv, ugraph
+ | _ ->
+ coerce_atom_to_something t infty expty subst metasenv context ugraph
+ in
+ try
+ coerce_to_something_aux t infty expty subst metasenv context ugraph
+ with Uncertain _ | RefineFailure _ ->
+ let exn =
+ RefineFailure (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context metasenv subst t context ^
+ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
+ infty context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context metasenv subst expty context))
+ in
+ enrich localization_tbl t exn
- and coerce_to_sort
- in_source tgt_sort t type_to_coerce subst context metasenv uragph =
- match CicReduction.whd ~subst:subst context type_to_coerce with
- | Cic.Meta _ | Cic.Sort _ ->
- t,type_to_coerce, subst, metasenv, ugraph
- | src ->
- let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
- let exn =
- RefineFailure (lazy ("(7)The term " ^
+ and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
+ match CicReduction.whd ~subst:subst context infty with
+ | Cic.Meta _ | Cic.Sort _ ->
+ t,infty, subst, metasenv, ugraph
+ | src ->
+ let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+ try
+ let (t, ty_t), subst, metasenv, ugraph =
+ coerce_to_something true
+ localization_tbl t src tgt subst metasenv context ugraph
+ in
+ t, ty_t, subst, metasenv, ugraph
+ with HExtlib.Localized (_, exn) ->
+ let f _ =
+ lazy ("(7)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst t context
^ " is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst src context
- ^ " that is not a sort"))
+ ^ " that is not a sort")
in
- try
- let (t, ty_t), subst, metasenv, ugraph =
- coerce_to_something t src tgt
- subst metasenv context exn ugraph
- in
- t, ty_t, subst, metasenv, ugraph
- with exn -> enrich localization_tbl t exn
+ enrich localization_tbl ~f t exn
in
(* eat prods ends here! *)
projects / helm.git / commitdiff