aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/mod_typing.ml27
-rw-r--r--kernel/subtyping.mli2
-rw-r--r--kernel/uGraph.ml12
-rw-r--r--kernel/uGraph.mli4
-rw-r--r--kernel/univ.ml3
-rw-r--r--kernel/univ.mli6
-rw-r--r--test-suite/modules/polymorphism.v81
7 files changed, 114 insertions, 21 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 71c037008..69fbd0f32 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -92,37 +92,28 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
c, Reduction.infer_conv env' (Environ.universes env') c c'
in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
| Polymorphic_const uctx ->
- let uctx = Univ.instantiate_univ_context uctx in
- let cus, ccst = Univ.UContext.dest uctx in
- let newus, cst = Univ.UContext.dest ctx in
- let () =
- if not (Univ.Instance.length cus == Univ.Instance.length newus) then
- error_incorrect_with_constraint lab
- in
- let inst = Univ.Instance.append cus newus in
- let csti = Univ.enforce_eq_instances cus newus cst in
- let csta = Univ.Constraint.union csti ccst in
- let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
- let () = if not (UGraph.check_constraints cst (Environ.universes env')) then
- error_incorrect_with_constraint lab
- in
+ let subst, ctx = Univ.abstract_universes ctx in
+ let c = Vars.subst_univs_level_constr subst c in
+ let () =
+ if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+ error_incorrect_with_constraint lab
+ in
+ let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in
let cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
let typ = Typeops.type_of_constant_type env' cb.const_type in
- let typ = Vars.subst_instance_constr cus typ in
let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
j.uj_type typ in
cst'
| Def cs ->
- let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+ let c' = Mod_subst.force_constr cs in
let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
cst'
in
if not (Univ.Constraint.is_empty cst) then
error_incorrect_with_constraint lab;
- let subst, ctx = Univ.abstract_universes ctx in
- Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty
+ c, Polymorphic_const ctx, Univ.ContextSet.empty
in
let def = Def (Mod_subst.from_val c') in
(* let ctx' = Univ.UContext.make (newus, cst) in *)
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 6590d7e71..b24c20aa0 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -11,5 +11,3 @@ open Declarations
open Environ
val check_subtypes : env -> module_type_body -> module_type_body -> constraints
-
-
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 487257a77..9793dd881 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -830,6 +830,18 @@ let sort_universes g =
in
normalize_universes g
+(** Subtyping of polymorphic contexts *)
+
+let check_subtype univs ctxT ctx =
+ if AUContext.size ctx == AUContext.size ctx then
+ let (inst, cst) = UContext.dest (AUContext.repr ctx) in
+ let cstT = UContext.constraints (AUContext.repr ctxT) in
+ let push accu v = add_universe v false accu in
+ let univs = Array.fold_left push univs (Instance.to_array inst) in
+ let univs = merge_constraints cstT univs in
+ check_constraints cst univs
+ else false
+
(** Instances *)
let check_eq_instances g t1 t2 =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 935a3cab4..4de373eb4 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -53,6 +53,10 @@ val check_constraints : constraints -> universes -> bool
val check_eq_instances : Instance.t check_function
(** Check equality of instances w.r.t. a universe graph *)
+val check_subtype : AUContext.t check_function
+(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
+ [ctx1]. *)
+
(** {6 Pretty-printing of universes. } *)
val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
diff --git a/kernel/univ.ml b/kernel/univ.ml
index cb19761b3..6614d6027 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1060,6 +1060,9 @@ module AUContext =
struct
include UContext
+ let repr (inst, cst) =
+ (Array.mapi (fun i l -> Level.var i) inst, cst)
+
let instantiate inst (u, cst) =
assert (Array.length u = Array.length inst);
subst_instance_constraints inst cst
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3d0d2234d..9d93ec26c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -319,11 +319,15 @@ module AUContext :
sig
type t
+ val repr : t -> UContext.t
+ (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of
+ the context and [cstr] the abstracted constraints. *)
+
val empty : t
val is_empty : t -> bool
val instance : t -> Instance.t
-
+
val size : t -> int
(** Keeps the order of the instances *)
diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v
new file mode 100644
index 000000000..63eaa382d
--- /dev/null
+++ b/test-suite/modules/polymorphism.v
@@ -0,0 +1,81 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Parameter foo : Type@{i} -> Type@{j}.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := A.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive X@{i} : Type@{i} :=.
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Definition foo@{i} (A : Type@{i}) : Type@{i} := A.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 12:59:08 +0000