aboutsummaryrefslogtreecommitdiff
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r--pretyping/coercion.ml390
1 files changed, 195 insertions, 195 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3c71871968..e07fec6b43 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -115,18 +115,18 @@ let disc_subset sigma x =
| App (c, l) ->
(match EConstr.kind sigma c with
Ind (i,_) ->
- let len = Array.length l in
- let sigty = delayed_force sig_typ in
- if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty)
- then
- let (a, b) = pair_of_array l in
- Some (a, b)
- else None
+ let len = Array.length l in
+ let sigty = delayed_force sig_typ in
+ if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty)
+ then
+ let (a, b) = pair_of_array l in
+ Some (a, b)
+ else None
| _ -> None)
| _ -> None
exception NoSubtacCoercion
-
+
let hnf env evd c = whd_all env evd c
let hnf_nodelta env evd c = whd_betaiota evd c
@@ -142,12 +142,12 @@ let mu env evdref t =
let v' = hnf env !evdref v in
match disc_subset !evdref v' with
| Some (u, p) ->
- let f, ct = aux u in
- let p = hnf_nodelta env !evdref p in
- (Some (fun x ->
- app_opt env evdref
- f (papp evdref sig_proj1 [| u; p; x |])),
- ct)
+ let f, ct = aux u in
+ let p = hnf_nodelta env !evdref p in
+ (Some (fun x ->
+ app_opt env evdref
+ f (papp evdref sig_proj1 [| u; p; x |])),
+ ct)
| None -> (None, v)
in aux t
@@ -159,7 +159,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
let x = hnf env !evdref x and y = hnf env !evdref y in
try
evdref := Evarconv.unify_leq_delay env !evdref x y;
- None
+ None
with UnableToUnify _ -> coerce' env x y
and coerce' env x y : (EConstr.constr -> EConstr.constr) option =
let subco () = subset_coerce env evdref x y in
@@ -171,162 +171,162 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
let coerce_application typ typ' c c' l l' =
let len = Array.length l in
let rec aux tele typ typ' i co =
- if i < len then
- let hdx = l.(i) and hdy = l'.(i) in
+ if i < len then
+ let hdx = l.(i) and hdy = l'.(i) in
try evdref := unify_leq_delay env !evdref hdx hdy;
- let (n, eqT), restT = dest_prod typ in
- let (n', eqT'), restT' = dest_prod typ' in
+ let (n, eqT), restT = dest_prod typ in
+ let (n', eqT'), restT' = dest_prod typ' in
aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
- with UnableToUnify _ ->
+ with UnableToUnify _ ->
let (n, eqT), restT = dest_prod typ in
- let (n', eqT'), restT' = dest_prod typ' in
+ let (n', eqT'), restT' = dest_prod typ' in
let () =
try evdref := unify_leq_delay env !evdref eqT eqT'
with UnableToUnify _ -> raise NoSubtacCoercion
in
- (* Disallow equalities on arities *)
- if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion;
- let restargs = lift_args 1
- (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
- in
- let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
+ (* Disallow equalities on arities *)
+ if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion;
+ let restargs = lift_args 1
+ (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
+ in
+ let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
- let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
+ let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
let evar = make_existential ?loc n.binder_name env evdref eq in
- let eq_app x = papp evdref coq_eq_rect
- [| eqT; hdx; pred; x; hdy; evar|]
- in
- aux (hdy :: tele) (subst1 hdx restT)
- (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
- else Some (fun x ->
- let term = co x in
+ let eq_app x = papp evdref coq_eq_rect
+ [| eqT; hdx; pred; x; hdy; evar|]
+ in
+ aux (hdy :: tele) (subst1 hdx restT)
+ (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
+ else Some (fun x ->
+ let term = co x in
let sigma, term = Typing.solve_evars env !evdref term in
evdref := sigma; term)
in
- if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
- (* Second-order unification needed. *)
- raise NoSubtacCoercion;
- aux [] typ typ' 0 (fun x -> x)
+ if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
+ (* Second-order unification needed. *)
+ raise NoSubtacCoercion;
+ aux [] typ typ' 0 (fun x -> x)
in
match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
| Sort s, Sort s' ->
(match ESorts.kind !evdref s, ESorts.kind !evdref s' with
| Prop, Prop | Set, Set -> None
| (Prop | Set), Type _ -> None
- | Type x, Type y when Univ.Universe.equal x y -> None (* false *)
- | _ -> subco ())
+ | Type x, Type y when Univ.Universe.equal x y -> None (* false *)
+ | _ -> subco ())
| Prod (name, a, b), Prod (name', a', b') ->
- let name' =
+ let name' =
{name' with
binder_name =
Name (Namegen.next_ident_away
Namegen.default_dependent_ident (Termops.vars_of_env 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
- (* env, x : a' |- c1[x] : lift 1 a *)
- let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
- (* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
- (match c1, c2 with
- | None, None -> None
- | _, _ ->
- Some
- (fun f ->
+ 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
+ (* env, x : a' |- c1[x] : lift 1 a *)
+ let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
+ (* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
+ (match c1, c2 with
+ | None, None -> None
+ | _, _ ->
+ Some
+ (fun f ->
mkLambda (name', a',
- app_opt env' evdref c2
- (mkApp (lift 1 f, [| coec1 |])))))
+ app_opt env' evdref c2
+ (mkApp (lift 1 f, [| coec1 |])))))
| App (c, l), App (c', l') ->
- (match EConstr.kind !evdref c, EConstr.kind !evdref c' with
- Ind (i, u), Ind (i', u') -> (* Inductive types *)
- let len = Array.length l in
- let sigT = delayed_force sigT_typ in
- let prod = delayed_force prod_typ in
- (* Sigma types *)
- if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
- && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod))
- then
- if eq_ind i (destIndRef sigT)
- then
- begin
- let (a, pb), (a', pb') =
- pair_of_array l, pair_of_array l'
- in
- let c1 = coerce_unify env a a' in
- let remove_head a c =
- match EConstr.kind !evdref c with
+ (match EConstr.kind !evdref c, EConstr.kind !evdref c' with
+ Ind (i, u), Ind (i', u') -> (* Inductive types *)
+ let len = Array.length l in
+ let sigT = delayed_force sigT_typ in
+ let prod = delayed_force prod_typ in
+ (* Sigma types *)
+ if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
+ && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod))
+ then
+ if eq_ind i (destIndRef sigT)
+ then
+ begin
+ let (a, pb), (a', pb') =
+ pair_of_array l, pair_of_array l'
+ in
+ let c1 = coerce_unify env a a' in
+ let remove_head a c =
+ match EConstr.kind !evdref c with
| Lambda (n, t, t') -> c, t'
- | Evar (k, args) ->
- let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
- evdref := evs;
+ | Evar (k, args) ->
+ let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
+ evdref := evs;
let (n, dom, rng) = destLambda !evdref t in
- if isEvar !evdref dom then
- let (domk, args) = destEvar !evdref dom in
+ if isEvar !evdref dom then
+ let (domk, args) = destEvar !evdref dom in
evdref := define domk a !evdref;
- else ();
- t, rng
- | _ -> raise NoSubtacCoercion
- in
+ else ();
+ t, rng
+ | _ -> raise NoSubtacCoercion
+ in
let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
let ra = Retyping.relevance_of_type env !evdref a in
let env' = push_rel
(LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a))
env
in
- let c2 = coerce_unify env' b b' in
- match c1, c2 with
- | None, None -> None
- | _, _ ->
- Some
- (fun x ->
- let x, y =
- app_opt env' evdref c1 (papp evdref sigT_proj1
- [| a; pb; x |]),
- app_opt env' evdref c2 (papp evdref sigT_proj2
- [| a; pb; x |])
- in
- papp evdref sigT_intro [| a'; pb'; x ; y |])
- end
- else
- begin
- let (a, b), (a', b') =
- pair_of_array l, pair_of_array l'
- in
- let c1 = coerce_unify env a a' in
- let c2 = coerce_unify env b b' in
- match c1, c2 with
- | None, None -> None
- | _, _ ->
- Some
- (fun x ->
- let x, y =
- app_opt env evdref c1 (papp evdref prod_proj1
- [| a; b; x |]),
- app_opt env evdref c2 (papp evdref prod_proj2
- [| a; b; x |])
- in
- papp evdref prod_intro [| a'; b'; x ; y |])
- end
- else
- if eq_ind i i' && Int.equal len (Array.length l') then
- let evm = !evdref in
- (try subco ()
- with NoSubtacCoercion ->
- let typ = Typing.unsafe_type_of env evm c in
- let typ' = Typing.unsafe_type_of env evm c' in
- coerce_application typ typ' c c' l l')
- else
- subco ()
- | x, y when EConstr.eq_constr !evdref c c' ->
- if Int.equal (Array.length l) (Array.length l') then
- 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
- coerce_application lam_type lam_type' c c' l l'
- else subco ()
- | _ -> subco ())
+ let c2 = coerce_unify env' b b' in
+ match c1, c2 with
+ | None, None -> None
+ | _, _ ->
+ Some
+ (fun x ->
+ let x, y =
+ app_opt env' evdref c1 (papp evdref sigT_proj1
+ [| a; pb; x |]),
+ app_opt env' evdref c2 (papp evdref sigT_proj2
+ [| a; pb; x |])
+ in
+ papp evdref sigT_intro [| a'; pb'; x ; y |])
+ end
+ else
+ begin
+ let (a, b), (a', b') =
+ pair_of_array l, pair_of_array l'
+ in
+ let c1 = coerce_unify env a a' in
+ let c2 = coerce_unify env b b' in
+ match c1, c2 with
+ | None, None -> None
+ | _, _ ->
+ Some
+ (fun x ->
+ let x, y =
+ app_opt env evdref c1 (papp evdref prod_proj1
+ [| a; b; x |]),
+ app_opt env evdref c2 (papp evdref prod_proj2
+ [| a; b; x |])
+ in
+ papp evdref prod_intro [| a'; b'; x ; y |])
+ end
+ else
+ if eq_ind i i' && Int.equal len (Array.length l') then
+ let evm = !evdref in
+ (try subco ()
+ with NoSubtacCoercion ->
+ let typ = Typing.unsafe_type_of env evm c in
+ let typ' = Typing.unsafe_type_of env evm c' in
+ coerce_application typ typ' c c' l l')
+ else
+ subco ()
+ | x, y when EConstr.eq_constr !evdref c c' ->
+ if Int.equal (Array.length l) (Array.length l') then
+ 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
+ coerce_application lam_type lam_type' c c' l l'
+ else subco ()
+ | _ -> subco ())
| _, _ -> subco ()
and subset_coerce env evdref x y =
@@ -334,20 +334,20 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
Some (u, p) ->
let c = coerce_unify env u y in
let f x =
- app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |])
+ app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |])
in Some f
| None ->
- match disc_subset !evdref y with
- Some (u, p) ->
- let c = coerce_unify env x u in
- Some
- (fun x ->
- let cx = app_opt env evdref c x in
- let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |]))
- in
- (papp evdref sig_intro [| u; p; cx; evar |]))
- | None ->
- raise NoSubtacCoercion
+ match disc_subset !evdref y with
+ Some (u, p) ->
+ let c = coerce_unify env x u in
+ Some
+ (fun x ->
+ let cx = app_opt env evdref c x in
+ let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |]))
+ in
+ (papp evdref sig_intro [| u; p; cx; evar |]))
+ | None ->
+ raise NoSubtacCoercion
in coerce_unify env x y
let app_coercion env evdref coercion v =
@@ -371,7 +371,7 @@ let saturate_evd env evd =
(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
try
- let j,t,evd =
+ let j,t,evd =
List.fold_left
(fun (ja,typ_cl,sigma) i ->
let isid = i.coe_is_identity in
@@ -379,15 +379,15 @@ let apply_coercion env sigma p hj typ_cl =
let sigma, c = new_global sigma i.coe_value in
let typ = Retyping.get_type_of env sigma c in
let fv = make_judge c typ in
- let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
- let sigma, jres =
- apply_coercion_args env sigma true isproj argl fv
- in
- (if isid then
- { uj_val = ja.uj_val; uj_type = jres.uj_type }
- else
- jres),
- jres.uj_type,sigma)
+ let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
+ let sigma, jres =
+ apply_coercion_args env sigma true isproj argl fv
+ in
+ (if isid then
+ { uj_val = ja.uj_val; uj_type = jres.uj_type }
+ else
+ jres),
+ jres.uj_type,sigma)
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
@@ -399,11 +399,11 @@ let inh_app_fun_core ~program_mode env evd j =
| Prod _ -> (evd,j)
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product env evd ev in
- (evd',{ uj_val = j.uj_val; uj_type = t })
+ (evd',{ uj_val = j.uj_val; uj_type = t })
| _ ->
- try let t,p =
- lookup_path_to_fun_from env evd j.uj_type in
- apply_coercion env evd p j t
+ try let t,p =
+ lookup_path_to_fun_from env evd j.uj_type in
+ apply_coercion env evd p j t
with Not_found | NoCoercion ->
if program_mode then
try
@@ -444,10 +444,10 @@ let inh_coerce_to_sort ?loc env evd j =
match EConstr.kind evd typ with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s })
| Evar ev ->
- let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
- (evd',{ utj_val = j.uj_val; utj_type = s })
+ 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
+ inh_tosort_force ?loc env evd j
let inh_coerce_to_base ?loc ~program_mode env evd j =
if program_mode then
@@ -455,7 +455,7 @@ let inh_coerce_to_base ?loc ~program_mode env evd j =
let ct, typ' = mu env evdref j.uj_type in
let res =
{ uj_val = (app_coercion env evdref ct j.uj_val);
- uj_type = typ' }
+ uj_type = typ' }
in !evdref, res
else (evd, j)
@@ -473,14 +473,14 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 =
else
let evd, v', t' =
try
- let t2,t1,p = lookup_path_between env evd (t,c1) in
- match v with
- | Some v ->
- let evd,j =
- apply_coercion env evd p
- {uj_val = v; uj_type = t} t2 in
- evd, Some j.uj_val, j.uj_type
- | None -> evd, None, t
+ let t2,t1,p = lookup_path_between env evd (t,c1) in
+ match v with
+ | Some v ->
+ let evd,j =
+ apply_coercion env evd p
+ {uj_val = v; uj_type = t} t2 in
+ evd, Some j.uj_val, j.uj_type
+ | None -> evd, None, t
with Not_found -> raise NoCoercion
in
try (unify_leq_delay ~flags env evd t' c1, v')
@@ -501,24 +501,24 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid
| Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
(* We eta-expand (hence possibly modifying the original term!) *)
- (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
- (* has type forall (x:u1), u2 (with v' recursively obtained) *)
+ (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
+ (* has type forall (x:u1), u2 (with v' recursively obtained) *)
(* Note: we retype the term because template polymorphism may have *)
(* weakened its type *)
let name = map_annot (function
- | Anonymous -> Name Namegen.default_dependent_ident
+ | Anonymous -> Name Namegen.default_dependent_ident
| na -> na) name in
- let open Context.Rel.Declaration 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
+ let (evd', v1) =
+ inh_conv_coerce_to_fail ?loc env1 evd rigidonly
(Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
let v1 = Option.get v1 in
- let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in
- let t2 = match v2 with
- | None -> subst_term evd' v1 t2
- | Some v2 -> Retyping.get_type_of env1 evd' v2 in
- let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in
+ let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in
+ let t2 = match v2 with
+ | None -> subst_term evd' v1 t2
+ | Some v2 -> Retyping.get_type_of env1 evd' v2 in
+ let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in
(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
| _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
@@ -530,20 +530,20 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd
with NoCoercionNoUnifier (best_failed_evd,e) ->
try
if program_mode then
- coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t
- else raise NoSubtacCoercion
+ coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t
+ else raise NoSubtacCoercion
with
| NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
- error_actual_type ?loc env best_failed_evd cj t e
+ error_actual_type ?loc env best_failed_evd cj t e
| NoSubtacCoercion ->
- let evd' = saturate_evd env evd in
- try
- if evd' == evd then
- error_actual_type ?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 (_evd,_error) ->
- error_actual_type ?loc env best_failed_evd cj t e
+ let evd' = saturate_evd env evd in
+ try
+ if evd' == evd then
+ error_actual_type ?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 (_evd,_error) ->
+ error_actual_type ?loc env best_failed_evd cj t e
in
let val' = match val' with Some v -> v | None -> assert(false) in
(evd',{ uj_val = val'; uj_type = t })
@@ -558,4 +558,4 @@ let inh_conv_coerces_to ?loc env evd ?(flags=default_flags_of env) t t' =
fst (inh_conv_coerce_to_fail ?loc env evd ~flags true None t t')
with NoCoercion ->
evd (* Maybe not enough information to unify *)
-
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 01:53:43 +0000