let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
+(*
let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv last t ugraph
with
| RefineFailure _ | Uncertain _ -> None
in
+*)
let (t',_,_,_,_) as res =
match t with
(* function *)
inferredty ty' ugraph2
in
C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- exn ->
- enrich localization_tbl te'
- ~f:(fun _ ->
- 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)) exn
- )
- | C.Prod (name,s,t) ->
- let carr t subst context = CicMetaSubst.apply_subst subst t in
- let coerce_to_sort in_source tgt_sort t type_to_coerce
- subst context metasenv uragph
- =
- if not !insert_coercions then
- t,type_to_coerce,subst,metasenv,ugraph
- else
- let coercion_src = carr type_to_coerce subst context in
- match coercion_src with
- | Cic.Sort _ ->
- t,type_to_coerce,subst,metasenv,ugraph
- | Cic.Meta _ as meta ->
- t, meta, subst, metasenv, ugraph
- | Cic.Cast _ as cast ->
- t, cast, subst, metasenv, ugraph
- | term ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
- let boh =
- CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
+ 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
- (match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("(4)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl t
- (Uncertain
- (lazy ("(5)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (try_coercion t subst context ugraph coercion_tgt)
- candidates
- in
- match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("(6)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^
- " that is not a sort"))))
- in
+ C.Cast (te, ty'), ty', subst, metasenv, ugraph
+ with exn -> enrich localization_tbl te' exn)
+ | C.Prod (name,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
| C.Lambda (n,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph in
+ type_of_aux subst metasenv context s ugraph
+ in
let s',sort1,subst',metasenv',ugraph1 =
- if not !insert_coercions then
- s',sort1, subst', metasenv', ugraph1
- else
- match CicReduction.whd ~subst:subst' context sort1 with
- | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
- | coercion_src ->
- let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
- let boh =
- CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
- in
- match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl s'
- (RefineFailure
- (lazy ("(7)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl s'
- (Uncertain
- (lazy ("(8)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (try_coercion s' subst' context ugraph1 coercion_tgt)
- candidates
- in
- match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl s'
- (RefineFailure
- (lazy ("(9)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv
- subst coercion_src context ^
- " that is not a sort")))
+ coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+ s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
expected_type' actual_type ugraph2
with
exn ->
- prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
- prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
enrich localization_tbl term' exn
~f:(function _ ->
lazy ("(10)The term " ^
candidate_oty,ugraph,metasenv,subst
with
CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
+ | RefineFailure _ | Uncertain _ ->
None,ugraph,metasenv,subst
) (Some instance',ugraph4,metasenv,subst) tl
in
debug_print (lazy " success!");
Some (subst,metasenv,ugraph,tty,t,remainder)
with
- | Uncertain _ | RefineFailure _
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
+ | Uncertain _ | RefineFailure _ ->
try
let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
fix_arity
match (CicReduction.whd ~subst context hetype) with
| Cic.Prod (n,s,t) ->
let arg,subst,metasenv,ugraph1 =
- try
+ try
+ (try
let subst,metasenv,ugraph1 =
fo_unif_subst_eat_prods2
subst context metasenv hety s ugraph
in
(hete,hety),subst,metasenv,ugraph1
- (* {{{ we search a coercion from hety to s if fails *)
with RefineFailure _ | Uncertain _ as exn
when allow_coercions && !insert_coercions ->
- let coer, tgt_carr =
- let carr t subst context =
- CicReduction.whd ~delta:false
- context (CicMetaSubst.apply_subst subst t )
- in
- let c_hety = carr hety subst context in
- let c_s = carr s subst context in
- CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
- in
- (match coer with
- | CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl hete exn
- ~f:(fun _ ->
- (lazy ("(15)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: " ^ Lazy.force e*))))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl hete exn
- ~f:(fun _ ->
- (lazy ("(16)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: " ^ Lazy.force e*))))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (fun (metasenv,last,c) ->
- try
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last hete
- ugraph in
- 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 tgt_carr
- in
- let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety s ugraph
- in
- Some ((newt,newty), subst, metasenv, ugraph)
- with Uncertain _ | RefineFailure _ -> None)
- candidates
- in
- (match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("(1)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: " ^ Lazy.force e*)))) exn))
- | exn ->
+ coerce_to_something
+ hete hety s subst metasenv context exn ugraph)
+ with exn ->
enrich localization_tbl hete
~f:(fun _ ->
(lazy ("(2)The term " ^
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
+ 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 pristinehe he
(CicSubstitution.subst (fst arg) t)
metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
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
+ match coer with
+ | CoercGraph.NotMetaClosed ->
+ (match exn with
+ | RefineFailure s -> raise (Uncertain s)
+ | HExtlib.Localized _ -> assert false
+ | _ -> raise exn)
+ | CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
+ | CoercGraph.NotHandled _ ->
+ raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun (metasenv,last,c) ->
+ try
+ let subst,metasenv,ugraph =
+ 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
+ let newt, newty, subst, metasenv, ugraph =
+ avoid_double_coercion context subst metasenv
+ ugraph newt expty
+ in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety expty ugraph
+ in
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None -> raise 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 " ^
+ 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"))
+ 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
in
(* eat prods ends here! *)
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
let b,_,_,_,_ = is_a_double_coercion t in
- (* prerr_endline "CANDIDATO!!!!"; *)
if b then
let ugraph = CicUniv.oblivion_ugraph in
let old_insert_coercions = !insert_coercions in
projects / helm.git / commitdiff