aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/coercionops.ml56
-rw-r--r--pretyping/coercionops.mli17
-rw-r--r--vernac/comCoercion.ml26
3 files changed, 38 insertions, 61 deletions
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index b62dbdb412..274dbfd7ed 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -68,6 +68,8 @@ type coe_info_typ = {
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
+ coe_source : cl_typ;
+ coe_target : cl_typ;
coe_param : int;
}
@@ -280,7 +282,7 @@ let different_class_params env ci =
| CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
| _ -> false
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph env sigma ic =
let old_inheritance_graph = !inheritance_graph in
let ambig_paths :
((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
@@ -312,45 +314,36 @@ let add_coercion_in_graph env sigma (ic,source,target) =
let try_add_new_path1 ij p =
let _ = try_add_new_path ij p in ()
in
- if try_add_new_path (source,target) [ic] then begin
+ if try_add_new_path (ic.coe_source, ic.coe_target) [ic] then begin
ClPairMap.iter
(fun (s,t) p ->
if not (cl_typ_eq s t) then begin
- if cl_typ_eq t source then begin
- try_add_new_path1 (s,target) (p@[ic]);
+ if cl_typ_eq t ic.coe_source then begin
+ try_add_new_path1 (s, ic.coe_target) (p@[ic]);
ClPairMap.iter
(fun (u,v) q ->
- if not (cl_typ_eq u v) && cl_typ_eq u target then
+ if not (cl_typ_eq u v) && cl_typ_eq u ic.coe_target then
try_add_new_path1 (s,v) (p@[ic]@q))
old_inheritance_graph
end;
- if cl_typ_eq s target then try_add_new_path1 (source,t) (ic::p)
+ if cl_typ_eq s ic.coe_target then
+ try_add_new_path1 (ic.coe_source, t) (ic::p)
end)
old_inheritance_graph
end;
match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
-type coercion = {
- coercion_type : coe_typ;
- coercion_local : bool;
- coercion_is_id : bool;
- coercion_is_proj : Projection.Repr.t option;
- coercion_source : cl_typ;
- coercion_target : cl_typ;
- coercion_params : int;
-}
-
let subst_coercion subst c =
let env = Global.env () in
- let coe = subst_coe_typ subst c.coercion_type in
- let cls = subst_cl_typ env subst c.coercion_source in
- let clt = subst_cl_typ env subst c.coercion_target in
- let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
- if c.coercion_type == coe && c.coercion_source == cls &&
- c.coercion_target == clt && c.coercion_is_proj == clp
+ let coe = subst_coe_typ subst c.coe_value in
+ let cls = subst_cl_typ env subst c.coe_source in
+ let clt = subst_cl_typ env subst c.coe_target in
+ let clp = Option.Smart.map (subst_proj_repr subst) c.coe_is_projection in
+ if c.coe_value == coe && c.coe_source == cls && c.coe_target == clt &&
+ c.coe_is_projection == clp
then c
- else { c with coercion_type = coe; coercion_source = cls;
- coercion_target = clt; coercion_is_proj = clp; }
+ else { c with coe_value = coe; coe_source = cls; coe_target = clt;
+ coe_is_projection = clp; }
(* Computation of the class arity *)
@@ -375,17 +368,10 @@ let add_class env sigma cl =
add_new_class cl { cl_param = class_params env sigma cl }
let declare_coercion env sigma c =
- let () = add_class env sigma c.coercion_source in
- let () = add_class env sigma c.coercion_target in
- let xf =
- { coe_value = c.coercion_type;
- coe_local = c.coercion_local;
- coe_is_identity = c.coercion_is_id;
- coe_is_projection = c.coercion_is_proj;
- coe_param = c.coercion_params;
- } in
- let () = add_new_coercion c.coercion_type xf in
- add_coercion_in_graph env sigma (xf, c.coercion_source, c.coercion_target)
+ let () = add_class env sigma c.coe_source in
+ let () = add_class env sigma c.coe_target in
+ let () = add_new_coercion c.coe_value c in
+ add_coercion_in_graph env sigma c
(* For printing purpose *)
let classes () =
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index b7c46122a4..fb5621dd3a 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -44,6 +44,8 @@ type coe_info_typ = {
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
+ coe_source : cl_typ;
+ coe_target : cl_typ;
coe_param : int;
}
@@ -66,20 +68,9 @@ val class_of : env -> evar_map -> types -> types * cl_typ
val class_args_of : env -> evar_map -> types -> constr list
-(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
-type coercion = {
- coercion_type : coe_typ;
- coercion_local : bool;
- coercion_is_id : bool;
- coercion_is_proj : Projection.Repr.t option;
- coercion_source : cl_typ;
- coercion_target : cl_typ;
- coercion_params : int;
-}
-
-val subst_coercion : substitution -> coercion -> coercion
+val subst_coercion : substitution -> coe_info_typ -> coe_info_typ
-val declare_coercion : env -> evar_map -> coercion -> unit
+val declare_coercion : env -> evar_map -> coe_info_typ -> unit
(** {6 Access to coercions infos } *)
val coercion_exists : coe_typ -> bool
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 15d8ebc4b5..86b15739f9 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -237,24 +237,24 @@ let open_coercion i o =
cache_coercion o
let discharge_coercion (_, c) =
- if c.coercion_local then None
+ if c.coe_local then None
else
let n =
try
- let ins = Lib.section_instance c.coercion_type in
+ let ins = Lib.section_instance c.coe_value in
Array.length (snd ins)
with Not_found -> 0
in
let nc = { c with
- coercion_params = n + c.coercion_params;
- coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
+ coe_param = n + c.coe_param;
+ coe_is_projection = Option.map Lib.discharge_proj_repr c.coe_is_projection;
} in
Some nc
let classify_coercion obj =
- if obj.coercion_local then Dispose else Substitute obj
+ if obj.coe_local then Dispose else Substitute obj
-let inCoercion : coercion -> obj =
+let inCoercion : coe_info_typ -> obj =
declare_object {(default_object "COERCION") with
open_function = simple_open open_coercion;
cache_function = cache_coercion;
@@ -269,13 +269,13 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps
| _ -> None
in
let c = {
- coercion_type = coef;
- coercion_local = local;
- coercion_is_id = isid;
- coercion_is_proj = isproj;
- coercion_source = cls;
- coercion_target = clt;
- coercion_params = ps;
+ coe_value = coef;
+ coe_local = local;
+ coe_is_identity = isid;
+ coe_is_projection = isproj;
+ coe_source = cls;
+ coe_target = clt;
+ coe_param = ps;
} in
Lib.add_anonymous_leaf (inCoercion c)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:18:29 +0000