summaryrefslogtreecommitdiff
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r--pretyping/coercion.ml64
1 files changed, 35 insertions, 29 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 489a311b..913e80f3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -14,7 +14,7 @@
Corbineau, Feb 2008 *)
(* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -63,7 +63,7 @@ let apply_coercion_args env evd check isproj argl funj =
{ uj_val = applist (j_val funj,argl);
uj_type = typ }
| h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
- match kind_of_term (whd_betadeltaiota env evd typ) with
+ match kind_of_term (whd_all env evd typ) with
| Prod (_,c1,c2) ->
if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
raise NoCoercion;
@@ -90,8 +90,9 @@ let inh_pattern_coerce_to loc env pat ind1 ind2 =
open Program
-let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c =
- Evarutil.e_new_evar env evdref ~src:(loc, Evar_kinds.QuestionMark opaque) c
+let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c =
+ let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
+ Evarutil.e_new_evar env evdref ~src c
let app_opt env evdref f t =
whd_betaiota !evdref (app_opt f t)
@@ -115,7 +116,7 @@ let disc_subset x =
exception NoSubtacCoercion
-let hnf env evd c = whd_betadeltaiota env evd c
+let hnf env evd c = whd_all env evd c
let hnf_nodelta env evd c = whd_betaiota evd c
let lift_args n sign =
@@ -129,7 +130,7 @@ let mu env evdref t =
let rec aux v =
let v' = hnf env !evdref v in
match disc_subset v' with
- Some (u, p) ->
+ | Some (u, p) ->
let f, ct = aux u in
let p = hnf_nodelta env !evdref p in
(Some (fun x ->
@@ -142,6 +143,7 @@ let mu env evdref t =
and coerce loc env evdref (x : Term.constr) (y : Term.constr)
: (Term.constr -> Term.constr) option
=
+ let open Context.Rel.Declaration in
let rec coerce_unify env x y =
let x = hnf env !evdref x and y = hnf env !evdref y in
try
@@ -151,8 +153,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env evdref x y in
let dest_prod c =
+ let open Context.Rel.Declaration in
match Reductionops.splay_prod_n env ( !evdref) 1 c with
- | [(na,b,t)], c -> (na,t), c
+ | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c
| _ -> raise NoSubtacCoercion
in
let coerce_application typ typ' c c' l l' =
@@ -187,9 +190,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
(subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some (fun x ->
let term = co x in
- Typing.solve_evars env evdref term)
+ Typing.e_solve_evars env evdref term)
in
- if isEvar c || isEvar c' then
+ if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
(* Second-order unification needed. *)
raise NoSubtacCoercion;
aux [] typ typ' 0 (fun x -> x)
@@ -205,7 +208,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let name' =
Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
in
- let env' = push_rel (name', None, a') env in
+ let env' = push_rel (LocalAssum (name', a')) env in
let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
let coec1 = app_opt env' evdref c1 (mkRel 1) in
@@ -241,9 +244,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let remove_head a c =
match kind_of_term c with
| Lambda (n, t, t') -> c, t'
- (*| Prod (n, t, t') -> t'*)
| Evar (k, args) ->
- let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in
+ let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
evdref := evs;
let (n, dom, rng) = destLambda t in
let dom = whd_evar !evdref dom in
@@ -255,7 +257,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
| _ -> raise NoSubtacCoercion
in
let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
- let env' = push_rel (Name Namegen.default_dependent_ident, None, a) env in
+ let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in
let c2 = coerce_unify env' b b' in
match c1, c2 with
| None, None -> None
@@ -278,7 +280,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let c1 = coerce_unify env a a' in
let c2 = coerce_unify env b b' in
match c1, c2 with
- None, None -> None
+ | None, None -> None
| _, _ ->
Some
(fun x ->
@@ -297,9 +299,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
with NoSubtacCoercion ->
let typ = Typing.unsafe_type_of env evm c in
let typ' = Typing.unsafe_type_of env evm c' in
- (* if not (is_arity env evm typ) then *)
coerce_application typ typ' c c' l l')
- (* else subco () *)
else
subco ()
| x, y when Constr.equal c c' ->
@@ -307,9 +307,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let evm = !evdref in
let lam_type = Typing.unsafe_type_of env evm c in
let lam_type' = Typing.unsafe_type_of env evm c' in
- (* if not (is_arity env evm lam_type) then ( *)
coerce_application lam_type lam_type' c c' l l'
- (* ) else subco () *)
else subco ()
| _ -> subco ())
| _, _ -> subco ()
@@ -335,10 +333,17 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
raise NoSubtacCoercion
in coerce_unify env x y
+let app_coercion env evdref coercion v =
+ match coercion with
+ | None -> v
+ | Some f ->
+ let v' = Typing.e_solve_evars env evdref (f v) in
+ whd_betaiota !evdref v'
+
let coerce_itf loc env evd v t c1 =
let evdref = ref evd in
let coercion = coerce loc env evdref t c1 in
- let t = Option.map (app_opt env evdref coercion) v in
+ let t = Option.map (app_coercion env evdref coercion) v in
!evdref, t
let saturate_evd env evd =
@@ -365,15 +370,15 @@ let apply_coercion env sigma p hj typ_cl =
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
- | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
+ | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion")
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
- let t = whd_betadeltaiota env evd j.uj_type in
+ let t = whd_all env evd j.uj_type in
match kind_of_term t with
| Prod (_,_,_) -> (evd,j)
| Evar ev ->
- let (evd',t) = define_evar_as_product evd ev in
+ let (evd',t) = Evardefine.define_evar_as_product evd ev in
(evd',{ uj_val = j.uj_val; uj_type = t })
| _ ->
try let t,p =
@@ -410,11 +415,11 @@ let inh_tosort_force loc env evd j =
error_not_a_type_loc loc env evd j
let inh_coerce_to_sort loc env evd j =
- let typ = whd_betadeltaiota env evd j.uj_type in
+ let typ = whd_all env evd j.uj_type in
match kind_of_term typ with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined evd (fst ev)) ->
- let (evd',s) = define_evar_as_sort env evd ev in
+ let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
(evd',{ utj_val = j.uj_val; utj_type = s })
| _ ->
inh_tosort_force loc env evd j
@@ -424,7 +429,7 @@ let inh_coerce_to_base loc env evd j =
let evdref = ref evd in
let ct, typ' = mu env evdref j.uj_type in
let res =
- { uj_val = app_opt env evdref ct j.uj_val;
+ { uj_val = app_coercion env evdref ct j.uj_val;
uj_type = typ' }
in !evdref, res
else (evd, j)
@@ -462,8 +467,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
- kind_of_term (whd_betadeltaiota env evd t),
- kind_of_term (whd_betadeltaiota env evd c1)
+ kind_of_term (whd_all env evd t),
+ kind_of_term (whd_all env evd c1)
with
| Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
@@ -475,7 +480,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
let name = match name with
| Anonymous -> Name Namegen.default_dependent_ident
| _ -> name in
- let env1 = push_rel (name,None,u1) env in
+ let open Context.Rel.Declaration in
+ let env1 = push_rel (LocalAssum (name,u1)) env in
let (evd', v1) =
inh_conv_coerce_to_fail loc env1 evd rigidonly
(Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
@@ -508,7 +514,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
error_actual_type_loc loc env best_failed_evd cj t e
else
inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
- with NoCoercionNoUnifier (best_failed_evd,e) ->
+ with NoCoercionNoUnifier (_evd,_error) ->
error_actual_type_loc loc env best_failed_evd cj t e
in
let val' = match val' with Some v -> v | None -> assert(false) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 03:57:07 +0000