aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml4
-rw-r--r--printing/ppvernac.ml22
-rw-r--r--printing/prettyp.ml12
-rw-r--r--printing/printer.ml16
-rw-r--r--printing/printer.mli2
-rw-r--r--printing/printmod.ml47
6 files changed, 66 insertions, 37 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 781af4789..d0536a174 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -561,17 +561,13 @@ open Decl_kinds
| GoalUid n -> spc () ++ str n in
let pr_showable = function
| ShowGoal n -> keyword "Show" ++ pr_goal_reference n
- | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
| ShowProof -> keyword "Show Proof"
- | ShowNode -> keyword "Show Node"
| ShowScript -> keyword "Show Script"
| ShowExistentials -> keyword "Show Existentials"
| ShowUniverses -> keyword "Show Universes"
- | ShowTree -> keyword "Show Tree"
| ShowProofNames -> keyword "Show Conjectures"
| ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
| ShowMatch id -> keyword "Show Match " ++ pr_reference id
- | ShowThesis -> keyword "Show Thesis"
in
return (pr_showable s)
| VernacCheckGuard ->
@@ -702,7 +698,7 @@ open Decl_kinds
| Some cc -> str" :=" ++ spc() ++ cc))
)
- | VernacStartTheoremProof (ki,l,_) ->
+ | VernacStartTheoremProof (ki,l) ->
return (
hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
@@ -731,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":") ++
@@ -758,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 3c31dd96b..3b0b6d5d2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -17,7 +17,6 @@ open Nametab
open Evd
open Proof_type
open Refiner
-open Pfedit
open Constrextern
open Ppconstr
open Declarations
@@ -262,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 *)
@@ -812,7 +819,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
end
let pr_nth_open_subgoal n =
- let pf = get_pftreestate () in
+ let pf = Proof_global.give_me_the_proof () in
let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
pr_subgoal n sigma gls
@@ -992,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-07 12:31:27 +0000