diff options
69 files changed, 356 insertions, 598 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index d2d1efcb2c..4329b2d743 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -28,11 +28,8 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = | PrimRecord data -> Some (Some (Array.map pi1 data)) in let mind_entry_universes = match mb.mind_universes with - | Monomorphic_ind univs -> Monomorphic_ind_entry univs - | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx) - | Cumulative_ind auctx -> - Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx), - ACumulativityInfo.repr auctx) + | Monomorphic univs -> Monomorphic_entry univs + | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> let mind_entry_arity, mind_entry_template = match ind.mind_arity with @@ -64,6 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; + mind_entry_variance = mb.mind_variance; mind_entry_private = mb.mind_private; } @@ -135,7 +133,8 @@ let check_same_record r1 r2 = match r1, r2 with let check_inductive env mind mb = let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; - mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes; + mind_nparams; mind_nparams_rec; mind_params_ctxt; + mind_universes; mind_variance; mind_private; mind_typing_flags; } = (* Locally set the oracle for further typechecking *) @@ -157,6 +156,7 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) + ignore mind_variance; (* Indtypes did the necessary checking *) ignore mind_private; (* passed through Indtypes *) ignore mind_typing_flags; diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index c33c6d5d09..b86d491d72 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -16,8 +16,8 @@ let check_constant_declaration env kn cb = (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with - | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env - | Polymorphic_const auctx -> + | Monomorphic ctx -> false, push_context_set ~strict:true ctx env + | Polymorphic auctx -> let ctx = Univ.AUContext.repr auctx in let env = push_context ~strict:false ctx env in true, env diff --git a/checker/values.ml b/checker/values.ml index 7ca2dc8050..66467fa8f5 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -112,7 +112,6 @@ let v_variance = v_enum "variance" 3 let v_instance = Annot ("instance", Array v_level) let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|] -let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) @@ -226,14 +225,14 @@ let v_cst_def = let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] -let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] +let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; v_constr; Any; - v_const_univs; + v_univs; Opt v_context_set; v_bool; v_typing_flags|] @@ -276,10 +275,6 @@ let v_record_info = v_sum "record_info" 2 [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |] -let v_ind_pack_univs = - v_sum "abstract_inductive_universes" 0 - [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] - let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; v_record_info; @@ -289,7 +284,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; Int; v_rctxt; - v_ind_pack_univs; (* universes *) + v_univs; (* universes *) + Opt (Array v_variance); Opt v_bool; v_typing_flags|] diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh new file mode 100644 index 0000000000..cca85a2f68 --- /dev/null +++ b/dev/ci/user-overlays/09439-sep-variance.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then + elpi_CI_REF=sep-variance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sep-variance + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=sep-variance + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sep-variance + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/include b/dev/include index b982f4c9fa..c5de83b900 100644 --- a/dev/include +++ b/dev/include @@ -41,8 +41,6 @@ #install_printer (* univ context *) ppuniverse_context;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* cumulativity info *) ppcumulativity_info;; -#install_printer (* abstract cumulativity info *) ppabstract_cumulativity_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2629cf8626..a3d2f33216 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -222,8 +222,6 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) -let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = let env = Global.env () in diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 4d874cdd12..cb32d2294c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit val ppconstraints : Univ.Constraint.t -> unit val ppuniverseconstraints : UnivProblem.Set.t -> unit val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit -val ppcumulativity_info : Univ.CumulativityInfo.t -> unit -val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit val ppuniverses : UGraph.t -> unit val ppnamedcontextval : Environ.named_context_val -> unit diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 8493119ee5..8756ebfdf2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some variances -> let num_param_arity = Reduction.inductive_cumulativity_arguments spec in - let variances = Univ.ACumulativityInfo.variance cumi in compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some _ -> let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in if not (Int.equal num_cnstr_args nargs) then enforce_eq_instances_univs false u1 u2 cstrs diff --git a/engine/evd.ml b/engine/evd.ml index eee2cb700c..f0433d3387 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes let to_universe_context evd = UState.context evd.universes -let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes -let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes +let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes + +let const_univ_entry = univ_entry let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl diff --git a/engine/evd.mli b/engine/evd.mli index de73144895..d2d18ca486 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -597,12 +597,12 @@ val universes : evar_map -> UGraph.t [Univ.ContextSet.to_context]. *) val to_universe_context : evar_map -> Univ.UContext.t -val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry +val univ_entry : poly:bool -> evar_map -> Entries.universes_entry -(** NB: [ind_univ_entry] cannot create cumulative entries. *) -val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes +val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry +[@@ocaml.deprecated "Use [univ_entry]."] -val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry +val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 430a3a2fd9..77d1896683 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -100,24 +100,16 @@ let constraints ctx = snd ctx.uctx_local let context ctx = ContextSet.to_context ctx.uctx_local -let const_univ_entry ~poly uctx = +let univ_entry ~poly uctx = let open Entries in if poly then let (binders, _) = uctx.uctx_names in let uctx = context uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Polymorphic_const_entry (nas, uctx) - else Monomorphic_const_entry (context_set uctx) + Polymorphic_entry (nas, uctx) + else Monomorphic_entry (context_set uctx) -(* does not support cumulativity since you need more info *) -let ind_univ_entry ~poly uctx = - let open Entries in - if poly then - let (binders, _) = uctx.uctx_names in - let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Polymorphic_ind_entry (nas, uctx) - else Monomorphic_ind_entry (context_set uctx) +let const_univ_entry = univ_entry let of_context_set ctx = { empty with uctx_local = ctx } @@ -422,10 +414,10 @@ let check_univ_decl ~poly uctx decl = let (binders, _) = uctx.uctx_names in let uctx = universe_context ~names ~extensible uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Entries.Polymorphic_const_entry (nas, uctx) + Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in - Entries.Monomorphic_const_entry uctx.uctx_local + Entries.Monomorphic_entry uctx.uctx_local in if not decl.univdecl_extensible_constraints then check_implication uctx @@ -458,8 +450,8 @@ let restrict ctx vars = let demote_seff_univs entry uctx = let open Entries in match entry.const_entry_universes with - | Polymorphic_const_entry _ -> uctx - | Monomorphic_const_entry (univs, _) -> + | Polymorphic_entry _ -> uctx + | Monomorphic_entry (univs, _) -> let seff = LSet.union uctx.uctx_seff_univs univs in { uctx with uctx_seff_univs = seff } diff --git a/engine/uState.mli b/engine/uState.mli index 5170184ef4..a358813825 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -64,12 +64,11 @@ val constraints : t -> Univ.Constraint.t val context : t -> Univ.UContext.t (** Shorthand for {!context_set} with {!Context_set.to_context}. *) -val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry +val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) -val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes -(** Pick from {!context} or {!context_set} based on [poly]. - Cannot create cumulative entries. *) +val const_univ_entry : poly:bool -> t -> Entries.universes_entry +[@@ocaml.deprecated "Use [univ_entry]."] (** {5 Constraints handling} *) @@ -177,7 +176,7 @@ val default_univ_decl : universe_decl When polymorphic, the universes corresponding to [decl.univdecl_instance] come first in the order defined by that list. *) -val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry +val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t diff --git a/interp/declare.ml b/interp/declare.ml index ea6ed8321d..175f9c66df 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -143,7 +143,7 @@ let declare_constant_common id cst = update_tables c; c -let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty +let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); @@ -156,8 +156,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let is_poly de = match de.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true + | Monomorphic_entry _ -> false + | Polymorphic_entry _ -> true in let in_section = Lib.sections_are_opened () in let export, decl = (* We deal with side effects *) @@ -217,8 +217,8 @@ let cache_variable ((sp,_),o) = section-local definition, but it's not enforced by typing *) let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with - | Monomorphic_const_entry uctx -> false, uctx - | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx + | Monomorphic_entry uctx -> false, uctx + | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (* We must declare the universe constraints before type-checking the @@ -328,21 +328,15 @@ let dummy_inductive_entry m = { mind_entry_record = None; mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; + mind_entry_universes = default_univ_entry; + mind_entry_variance = None; mind_entry_private = None; } (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping mind_ent = - match mind_ent.mind_entry_universes with - | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - mind_ent - | Cumulative_ind_entry (_, cumi) -> - begin - let env = Global.env () in - (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - InferCumulativity.infer_inductive env mind_ent - end +let rebuild_inductive mind_ent = + let env = Global.env () in + InferCumulativity.infer_inductive env mind_ent let inInductive : mutual_inductive_entry -> obj = declare_object {(default_object "INDUCTIVE") with @@ -352,25 +346,19 @@ let inInductive : mutual_inductive_entry -> obj = classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; discharge_function = discharge_inductive; - rebuild_function = infer_inductive_subtyping } + rebuild_function = rebuild_inductive } let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in - let univs = match univs with - | Monomorphic_ind_entry _ -> + let univs, u = match univs with + | Monomorphic_entry _ -> (* Global constraints already defined through the inductive *) - Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry (nas, ctx) -> - Polymorphic_const_entry (nas, ctx) - | Cumulative_ind_entry (nas, ctx) -> - Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx) - in - let term, types = match univs with - | Monomorphic_const_entry _ -> term, types - | Polymorphic_const_entry (_, ctx) -> - let u = Univ.UContext.instance ctx in - Vars.subst_instance_constr u term, Vars.subst_instance_constr u types + default_univ_entry, Univ.Instance.empty + | Polymorphic_entry (nas, ctx) -> + Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx in + let term = Vars.subst_instance_constr u term in + let types = Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in diff --git a/interp/declare.mli b/interp/declare.mli index 669657af6f..6f53d6872b 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -43,7 +43,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.constant_universes_entry -> + ?univs:Entries.universes_entry -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -58,7 +58,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> Id.t -> ?types:constr -> - constr Entries.in_constant_universes_entry -> Constant.t + constr Entries.in_universes_entry -> Constant.t (** Since transparent constants' side effects are globally declared, we * need that *) diff --git a/interp/discharge.ml b/interp/discharge.ml index eeda5a6867..353b0f6057 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -76,18 +76,16 @@ let process_inductive info modlist mib = let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with - | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx - | Polymorphic_ind auctx -> + | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx + | Polymorphic auctx -> let subst, auctx = Lib.discharge_abstract_universe_context info auctx in let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_ind_entry (nas, auctx) - | Cumulative_ind cumi -> - let auctx = Univ.ACumulativityInfo.univ_context cumi in - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx) + subst, Polymorphic_entry (nas, auctx) + in + let variance = match mib.mind_variance with + | None -> None + | Some _ -> Some (InferCumulativity.dummy_variance ind_univs) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = @@ -114,6 +112,7 @@ let process_inductive info modlist mib = mind_entry_params = params'; mind_entry_inds = inds'; mind_entry_private = mib.mind_private; + mind_entry_variance = variance; mind_entry_universes = ind_univs } diff --git a/interp/modintern.ml b/interp/modintern.ml index 60056dfd90..2f516f4f3c 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -107,12 +107,12 @@ let transl_with_decl env base kind = function let c, ectx = interp_constr env sigma c in let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with - | Entries.Polymorphic_const_entry (nas, ctx) -> + | Entries.Polymorphic_entry (nas, ctx) -> let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty - | Entries.Monomorphic_const_entry ctx -> + | Entries.Monomorphic_entry ctx -> let c = EConstr.to_constr sigma c in WithDef (fqid,(c, None)), ctx end diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b95a940c14..718584b3d4 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -881,11 +881,7 @@ let compile_constant_body ~fail_on_error env univs = function | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in - let instance_size = - match univs with - | Monomorphic_const _ -> 0 - | Polymorphic_const univ -> Univ.AUContext.size univ - in + let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in match kind body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index b1b55aef48..6a9550342c 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -20,7 +20,7 @@ val compile : fail_on_error:bool -> (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> - env -> constant_universes -> Constr.t Mod_subst.substituted constant_def -> + env -> universes -> Constr.t Mod_subst.substituted constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 88586352f6..22de9bfad5 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -157,7 +157,7 @@ type inline = bool type result = { cook_body : constr Mod_subst.substituted constant_def; cook_type : types; - cook_universes : constant_universes; + cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; @@ -185,10 +185,10 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let lift_univs cb subst auctx0 = match cb.const_universes with - | Monomorphic_const ctx -> + | Monomorphic ctx -> assert (AUContext.is_empty auctx0); - subst, (Monomorphic_const ctx) - | Polymorphic_const auctx -> + subst, (Monomorphic ctx) + | Polymorphic auctx -> (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, and another abstract context relative to the former context @@ -202,13 +202,13 @@ let lift_univs cb subst auctx0 = *) if (Univ.Instance.is_empty subst) then (** Still need to take the union for the constraints between globals *) - subst, (Polymorphic_const (AUContext.union auctx0 auctx)) + subst, (Polymorphic (AUContext.union auctx0 auctx)) else let ainst = Univ.make_abstract_instance auctx in let subst = Instance.append subst ainst in let substf = Univ.make_instance_subst subst in let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in - subst, (Polymorphic_const (AUContext.union auctx0 auctx')) + subst, (Polymorphic (AUContext.union auctx0 auctx')) let cook_constant ~hcons { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 07c6f37fab..89b5c60ad5 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -20,7 +20,7 @@ type inline = bool type result = { cook_body : constr Mod_subst.substituted constant_def; cook_type : types; - cook_universes : constant_universes; + cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; cook_inline : inline; cook_context : Constr.named_context option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1008492825..6777e0c223 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -53,9 +53,9 @@ type 'a constant_def = | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) -type constant_universes = - | Monomorphic_const of Univ.ContextSet.t - | Polymorphic_const of Univ.AUContext.t +type universes = + | Monomorphic of Univ.ContextSet.t + | Polymorphic of Univ.AUContext.t (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -92,7 +92,7 @@ type constant_body = { const_body : Constr.t Mod_subst.substituted constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; - const_universes : constant_universes; + const_universes : universes; const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which @@ -185,11 +185,6 @@ type one_inductive_body = { mind_reloc_tbl : Vmvalues.reloc_table; } -type abstract_inductive_universes = - | Monomorphic_ind of Univ.ContextSet.t - | Polymorphic_ind of Univ.AUContext.t - | Cumulative_ind of Univ.ACumulativityInfo.t - type recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) @@ -213,7 +208,9 @@ type mutual_inductive_body = { mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) - mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 5686c4071d..9e0230c3ba 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,12 +49,24 @@ let hcons_template_arity ar = (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } +let universes_context = function + | Monomorphic _ -> Univ.AUContext.empty + | Polymorphic ctx -> ctx + +let abstract_universes = function + | Entries.Monomorphic_entry ctx -> + Univ.empty_level_subst, Monomorphic ctx + | Entries.Polymorphic_entry (nas, ctx) -> + let (inst, auctx) = Univ.abstract_universes nas ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic auctx) + (** {6 Constants } *) let constant_is_polymorphic cb = match cb.const_universes with - | Monomorphic_const _ -> false - | Polymorphic_const _ -> true + | Monomorphic _ -> false + | Polymorphic _ -> true let constant_has_body cb = match cb.const_body with @@ -62,9 +74,7 @@ let constant_has_body cb = match cb.const_body with | Def _ | OpaqueDef _ -> true let constant_polymorphic_context cb = - match cb.const_universes with - | Monomorphic_const _ -> Univ.AUContext.empty - | Polymorphic_const ctx -> ctx + universes_context cb.const_universes let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true @@ -126,12 +136,12 @@ let hcons_const_def = function Def (from_val (Constr.hcons constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) -let hcons_const_universes cbu = +let hcons_universes cbu = match cbu with - | Monomorphic_const ctx -> - Monomorphic_const (Univ.hcons_universe_context_set ctx) - | Polymorphic_const ctx -> - Polymorphic_const (Univ.hcons_abstract_universe_context ctx) + | Monomorphic ctx -> + Monomorphic (Univ.hcons_universe_context_set ctx) + | Polymorphic ctx -> + Polymorphic (Univ.hcons_abstract_universe_context ctx) let hcons_const_private_univs = function | None -> None @@ -141,7 +151,7 @@ let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; - const_universes = hcons_const_universes cb.const_universes; + const_universes = hcons_universes cb.const_universes; const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; } @@ -239,27 +249,21 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; + mind_variance = mib.mind_variance; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } let inductive_polymorphic_context mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.AUContext.empty - | Polymorphic_ind ctx -> ctx - | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi + universes_context mib.mind_universes let inductive_is_polymorphic mib = match mib.mind_universes with - | Monomorphic_ind _ -> false - | Polymorphic_ind _ctx -> true - | Cumulative_ind _cumi -> true + | Monomorphic _ -> false + | Polymorphic _ctx -> true let inductive_is_cumulative mib = - match mib.mind_universes with - | Monomorphic_ind _ -> false - | Polymorphic_ind _ctx -> false - | Cumulative_ind _cumi -> true + Option.has_some mib.mind_variance let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with @@ -306,17 +310,11 @@ let hcons_mind_packet oib = mind_user_lc = user; mind_nf_lc = nf } -let hcons_mind_universes miu = - match miu with - | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx) - | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) - | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) - let hcons_mind mib = { mib with mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; - mind_universes = hcons_mind_universes mib.mind_universes } + mind_universes = hcons_universes mib.mind_universes } (** Hashconsing of modules *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 35490ceef9..23a44433b3 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -15,6 +15,10 @@ open Univ (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +val universes_context : universes -> AUContext.t + +val abstract_universes : Entries.universes_entry -> Univ.universe_level_subst * universes + (** {6 Arities} *) val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> diff --git a/kernel/entries.ml b/kernel/entries.ml index 013327599d..a3d32267a7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -16,6 +16,12 @@ open Constr constants/axioms, mutual inductive definitions, modules and module types *) +type universes_entry = + | Monomorphic_entry of Univ.ContextSet.t + | Polymorphic_entry of Name.t array * Univ.UContext.t + +type 'a in_universes_entry = 'a * universes_entry + (** {6 Declaration of inductive types. } *) (** Assume the following definition in concrete syntax: @@ -28,11 +34,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]]. *) -type inductive_universes = - | Monomorphic_ind_entry of Univ.ContextSet.t - | Polymorphic_ind_entry of Name.t array * Univ.UContext.t - | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t - type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; @@ -48,7 +49,8 @@ type mutual_inductive_entry = { mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; - mind_entry_universes : inductive_universes; + mind_entry_universes : universes_entry; + mind_entry_variance : Univ.Variance.t array option; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; @@ -58,12 +60,6 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type constant_universes_entry = - | Monomorphic_const_entry of Univ.ContextSet.t - | Polymorphic_const_entry of Name.t array * Univ.UContext.t - -type 'a in_constant_universes_entry = 'a * constant_universes_entry - type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -71,7 +67,7 @@ type 'a definition_entry = { (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; - const_entry_universes : constant_universes_entry; + const_entry_universes : universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } @@ -85,7 +81,7 @@ type section_def_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_constant_universes_entry * inline + Constr.named_context option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 6976b2019d..a5dafc5ab5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -87,23 +87,28 @@ let check_subtyping_arity_constructor env subst arcn numparams is_arity = let last_env = Context.Rel.fold_outside check_typ typs ~init:env in if not is_arity then basic_check last_env codom else () -let check_cumulativity univs env_ar params data = +let check_cumulativity univs variances env_ar params data = + let uctx = match univs with + | Monomorphic_entry _ -> raise (InductiveError BadUnivs) + | Polymorphic_entry (_,uctx) -> uctx + in + let instance = UContext.instance uctx in + if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs); let numparams = Context.Rel.nhyps params in - let uctx = CumulativityInfo.univ_context univs in - let new_levels = Array.init (UContext.size uctx) + let new_levels = Array.init (Instance.length instance) (fun i -> Level.(make (UGlobal.make DirPath.empty i))) in let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + LMap.empty (Instance.to_array instance) new_levels in let dosubst = Vars.subst_univs_level_constr lmap in let instance_other = Instance.of_array new_levels in - let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in + let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env = Environ.push_context uctx_other env_ar in let subtyp_constraints = - CumulativityInfo.leq_constraints univs - (UContext.instance uctx) instance_other + Univ.enforce_leq_variance_instances variances + instance instance_other Constraint.empty in let env = Environ.add_constraints subtyp_constraints env in @@ -236,8 +241,8 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ} | Some min_univ -> ((match univs with - | Monomorphic_ind _ -> () - | Polymorphic_ind _ | Cumulative_ind _ -> + | Monomorphic _ -> () + | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")); TemplateArity {template_param_levels=param_ccls params; template_level=min_univ}) @@ -246,17 +251,6 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let abstract_inductive_universes = function - | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) - | Polymorphic_ind_entry (nas, ctx) -> - let (inst, auctx) = Univ.abstract_universes nas ctx in - let inst = Univ.make_instance_subst inst in - (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry (nas, cumi) -> - let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in - let inst = Univ.make_instance_subst inst in - (inst, Cumulative_ind acumi) - let typecheck_inductive env (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") @@ -269,9 +263,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = (* universes *) let env_univs = match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry (_, ctx) -> push_context ctx env - | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env + | Monomorphic_entry ctx -> push_context_set ctx env + | Polymorphic_entry (_, ctx) -> push_context ctx env in (* Params *) @@ -287,13 +280,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = mie.mind_entry_inds data in - let () = match mie.mind_entry_universes with - | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data) - | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> () + let () = match mie.mind_entry_variance with + | None -> () + | Some variances -> + check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data) in (* Abstract universes *) - let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in + let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in let data = List.map (abstract_packets univs usubst params) data in @@ -304,4 +298,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, params, Array.of_list data + env_ar_par, univs, mie.mind_entry_variance, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8841e38636..2598548f3f 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -16,6 +16,7 @@ open Declarations Returns: - environment with inductives + parameters in rel context - abstracted universes + - checked variance info - parameters - for each inductive, (arity * constructors) (with params) @@ -24,7 +25,7 @@ open Declarations *) val typecheck_inductive : env -> mutual_inductive_entry -> env - * abstract_inductive_universes + * universes * Univ.Variance.t array option * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 674d7a2a91..8f06e1e4b8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -414,11 +414,7 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections (kn, i as ind) mib = let pkt = mib.mind_packets.(i) in - let u = match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx - | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi) - in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in @@ -471,7 +467,7 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev labs), Array.of_list (List.rev pbs) -let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -529,6 +525,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr mind_params_ctxt = paramsctxt; mind_packets = packets; mind_universes = univs; + mind_variance = variance; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -563,7 +560,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in + let (env_ar_par, univs, variance, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_guarded in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) @@ -574,6 +571,6 @@ let check_inductive env kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env names mie.mind_entry_private univs + build_inductive env names mie.mind_entry_private univs variance paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c62d0e7ded..848ae65c51 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -56,12 +56,7 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - let process auctx = Univ.AUContext.instantiate u auctx in - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Constraint.empty - | Polymorphic_ind auctx -> process auctx - | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) - + Univ.AUContext.instantiate u (Declareops.inductive_polymorphic_context mib) (************************************************************************) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f68dd158c2..421d932d9a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -76,7 +76,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = as long as they have the right type *) let c', univs, ctx' = match cb.const_universes, ctx with - | Monomorphic_const _, None -> + | Monomorphic _, None -> let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in @@ -90,8 +90,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Primitive _ -> error_incorrect_with_constraint lab in - c', Monomorphic_const Univ.ContextSet.empty, cst - | Polymorphic_const uctx, Some ctx -> + c', Monomorphic Univ.ContextSet.empty, cst + | Polymorphic uctx, Some ctx -> let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab @@ -114,7 +114,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - c, Polymorphic_const ctx, Univ.Constraint.empty + c, Polymorphic ctx, Univ.Constraint.empty | _ -> error_incorrect_with_constraint lab in let def = Def (Mod_subst.from_val c') in diff --git a/kernel/modops.ml b/kernel/modops.ml index 1dc8eec0da..4f992d3972 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -50,6 +50,7 @@ type signature_mismatch_error = | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } + | IncompatibleVariance type module_typing_error = | SignatureMismatch of @@ -325,11 +326,7 @@ let strengthen_const mp_from l cb resolver = |_ -> let kn = KerName.make mp_from l in let con = constant_of_delta_kn resolver kn in - let u = - match cb.const_universes with - | Monomorphic_const _ -> Univ.Instance.empty - | Polymorphic_const ctx -> Univ.make_abstract_instance ctx - in + let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); const_private_poly_univs = None; diff --git a/kernel/modops.mli b/kernel/modops.mli index bb97f0171e..119ce2b359 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -111,6 +111,7 @@ type signature_mismatch_error = | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } + | IncompatibleVariance type module_typing_error = | SignatureMismatch of diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c32bdb85d6..df60899b95 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1851,11 +1851,7 @@ and compile_named env sigma univ auxdefs id = Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs let compile_constant env sigma prefix ~interactive con cb = - let no_univs = - match cb.const_universes with - | Monomorphic_const _ -> true - | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0 - in + let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in begin match cb.const_body with | Def t -> let t = Mod_subst.force_constr t in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 61051c001d..b583d33e29 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -244,18 +244,14 @@ let inductive_cumulativity_arguments (mind,ind) = mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - s - | Declarations.Polymorphic_ind _ -> - cmp_instances u1 u2 s - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> cmp_instances u1 u2 s + | Some variances -> let num_param_arity = inductive_cumulativity_arguments (mind,ind) in if not (Int.equal num_param_arity nargs) then cmp_instances u1 u2 s else - cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s + cmp_cumul cv_pb variances u1 u2 s let convert_inductives cv_pb ind nargs u1 u2 (s, check) = convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances @@ -266,13 +262,9 @@ let constructor_cumulativity_arguments (mind, ind, ctor) = mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - s - | Declarations.Polymorphic_ind _ -> - cmp_instances u1 u2 s - | Declarations.Cumulative_ind _cumi -> + match mind.Declarations.mind_variance with + | None -> cmp_instances u1 u2 s + | Some _ -> let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 18a257047d..dc15d9d25e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -312,8 +312,8 @@ let universes_of_private eff = | `Opaque (_, ctx) -> ctx :: acc in match eff.seff_body.const_universes with - | Monomorphic_const ctx -> ctx :: acc - | Polymorphic_const _ -> acc + | Monomorphic ctx -> ctx :: acc + | Polymorphic _ -> acc in List.fold_left fold [] (side_effects_of_private_constants eff) @@ -465,7 +465,7 @@ let labels_of_mib mib = let globalize_constant_universes env cb = match cb.const_universes with - | Monomorphic_const cstrs -> + | Monomorphic cstrs -> Now (false, cstrs) :: (match cb.const_body with | (Undef _ | Def _ | Primitive _) -> [] @@ -476,15 +476,14 @@ let globalize_constant_universes env cb = match Future.peek_val fc with | None -> [Later fc] | Some c -> [Now (false, c)]) - | Polymorphic_const _ -> + | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] let globalize_mind_universes mb = match mb.mind_universes with - | Monomorphic_ind ctx -> + | Monomorphic ctx -> [Now (false, ctx)] - | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] - | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] + | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] let constraints_of_sfb env sfb = match sfb with @@ -612,13 +611,13 @@ let inline_side_effects env body side_eff = | _ -> assert false in match cb.const_universes with - | Monomorphic_const univs -> + | Monomorphic univs -> (** Abstract over the term at the top of the proof *) let ty = cb.const_type in let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _ -> + | Polymorphic _ -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) @@ -700,10 +699,10 @@ let constant_entry_of_side_effect cb u = let open Entries in let univs = match cb.const_universes with - | Monomorphic_const uctx -> - Monomorphic_const_entry uctx - | Polymorphic_const auctx -> - Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) + | Monomorphic uctx -> + Monomorphic_entry uctx + | Polymorphic auctx -> + Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -756,8 +755,8 @@ let export_side_effects mb env c = let { seff_constant = kn; seff_body = cb ; _ } = eff in let env = Environ.add_constant kn cb env in match cb.const_universes with - | Polymorphic_const _ -> env - | Monomorphic_const ctx -> + | Polymorphic _ -> env + | Monomorphic ctx -> let ctx = match eff.seff_env with | `Nothing -> ctx | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2fc3aa99b5..dea72e8b59 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -92,11 +92,25 @@ let check_conv_error error why cst poly f env a1 a2 = with NotConvertible -> error why | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) -let check_polymorphic_instance error env auctx1 auctx2 = - if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then - error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) - else - Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env +let check_universes error env u1 u2 = + match u1, u2 with + | Monomorphic _, Monomorphic _ -> env + | Polymorphic auctx1, Polymorphic auctx2 -> + if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) + else + Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env + | Monomorphic _, Polymorphic _ -> error (PolymorphicStatusExpected true) + | Polymorphic _, Monomorphic _ -> error (PolymorphicStatusExpected false) + +let check_variance error v1 v2 = + match v1, v2 with + | None, None -> () + | Some v1, Some v2 -> + if not (Array.for_all2 Variance.check_subtype v2 v1) then + error IncompatibleVariance + | None, Some _ -> error (CumulativeStatusExpected true) + | Some _, None -> error (CumulativeStatusExpected false) (* for now we do not allow reorderings *) @@ -110,29 +124,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let env, inst = - match mib1.mind_universes, mib2.mind_universes with - | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty - | Polymorphic_ind auctx, Polymorphic_ind auctx' -> - let env = check_polymorphic_instance error env auctx auctx' in - env, Univ.make_abstract_instance auctx' - | Cumulative_ind cumi, Cumulative_ind cumi' -> - (** Currently there is no way to control variance of inductive types, but - just in case we require that they are in a subtyping relation. *) - let () = - let v = ACumulativityInfo.variance cumi in - let v' = ACumulativityInfo.variance cumi' in - if not (Array.for_all2 Variance.check_subtype v' v) then - CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++ - str " is not compatible with the one of " ++ KerName.print kn2) - in - let auctx = Univ.ACumulativityInfo.univ_context cumi in - let auctx' = Univ.ACumulativityInfo.univ_context cumi' in - let env = check_polymorphic_instance error env auctx auctx' in - env, Univ.make_abstract_instance auctx' - | _ -> error - (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2)) - in + let env = check_universes error env mib1.mind_universes mib2.mind_universes in + let () = check_variance error mib1.mind_variance mib2.mind_variance in + let inst = make_abstract_instance (Declareops.inductive_polymorphic_context mib1) in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = check_conv (NotConvertibleInductiveField name) @@ -235,17 +229,8 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let cb1 = Declareops.subst_const_body subst1 cb1 in let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking universes *) - let poly, env = - match cb1.const_universes, cb2.const_universes with - | Monomorphic_const _, Monomorphic_const _ -> - false, env - | Polymorphic_const auctx1, Polymorphic_const auctx2 -> - true, check_polymorphic_instance error env auctx1 auctx2 - | Monomorphic_const _, Polymorphic_const _ -> - error (PolymorphicStatusExpected true) - | Polymorphic_const _, Monomorphic_const _ -> - error (PolymorphicStatusExpected false) - in + let env = check_universes error env cb1.const_universes cb2.const_universes in + let poly = Declareops.constant_is_polymorphic cb1 in (* Now check types *) let typ1 = cb1.const_type in let typ2 = cb2.const_type in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3cb5d17d34..929f1c13a3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -65,23 +65,15 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> Feedback.feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes = function - | Monomorphic_const_entry uctx -> - Univ.empty_level_subst, Monomorphic_const uctx - | Polymorphic_const_entry (nas, uctx) -> - let sbst, auctx = Univ.abstract_universes nas uctx in - let sbst = Univ.make_instance_subst sbst in - sbst, Polymorphic_const auctx - let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with - | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env + | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env + | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env in let j = infer env t in - let usubst, univs = abstract_constant_universes uctx in + let usubst, univs = Declareops.abstract_universes uctx in let c = Typeops.assumption_of_judgment env j in let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in { @@ -115,7 +107,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | CPrimitives.OT_type _ -> Undef None in { Cooking.cook_body = cd; cook_type = ty; - cook_universes = Monomorphic_const uctxt; + cook_universes = Monomorphic uctxt; cook_private_univs = None; cook_inline = false; cook_context = None @@ -134,7 +126,7 @@ the polymorphic case *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_universes = Monomorphic_const_entry univs; _ } as c) -> + const_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in let tyj = infer_type env typ in @@ -165,7 +157,7 @@ the polymorphic case { Cooking.cook_body = def; cook_type = typ; - cook_universes = Monomorphic_const univs; + cook_universes = Monomorphic univs; cook_private_univs = None; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -183,11 +175,11 @@ the polymorphic case body, Univ.ContextSet.union ctx ctx' in let env, usubst, univs, private_univs = match c.const_entry_universes with - | Monomorphic_const_entry univs -> + | Monomorphic_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic_const ctx, None - | Polymorphic_const_entry (nas, uctx) -> + env, Univ.empty_level_subst, Monomorphic ctx, None + | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in @@ -200,7 +192,7 @@ the polymorphic case if Univ.ContextSet.is_empty ctx then env, None else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") in - env, sbst, Polymorphic_const auctx, local + env, sbst, Polymorphic auctx, local in let j = infer env body in let typ = match typ with @@ -342,7 +334,7 @@ let translate_local_def env _id centry = const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; - const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty; + const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; const_entry_opaque = false; const_entry_inline_code = false; } in @@ -360,8 +352,8 @@ let translate_local_def env _id centry = record_aux env ids_typ ids_def end; let () = match decl.cook_universes with - | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx) - | Polymorphic_const _ -> assert false + | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Polymorphic _ -> assert false in let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c diff --git a/kernel/univ.ml b/kernel/univ.ml index 8940c0337e..09bf695915 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -989,68 +989,6 @@ let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} = let hcons_abstract_universe_context = AUContext.hcons -(** Universe info for cumulative inductive types: A context of - universe levels with universe constraints, representing local - universe variables and constraints, together with an array of - Variance.t. - - This data structure maintains the invariant that the variance - array has the same length as the universe instance. *) -module CumulativityInfo = -struct - type t = universe_context * Variance.t array - - let make x = - if (Instance.length (UContext.instance (fst x))) = - (Array.length (snd x)) then x - else anomaly (Pp.str "Invalid subtyping information encountered!") - - let empty = (UContext.empty, [||]) - let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance - - let pr prl (univs, variance) = - UContext.pr prl ~variance univs - - let hcons (univs, variance) = (* should variance be hconsed? *) - (UContext.hcons univs, variance) - - let univ_context (univs, _subtypcst) = univs - let variance (_univs, variance) = variance - - (** This function takes a universe context representing constraints - of an inductive and produces a CumulativityInfo.t with the - trivial subtyping relation. *) - let from_universe_context univs = - (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant)) - - let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts - let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts - -end - -let hcons_cumulativity_info = CumulativityInfo.hcons - -module ACumulativityInfo = -struct - type t = AUContext.t * Variance.t array - - let repr (auctx,var) = AUContext.repr auctx, var - - let pr prl (univs, variance) = - AUContext.pr prl ~variance univs - - let hcons (univs, variance) = (* should variance be hconsed? *) - (AUContext.hcons univs, variance) - - let univ_context (univs, _subtypcst) = univs - let variance (_univs, variance) = variance - - let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts - let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts -end - -let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons - (** A set of universes with universe constraints. We linearize the set to a list after typechecking. Beware, representation could change. @@ -1211,10 +1149,6 @@ let abstract_universes nas ctx = let ctx = (nas, cstrs) in instance, ctx -let abstract_cumulativity_info nas (univs, variance) = - let subst, univs = abstract_universes nas univs in - subst, (univs, variance) - let rec compact_univ s vars i u = match u with | [] -> (s, List.rev vars) @@ -1235,12 +1169,8 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr -let pr_cumulativity_info = CumulativityInfo.pr - let pr_abstract_universe_context = AUContext.pr -let pr_abstract_cumulativity_info = ACumulativityInfo.pr - let pr_universe_context_set = ContextSet.pr let pr_universe_subst = diff --git a/kernel/univ.mli b/kernel/univ.mli index b83251e983..1fbebee350 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -368,45 +368,6 @@ type 'a univ_abstracted = { val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted -(** Universe info for cumulative inductive types: A context of - universe levels with universe constraints, representing local - universe variables and constraints, together with an array of - Variance.t. - - This data structure maintains the invariant that the variance - array has the same length as the universe instance. *) -module CumulativityInfo : -sig - type t - - val make : UContext.t * Variance.t array -> t - - val empty : t - val is_empty : t -> bool - - val univ_context : t -> UContext.t - val variance : t -> Variance.t array - - (** This function takes a universe context representing constraints - of an inductive and produces a CumulativityInfo.t with the - trivial subtyping relation. *) - val from_universe_context : UContext.t -> t - - val leq_constraints : t -> Instance.t constraint_function - val eq_constraints : t -> Instance.t constraint_function -end - -module ACumulativityInfo : -sig - type t - - val repr : t -> CumulativityInfo.t - val univ_context : t -> AUContext.t - val variance : t -> Variance.t array - val leq_constraints : t -> Instance.t constraint_function - val eq_constraints : t -> Instance.t constraint_function -end - (** Universe contexts (as sets) *) (** A set of universes with universe Constraint.t. @@ -487,7 +448,6 @@ val make_instance_subst : Instance.t -> universe_level_subst val make_inverse_instance_subst : Instance.t -> universe_level_subst val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t -val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t (** TODO: move universe abstraction out of the kernel *) val make_abstract_instance : AUContext.t -> Instance.t @@ -505,10 +465,8 @@ val pr_constraint_type : constraint_type -> Pp.t val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t -val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> AUContext.t -> Pp.t -val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t val explain_universe_inconsistency : (Level.t -> Pp.t) -> univ_inconsistency -> Pp.t @@ -524,5 +482,3 @@ val hcons_universe_set : LSet.t -> LSet.t val hcons_universe_context : UContext.t -> UContext.t val hcons_abstract_universe_context : AUContext.t -> AUContext.t val hcons_universe_context_set : ContextSet.t -> ContextSet.t -val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t -val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 12b68e208c..25a7675113 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -364,7 +364,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = Evd.const_univ_entry ~poly:false evd' in + let univs = Evd.univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0c97f9f373..a8517e9ab1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1547,7 +1547,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in + let univs = Evd.univ_entry ~poly:false evd in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2055b25ff4..7da4464e59 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1889,7 +1889,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = @@ -1975,7 +1975,7 @@ let add_morphism_infer atts m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 65201d922f..3f69701bd3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,7 +153,7 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context univs vars in - let univs = Monomorphic_const_entry univs in + let univs = Monomorphic_entry univs in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs c), IsProof Lemma)) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aa30ed8d2e..bb163ddaee 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -468,17 +468,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let u = EInstance.kind evd u and u' = EInstance.kind evd u' in let mind = Environ.lookup_mind mi env in let open Declarations in - begin match mind.mind_universes with - | Monomorphic_ind _ -> assert false - | Polymorphic_ind _ -> check_strict evd u u' - | Cumulative_ind cumi -> + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let needed = Reduction.inductive_cumulativity_arguments (mind,i) in if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) then check_strict evd u u' else - compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u' + compare_cumulative_instances evd variances u u' end | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') @@ -488,10 +487,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let u = EInstance.kind evd u and u' = EInstance.kind evd u' in let mind = Environ.lookup_mind mi env in let open Declarations in - begin match mind.mind_universes with - | Monomorphic_ind _ -> assert false - | Polymorphic_ind _ -> check_strict evd u u' - | Cumulative_ind cumi -> + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ff552c7caf..2c4ca46343 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -453,12 +453,7 @@ let build_branch_type env sigma dep p cs = let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in - let u = match mib.mind_universes with - | Monomorphic_ind _ -> Instance.empty - | Polymorphic_ind auctx -> make_abstract_instance auctx - | Cumulative_ind acumi -> - make_abstract_instance (ACumulativityInfo.univ_context acumi) - in + let u = make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index b5a6ba6be5..bf8a38a353 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -41,33 +41,31 @@ let variance_pb cv_pb var = | CONV, Covariant -> Invariant | CUMUL, Covariant -> Covariant -let infer_cumulative_ind_instance cv_pb cumi variances u = +let infer_cumulative_ind_instance cv_pb mind_variance variances u = Array.fold_left2 (fun variances varu u -> match LMap.find u variances with | exception Not_found -> variances | varu' -> LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) - variances (ACumulativityInfo.variance cumi) (Instance.to_array u) + variances mind_variance (Instance.to_array u) let infer_inductive_instance cv_pb env variances ind nargs u = let mind = Environ.lookup_mind (fst ind) env in - match mind.mind_universes with - | Monomorphic_ind _ -> assert (Instance.is_empty u); variances - | Polymorphic_ind _ -> infer_generic_instance_eq variances u - | Cumulative_ind cumi -> + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some mind_variance -> if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) then infer_generic_instance_eq variances u - else infer_cumulative_ind_instance cv_pb cumi variances u + else infer_cumulative_ind_instance cv_pb mind_variance variances u let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = let mind = Environ.lookup_mind mi env in - match mind.mind_universes with - | Monomorphic_ind _ -> assert (Instance.is_empty u); variances - | Polymorphic_ind _ -> infer_generic_instance_eq variances u - | Cumulative_ind cumi -> + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some _ -> if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) then infer_generic_instance_eq variances u - else infer_cumulative_ind_instance CONV cumi variances u + else variances (* constructors are convertible at common supertype *) let infer_sort cv_pb variances s = match cv_pb with @@ -189,12 +187,14 @@ let infer_inductive env mie = let { mind_entry_params = params; mind_entry_inds = entries; } = mie in - let univs = - match mie.mind_entry_universes with - | Monomorphic_ind_entry _ - | Polymorphic_ind_entry _ as univs -> univs - | Cumulative_ind_entry (nas, cumi) -> - let uctx = CumulativityInfo.univ_context cumi in + let variances = + match mie.mind_entry_variance with + | None -> None + | Some _ -> + let uctx = match mie.mind_entry_universes with + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> uctx + in let uarray = Instance.to_array @@ UContext.instance uctx in let env = Environ.push_context uctx env in let variances = @@ -212,6 +212,10 @@ let infer_inductive env mie = entries in let variances = Array.map (fun u -> LMap.find u variances) uarray in - Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances)) + Some variances in - { mie with mind_entry_universes = univs } + { mie with mind_entry_variance = variances } + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Variance.Irrelevant diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli index a0c8d339ac..6e5bf30f6b 100644 --- a/pretyping/inferCumulativity.mli +++ b/pretyping/inferCumulativity.mli @@ -10,3 +10,5 @@ val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry + +val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e0403a9f97..797b6faa08 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -86,10 +86,7 @@ let print_ref reduce ref udecl = | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> let mind = Environ.lookup_mind ind env in - begin match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None - | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) - end + mind.Declarations.mind_variance in let inst = if Global.is_polymorphic ref @@ -98,7 +95,7 @@ let print_ref reduce ref udecl = in let priv = None in (* We deliberately don't print private univs in About. *) hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv) + Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) (** Printing implicit arguments *) @@ -562,11 +559,11 @@ let print_constant with_values sep sp udecl = | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with - | Monomorphic_const ctx -> - Monomorphic_const (ContextSet.union body_uctxs ctx) - | Polymorphic_const ctx -> + | Monomorphic ctx -> + Monomorphic (ContextSet.union body_uctxs ctx) + | Polymorphic ctx -> assert(ContextSet.is_empty body_uctxs); - Polymorphic_const ctx + Polymorphic ctx in let ctx = UState.of_binders @@ -580,11 +577,11 @@ let print_constant with_values sep sp udecl = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs + Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs | Some (c, ctx) -> print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs) + Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs) let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ diff --git a/printing/printer.ml b/printing/printer.ml index 3f7837fd6e..bc936975c2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -209,7 +209,7 @@ let pr_universe_ctx sigma ?variance c = else mt() -let pr_abstract_universe_ctx sigma ?variance c ~priv = +let pr_abstract_universe_ctx sigma ?variance ?priv c = let open Univ in let priv = Option.default Univ.ContextSet.empty priv in let has_priv = not (ContextSet.is_empty priv) in @@ -221,23 +221,9 @@ let pr_abstract_universe_ctx sigma ?variance c ~priv = else mt() -let pr_constant_universes sigma ~priv = function - | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx - | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv - -let pr_cumulativity_info sigma cumi = - if !Detyping.print_universes - && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi)) - else - mt() - -let pr_abstract_cumulativity_info sigma cumi = - if !Detyping.print_universes - && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then - fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi)) - else - mt() +let pr_universes sigma ?variance ?priv = function + | Declarations.Monomorphic ctx -> pr_universe_ctx_set sigma ctx + | Declarations.Polymorphic ctx -> pr_abstract_universe_ctx sigma ?variance ?priv ctx (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 9a06d555e4..4e27268c4d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -86,11 +86,11 @@ val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Const val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> - Univ.AUContext.t -> priv:Univ.ContextSet.t option -> Pp.t + ?priv:Univ.ContextSet.t -> Univ.AUContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> priv:Univ.ContextSet.t option -> Declarations.constant_universes -> Pp.t -val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t -val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t +val pr_universes : evar_map -> + ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> + Declarations.universes -> Pp.t (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 898f231a8b..3438063f76 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -126,10 +126,7 @@ let print_mutual_inductive env mind mib udecl = hov 0 (def keyword ++ spc () ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env sigma mib) inds ++ - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> str "" - | Cumulative_ind cumi -> - Printer.pr_abstract_cumulativity_info sigma cumi) + Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes) let get_fields = let rec prodec_rec l subst c = @@ -178,10 +175,7 @@ let print_record env mind mib udecl = (fun (id,b,c) -> Id.print id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> str "" - | Cumulative_ind cumi -> - Printer.pr_abstract_cumulativity_info sigma cumi + Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes ) let pr_mutual_inductive_body env mind mib udecl = @@ -302,7 +296,7 @@ let print_body is_impl extent env mp (l,body) = hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_abstract_universe_ctx sigma ctx ~priv:cb.const_private_poly_univs) + Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs) | SFBmind mib -> match extent with | WithContents -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0cfc010c1a..a47fa78f4d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -268,7 +268,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in if allow_deferred then - let initunivs = UState.const_univ_entry ~poly initial_euctx in + let initunivs = UState.univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of @@ -302,7 +302,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now else fun t p -> (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in + let univctx = UState.univ_entry ~poly:false universes in let t = nf t in Future.from_val (univctx, t), Future.chain p (fun (pt,eff) -> diff --git a/tactics/abstract.ml b/tactics/abstract.ml index c3e3a62e26..7a61deba0c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -162,8 +162,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let cst = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with - | Entries.Monomorphic_const_entry _ -> EInstance.empty - | Entries.Polymorphic_const_entry (_, ctx) -> + | Entries.Monomorphic_entry _ -> EInstance.empty + | Entries.Polymorphic_entry (_, ctx) -> (* We mimick what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 571ad9d160..c1f6365f5d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1309,7 +1309,7 @@ let project_hint ~poly pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.const_univ_entry ~poly sigma in + let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index a67f5f6d6e..d1b77f3758 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -121,7 +121,7 @@ let define internal id c poly univs = let id = compute_name internal id in let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in - let univs = UState.const_univ_entry ~poly ctx in + let univs = UState.univ_entry ~poly ctx in let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 48997163de..335f3c74ff 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -237,9 +237,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in - let univs = - Evd.const_univ_entry ~poly sigma - in + let univs = Evd.univ_entry ~poly sigma in let entry = definition_entry ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 047f4cd080..f5043db099 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -9,13 +9,13 @@ let evil t f = let u = Level.var 0 in let tu = mkType (Universe.make u) in let te = Declare.definition_entry - ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu + ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in let tc = Declare.declare_constant t (DefinitionEntry te, k) in let tc = mkConst tc in let fe = Declare.definition_entry - ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) ~types:(Term.mkArrow tc tu) (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) in diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index a960fe3441..222a808768 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,5 +1,7 @@ Inductive Empty@{u} : Type@{u} := +(* u |= *) Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } +(* u |= *) PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -11,6 +13,7 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p Argument scopes are [type_scope _] Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } +(* u |= *) For RWrap: Argument scope is [type_scope] For rwrap: Argument scopes are [type_scope _] @@ -79,7 +82,9 @@ Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) Inductive Empty@{E} : Type@{E} := +(* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +(* E |= *) PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] @@ -109,7 +114,9 @@ bind_univs.poly@{u} = Type@{u} insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) -Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} +Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} +(* k |= *) For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} @@ -117,6 +124,7 @@ insec@{u v} = Type@{u} -> Type@{v} (* u v |= *) Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} +(* u k |= *) For inseccstr: Argument scope is [type_scope] insec2@{u} = Prop diff --git a/vernac/class.ml b/vernac/class.ml index 8374a5c84f..823177d4d1 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -215,7 +215,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~univs diff --git a/vernac/classes.ml b/vernac/classes.ml index ea434dbc4f..27d8b7390d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,7 +374,7 @@ let context poly l = let univs = match ctx with | [] -> assert false - | [_] -> Evd.const_univ_entry ~poly sigma + | [_] -> Evd.univ_entry ~poly sigma | _::_::_ -> if Lib.sections_are_opened () then @@ -384,19 +384,19 @@ let context poly l = begin let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - if poly then Polymorphic_const_entry ([||], Univ.UContext.empty) - else Monomorphic_const_entry Univ.ContextSet.empty + if poly then Polymorphic_entry ([||], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty end else if poly then (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.const_univ_entry ~poly sigma + Evd.univ_entry ~poly sigma else (* Multiple monomorphic axioms: declare universes separately to avoid redeclaring them. *) begin let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - Monomorphic_const_entry Univ.ContextSet.empty + Monomorphic_entry Univ.ContextSet.empty end in let fn status (id, b, t) = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 73d0be04df..466757c6bd 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -46,8 +46,8 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ide match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with - | Monomorphic_const_entry ctx -> ctx - | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx + | Monomorphic_entry ctx -> ctx + | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx in let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in @@ -79,8 +79,8 @@ match local with let () = if do_instance then Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with - | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx - | Monomorphic_const_entry _ -> Univ.Instance.empty + | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx + | Monomorphic_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) @@ -90,10 +90,10 @@ let interp_assumption ~program_mode sigma env impls c = (* When monomorphic the universe constraints are declared with the first declaration only. *) let next_uctx = - let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in + let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in function - | Polymorphic_const_entry _ as uctx -> uctx - | Monomorphic_const_entry _ -> empty_uctx + | Polymorphic_entry _ as uctx -> uctx + | Monomorphic_entry _ -> empty_uctx let declare_assumptions idl is_coe k (c,uctx) pl imps nl = let refs, status, _ = diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 385ec33bea..2b794b001a 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -29,7 +29,7 @@ val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_ob (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> - types in_constant_universes_entry -> + types in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t * bool diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 68ad276113..9bbfb8eec6 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -457,15 +457,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in - let univs = - match uctx with - | Polymorphic_const_entry (nas, uctx) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx) - else Polymorphic_ind_entry (nas, uctx) - | Monomorphic_const_entry uctx -> - Monomorphic_ind_entry uctx - in + let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -473,7 +465,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_private = if prv then Some false else None; - mind_entry_universes = univs; + mind_entry_universes = uctx; + mind_entry_variance = variance; } in (if poly && cum then diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1e3644c371..e455b59ab2 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -19,7 +19,7 @@ val declare_definition : Id.t -> definition_kind -> GlobRef.t val declare_fix : ?opaque:bool -> definition_kind -> - UnivNames.universe_binders -> Entries.constant_universes_entry -> + UnivNames.universe_binders -> Entries.universes_entry -> Id.t -> Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> GlobRef.t diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 367fa4ce98..9dd321be51 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -923,6 +923,8 @@ let explain_not_match_error = function str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else fnl() ++ str "(incompatible constraints)") + | IncompatibleVariance -> + str "incompatible variance information" let explain_signature_mismatch l spec why = str "Signature components for label " ++ Label.print l ++ diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index d29f66f81f..caafd6ac2f 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -103,7 +103,7 @@ let () = let define ~poly id internal sigma c t = let f = declare_constant ~internal in - let univs = Evd.const_univ_entry ~poly sigma in + let univs = Evd.univ_entry ~poly sigma in let kn = f id (DefinitionEntry { const_entry_body = c; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 79182a3f9d..83dd1aa8e4 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -230,10 +230,10 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_, | Discharge -> let impl = false in (* copy values from Vernacentries *) let univs = match univs with - | Polymorphic_const_entry (_, univs) -> + | Polymorphic_entry (_, univs) -> (* What is going on here? *) Univ.ContextSet.of_context univs - | Monomorphic_const_entry univs -> univs + | Monomorphic_entry univs -> univs in let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in @@ -476,7 +476,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in + let ctx = UState.univ_entry ~poly:(pi2 k) universes in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index b20758dac5..ba78c73131 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -557,7 +557,7 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let univs = UState.const_univ_entry ~poly first.prg_ctx in + let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) fixnames fixdecls fixtypes fiximps in @@ -656,9 +656,9 @@ let declare_obligation prg obl body ty uctx = if not opaque then add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; let body = match uctx with - | Polymorphic_const_entry (_, uctx) -> + | Polymorphic_entry (_, uctx) -> Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_const_entry _ -> + | Monomorphic_entry _ -> Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) in true, { obl with obl_body = body } @@ -879,7 +879,7 @@ let obligation_terminator ?univ_hook name num guard auto pf = if pi2 prg.prg_kind then ctx else UState.union prg.prg_ctx ctx in - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let () = obls.(num) <- obl in @@ -1010,7 +1010,7 @@ and solve_obligation_by_tac prg obls i tac = (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with | None -> None | Some (t, ty, ctx) -> - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; @@ -1159,7 +1159,7 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in + let ctx = UState.univ_entry ~poly:false prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in diff --git a/vernac/record.ml b/vernac/record.ml index 6b9a564b9e..0bd15e203b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -277,8 +277,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in let u = match ctx with - | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx - | Monomorphic_const_entry ctx -> Univ.Instance.empty + | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx + | Monomorphic_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let r = mkIndU (indsp,u) in @@ -369,17 +369,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f open Typeclasses -let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = +let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = let nparams = List.length params in let poly, ctx = match univs with - | Monomorphic_ind_entry ctx -> - false, Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry (nas, ctx) -> - true, Polymorphic_const_entry (nas, ctx) - | Cumulative_ind_entry (nas, cumi) -> - true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi) + | Monomorphic_entry ctx -> + false, Monomorphic_entry Univ.ContextSet.empty + | Polymorphic_entry (nas, ctx) -> + true, Polymorphic_entry (nas, ctx) in + let variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -427,6 +426,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; + mind_entry_variance = variance; } in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in @@ -472,8 +472,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity (DefinitionEntry class_entry, IsDefinition Definition) in let inst, univs = match univs with - | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs - | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs + | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty in let cstu = (cst, inst) in let inst_type = appvectc (mkConstU cstu) @@ -496,18 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity in [cref, [Name proj_name, sub, Some proj_cst]] | _ -> - let univs = - match univs with - | Polymorphic_const_entry (nas, univs) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) - else - Polymorphic_ind_entry (nas, univs) - | Monomorphic_const_entry univs -> - Monomorphic_ind_entry univs - in let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in - let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls + let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls params template ~kind:Method ~name:[|binder_name|] record_data in let coers = List.map2 (fun coe pri -> @@ -531,14 +521,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity in let univs, ctx_context, fields = match univs with - | Polymorphic_const_entry (nas, univs) -> + | Polymorphic_entry (nas, univs) -> let usubst, auctx = Univ.abstract_universes nas univs in let usubst = Univ.make_instance_subst usubst 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 - | Monomorphic_const_entry _ -> + | Monomorphic_entry _ -> Univ.AUContext.empty, ctx_context, fields in let map (impl, projs) = @@ -670,21 +660,11 @@ let definition_structure udecl kind ~template cum poly finite records = | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in - let univs = - match univs with - | Polymorphic_const_entry (nas, univs) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) - else - Polymorphic_ind_entry (nas, univs) - | Monomorphic_const_entry univs -> - Monomorphic_ind_entry univs - in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in - let inds = declare_structure finite ubinders univs implpars params template data in + let inds = declare_structure ~cum finite ubinders univs implpars params template data in List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index 04984030f7..9852840d12 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -16,7 +16,7 @@ val primitive_flag : bool ref val declare_projections : inductive -> - Entries.constant_universes_entry -> + Entries.universes_entry -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> bool list -> |