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 *)
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
- 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
- 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"))))
+ 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 =
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 localization_tbl
+ 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
| (hete, hety)::tl ->
match (CicReduction.whd ~subst context hetype) with
| Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph1 =
- 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 ->
- 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
- (* }}} end coercion stuff *)
- 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
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
+ allow_coercions localization_tbl t infty expty subst metasenv context ugraph
+ =
+ let module CS = CicSubstitution in
+ let module CR = CicReduction in
+ let cs_subst = CS.subst ~avoid_beta_redexes:true in
+ 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 -> raise (Uncertain (lazy
+ "coerce_atom_to_something fails since not meta closed"))
+ | CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
+ | 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 *)
+ let posibilities =
+ HExtlib.filter_map
+ (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,ugraph =
+ fo_unif_subst subst context metasenv newhety expty ugraph in
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with
+ | Uncertain _ -> uncertain := true; None
+ | RefineFailure _ -> None)
+ candidates
+ in
+ match
+ List.fast_sort
+ (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
+ posibilities
+ with
+ | [] -> None
+ | x::_ -> Some x
+ in
+ match selected with
+ | Some x -> x
+ | 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 whd = CicReduction.whd ~delta:false in
+ let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
+ let infty = clean infty subst context in
+ let expty = clean expty subst context in
+ match infty, expty, t with
+ | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
+ (match fl with
+ [name,i,_(* infty *),bo] ->
+ let context_bo =
+ Some (Cic.Name name,Cic.Decl expty)::context in
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something_aux (Cic.Rel 1)
+ (CS.lift 1 expty) (CS.lift 1 infty) subst
+ metasenv context_bo ugraph in
+ let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
+ let (bo,_), subst, metasenv, ugraph =
+ coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
+ expty) subst
+ metasenv context_bo ugraph
+ in
+ (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
+ | _ -> assert false (* not implemented yet *))
+ | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
+ (* move this stuff away *)
+ let get_cl_and_left_p uri tyno outty ugraph =
+ match CicEnvironment.get_obj ugraph uri with
+ | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
+ let count_pis t =
+ let rec aux ctx t =
+ match CicReduction.whd ~delta:false ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ let ctx = Some (name, Cic.Decl src) :: ctx in
+ 1 + aux ctx tgt
+ | _ -> 0
+ in
+ aux [] t
+ in
+ let rec skip_lambda_delifting t n =
+ match t,n with
+ | _,0 -> t
+ | Cic.Lambda (_,_,t),n ->
+ skip_lambda_delifting
+ (CS.subst (Cic.Implicit None) t) (n - 1)
+ | _ -> assert false
+ in
+ let get_l_r_p n = function
+ | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
+ | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
+ HExtlib.split_nth n args
+ | _ -> assert false
+ in
+ let _, _, ty, cl = List.nth tl tyno in
+ let pis = count_pis ty in
+ let rno = pis - leftno in
+ let t = skip_lambda_delifting outty rno in
+ let left_p, _ = get_l_r_p leftno t in
+ let instantiale_with_left cl =
+ List.map
+ (fun ty ->
+ List.fold_left
+ (fun t p -> match t with
+ | Cic.Prod (_,_,t) ->
+ cs_subst p t
+ | _-> assert false)
+ ty left_p)
+ cl
+ in
+ let cl = instantiale_with_left (List.map snd cl) in
+ cl, left_p, leftno, rno, ugraph
+ | _ -> raise exn
+ in
+ let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
+ match t,n with
+ | _,0 ->
+ let rec mkr n = function
+ | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
+ in
+ let bo =
+ CicReplace.replace_lifting
+ ~equality:(fun _ -> CicUtil.alpha_equivalence)
+ ~context:ctx
+ ~what:(matched::right_p)
+ ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
+ ~where:bo
+ in
+ bo
+ | Cic.Lambda (name, src, tgt),_ ->
+ Cic.Lambda (name, src,
+ keep_lambdas_and_put_expty
+ (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
+ (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
+ | _ -> assert false
+ in
+ let add_params
+ metasenv subst context uri tyno cty outty leftno i
+ =
+ let mytl = function [] -> [] | _::tl -> tl in
+ let rec aux context outty par k = function
+ | Cic.Prod (name, src, tgt) ->
+ Cic.Prod (name, src,
+ aux
+ (Some (name, Cic.Decl src) :: context)
+ (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
+ | Cic.MutInd _ ->
+ let par = mytl par in
+ let k =
+ let k = Cic.MutConstruct (uri,tyno,i,[]) in
+ if par <> [] then Cic.Appl (k::par) else k
+ in
+ CR.head_beta_reduce ~delta:false
+ (Cic.Appl [outty;k])
+ | Cic.Appl (Cic.MutInd _::pl) ->
+ let left_p,_ = HExtlib.split_nth leftno pl in
+ let k =
+ let k = Cic.MutConstruct (uri,tyno,i,[]) in
+ Cic.Appl (k::left_p@par)
+ in
+ let right_p =
+ try match
+ CicTypeChecker.type_of_aux' ~subst metasenv context k
+ CicUniv.oblivion_ugraph
+ with
+ | Cic.Appl (Cic.MutInd _::args),_ ->
+ snd (HExtlib.split_nth leftno args)
+ | _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ CR.head_beta_reduce ~delta:false
+ (Cic.Appl (outty ::right_p @ [k]))
+ | _ -> assert false
+ in
+ aux context outty [] 1 cty
+ in
+ (* constructors types with left params already instantiated *)
+ let outty = CicMetaSubst.apply_subst subst outty in
+ let cl, left_p, leftno,rno,ugraph =
+ get_cl_and_left_p uri tyno outty ugraph
+ in
+ let right_p =
+ try
+ match
+ CicTypeChecker.type_of_aux' ~subst metasenv context m
+ CicUniv.oblivion_ugraph
+ with
+ | Cic.MutInd _,_ -> []
+ | Cic.Appl (Cic.MutInd _::args),_ ->
+ snd (HExtlib.split_nth leftno args)
+ | _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _ ->
+ let rec foo =
+ function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
+ in
+ foo rno
+ in
+ let new_outty =
+ keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
+ in
+ let _,pl,subst,metasenv,ugraph =
+ List.fold_right2
+ (fun cty pbo (i, acc, s, m, ugraph) ->
+ (* Pi k_par, (naw_)outty right_par (K_i left_par k_par) *)
+ let infty_pbo =
+ add_params m s context uri tyno cty outty leftno i in
+ let expty_pbo =
+ add_params m s context uri tyno cty new_outty leftno i in
+ let (pbo, _), subst, metasenv, ugraph =
+ coerce_to_something_aux pbo infty_pbo expty_pbo
+ s m context ugraph
+ in
+ (i-1, pbo::acc, subst, metasenv, ugraph))
+ cl pl (List.length pl, [], subst, metasenv, ugraph)
+ in
+ let t = Cic.MutCase(uri, tyno, new_outty, m, pl) in
+ (t, expty), subst, metasenv, ugraph
+ | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
+ let name_con =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst metasenv context Cic.Anonymous ~typ:src2
+ in
+ let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
+ (* contravariant part: the argument of f:src->ty *)
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something_aux
+ (Cic.Rel 1) (CS.lift 1 src2)
+ (CS.lift 1 src) subst metasenv context_src2 ugraph
+ in
+ (* covariant part: the result of f(c x); x:src2; (c x):src *)
+ let name_t, bo =
+ match t with
+ | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
+ | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
+ in
+ (* we fix the possible dependency problem in the source ty *)
+ let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
+ let (bo, _), subst, metasenv, ugraph =
+ coerce_to_something_aux
+ bo ty ty2 subst metasenv context_src2 ugraph
+ in
+ let coerced = Cic.Lambda (name_t,src2, bo) in
+ debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst coerced context));
+ (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 _ as exn ->
+ let f _ =
+ 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 ~f t exn
+
+ 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")
+ in
+ enrich localization_tbl ~f 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 / blobdiff