aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml23
-rw-r--r--printing/ppvernac.ml14
-rw-r--r--printing/prettyp.ml16
-rw-r--r--printing/printer.ml53
-rw-r--r--printing/printer.mli7
-rw-r--r--printing/printmod.ml3
6 files changed, 82 insertions, 34 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 92b4bf4961..950594397a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -118,6 +118,12 @@ let pr_name = pr_name
let pr_qualid = pr_qualid
let pr_patvar = pr_id
+let pr_universe_instance l =
+ pr_opt (pr_in_comment Univ.Instance.pr) l
+
+let pr_cref ref us =
+ pr_reference ref ++ pr_universe_instance us
+
let pr_expl_args pr (a,expl) =
match expl with
| None -> pr (lapp,L) a
@@ -397,9 +403,10 @@ let pr_simple_return_type pr na po =
let pr_proj pr pr_app a f l =
hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
-let pr_appexpl pr f l =
+let pr_appexpl pr (f,us) l =
hov 2 (
str "@" ++ pr_reference f ++
+ pr_universe_instance us ++
prlist (pr_sep_com spc (pr (lapp,L))) l)
let pr_app pr a l =
@@ -421,7 +428,7 @@ let pr_dangling_with_for sep pr inherited a =
let pr pr sep inherited a =
let (strm,prec) = match a with
- | CRef r -> pr_reference r, latom
+ | CRef (r,us) -> pr_cref r us, latom
| CFix (_,id,fix) ->
hov 0 (str"fix " ++
pr_recursive
@@ -458,19 +465,19 @@ let pr pr sep inherited a =
pr spc ltop a ++ str " in") ++
pr spc ltop b),
lletin
- | CAppExpl (_,(Some i,f),l) ->
+ | CAppExpl (_,(Some i,f,us),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
- let p = pr_proj (pr mt) pr_appexpl c f l1 in
+ let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
if not (List.is_empty l2) then
p ++ prlist (pr spc (lapp,L)) l2, lapp
else
p, lproj
- | CAppExpl (_,(None,Ident (_,var)),[t])
- | CApp (_,(_,CRef(Ident(_,var))),[t,None])
+ | CAppExpl (_,(None,Ident (_,var),us),[t])
+ | CApp (_,(_,CRef(Ident(_,var),us)),[t,None])
when Id.equal var Notation_ops.ldots_var ->
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg
- | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
+ | CAppExpl (_,(None,f,us),l) -> pr_appexpl (pr mt) (f,us) l, lapp
| CApp (_,(Some i,f),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
@@ -567,7 +574,7 @@ let rec fix rf x =rf (fix rf) x
let pr = fix modular_constr_pr mt
let pr_simpleconstr = function
- | CAppExpl (_,(None,f),[]) -> str "@" ++ pr_reference f
+ | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us
| c -> pr lsimpleconstr c
let default_term_pr = {
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ecc80c2cf3..e2d237815e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -176,7 +176,8 @@ let pr_hints db h pr_c pr_pat =
match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
l
| HintsImmediate l ->
- str"Immediate" ++ spc() ++ prlist_with_sep sep (pr_reference_or_constr pr_c) l
+ str"Immediate" ++ spc() ++
+ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
| HintsUnfold l ->
str "Unfold " ++ prlist_with_sep sep pr_reference l
| HintsTransparency (l, b) ->
@@ -374,6 +375,11 @@ let pr_priority = function
| None -> mt ()
| Some i -> spc () ++ str "|" ++ spc () ++ int i
+let pr_poly p =
+ if Flags.is_universe_polymorphism () then
+ if not p then str"Monomorphic " else mt ()
+ else if p then str"Polymorphic " else mt ()
+
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
@@ -466,6 +472,9 @@ in
let pr_using e = str (Proof_using.to_string e) in
let rec pr_vernac = function
+ | VernacPolymorphic (poly, v) ->
+ let s = if poly then str"Polymorphic" else str"Monomorphic" in
+ s ++ pr_vernac v
| VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
| VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
@@ -579,7 +588,7 @@ let rec pr_vernac = function
| VernacDefinition (d,id,b) -> (* A verifier... *)
let pr_def_token (l,dk) =
let l = match l with Some x -> x | None -> Decl_kinds.Global in
- str (Kindops.string_of_definition_kind (l,dk)) in
+ str (Kindops.string_of_definition_kind (l,false,dk)) in
let pr_reduce = function
| None -> mt()
| Some r ->
@@ -619,7 +628,6 @@ let rec pr_vernac = function
(pr_assumption_token (n > 1) stre ++ spc() ++
pr_ne_params_list pr_lconstr_expr l)
| VernacInductive (f,i,l) ->
-
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 89808ef4db..e885f5978c 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -66,7 +66,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
let print_basename sp = pr_global (ConstRef sp)
let print_ref reduce ref =
- let typ = Global.type_of_global ref in
+ let typ = Global.type_of_global_unsafe ref in
let typ =
if reduce then
let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
@@ -122,7 +122,7 @@ let print_renames_list prefix l =
hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
let need_expansion impl ref =
- let typ = Global.type_of_global ref in
+ let typ = Global.type_of_global_unsafe ref in
let ctx = prod_assum typ in
let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in
not (List.is_empty impl) && List.length impl >= nprods &&
@@ -371,25 +371,23 @@ let print_body = function
let print_typed_body (val_0,typ) =
(print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ)
-let ungeneralized_type_of_constant_type = function
- | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
- | NonPolymorphicType t -> t
+let ungeneralized_type_of_constant_type t = t
let print_constant with_values sep sp =
let cb = Global.lookup_constant sp in
let val_0 = Declareops.body_of_constant cb in
let typ = ungeneralized_type_of_constant_type cb.const_type in
- hov 0 (
+ hov 0 (pr_polymorphic cb.const_polymorphic ++
match val_0 with
| None ->
str"*** [ " ++
print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_univ_cstr (Declareops.constraints_of_constant cb)
+ Printer.pr_universe_ctx (Future.force cb.const_universes)
| _ ->
print_basename sp ++ str sep ++ cut () ++
(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
- Printer.pr_univ_cstr (Declareops.constraints_of_constant cb))
+ Printer.pr_universe_ctx (Future.force cb.const_universes))
let gallina_print_constant_with_infos sp =
print_constant true " = " sp ++
@@ -626,7 +624,7 @@ let print_opaque_name qid =
| IndRef (sp,_) ->
print_inductive sp
| ConstructRef cstr ->
- let ty = Inductiveops.type_of_constructor env cstr in
+ let ty = Inductiveops.type_of_constructor env (cstr,Univ.Instance.empty) in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
let (_,c,ty) = lookup_named id env in
diff --git a/printing/printer.ml b/printing/printer.ml
index 935153bff6..91156e21f5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -119,12 +119,11 @@ let _ = Termops.set_print_constr pr_lconstr_env
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
let pr_univ_cstr (c:Univ.constraints) =
- if !Detyping.print_universes && not (Univ.is_empty_constraint c) then
+ if !Detyping.print_universes && not (Univ.Constraint.is_empty c) then
fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_constraints c)) c
else
mt()
-
(** Term printers resilient to [Nametab] errors *)
(** When the nametab isn't up-to-date, the term printers above
@@ -179,6 +178,11 @@ let safe_pr_constr_env = safe_gen pr_constr_env
let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
+let pr_universe_ctx c =
+ if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
+ fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_universe_context c)) c
+ else
+ mt()
(**********************************************************************)
(* Global references *)
@@ -186,12 +190,22 @@ let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
let pr_global_env = pr_global_env
let pr_global = pr_global_env Id.Set.empty
+let pr_puniverses f env (c,u) =
+ f env c ++
+ (if !Constrextern.print_universes then
+ str"(*" ++ Univ.Instance.pr u ++ str"*)"
+ else mt ())
+
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
let pr_existential_key evk = str (string_of_existential evk)
let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
+let pr_pconstant = pr_puniverses pr_constant
+let pr_pinductive = pr_puniverses pr_inductive
+let pr_pconstructor = pr_puniverses pr_constructor
+
let pr_evaluable_reference ref =
pr_global (Tacred.global_of_evaluable_reference ref)
@@ -713,6 +727,17 @@ let pr_assumptionset env s =
] in
prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
+open Typeclasses
+
+let xor a b =
+ (a && not b) || (not a && b)
+
+let pr_polymorphic b =
+ let print = xor (Flags.is_universe_polymorphism ()) b in
+ if print then
+ if b then str"Polymorphic " else str"Monomorphic "
+ else mt ()
+
(** Inductive declarations *)
open Termops
@@ -730,17 +755,17 @@ let print_constructors envpar names types =
hv 0 (str " " ++ pc)
let build_ind_type env mip =
- match mip.mind_arity with
- | Monomorphic ar -> ar.mind_user_arity
- | Polymorphic ar ->
- it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt
+ mip.mind_arity.mind_user_arity
let print_one_inductive env mib ((_,i) as ind) =
let mip = mib.mind_packets.(i) in
let params = mib.mind_params_ctxt in
let args = extended_rel_list 0 params in
let arity = hnf_prod_applist env (build_ind_type env mip) args in
- let cstrtypes = Inductive.type_of_constructors ind (mib,mip) in
+ let u = if mib.mind_polymorphic then
+ Univ.UContext.instance mib.mind_universes
+ else Univ.Instance.empty in
+ let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
let envpar = push_rel_context params env in
hov 0 (
@@ -751,11 +776,11 @@ let print_one_inductive env mib ((_,i) as ind) =
let print_mutual_inductive env mind mib =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
in
- hov 0 (
+ hov 0 (pr_polymorphic mib.mind_polymorphic ++
str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
prlist_with_sep (fun () -> fnl () ++ str" with ")
(print_one_inductive env mib) inds ++
- pr_univ_cstr mib.mind_constraints)
+ pr_universe_ctx mib.mind_universes)
let get_fields =
let rec prodec_rec l subst c =
@@ -774,13 +799,17 @@ let print_record env mind mib =
let mip = mib.mind_packets.(0) in
let params = mib.mind_params_ctxt in
let args = extended_rel_list 0 params in
+ let u = if mib.mind_polymorphic then
+ Univ.UContext.instance mib.mind_universes
+ else Univ.Instance.empty in
let arity = hnf_prod_applist env (build_ind_type env mip) args in
- let cstrtypes = Inductive.type_of_constructors (mind,0) (mib,mip) in
+ let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
hov 0 (
hov 0 (
+ pr_polymorphic mib.mind_polymorphic ++
str "Record " ++ pr_id mip.mind_typename ++ brk(1,4) ++
print_params env params ++
str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
@@ -791,10 +820,10 @@ let print_record env mind mib =
(fun (id,b,c) ->
pr_id id ++ str (if b then " : " else " := ") ++
pr_lconstr_env envpar c) fields) ++ str" }" ++
- pr_univ_cstr mib.mind_constraints)
+ pr_universe_ctx mib.mind_universes)
let pr_mutual_inductive_body env mind mib =
- if mib.mind_record && not !Flags.raw_print then
+ if mib.mind_record <> None && not !Flags.raw_print then
print_record env mind mib
else
print_mutual_inductive env mind mib
diff --git a/printing/printer.mli b/printing/printer.mli
index 6ca55b16b5..eb181d4265 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -80,7 +80,9 @@ val pr_sort : sorts -> std_ppcmds
(** Universe constraints *)
+val pr_polymorphic : bool -> std_ppcmds
val pr_univ_cstr : Univ.constraints -> std_ppcmds
+val pr_universe_ctx : Univ.universe_context -> std_ppcmds
(** Printing global references using names as short as possible *)
@@ -94,6 +96,11 @@ val pr_constructor : env -> constructor -> std_ppcmds
val pr_inductive : env -> inductive -> std_ppcmds
val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
+val pr_pconstant : env -> pconstant -> std_ppcmds
+val pr_pinductive : env -> pinductive -> std_ppcmds
+val pr_pconstructor : env -> pconstructor -> std_ppcmds
+
+
(** Contexts *)
val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 112abeec9c..da5546baca 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -146,8 +146,7 @@ let print_body is_impl env mp (l,body) =
| None -> mt ()
| Some env ->
str " :" ++ spc () ++
- hov 0 (Printer.pr_ltype_env env
- (Typeops.type_of_constant_type env cb.const_type)) ++
+ hov 0 (Printer.pr_ltype_env env cb.const_type) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 11:27:19 +0000