aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml4
-rw-r--r--printing/ppvernac.ml16
-rw-r--r--printing/prettyp.ml12
-rw-r--r--printing/printer.ml13
-rw-r--r--printing/printer.mli2
-rw-r--r--printing/printmod.ml47
6 files changed, 64 insertions, 30 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 626464b96..49eedb767 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -80,7 +80,7 @@ let tag_var = tag Tag.variable
| Any -> true
let prec_of_prim_token = function
- | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+ | Numeral (_,b) -> if b then lposint else lnegint
| String _ -> latom
open Notation
@@ -231,7 +231,7 @@ let tag_var = tag Tag.variable
| ArgVar (loc,s) -> pr_lident (loc,s)
let pr_prim_token = function
- | Numeral n -> str (Bigint.to_string n)
+ | Numeral (n,s) -> str (if s then n else "-"^n)
| String s -> qs s
let pr_evar pr id l =
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9d28bc4f8..4a5cfe630 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -727,7 +727,7 @@ open Decl_kinds
let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
return (hov 2 (pr_assumption_token (n > 1) stre ++
pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
- | VernacInductive (p,f,l) ->
+ | VernacInductive (cum, p,f,l) ->
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
@@ -754,13 +754,19 @@ open Decl_kinds
in
let key =
let (_,_,_,k,_),_ = List.hd l in
- match k with Record -> "Record" | Structure -> "Structure"
- | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
- | Class _ -> "Class" | Variant -> "Variant"
+ let kind =
+ match k with Record -> "Record" | Structure -> "Structure"
+ | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+ | Class _ -> "Class" | Variant -> "Variant"
+ in
+ if p then
+ let cm = if cum then "Cumulative" else "NonCumulative" in
+ cm ^ " " ^ kind
+ else kind
in
return (
hov 1 (pr_oneind key (List.hd l)) ++
- (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
)
| VernacFixpoint (local, recs) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b21b3f9e..6d2bf6b73 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -502,8 +502,8 @@ let ungeneralized_type_of_constant_type t =
Typeops.type_of_constant_type (Global.env ()) t
let print_instance sigma cb =
- if cb.const_polymorphic then
- pr_universe_instance sigma cb.const_universes
+ if Declareops.constant_is_polymorphic cb then
+ pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
else mt()
let print_constant with_values sep sp =
@@ -511,16 +511,14 @@ let print_constant with_values sep sp =
let val_0 = Global.body_of_constant_body cb in
let typ = Declareops.type_of_constant cb in
let typ = ungeneralized_type_of_constant_type typ in
- let univs = Univ.instantiate_univ_context
- (Global.universes_of_constant_body cb)
- in
+ let univs = Global.universes_of_constant_body cb in
let ctx =
Evd.evar_universe_context_of_binders
(Universes.universe_binders_of_global (ConstRef sp))
in
let env = Global.env () and sigma = Evd.from_ctx ctx in
let pr_ltype = pr_ltype_env env sigma in
- hov 0 (pr_polymorphic cb.const_polymorphic ++
+ hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++
match val_0 with
| None ->
str"*** [ " ++
@@ -587,8 +585,6 @@ let gallina_print_library_entry with_values ent =
Some (str " >>>>>>> Module " ++ pr_name oname)
| (oname,Lib.ClosedModule _) ->
Some (str " >>>>>>> Closed Module " ++ pr_name oname)
- | (_,Lib.FrozenState _) ->
- None
let gallina_print_context with_values =
let rec prec n = function
diff --git a/printing/printer.ml b/printing/printer.ml
index d6f0778f7..3b0b6d5d2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,6 +261,14 @@ let pr_universe_ctx sigma c =
else
mt()
+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 (fun uii -> v 0
+ (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+ else
+ mt()
+
(**********************************************************************)
(* Global references *)
@@ -991,6 +999,11 @@ let pr_assumptionset env s =
let xor a b =
(a && not b) || (not a && b)
+let pr_cumulative poly cum =
+ if poly then
+ if cum then str "Cumulative " else str "NonCumulative "
+ else mt ()
+
let pr_polymorphic b =
let print = xor (Flags.is_universe_polymorphism ()) b in
if print then
diff --git a/printing/printer.mli b/printing/printer.mli
index 3fce06561..f0a32bbbd 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -95,8 +95,10 @@ val pr_sort : evar_map -> sorts -> std_ppcmds
(** Universe constraints *)
val pr_polymorphic : bool -> std_ppcmds
+val pr_cumulative : bool -> bool -> std_ppcmds
val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds
val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> std_ppcmds
(** Printing global references using names as short as possible *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c4affd4ac..08d177f53 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -88,8 +88,8 @@ let build_ind_type env mip =
Inductive.type_of_inductive env mip
let print_one_inductive env sigma mib ((_,i) as ind) =
- let u = if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ let u = if Declareops.inductive_is_polymorphic mib then
+ Declareops.inductive_polymorphic_instance mib
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
@@ -99,8 +99,8 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
let envpar = push_rel_context params env in
let inst =
- if mib.mind_polymorphic then
- Printer.pr_universe_instance sigma mib.mind_universes
+ if Declareops.inductive_is_polymorphic mib then
+ Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
else mt ()
in
hov 0 (
@@ -120,11 +120,18 @@ let print_mutual_inductive env mind mib =
in
let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
- hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
- def keyword ++ spc () ++
- prlist_with_sep (fun () -> fnl () ++ str" with ")
- (print_one_inductive env sigma mib) inds ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+ hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
+ Printer.pr_cumulative
+ (Declareops.inductive_is_polymorphic mib)
+ (Declareops.inductive_is_cumulative mib) ++
+ 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_cumulativity_info
+ sigma (Univ.instantiate_cumulativity_info cumi))
let get_fields =
let rec prodec_rec l subst c =
@@ -141,8 +148,8 @@ let get_fields =
let print_record env mind mib =
let u =
- if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ if Declareops.inductive_is_polymorphic mib then
+ Declareops.inductive_polymorphic_instance mib
else Univ.Instance.empty
in
let mip = mib.mind_packets.(0) in
@@ -164,7 +171,10 @@ let print_record env mind mib =
in
hov 0 (
hov 0 (
- Printer.pr_polymorphic mib.mind_polymorphic ++
+ Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
+ Printer.pr_cumulative
+ (Declareops.inductive_is_polymorphic mib)
+ (Declareops.inductive_is_cumulative mib) ++
def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
print_params env sigma params ++
str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
@@ -175,7 +185,12 @@ let print_record env mind mib =
(fun (id,b,c) ->
pr_id id ++ str (if b then " : " else " := ") ++
Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+ match mib.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+ | Cumulative_ind cumi ->
+ Printer.pr_cumulativity_info
+ sigma (Univ.instantiate_cumulativity_info cumi)
+ )
let pr_mutual_inductive_body env mind mib =
if mib.mind_record <> None && not !Flags.raw_print then
@@ -278,7 +293,8 @@ let print_body is_impl env mp (l,body) =
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
| SFBconst cb ->
let u =
- if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+ if Declareops.constant_is_polymorphic cb then
+ Declareops.constant_polymorphic_instance cb
else Univ.Instance.empty
in
let sigma = Evd.empty in
@@ -300,7 +316,8 @@ let print_body is_impl env mp (l,body) =
Printer.pr_lconstr_env env sigma
(Vars.subst_instance_constr u (Mod_subst.force_constr l)))
| _ -> mt ()) ++ str "." ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
+ Printer.pr_universe_ctx sigma
+ (Declareops.constant_polymorphic_context cb))
| SFBmind mib ->
try
let env = Option.get env in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 16:38:24 +0000