diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 22:49:32 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
commit | 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (patch) | |
tree | 0fd697ed68507449268811a630a201f7637c3553 | |
parent | 9938aed874d3e15e5d21689ea841bdc3e6ebb40e (diff) |
Make the typeclass implementation fully compatible with universe polymorphism.
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
-rw-r--r-- | API/API.mli | 1 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 65 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 6 | ||||
-rw-r--r-- | vernac/classes.ml | 2 | ||||
-rw-r--r-- | vernac/record.ml | 30 |
5 files changed, 64 insertions, 40 deletions
diff --git a/API/API.mli b/API/API.mli index 48fd3a682..0f3394fe9 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 6de5bc28b..5af36fc6b 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 a8e90ca17..99cdbd3a3 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 a528b9640..d6d4b164b 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 b17961648..63ca22786 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 = []; |