From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- printing/prettyp.ml | 14 +++++++------- printing/printer.ml | 4 ++++ printing/printer.mli | 1 + 3 files changed, 12 insertions(+), 7 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8fc00ed96..b4ac94103 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -556,26 +556,26 @@ let print_constant with_values sep sp = Vars.subst_instance_constr inst cb.const_type in let univs = + let open Entries in let otab = Global.opaque_tables () in match cb.const_body with | Undef _ | Def _ -> begin match cb.const_universes with - | Monomorphic_const ctx -> ctx + | Monomorphic_const ctx -> Monomorphic_const_entry ctx | Polymorphic_const ctx -> let inst = Univ.AUContext.instance ctx in - Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)) end | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - let uctxs = Univ.ContextSet.of_context ctx in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + Monomorphic_const_entry (Univ.ContextSet.union body_uctxs ctx) | Polymorphic_const ctx -> assert(Univ.ContextSet.is_empty body_uctxs); let inst = Univ.AUContext.instance ctx in - Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)) in let ctx = Evd.evar_universe_context_of_binders @@ -589,12 +589,12 @@ let print_constant with_values sep sp = str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx sigma univs + Printer.pr_constant_universes sigma univs | Some (c, ctx) -> let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in 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_universe_ctx sigma univs) + Printer.pr_constant_universes sigma univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ diff --git a/printing/printer.ml b/printing/printer.ml index 4d5cfcba3..ae6292024 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -270,6 +270,10 @@ let pr_universe_ctx sigma c = else mt() +let pr_constant_universes sigma = function + | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx + | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx + let pr_cumulativity_info sigma cumi = if !Detyping.print_universes && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then diff --git a/printing/printer.mli b/printing/printer.mli index a3d0eaac2..67128da40 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -122,6 +122,7 @@ val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t +val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -- cgit v1.2.3