aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml8
-rw-r--r--printing/pptactic.ml105
-rw-r--r--printing/pptacticsig.mli13
-rw-r--r--printing/ppvernac.ml5
-rw-r--r--printing/prettyp.ml2
-rw-r--r--printing/printer.ml8
-rw-r--r--printing/printmod.ml2
7 files changed, 65 insertions, 78 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 56429410cb..c07057a096 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -136,8 +136,6 @@ end) = struct
let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
- let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-
let pr_univ l =
match l with
| [_,x] -> str x
@@ -153,11 +151,11 @@ end) = struct
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
- let id = tag_ref (str (Id.to_string id)) in
+ let id = tag_ref (pr_id id) in
let sl = match List.rev (DirPath.repr sl) with
| [] -> mt ()
| sl ->
- let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in
+ let pr dir = tag_path (pr_id dir) ++ str "." in
prlist pr sl
in
sl ++ id
@@ -182,7 +180,7 @@ end) = struct
let pr_reference = function
| Qualid (_, qid) -> pr_qualid qid
- | Ident (_, id) -> tag_var (str (Id.to_string id))
+ | Ident (_, id) -> tag_var (pr_id id)
let pr_cref ref us =
pr_reference ref ++ pr_universe_instance us
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4d14cae7a7..a5716279f3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -267,15 +267,9 @@ module Make
let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
- | GenArgType -> pr_raw_generic_rec prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
- | ConstrMayEvalArgType ->
- pr_may_eval prc prlc (pr_or_by_notation prref) prpat
- (out_gen (rawwit wit_constr_may_eval) x)
- | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
@@ -303,16 +297,9 @@ module Make
let rec pr_glb_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
- | GenArgType -> pr_glb_generic_rec prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
- | ConstrMayEvalArgType ->
- pr_may_eval prc prlc
- (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
- (out_gen (glbwit wit_constr_may_eval) x)
- | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
@@ -339,13 +326,9 @@ module Make
let rec pr_top_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
| VarArgType -> pr_id (out_gen (topwit wit_var) x)
- | GenArgType -> pr_top_generic_rec prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (topwit wit_constr) x)
- | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
- | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
@@ -388,10 +371,11 @@ module Make
in
pr_sequence (fun x -> x) l
- let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+ let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
try
let pp_rules = Hashtbl.find prtac_tab s in
let pp = pp_rules.(i) in
+ let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in
let (lev', pl) = pp.pptac_prods in
let p = pr_tacarg_using_rule pr_gen (pl,l) in
if lev' > lev then surround p else p
@@ -406,28 +390,35 @@ module Make
in
str "<" ++ name ++ str ">" ++ args
- let pr_alias_gen pr_gen lev key l =
+ let pr_alias_gen check pr_gen lev key l =
try
let pp = KNmap.find key !prnotation_tab in
let (lev', pl) = pp.pptac_prods in
+ let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in
let p = pr_tacarg_using_rule pr_gen (pl, l) in
if lev' > lev then surround p else p
with Not_found ->
KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+ let check_type t arg = match arg with
+ | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
+ | _ -> false
+
+ let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false
+
let pr_raw_extend_rec prc prlc prtac prpat =
- pr_extend_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+ pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
let pr_glob_extend_rec prc prlc prtac prpat =
- pr_extend_gen (pr_glb_generic_rec prc prlc prtac prpat)
+ pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
let pr_extend_rec prc prlc prtac prpat =
- pr_extend_gen (pr_top_generic_rec prc prlc prtac prpat)
+ pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
let pr_raw_alias prc prlc prtac prpat =
- pr_alias_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+ pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
let pr_glob_alias prc prlc prtac prpat =
- pr_alias_gen (pr_glb_generic_rec prc prlc prtac prpat)
+ pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
let pr_alias prc prlc prtac prpat =
- pr_alias_gen (pr_top_generic_rec prc prlc prtac prpat)
+ pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
(**********************************************************************)
(* The tactic printer *)
@@ -694,11 +685,6 @@ module Make
| l -> spc () ++
hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
- let string_of_debug = function
- | Off -> ""
- | Debug -> "debug "
- | Info -> "info_"
-
let pr_then () = str ";"
let ltop = (5,E)
@@ -733,8 +719,8 @@ module Make
pr_reference : 'ref -> std_ppcmds;
pr_name : 'nam -> std_ppcmds;
pr_generic : 'lev generic_argument -> std_ppcmds;
- pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds;
- pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+ pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+ pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
}
constraint 'a = <
@@ -821,8 +807,6 @@ module Make
let rec pr_atom0 a = tag_atom a (match a with
| TacIntroPattern [] -> primitive "intros"
| TacIntroMove (None,MoveLast) -> primitive "intro"
- | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial"
- | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto"
| TacClear (true,[]) -> primitive "clear"
| t -> str "(" ++ pr_atom1 t ++ str ")"
)
@@ -931,23 +915,6 @@ module Make
++ pr_arg pr_quantified_hypothesis h2
)
- (* Automation tactics *)
- | TacTrivial (_,[],Some []) as x ->
- pr_atom0 x
- | TacTrivial (d,lems,db) ->
- hov 0 (
- str (string_of_debug d) ++ primitive "trivial"
- ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
- )
- | TacAuto (_,None,[],Some []) as x ->
- pr_atom0 x
- | TacAuto (d,n,lems,db) ->
- hov 0 (
- str (string_of_debug d) ++ primitive "auto"
- ++ pr_opt (pr_or_var int) n
- ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
- )
-
(* Context management *)
| TacClear (true,[]) as t ->
pr_atom0 t
@@ -1229,7 +1196,7 @@ module Make
| TacML (loc,s,l) ->
pr_with_comments loc (pr.pr_extend 1 s l), lcall
| TacAlias (loc,kn,l) ->
- pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+ pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
)
in
if prec_less prec inherited then strm
@@ -1296,7 +1263,7 @@ module Make
let pr_pat_and_constr_expr pr ((c,_),_) = pr c
- let rec pr_glob_tactic_level env n t =
+ let pr_glob_tactic_level env n t =
let glob_printers =
(strip_prod_binders_glob_constr)
in
@@ -1388,9 +1355,18 @@ module Make
(pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
(pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
- let pr_extend env = pr_extend_rec
- (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern
+ let check_val_type t arg =
+ let t = Genarg.val_tag (Obj.magic t) in (** FIXME *)
+ let Val.Dyn (t', _) = arg in
+ match Genarg.Val.eq t t' with
+ | None -> false
+ | Some _ -> true
+
+ let pr_alias pr lev key args =
+ pr_alias_gen check_val_type pr lev key args
+
+ let pr_extend pr lev ml args =
+ pr_extend_gen check_val_type pr lev ml args
let pr_tactic env = pr_tactic_level env ltop
@@ -1435,6 +1411,8 @@ let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
let pr_string s = str "\"" ++ str s ++ str "\"" in
+ Genprint.register_print0 Constrarg.wit_int_or_var
+ (pr_or_var int) (pr_or_var int) int;
Genprint.register_print0 Constrarg.wit_ref
pr_reference (pr_or_var (pr_located pr_global)) pr_global;
Genprint.register_print0
@@ -1456,6 +1434,12 @@ let () =
(fun (c,_) -> Printer.pr_glob_constr c)
Printer.pr_closed_glob
;
+ Genprint.register_print0
+ Constrarg.wit_open_constr
+ Ppconstr.pr_constr_expr
+ (fun (c, _) -> Printer.pr_glob_constr c)
+ Printer.pr_constr
+ ;
Genprint.register_print0 Constrarg.wit_red_expr
(pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
(pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
@@ -1464,11 +1448,16 @@ let () =
Genprint.register_print0 Constrarg.wit_bindings
(pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
(pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it);
+ (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+ Genprint.register_print0 Constrarg.wit_constr_may_eval
+ (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
+ (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
+ (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr))
+ pr_constr;
Genprint.register_print0 Constrarg.wit_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
(pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun { Evd.it = it } -> pr_with_bindings pr_constr pr_lconstr it);
+ (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
Genprint.register_print0 Stdarg.wit_int int int int;
Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 1c17d04928..5b89266553 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -8,11 +8,9 @@
open Pp
open Genarg
-open Constrexpr
open Tacexpr
open Ppextend
open Environ
-open Pattern
open Misctypes
module type Pp = sig
@@ -40,13 +38,16 @@ module type Pp = sig
val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds
val pr_raw_extend: env -> int ->
- ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
+ ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
val pr_glob_extend: env -> int ->
- ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
+ ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
- val pr_extend : env -> int ->
- ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
+ val pr_extend :
+ (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+ val pr_alias : (Val.t -> std_ppcmds) ->
+ int -> Names.KerName.t -> Val.t list -> std_ppcmds
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f216c599d0..daba18bad2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -105,10 +105,9 @@ module Make
else id
let pr_production_item = function
- | TacNonTerm (loc,nt,Some (p,sep)) ->
+ | TacNonTerm (loc, nt, (p, sep)) ->
let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
- | TacNonTerm (loc,nt,None) -> str nt
| TacTerm s -> qs s
let pr_comment pr_c = function
@@ -1034,7 +1033,7 @@ module Make
let pr_tac_body tacdef_body =
let id, redef, body =
match tacdef_body with
- | TacticDefinition ((_,id), body) -> str (Id.to_string id), false, body
+ | TacticDefinition ((_,id), body) -> pr_id id, false, body
| TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
in
let idl, body =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 84649e6ebf..08228cb209 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -132,7 +132,7 @@ let print_renames_list prefix l =
let need_expansion impl ref =
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
+ let nprods = List.count (fun (_,b,_) -> Option.is_empty b) ctx in
not (List.is_empty impl) && List.length impl >= nprods &&
let _,lastimpl = List.chop nprods impl in
List.exists is_status_implicit lastimpl
diff --git a/printing/printer.ml b/printing/printer.ml
index 773127c772..08fd0186a0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -639,8 +639,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
| _ , _, _ ->
let end_cmd =
str "This subproof is complete, but there are some unfocused goals." ++
- (match Proof_global.Bullet.suggest p
- with None -> str"" | Some s -> fnl () ++ str s) ++
+ (let s = Proof_global.Bullet.suggest p in
+ if Pp.is_empty s then s else fnl () ++ s) ++
fnl ()
in
pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
@@ -777,7 +777,7 @@ let pr_assumptionset env s =
let (v, a, o, tr) = accu in
match t with
| Variable id ->
- let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
+ let var = pr_id id ++ str " : " ++ pr_ltype typ in
(var :: v, a, o, tr)
| Axiom (kn,[]) ->
let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
@@ -786,7 +786,7 @@ let pr_assumptionset env s =
let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++
cut() ++
prlist_with_sep cut (fun (lbl, ctx, ty) ->
- str " used in " ++ str (Names.Label.to_string lbl) ++
+ str " used in " ++ pr_label lbl ++
str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
l in
(v, ax :: a, o, tr)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index d277d3782a..3973c2db67 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -263,7 +263,7 @@ let nametab_register_modparam mbid mtb =
List.iter (nametab_register_body mp dir) struc
let print_body is_impl env mp (l,body) =
- let name = str (Label.to_string l) in
+ let name = pr_label l in
hov 2 (match body with
| SFBmodule _ -> keyword "Module" ++ spc () ++ name
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:35:23 +0000