aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli1
-rw-r--r--pretyping/typeclasses.ml65
-rw-r--r--pretyping/typeclasses.mli6
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/record.ml30
5 files changed, 64 insertions, 40 deletions
diff --git a/API/API.mli b/API/API.mli
index 48fd3a682f..0f3394fe9f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3048,6 +3048,7 @@ end
module Typeclasses :
sig
type typeclass = Typeclasses.typeclass = {
+ cl_univs : Univ.AUContext.t;
cl_impl : Globnames.global_reference;
cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
cl_props : Context.Rel.t;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 6de5bc28ba..5af36fc6b0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -57,6 +57,9 @@ type direction = Forward | Backward
(* This module defines type-classes *)
type typeclass = {
+ (* Universe quantification *)
+ cl_univs : Univ.AUContext.t;
+
(* The class implementation *)
cl_impl : global_reference;
@@ -111,23 +114,11 @@ let new_instance cl info glob poly impl =
let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
-let typeclass_univ_instance (cl,u') =
- let subst =
- let u =
- match cl.cl_impl with
- | ConstRef c ->
- let cb = Global.lookup_constant c in
- Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
- | IndRef c ->
- let mib,oib = Global.lookup_inductive c in
- Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
- | _ -> Univ.Instance.empty
- in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst)
- Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
- in
- let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
- { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
- cl_props = subst_ctx cl.cl_props}, u'
+let typeclass_univ_instance (cl, u) =
+ assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
+ let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
+ { cl with cl_context = on_snd subst_ctx cl.cl_context;
+ cl_props = subst_ctx cl.cl_props}
let class_info c =
try Refmap.find c !classes
@@ -185,13 +176,28 @@ let subst_class (subst,cl) =
do_subst_ctx ctx in
let do_subst_projs projs = List.smartmap (fun (x, y, z) ->
(x, y, Option.smartmap do_subst_con z)) projs in
- { cl_impl = do_subst_gr cl.cl_impl;
+ { cl_univs = cl.cl_univs;
+ cl_impl = do_subst_gr cl.cl_impl;
cl_context = do_subst_context cl.cl_context;
cl_props = do_subst_ctx cl.cl_props;
cl_projs = do_subst_projs cl.cl_projs;
cl_strict = cl.cl_strict;
cl_unique = cl.cl_unique }
+(** FIXME: share this with Cooking somewhere in a nicely packed API *)
+let lift_abstract_context subst abs_ctx auctx =
+ let open Univ in
+ let len = LMap.cardinal subst in
+ let rec gen_subst i acc =
+ if i < 0 then acc
+ else
+ let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
+ gen_subst (pred i) acc
+ in
+ let subst = gen_subst (AUContext.size auctx - 1) subst in
+ let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
+ subst, AUContext.union abs_ctx auctx
+
let discharge_class (_,cl) =
let repl = Lib.replacement_context () in
let rel_of_variable_context ctx = List.fold_right
@@ -199,15 +205,14 @@ let discharge_class (_,cl) =
let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
(decl' :: ctx', NamedDecl.get_id decl :: subst)
) ctx ([], []) in
- let discharge_rel_context subst n rel =
+ let discharge_rel_context (subst, usubst) n rel =
let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
- let ctx, _ =
- List.fold_right
- (fun decl (ctx, k) ->
- RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
- )
- rel ([], n)
- in ctx
+ let fold decl (ctx, k) =
+ let map c = subst_univs_level_constr usubst (substn_vars k subst c) in
+ RelDecl.map_constr map decl :: ctx, succ k
+ in
+ let ctx, _ = List.fold_right fold rel ([], n) in
+ ctx
in
let abs_context cl =
match cl.cl_impl with
@@ -229,10 +234,12 @@ let discharge_class (_,cl) =
if cl_impl' == cl.cl_impl then cl else
let ctx, usubst, uctx = abs_context cl in
let ctx, subst = rel_of_variable_context ctx in
- let context = discharge_context ctx subst cl.cl_context in
- let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
+ let usubst, cl_univs' = lift_abstract_context usubst uctx cl.cl_univs in
+ let context = discharge_context ctx (subst, usubst) cl.cl_context in
+ let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
- { cl_impl = cl_impl';
+ { cl_univs = cl_univs';
+ cl_impl = cl_impl';
cl_context = context;
cl_props = props;
cl_projs = List.smartmap discharge_proj cl.cl_projs;
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8e90ca17d..99cdbd3a36 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,10 @@ type direction = Forward | Backward
(** This module defines type-classes *)
type typeclass = {
+ (** The toplevel universe quantification in which the typeclass lives. In
+ particular, [cl_props] and [cl_context] are quantified over it. *)
+ cl_univs : Univ.AUContext.t;
+
(** The class implementation: a record parameterized by the context with defs in it or a definition if
the class is a singleton. This acts as the class' global identifier. *)
cl_impl : global_reference;
@@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list
(** Get the instantiated typeclass structure for a given universe instance. *)
-val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
+val typeclass_univ_instance : typeclass puniverses -> typeclass
(** Just return None if not a class *)
val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a528b96407..d6d4b164b3 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -164,7 +164,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let ctx'' = ctx' @ ctx in
let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
let u = EConstr.EInstance.kind !evars u in
- let cl, u = Typeclasses.typeclass_univ_instance (k, u) in
+ let cl = Typeclasses.typeclass_univ_instance (k, u) in
let _, args =
List.fold_right (fun decl (args, args') ->
match decl with
diff --git a/vernac/record.ml b/vernac/record.ml
index b179616487..63ca227862 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -517,8 +517,18 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
| None -> None)
params, params
in
+ let univs, ctx_context, fields =
+ if poly then
+ let usubst, auctx = Univ.abstract_universes ctx in
+ let map c = Vars.subst_univs_level_constr usubst c in
+ let fields = Context.Rel.map map fields in
+ let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
+ auctx, ctx_context, fields
+ else Univ.AUContext.empty, ctx_context, fields
+ in
let k =
- { cl_impl = impl;
+ { cl_univs = univs;
+ cl_impl = impl;
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique;
cl_context = ctx_context;
@@ -529,10 +539,11 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
let add_constant_class cst =
- let ty = Universes.unsafe_type_of_global (ConstRef cst) in
+ let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in
let ctx, arity = decompose_prod_assum ty in
let tc =
- { cl_impl = ConstRef cst;
+ { cl_univs = univs;
+ cl_impl = ConstRef cst;
cl_context = (List.map (const None) ctx, ctx);
cl_props = [LocalAssum (Anonymous, arity)];
cl_projs = [];
@@ -546,12 +557,13 @@ let add_inductive_class ind =
let mind, oneind = Global.lookup_inductive ind in
let k =
let ctx = oneind.mind_arity_ctxt in
- let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in
- let ty = Inductive.type_of_inductive
- (push_rel_context ctx (Global.env ()))
- ((mind,oneind),inst)
- in
- { cl_impl = IndRef ind;
+ let univs = Declareops.inductive_polymorphic_context mind in
+ let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in
+ let env = push_rel_context ctx env in
+ let inst = Univ.make_abstract_instance univs in
+ let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+ { cl_univs = univs;
+ cl_impl = IndRef ind;
cl_context = List.map (const None) ctx, ctx;
cl_props = [LocalAssum (Anonymous, ty)];
cl_projs = [];
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 12:52:06 +0000