aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml5
-rw-r--r--printing/ppannotation.ml2
-rw-r--r--printing/ppannotation.mli1
-rw-r--r--printing/ppconstr.ml8
-rw-r--r--printing/pptactic.ml674
-rw-r--r--printing/pptactic.mli3
-rw-r--r--printing/pptacticsig.mli9
-rw-r--r--printing/ppvernac.ml93
-rw-r--r--printing/prettyp.ml4
-rw-r--r--printing/printer.ml28
-rw-r--r--printing/richprinter.ml1
-rw-r--r--printing/richprinter.mli3
12 files changed, 343 insertions, 488 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index d8bd81c4cc..0ec35e07be 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,8 +19,9 @@ module PrintObj =
struct
type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
let name = "printer"
- let default wit = match unquote (rawwit wit) with
- | ExtraArgType name ->
+ let default wit = match wit with
+ | ExtraArg tag ->
+ let name = ArgT.repr tag in
let printer = {
raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index df7f925b73..511f93569c 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -20,7 +20,6 @@ type t =
| AGlobAtomicTacticExpr of glob_atomic_tactic_expr
| ARawTacticExpr of raw_tactic_expr
| ARawAtomicTacticExpr of raw_atomic_tactic_expr
- | ATacticExpr of tactic_expr
| AAtomicTacticExpr of atomic_tactic_expr
let tag_of_annotation = function
@@ -32,7 +31,6 @@ let tag_of_annotation = function
| AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
| ARawTacticExpr _ -> "raw_tactic_expr"
| ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr"
- | ATacticExpr _ -> "tactic_expr"
| AAtomicTacticExpr _ -> "atomic_tactic_expr"
let attributes_of_annotation a =
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index 84724053ed..a0fef1a757 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -23,7 +23,6 @@ type t =
| AGlobAtomicTacticExpr of glob_atomic_tactic_expr
| ARawTacticExpr of raw_tactic_expr
| ARawAtomicTacticExpr of raw_atomic_tactic_expr
- | ATacticExpr of tactic_expr
| AAtomicTacticExpr of atomic_tactic_expr
val tag_of_annotation : t -> string
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8a0df18ca5..1866ca5042 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -244,16 +244,16 @@ end) = struct
| CPatAlias (_, p, id) ->
pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
- | CPatCstr (_,c, [], []) ->
+ | CPatCstr (_,c, None, []) ->
pr_reference c, latom
- | CPatCstr (_, c, [], args) ->
+ | CPatCstr (_, c, None, args) ->
pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, args, []) ->
+ | CPatCstr (_, c, Some args, []) ->
str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, expl_args, extra_args) ->
+ | CPatCstr (_, c, Some expl_args, extra_args) ->
surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c00036bb3c..7949bafcbb 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -33,16 +33,9 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-(* ML Extensions *)
-let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
- Hashtbl.create 17
-
(* Tactic notations *)
let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
-let declare_ml_tactic_pprule key pt =
- Hashtbl.add prtac_tab key pt
-
let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -61,14 +54,14 @@ type 'a glob_extra_genarg_printer =
type 'a extra_genarg_printer =
(Term.constr -> std_ppcmds) ->
(Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
let genarg_pprule = ref String.Map.empty
let declare_extra_genarg_pprule wit f g h =
- let s = match unquote (topwit wit) with
- | ExtraArgType s -> s
+ let s = match wit with
+ | ExtraArg s -> ArgT.repr s
| _ -> error
"Can declare a pretty-printing rule only for extra argument types."
in
@@ -94,8 +87,6 @@ module Make
: raw_tactic_expr -> std_ppcmds -> std_ppcmds
val tag_raw_atomic_tactic_expr
: raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_tactic_expr
- : tactic_expr -> std_ppcmds -> std_ppcmds
val tag_atomic_tactic_expr
: atomic_tactic_expr -> std_ppcmds -> std_ppcmds
end)
@@ -106,6 +97,24 @@ module Make
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
+ let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with
+ | Val.List tag ->
+ pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x
+ | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x
+ | Val.Pair (tag1, tag2) ->
+ str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++
+ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")"
+ | Val.Base t ->
+ let name = Val.repr t in
+ let default = str "<" ++ str name ++ str ">" in
+ match ArgT.name name with
+ | None -> default
+ | Some (ArgT.Any arg) ->
+ let wit = ExtraArg arg in
+ match Val.eq (val_tag (Topwit wit)) (Val.Base t) with
+ | None -> default
+ | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+
let pr_with_occurrences pr (occs,c) =
match occs with
| AllOccurrences ->
@@ -264,24 +273,25 @@ module Make
let with_evars ev s = if ev then "e" ^ s else s
+ let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
match wit with
| ListArg wit ->
let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
let ans = pr_sequence map x in
- hov 0 ans
+ hov_if_not_empty 0 ans
| OptArg wit ->
let ans = match x with
| None -> mt ()
| Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
in
- hov 0 ans
+ hov_if_not_empty 0 ans
| PairArg (wit1, wit2) ->
let p, q = x in
let p = in_gen (rawwit wit1) p in
let q = in_gen (rawwit wit2) q in
- hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
+ hov_if_not_empty 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
| ExtraArg s ->
try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
@@ -292,19 +302,19 @@ module Make
| ListArg wit ->
let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
let ans = pr_sequence map x in
- hov 0 ans
+ hov_if_not_empty 0 ans
| OptArg wit ->
let ans = match x with
| None -> mt ()
| Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
in
- hov 0 ans
+ hov_if_not_empty 0 ans
| PairArg (wit1, wit2) ->
let p, q = x in
let p = in_gen (glbwit wit1) p in
let q = in_gen (glbwit wit2) q in
let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in
- hov 0 ans
+ hov_if_not_empty 0 ans
| ExtraArg s ->
try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
@@ -314,19 +324,19 @@ module Make
| ListArg wit ->
let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
let ans = pr_sequence map x in
- hov 0 ans
+ hov_if_not_empty 0 ans
| OptArg wit ->
let ans = match x with
| None -> mt ()
| Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x)
in
- hov 0 ans
+ hov_if_not_empty 0 ans
| PairArg (wit1, wit2) ->
let p, q = x in
let p = in_gen (topwit wit1) p in
let q = in_gen (topwit wit2) q in
let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in
- hov 0 ans
+ hov_if_not_empty 0 ans
| ExtraArg s ->
try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x)
with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x)
@@ -339,11 +349,9 @@ module Make
| [], [] -> []
| _ -> failwith "Inconsistent arguments of extended tactic"
- type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg
-
let filter_arg = function
| Egramml.GramTerminal _ -> None
- | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t)
+ | Egramml.GramNonTerminal (_, Rawwit t, _) -> Some (ArgumentType t)
let pr_tacarg_using_rule pr_gen l =
let l = match l with
@@ -356,14 +364,6 @@ module Make
pr_sequence (fun x -> x) 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 args = List.map_filter filter_arg pp.pptac_prods in
- let () = if not (List.for_all2eq check args l) then raise Not_found in
- let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
- if pp.pptac_level > lev then surround p else p
- with Not_found ->
let name =
str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
str "@" ++ int i
@@ -384,25 +384,21 @@ module Make
with Not_found ->
KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
- let check_type t arg = match t, arg with
- | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg)
- | _ -> false
+ let check_type t arg = match arg with
+ | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
+ | _ -> argument_type_eq t (ArgumentType wit_tactic)
- let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false
+ let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
let pr_raw_extend_rec prc prlc prtac prpat =
- pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
+ pr_extend_gen check_type (pr_farg prtac)
let pr_glob_extend_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 check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
+ pr_extend_gen check_type (pr_farg prtac)
let pr_raw_alias prc prlc prtac prpat =
- pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
+ pr_alias_gen check_type (pr_farg prtac)
let pr_glob_alias 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 check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
+ pr_alias_gen check_type (pr_farg prtac)
(**********************************************************************)
(* The tactic printer *)
@@ -511,9 +507,8 @@ module Make
| ipat ->
spc() ++ prc c ++ pr_as_ipat prdc ipat
- let pr_by_tactic prt = function
- | TacId [] -> mt ()
- | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac
+ let pr_by_tactic prt tac =
+ spc() ++ keyword "by" ++ spc () ++ prt tac
let pr_hyp_location pr_id = function
| occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
@@ -526,7 +521,7 @@ module Make
str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
) occs
- let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp)
+ let pr_in pp = hov 0 (keyword "in" ++ pp)
let pr_simple_hyp_clause pr_id = function
| [] -> mt ()
@@ -659,15 +654,13 @@ module Make
str " ]")
let pr_hintbases = function
- | None -> spc () ++ keyword "with" ++ str" *"
+ | None -> keyword "with" ++ str" *"
| Some [] -> mt ()
- | Some l ->
- spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
+ | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
let pr_auto_using prc = function
| [] -> mt ()
- | l -> spc () ++
- hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
+ | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
let pr_then () = str ";"
@@ -694,7 +687,6 @@ module Make
type 'a printer = {
pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
pr_constr : 'trm -> std_ppcmds;
- pr_uconstr : 'utrm -> std_ppcmds;
pr_lconstr : 'trm -> std_ppcmds;
pr_dconstr : 'dtrm -> std_ppcmds;
pr_pattern : 'pat -> std_ppcmds;
@@ -709,7 +701,6 @@ module Make
constraint 'a = <
term :'trm;
- utrm :'utrm;
dterm :'dtrm;
pattern :'pat;
constant :'cst;
@@ -719,287 +710,246 @@ module Make
level :'lev
>
- let make_pr_tac pr strip_prod_binders tag_atom tag =
-
- (* some shortcuts *)
- let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
- let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
- let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
- let pr_with_bindings_arg_full = pr_with_bindings_arg in
- let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
- let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
-
- let pr_constrarg c = spc () ++ pr.pr_constr c in
- let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
- let pr_intarg n = spc () ++ int n in
-
- (* Some printing combinators *)
- let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
-
- let extract_binders = function
- | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
- | body -> ([],body) in
-
- let pr_binder_fix (nal,t) =
- (* match t with
- | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
- | _ ->*)
- let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
- spc() ++ hov 1 (str"(" ++ s ++ str")") in
-
- let pr_fix_tac (id,n,c) =
- let rec set_nth_name avoid n = function
- (nal,ty)::bll ->
- if n <= List.length nal then
- match List.chop (n-1) nal with
- _, (_,Name id) :: _ -> id, (nal,ty)::bll
- | bef, (loc,Anonymous) :: aft ->
- let id = next_ident_away (Id.of_string"y") avoid in
- id, ((bef@(loc,Name id)::aft, ty)::bll)
- | _ -> assert false
- else
- let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
- (id,(nal,ty)::bll')
- | [] -> assert false in
- let (bll,ty) = strip_prod_binders n c in
- let names =
- List.fold_left
- (fun ln (nal,_) -> List.fold_left
- (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
- ln nal)
- [] bll in
- let idarg,bll = set_nth_name names n bll in
- let annot = match names with
- | [_] ->
- mt ()
- | _ ->
- spc() ++ str"{"
- ++ keyword "struct" ++ spc ()
- ++ pr_id idarg ++ str"}"
- in
- hov 1 (str"(" ++ pr_id id ++
- prlist pr_binder_fix bll ++ annot ++ str" :" ++
- pr_lconstrarg ty ++ str")") in
- (* spc() ++
- hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
- c)
+ let pr_atom pr strip_prod_binders tag_atom =
+ let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+ let pr_with_bindings_arg_full = pr_with_bindings_arg in
+ let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
+ let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+ let pr_constrarg c = spc () ++ pr.pr_constr c in
+ let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+ let pr_intarg n = spc () ++ int n in
+
+ (* Some printing combinators *)
+ let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+
+ let pr_binder_fix (nal,t) =
+ (* match t with
+ | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
+ | _ ->*)
+ let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+ spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+ let pr_fix_tac (id,n,c) =
+ let rec set_nth_name avoid n = function
+ (nal,ty)::bll ->
+ if n <= List.length nal then
+ match List.chop (n-1) nal with
+ _, (_,Name id) :: _ -> id, (nal,ty)::bll
+ | bef, (loc,Anonymous) :: aft ->
+ let id = next_ident_away (Id.of_string"y") avoid in
+ id, ((bef@(loc,Name id)::aft, ty)::bll)
+ | _ -> assert false
+ else
+ let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+ (id,(nal,ty)::bll')
+ | [] -> assert false in
+ let (bll,ty) = strip_prod_binders n c in
+ let names =
+ List.fold_left
+ (fun ln (nal,_) -> List.fold_left
+ (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+ ln nal)
+ [] bll in
+ let idarg,bll = set_nth_name names n bll in
+ let annot = match names with
+ | [_] ->
+ mt ()
+ | _ ->
+ spc() ++ str"{"
+ ++ keyword "struct" ++ spc ()
+ ++ pr_id idarg ++ str"}"
+ in
+ hov 1 (str"(" ++ pr_id id ++
+ prlist pr_binder_fix bll ++ annot ++ str" :" ++
+ pr_lconstrarg ty ++ str")") in
+ (* spc() ++
+ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+ c)
+ *)
+ let pr_cofix_tac (id,c) =
+ hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+ (* Printing tactics as arguments *)
+ let rec pr_atom0 a = tag_atom a (match a with
+ | TacIntroPattern [] -> primitive "intros"
+ | TacIntroMove (None,MoveLast) -> primitive "intro"
+ | t -> str "(" ++ pr_atom1 t ++ str ")"
+ )
+
+ (* Main tactic printer *)
+ and pr_atom1 a = tag_atom a (match a with
+ (* Basic tactics *)
+ | TacIntroPattern [] as t ->
+ pr_atom0 t
+ | TacIntroPattern (_::_ as p) ->
+ hov 1 (primitive "intros" ++ spc () ++
+ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+ | TacIntroMove (None,MoveLast) as t ->
+ pr_atom0 t
+ | TacIntroMove (Some id,MoveLast) ->
+ primitive "intro" ++ spc () ++ pr_id id
+ | TacIntroMove (ido,hto) ->
+ hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
+ Miscprint.pr_move_location pr.pr_name hto)
+ | TacExact c ->
+ hov 1 (primitive "exact" ++ pr_constrarg c)
+ | TacApply (a,ev,cb,inhyp) ->
+ hov 1 (
+ (if a then mt() else primitive "simple ") ++
+ primitive (with_evars ev "apply") ++ spc () ++
+ prlist_with_sep pr_comma pr_with_bindings_arg cb ++
+ pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+ )
+ | TacElim (ev,cb,cbo) ->
+ hov 1 (
+ primitive (with_evars ev "elim")
+ ++ pr_arg pr_with_bindings_arg cb
+ ++ pr_opt pr_eliminator cbo)
+ | TacCase (ev,cb) ->
+ hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+ | TacMutualFix (id,n,l) ->
+ hov 1 (
+ primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+ ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+ | TacMutualCofix (id,l) ->
+ hov 1 (
+ primitive "cofix" ++ spc () ++ pr_id id ++ spc()
+ ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
+ )
+ | TacAssert (b,Some tac,ipat,c) ->
+ hov 1 (
+ primitive (if b then "assert" else "enough") ++
+ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+ pr_by_tactic (pr.pr_tactic ltop) tac
+ )
+ | TacAssert (_,None,ipat,c) ->
+ hov 1 (
+ primitive "pose proof"
+ ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+ )
+ | TacGeneralize l ->
+ hov 1 (
+ primitive "generalize" ++ spc ()
+ ++ prlist_with_sep pr_comma (fun (cl,na) ->
+ pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+ l
+ )
+ | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+ hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+ | TacLetTac (na,c,cl,b,e) ->
+ hov 1 (
+ (if b then primitive "set" else primitive "remember") ++
+ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+ else pr_pose_as_style pr.pr_constr na c) ++
+ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+ pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
+ (* | TacInstantiate (n,c,ConclLocation ()) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg c ++ str ")" ))
+ | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg c ++ str ")" )
+ ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
*)
- let pr_cofix_tac (id,c) =
- hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
-
- (* Printing tactics as arguments *)
- let rec pr_atom0 a = tag_atom a (match a with
- | TacIntroPattern [] -> primitive "intros"
- | TacIntroMove (None,MoveLast) -> primitive "intro"
- | TacClear (true,[]) -> primitive "clear"
- | t -> str "(" ++ pr_atom1 t ++ str ")"
- )
-
- (* Main tactic printer *)
- and pr_atom1 a = tag_atom a (match a with
- (* Basic tactics *)
- | TacIntroPattern [] as t ->
- pr_atom0 t
- | TacIntroPattern (_::_ as p) ->
- hov 1 (primitive "intros" ++ spc () ++
- prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
- | TacIntroMove (None,MoveLast) as t ->
- pr_atom0 t
- | TacIntroMove (Some id,MoveLast) ->
- primitive "intro" ++ spc () ++ pr_id id
- | TacIntroMove (ido,hto) ->
- hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
- Miscprint.pr_move_location pr.pr_name hto)
- | TacExact c ->
- hov 1 (primitive "exact" ++ pr_constrarg c)
- | TacApply (a,ev,cb,inhyp) ->
- hov 1 (
- (if a then mt() else primitive "simple ") ++
- primitive (with_evars ev "apply") ++ spc () ++
- prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp
- )
- | TacElim (ev,cb,cbo) ->
- hov 1 (
- primitive (with_evars ev "elim")
- ++ pr_arg pr_with_bindings_arg cb
- ++ pr_opt pr_eliminator cbo)
- | TacCase (ev,cb) ->
- hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
- | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
- | TacMutualFix (id,n,l) ->
- hov 1 (
- primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
- ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
- | TacCofix ido ->
- hov 1 (primitive "cofix" ++ pr_opt pr_id ido)
- | TacMutualCofix (id,l) ->
- hov 1 (
- primitive "cofix" ++ spc () ++ pr_id id ++ spc()
- ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
- )
- | TacAssert (b,Some tac,ipat,c) ->
- hov 1 (
- primitive (if b then "assert" else "enough") ++
- pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
- pr_by_tactic (pr.pr_tactic ltop) tac
- )
- | TacAssert (_,None,ipat,c) ->
- hov 1 (
- primitive "pose proof"
- ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
- )
- | TacGeneralize l ->
- hov 1 (
- primitive "generalize" ++ spc ()
- ++ prlist_with_sep pr_comma (fun (cl,na) ->
- pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
- l
- )
- | TacGeneralizeDep c ->
- hov 1 (
- primitive "generalize" ++ spc () ++ str "dependent"
- ++ pr_constrarg c
- )
- | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
- hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
- | TacLetTac (na,c,cl,b,e) ->
- hov 1 (
- (if b then primitive "set" else primitive "remember") ++
- (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
- else pr_pose_as_style pr.pr_constr na c) ++
- pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
- pr_clauses (Some b) pr.pr_name cl)
- (* | TacInstantiate (n,c,ConclLocation ()) ->
- hov 1 (str "instantiate" ++ spc() ++
- hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg c ++ str ")" ))
- | TacInstantiate (n,c,HypLocation (id,hloc)) ->
- hov 1 (str "instantiate" ++ spc() ++
- hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg c ++ str ")" )
- ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
- *)
-
- (* Derived basic tactics *)
- | TacInductionDestruct (isrec,ev,(l,el)) ->
- hov 1 (
- primitive (with_evars ev (if isrec then "induction" else "destruct"))
- ++ spc ()
- ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
- pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
- pr_with_induction_names pr.pr_dconstr ids ++
- pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
- pr_opt pr_eliminator el
- )
- | TacDoubleInduction (h1,h2) ->
- hov 1 (
- primitive "double induction"
- ++ pr_arg pr_quantified_hypothesis h1
- ++ pr_arg pr_quantified_hypothesis h2
- )
- (* Context management *)
- | TacClear (true,[]) as t ->
- pr_atom0 t
- | TacClear (keep,l) ->
- hov 1 (
- primitive "clear" ++ spc ()
- ++ (if keep then str "- " else mt ())
- ++ prlist_with_sep spc pr.pr_name l
- )
- | TacClearBody l ->
- hov 1 (
- primitive "clearbody" ++ spc ()
- ++ prlist_with_sep spc pr.pr_name l
- )
- | TacMove (id1,id2) ->
- hov 1 (
- primitive "move"
- ++ brk (1,1) ++ pr.pr_name id1
- ++ Miscprint.pr_move_location pr.pr_name id2
- )
- | TacRename l ->
- hov 1 (
- primitive "rename" ++ brk (1,1)
- ++ prlist_with_sep
- (fun () -> str "," ++ brk (1,1))
- (fun (i1,i2) ->
- pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
- l
- )
+ (* Derived basic tactics *)
+ | TacInductionDestruct (isrec,ev,(l,el)) ->
+ hov 1 (
+ primitive (with_evars ev (if isrec then "induction" else "destruct"))
+ ++ spc ()
+ ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
+ pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+ pr_with_induction_names pr.pr_dconstr ids ++
+ pr_opt (pr_clauses None pr.pr_name) cl) l ++
+ pr_opt pr_eliminator el
+ )
+ | TacDoubleInduction (h1,h2) ->
+ hov 1 (
+ primitive "double induction"
+ ++ pr_arg pr_quantified_hypothesis h1
+ ++ pr_arg pr_quantified_hypothesis h2
+ )
- (* Constructors *)
- | TacSplit (ev,l) ->
- hov 1 (
- primitive (with_evars ev "exists")
- ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l
- )
+ (* Context management *)
+ | TacRename l ->
+ hov 1 (
+ primitive "rename" ++ brk (1,1)
+ ++ prlist_with_sep
+ (fun () -> str "," ++ brk (1,1))
+ (fun (i1,i2) ->
+ pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
+ l
+ )
- (* Conversion *)
- | TacReduce (r,h) ->
- hov 1 (
- pr_red_expr r
- ++ pr_clauses (Some true) pr.pr_name h
- )
- | TacChange (op,c,h) ->
- hov 1 (
- primitive "change" ++ brk (1,1)
- ++ (
- match op with
- None ->
- mt ()
- | Some p ->
- pr.pr_pattern p ++ spc ()
- ++ keyword "with" ++ spc ()
- ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h
- )
+ (* Conversion *)
+ | TacReduce (r,h) ->
+ hov 1 (
+ pr_red_expr r
+ ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ )
+ | TacChange (op,c,h) ->
+ hov 1 (
+ primitive "change" ++ brk (1,1)
+ ++ (
+ match op with
+ None ->
+ mt ()
+ | Some p ->
+ pr.pr_pattern p ++ spc ()
+ ++ keyword "with" ++ spc ()
+ ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ )
- (* Equivalence relations *)
- | TacSymmetry cls ->
- primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
-
- (* Equality and inversion *)
- | TacRewrite (ev,l,cl,by) ->
- hov 1 (
- primitive (with_evars ev "rewrite") ++ spc ()
- ++ prlist_with_sep
- (fun () -> str ","++spc())
- (fun (b,m,c) ->
- pr_orient b ++ pr_multi m ++
- pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
- l
- ++ pr_clauses (Some true) pr.pr_name cl
- ++ (
- match by with
- | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
- | None -> mt()
- )
- )
- | TacInversion (DepInversion (k,c,ids),hyp) ->
- hov 1 (
- primitive "dependent " ++ pr_induction_kind k ++ spc ()
- ++ pr_quantified_hypothesis hyp
- ++ pr_with_inversion_names pr.pr_dconstr ids
- ++ pr_with_constr pr.pr_constr c
- )
- | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
- hov 1 (
- pr_induction_kind k ++ spc ()
- ++ pr_quantified_hypothesis hyp
- ++ pr_with_inversion_names pr.pr_dconstr ids
- ++ pr_simple_hyp_clause pr.pr_name cl
+ (* Equality and inversion *)
+ | TacRewrite (ev,l,cl,by) ->
+ hov 1 (
+ primitive (with_evars ev "rewrite") ++ spc ()
+ ++ prlist_with_sep
+ (fun () -> str ","++spc())
+ (fun (b,m,c) ->
+ pr_orient b ++ pr_multi m ++
+ pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+ l
+ ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
+ ++ (
+ match by with
+ | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
+ | None -> mt()
)
- | TacInversion (InversionUsing (c,cl),hyp) ->
- hov 1 (
- primitive "inversion" ++ spc()
- ++ pr_quantified_hypothesis hyp ++ spc ()
- ++ keyword "using" ++ spc () ++ pr.pr_constr c
- ++ pr_simple_hyp_clause pr.pr_name cl
- )
- )
- in
+ )
+ | TacInversion (DepInversion (k,c,ids),hyp) ->
+ hov 1 (
+ primitive "dependent " ++ pr_induction_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_with_inversion_names pr.pr_dconstr ids
+ ++ pr_with_constr pr.pr_constr c
+ )
+ | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+ hov 1 (
+ pr_induction_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_with_inversion_names pr.pr_dconstr ids
+ ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+ )
+ | TacInversion (InversionUsing (c,cl),hyp) ->
+ hov 1 (
+ primitive "inversion" ++ spc()
+ ++ pr_quantified_hypothesis hyp ++ spc ()
+ ++ keyword "using" ++ spc () ++ pr.pr_constr c
+ ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+ )
+ )
+ in
+ pr_atom1
+
+ let make_pr_tac pr strip_prod_binders tag_atom tag =
+ let extract_binders = function
+ | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+ | body -> ([],body) in
let rec pr_tac inherited tac =
let return (doc, l) = (tag tac doc, l) in
let (strm, prec) = return (match tac with
@@ -1157,7 +1107,7 @@ module Make
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom (loc,t) ->
- pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
+ pr_with_comments loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
| TacArg(_,Tacexp e) ->
pr.pr_tactic (latom,E) e, latom
| TacArg(_,ConstrMayEval (ConstrTerm c)) ->
@@ -1187,16 +1137,10 @@ module Make
else str"(" ++ strm ++ str")"
and pr_tacarg = function
- | MetaIdArg (loc,true,s) ->
- pr_with_comments loc (str "$" ++ str s)
- | MetaIdArg (loc,false,s) ->
- pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
| Reference r ->
pr.pr_reference r
| ConstrMayEval c ->
pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
- | UConstr c ->
- keyword "uconstr:" ++ pr.pr_uconstr c
| TacFreshId l ->
keyword "fresh" ++ pr_fresh_ids l
| TacPretype c ->
@@ -1224,7 +1168,6 @@ module Make
let pr = {
pr_tactic = pr_raw_tactic_level;
pr_constr = pr_constr_expr;
- pr_uconstr = pr_constr_expr;
pr_dconstr = pr_constr_expr;
pr_lconstr = pr_lconstr_expr;
pr_pattern = pr_constr_pattern_expr;
@@ -1232,7 +1175,7 @@ module Make
pr_constant = pr_or_by_notation pr_reference;
pr_reference = pr_reference;
pr_name = pr_lident;
- pr_generic = Genprint.generic_raw_print;
+ pr_generic = pr_raw_generic_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference;
pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
} in
@@ -1245,7 +1188,7 @@ module Make
let pr_and_constr_expr pr (c,_) = pr c
- let pr_pat_and_constr_expr pr ((c,_),_) = pr c
+ let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c
let pr_glob_tactic_level env n t =
let glob_printers =
@@ -1255,7 +1198,6 @@ module Make
let pr = {
pr_tactic = prtac;
pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
- pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
@@ -1263,7 +1205,9 @@ module Make
pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
- pr_generic = Genprint.generic_glb_print;
+ pr_generic = pr_glb_generic_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
pr_extend = pr_glob_extend_rec
(pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
@@ -1289,15 +1233,11 @@ module Make
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
- let pr_tactic_level env n t =
- let typed_printers =
- (strip_prod_binders_constr)
- in
- let prtac n (t:tactic_expr) =
+ let pr_atomic_tactic_level env n t =
+ let prtac n (t:atomic_tactic_expr) =
let pr = {
- pr_tactic = pr_glob_tactic_level env;
+ pr_tactic = (fun _ _ -> str "<tactic>");
pr_constr = pr_constr_env env Evd.empty;
- pr_uconstr = pr_closed_glob_env env Evd.empty;
pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
pr_lconstr = pr_lconstr_env env Evd.empty;
pr_pattern = pr_constr_pattern_env env Evd.empty;
@@ -1305,19 +1245,13 @@ module Make
pr_constant = pr_evaluable_reference_env env;
pr_reference = pr_located pr_ltac_constant;
pr_name = pr_id;
- pr_generic = Genprint.generic_top_print;
- pr_extend = pr_extend_rec
- (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern;
- pr_alias = pr_alias
- (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern;
+ (** Those are not used by the atomic printer *)
+ pr_generic = (fun _ -> assert false);
+ pr_extend = (fun _ _ _ -> assert false);
+ pr_alias = (fun _ _ _ -> assert false);
}
in
- make_pr_tac
- pr typed_printers
- tag_atomic_tactic_expr tag_tactic_expr
- n t
+ pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
in
prtac n t
@@ -1330,7 +1264,7 @@ module Make
let pr_top_generic env = pr_top_generic_rec
(pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern
+ pr_value pr_constr_pattern
let pr_raw_extend env = pr_raw_extend_rec
pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
@@ -1340,7 +1274,7 @@ module Make
(pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
let check_val_type t arg =
- let AnyArg t = t in
+ let ArgumentType t = t in
(* let t = Genarg.val_tag (Obj.magic t) in *)
(* let Val.Dyn (t', _) = arg in *)
(* match Genarg.Val.eq t t' with *)
@@ -1354,7 +1288,7 @@ module Make
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
+ let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
end
@@ -1384,7 +1318,6 @@ include Make (Ppconstr) (struct
let tag_glob_atomic_tactic_expr = do_not_tag
let tag_raw_tactic_expr = do_not_tag
let tag_raw_atomic_tactic_expr = do_not_tag
- let tag_tactic_expr = do_not_tag
let tag_atomic_tactic_expr = do_not_tag
end)
@@ -1464,16 +1397,10 @@ let () =
let printer _ _ prtac = prtac (0, E) in
declare_extra_genarg_pprule wit_tactic printer printer printer
-let _ = Hook.set Tactic_debug.tactic_printer
- (fun x -> pr_glob_tactic (Global.env()) x)
-
-let _ = Hook.set Tactic_debug.match_pattern_printer
- (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp)
-
-let _ = Hook.set Tactic_debug.match_rule_printer
- (fun rl ->
- pr_match_rule false (pr_glob_tactic (Global.env()))
- (fun (_,p) -> pr_constr_pattern p) rl)
+let () =
+ let pr_unit _ _ _ () = str "()" in
+ let printer _ _ prtac = prtac (0, E) in
+ declare_extra_genarg_pprule wit_ltac printer printer pr_unit
module Richpp = struct
@@ -1488,7 +1415,6 @@ module Richpp = struct
let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
let tag_raw_tactic_expr e = tag (ARawTacticExpr e)
let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a)
- let tag_tactic_expr e = tag (ATacticExpr e)
let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a)
end)
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 2bc64509f0..1608cae751 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -32,7 +32,7 @@ type 'a glob_extra_genarg_printer =
type 'a extra_genarg_printer =
(Term.constr -> std_ppcmds) ->
(Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ (tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
val declare_extra_genarg_pprule :
@@ -48,7 +48,6 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
(** The default pretty-printers produce {!Pp.std_ppcmds} that are
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index c5ec6bb092..d4858bac4f 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -57,7 +57,7 @@ module type Pp = sig
val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
- val pr_tactic : env -> tactic_expr -> std_ppcmds
+ val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
val pr_hintbases : string list option -> std_ppcmds
@@ -67,4 +67,11 @@ module type Pp = sig
('constr -> std_ppcmds) ->
('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+ val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+ val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('b, 'a) match_rule -> std_ppcmds
+
+ val pr_value : tolerability -> Val.t -> std_ppcmds
+
end
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ffec926a84..f0548238a7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -104,12 +104,6 @@ module Make
if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
else id
- let pr_production_item = function
- | 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")"
- | TacTerm s -> qs s
-
let pr_comment pr_c = function
| CommentConstr c -> pr_c c
| CommentString s -> qs s
@@ -378,17 +372,6 @@ module Make
| l -> spc() ++
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
- let print_level n =
- if not (Int.equal n 0) then
- spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")")
- else
- mt ()
-
- let pr_grammar_tactic_rule n (_,pil,t) =
- hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++
- hov 0 (prlist_with_sep sep pr_production_item pil ++
- spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
-
let pr_univs pl =
match pl with
| None -> mt ()
@@ -466,8 +449,6 @@ module Make
keyword "Print TypeClasses"
| PrintInstances qid ->
keyword "Print Instances" ++ spc () ++ pr_smart_global qid
- | PrintLtac qid ->
- keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
| PrintCoercions ->
keyword "Print Coercions"
| PrintCoercionPaths (s,t) ->
@@ -486,8 +467,6 @@ module Make
keyword "Print Hint *"
| PrintHintDbName s ->
keyword "Print HintDb" ++ spc () ++ str s
- | PrintRewriteHintDbName s ->
- keyword "Print Rewrite HintDb" ++ spc() ++ str s
| PrintUniverses (b, fopt) ->
let cmd =
if b then "Print Sorted Universes"
@@ -646,8 +625,6 @@ module Make
return (keyword "No-parsing-rule for VernacError")
(* Syntax *)
- | VernacTacticNotation (n,r,e) ->
- return (pr_grammar_tactic_rule n ("",r,e))
| VernacOpenCloseScope (_,(opening,sc)) ->
return (
keyword (if opening then "Open " else "Close ") ++
@@ -665,7 +642,7 @@ module Make
| VernacBindScope (sc,cll) ->
return (
keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
+ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
)
| VernacArgumentsScope (q,scl) ->
let pr_opt_scope = function
@@ -795,8 +772,8 @@ module Make
hov 0 (
str key ++ spc() ++
(if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
- pr_and_type_binders_arg indpar ++ spc() ++
- Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+ pr_and_type_binders_arg indpar ++
+ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
str" :=") ++ pr_constructor_list k lc ++
prlist (pr_decl_notation pr_constr) ntn
in
@@ -981,24 +958,6 @@ module Make
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
)
(* Solving *)
- | VernacSolve (i,info,tac,deftac) ->
- let pr_goal_selector = function
- | SelectNth i -> int i ++ str":"
- | SelectId id -> pr_id id ++ str":"
- | SelectAll -> str"all" ++ str":"
- | SelectAllParallel -> str"par"
- in
- let pr_info =
- match info with
- | None -> mt ()
- | Some i -> str"Info"++spc()++int i++spc()
- in
- return (
- (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
- pr_info ++
- pr_raw_tactic tac
- ++ (if deftac then str ".." else mt ())
- )
| VernacSolveExistential (i,c) ->
return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
@@ -1030,29 +989,6 @@ module Make
return (keyword "Cd" ++ pr_opt qs s)
(* Commands *)
- | VernacDeclareTacticDefinition l ->
- let pr_tac_body tacdef_body =
- let id, redef, body =
- match tacdef_body with
- | TacticDefinition ((_,id), body) -> pr_id id, false, body
- | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
- in
- let idl, body =
- match body with
- | Tacexpr.TacFun (idl,b) -> idl,b
- | _ -> [], body in
- id ++
- prlist (function None -> str " _"
- | Some id -> spc () ++ pr_id id) idl
- ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
- pr_raw_tactic body
- in
- return (
- hov 1
- (keyword "Ltac" ++ spc () ++
- prlist_with_sep (fun () ->
- fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
- )
| VernacCreateHintDb (dbname,b) ->
return (
hov 1 (keyword "Create HintDb" ++ spc () ++
@@ -1271,22 +1207,15 @@ module Make
with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
try
let rl = Egramml.get_extend_vernac_rule s in
- let start,rl,cl =
- match rl with
- | Egramml.GramTerminal s :: rl -> str s, rl, cl
- | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
- | [] -> anomaly (Pp.str "Empty entry") in
- let (pp,_) =
- List.fold_left
- (fun (strm,args) pi ->
- let pp,args = match pi with
- | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
- | Egramml.GramTerminal s -> (str s, args) in
- (strm ++ spc() ++ pp), args)
- (start,cl) rl in
- hov 1 pp
+ let rec aux rl cl =
+ match rl, cl with
+ | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+ | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+ | [], [] -> []
+ | _ -> assert false in
+ hov 1 (pr_sequence (fun x -> x) (aux rl cl))
with Not_found ->
- hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+ hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
in pr_vernac
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b7b1d67f03..9745a79250 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -218,8 +218,8 @@ let print_polymorphism ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite -> mt ()
- | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+ | Decl_kinds.BiFinite -> str " and has eta conversion"
in
[pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
| _ -> []
diff --git a/printing/printer.ml b/printing/printer.ml
index b89005887f..22bc122bd5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -30,7 +30,8 @@ let delayed_emacs_cmd s =
let get_current_context () =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e ->
- (Evd.empty, Global.env())
+ let env = Global.env () in
+ (Evd.from_env env, env)
(**********************************************************************)
(** Terms *)
@@ -50,7 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t =
let pr_lconstr_env env = pr_lconstr_core false env
let pr_constr_env env = pr_constr_core false env
-let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
+let _ = Hook.set Refine.pr_constr pr_constr_env
let pr_lconstr_goal_style_env env = pr_lconstr_core true env
let pr_constr_goal_style_env env = pr_constr_core true env
@@ -739,18 +740,17 @@ module OrderedContextObject =
struct
type t = context_object
let compare x y =
- match x , y with
- | Variable i1 , Variable i2 -> Id.compare i1 i2
- | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
- | Opaque k1 , Opaque k2 -> con_ord k1 k2
- | Transparent k1 , Transparent k2 -> con_ord k1 k2
- | Axiom _ , Variable _ -> 1
- | Opaque _ , Variable _
- | Opaque _ , Axiom _ -> 1
- | Transparent _ , Variable _
- | Transparent _ , Axiom _
- | Transparent _ , Opaque _ -> 1
- | _ , _ -> -1
+ match x , y with
+ | Variable i1 , Variable i2 -> Id.compare i1 i2
+ | Variable _ , _ -> -1
+ | _ , Variable _ -> 1
+ | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
+ | Axiom _ , _ -> -1
+ | _ , Axiom _ -> 1
+ | Opaque k1 , Opaque k2 -> con_ord k1 k2
+ | Opaque _ , _ -> -1
+ | _ , Opaque _ -> 1
+ | Transparent k1 , Transparent k2 -> con_ord k1 k2
end
module ContextObjectSet = Set.Make (OrderedContextObject)
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d95e190749..5f39f36eab 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -22,4 +22,3 @@ let make_richpp pr ast =
let richpp_vernac = make_richpp RichppVernac.pr_vernac
let richpp_constr = make_richpp RichppConstr.pr_constr_expr
-let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env)
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index 261d22c4c3..c9e84e3eb4 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -34,6 +34,3 @@ val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
val richpp_constr : Constrexpr.constr_expr -> rich_pp
-
-(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *)
-val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:09:58 +0000