aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml11
-rw-r--r--printing/miscprint.ml4
-rw-r--r--printing/ppannotation.ml2
-rw-r--r--printing/ppannotation.mli1
-rw-r--r--printing/ppconstr.ml38
-rw-r--r--printing/pptactic.ml1029
-rw-r--r--printing/pptactic.mli13
-rw-r--r--printing/pptacticsig.mli64
-rw-r--r--printing/ppvernac.ml117
-rw-r--r--printing/prettyp.ml31
-rw-r--r--printing/prettyp.mli2
-rw-r--r--printing/printer.ml90
-rw-r--r--printing/printer.mli13
-rw-r--r--printing/printmod.ml7
-rw-r--r--printing/richprinter.ml1
-rw-r--r--printing/richprinter.mli3
16 files changed, 619 insertions, 807 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index d4f792b753..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 ">");
@@ -40,6 +41,6 @@ let raw_print wit v = (Print.obj wit).raw v
let glb_print wit v = (Print.obj wit).glb v
let top_print wit v = (Print.obj wit).top v
-let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v
-let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v
-let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v
+let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v
+let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v
+let generic_top_print (GenArg (Topwit w, v)) = top_print w v
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 22db3d0bf6..5e86c6bd76 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -33,9 +33,9 @@ and pr_intro_pattern_action prc = function
| IntroRewrite false -> str "<-"
and pr_or_and_intro_pattern prc = function
- | [pl] ->
+ | IntroAndPattern pl ->
str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
- | pll ->
+ | IntroOrPattern pll ->
str "[" ++
hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
++ 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 e21bfa007d..1866ca5042 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
@@ -246,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
@@ -457,7 +455,7 @@ end) = struct
(pr_decl true) dl ++
fnl() ++ keyword "for" ++ spc () ++ pr_id id
- let pr_asin pr (na,indnalopt) =
+ let pr_asin pr na indnalopt =
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
| Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na
| None -> mt ()) ++
@@ -465,8 +463,8 @@ end) = struct
| None -> mt ()
| Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
- let pr_case_item pr (tm,asin) =
- hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
+ let pr_case_item pr (tm,as_clause, in_clause) =
+ hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
let pr_case_type pr po =
match po with
@@ -595,28 +593,20 @@ end) = struct
return (p, lproj)
| CApp (_,(None,a),l) ->
return (pr_app (pr mt) a l, lapp)
- | CRecord (_,w,l) ->
- let beg =
- match w with
- | None ->
- spc ()
- | Some t ->
- spc () ++ pr spc ltop t ++ spc ()
- ++ keyword "with" ++ spc ()
- in
+ | CRecord (_,l) ->
return (
- hv 0 (str"{|" ++ beg ++
+ hv 0 (str"{|" ++ spc () ++
prlist_with_sep pr_semicolon
(fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
++ str" |}"),
latom
)
- | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+ | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
hov 0 (pr_patt ltop p ++
- pr_asin (pr_dangling_with_for mt pr) asin ++
+ pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
str " :=" ++ pr spc ltop c ++
pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
spc () ++ keyword "in" ++ pr spc ltop b)),
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7e903d2d3d..44c832bd7a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -14,6 +14,7 @@ open Util
open Constrexpr
open Tacexpr
open Genarg
+open Geninterp
open Constrarg
open Libnames
open Ppextend
@@ -26,22 +27,20 @@ open Printer
let pr_global x = Nametab.pr_global_env Id.Set.empty x
-type grammar_terminals = string option list
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
type pp_tactic = {
- pptac_args : argument_type list;
- pptac_prods : int * grammar_terminals;
+ pptac_level : int;
+ pptac_prods : grammar_terminals;
}
-(* ML Extensions *)
-let prtac_tab = 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.pptac_args) pt.pptac_prods
-
let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -60,14 +59,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
@@ -93,8 +92,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)
@@ -105,6 +102,39 @@ module Make
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
+ let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+ | None -> false
+ | Some _ -> true
+
+ let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t ->
+ match Val.eq tag t with
+ | None -> assert false
+ | Some Refl -> x
+
+ let rec pr_value lev v : std_ppcmds =
+ if has_type v Val.typ_list then
+ pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
+ else if has_type v Val.typ_opt then
+ pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt)
+ else if has_type v Val.typ_pair then
+ let (v1, v2) = unbox v Val.typ_pair in
+ str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
+ else
+ let Val.Dyn (tag, x) = v in
+ let name = Val.repr tag 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_tag (Topwit wit) with
+ | Val.Base t ->
+ begin match Val.eq t tag with
+ | None -> default
+ | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+ end
+ | _ -> default
+
let pr_with_occurrences pr (occs,c) =
match occs with
| AllOccurrences ->
@@ -263,165 +293,73 @@ 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 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 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)
- | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
- | RedExprArgType ->
- pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
- (out_gen (rawwit wit_red_expr) x)
- | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
- | ConstrWithBindingsArgType ->
- pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
- | BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
- | ListArgType _ ->
- let list_unpacker wit l =
- let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
- pr_sequence map (raw l)
- in
- hov 0 (list_unpack { list_unpacker } x)
- | OptArgType _ ->
- let opt_unpacker wit o = match raw o with
+ 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_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
| None -> mt ()
- | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
- in
- hov 0 (opt_unpack { opt_unpacker } x)
- | PairArgType _ ->
- let pair_unpacker wit1 wit2 o =
- let p, q = raw o in
- let p = in_gen (rawwit wit1) p in
- let q = in_gen (rawwit wit2) q in
- pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
- in
- hov 0 (pair_unpack { pair_unpacker } x)
- | ExtraArgType s ->
- try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> Genprint.generic_raw_print x
-
-
- let rec pr_glb_generic 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 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)
- | QuantHypArgType ->
- pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
- | RedExprArgType ->
- pr_red_expr
- (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
- (out_gen (glbwit wit_red_expr) x)
- | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
- | ConstrWithBindingsArgType ->
- pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
- | BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
- | ListArgType _ ->
- let list_unpacker wit l =
- let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
- pr_sequence map (glb l)
- in
- hov 0 (list_unpack { list_unpacker } x)
- | OptArgType _ ->
- let opt_unpacker wit o = match glb o with
- | None -> mt ()
- | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
- in
- hov 0 (opt_unpack { opt_unpacker } x)
- | PairArgType _ ->
- let pair_unpacker wit1 wit2 o =
- let p, q = glb o in
- let p = in_gen (glbwit wit1) p in
- let q = in_gen (glbwit wit2) q in
- pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
- in
- hov 0 (pair_unpack { pair_unpacker } x)
- | ExtraArgType s ->
- try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> Genprint.generic_glb_print x
-
- let rec pr_top_generic 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 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)
- | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
- | RedExprArgType ->
- pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
- (out_gen (topwit wit_red_expr) x)
- | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
- | ConstrWithBindingsArgType ->
- let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
- pr_with_bindings prc prlc (c,b)
- | BindingsArgType ->
- pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
- | ListArgType _ ->
- let list_unpacker wit l =
- let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
- pr_sequence map (top l)
+ | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
in
- hov 0 (list_unpack { list_unpacker } x)
- | OptArgType _ ->
- let opt_unpacker wit o = match top o with
+ 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_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)
+
+
+ let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
+ match wit with
+ | 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_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
| None -> mt ()
- | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
+ | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
in
- hov 0 (opt_unpack { opt_unpacker } x)
- | PairArgType _ ->
- let pair_unpacker wit1 wit2 o =
- let p, q = top o in
- let p = in_gen (topwit wit1) p in
- let q = in_gen (topwit wit2) q in
- pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
- in
- hov 0 (pair_unpack { pair_unpacker } x)
- | ExtraArgType s ->
- try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
- with Not_found -> Genprint.generic_top_print x
+ 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_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)
let rec tacarg_using_rule_token pr_gen = function
- | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
- | None :: l, a :: al ->
- let r = tacarg_using_rule_token pr_gen (l,al) in
- pr_gen a :: r
- | [], [] -> []
- | _ -> failwith "Inconsistent arguments of extended tactic"
+ | [] -> []
+ | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
+ | TacNonTerm (_, (symb, arg), _) :: l ->
+ pr_gen symb arg :: tacarg_using_rule_token pr_gen l
let pr_tacarg_using_rule pr_gen l =
let l = match l with
- | (Some s :: l, al) ->
+ | TacTerm s :: l ->
(** First terminal token should be considered as the name of the tactic,
so we tag it differently than the other terminal tokens. *)
- primitive s :: (tacarg_using_rule_token pr_gen (l, al))
+ primitive s :: tacarg_using_rule_token pr_gen l
| _ -> tacarg_using_rule_token pr_gen l
in
pr_sequence (fun x -> x) l
- let pr_extend_gen pr_gen lev s l =
- try
- let tags = List.map genarg_tag l in
- let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
- let p = pr_tacarg_using_rule pr_gen (pl,l) in
- if lev' > lev then surround p else p
- with Not_found ->
- let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+ let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+ let name =
+ str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
+ str "@" ++ int i
+ in
let args = match l with
| [] -> mt ()
| _ -> spc() ++ pr_sequence pr_gen l
@@ -431,25 +369,79 @@ module Make
let pr_alias_gen pr_gen lev key l =
try
let pp = KNmap.find key !prnotation_tab 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
+ let rec pack prods args = match prods, args with
+ | [], [] -> []
+ | TacTerm s :: prods, args -> TacTerm s :: pack prods args
+ | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
+ TacNonTerm (loc, (symb, arg), id) :: pack prods args
+ | _ -> raise Not_found
+ in
+ let prods = pack pp.pptac_prods l in
+ let p = pr_tacarg_using_rule pr_gen prods in
+ if pp.pptac_level > lev then surround p else p
with Not_found ->
- KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
-
- let pr_raw_extend prc prlc prtac prpat =
- pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
- let pr_glob_extend prc prlc prtac prpat =
- pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
- let pr_extend prc prlc prtac prpat =
- pr_extend_gen (pr_top_generic prc prlc prtac prpat)
-
- let pr_raw_alias prc prlc prtac prpat =
- pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
- let pr_glob_alias prc prlc prtac prpat =
- pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
- let pr_alias prc prlc prtac prpat =
- pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+ let pr arg = str "_" in
+ KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
+
+ let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg))
+
+ let is_genarg tag wit =
+ let ArgT.Any tag = tag in
+ argument_type_eq (ArgumentType (ExtraArg tag)) wit
+
+ let get_list : type l. l generic_argument -> l generic_argument list option =
+ function (GenArg (wit, arg)) -> match wit with
+ | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg)
+ | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg)
+ | _ -> None
+
+ let get_opt : type l. l generic_argument -> l generic_argument option option =
+ function (GenArg (wit, arg)) -> match wit with
+ | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg)
+ | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
+ | _ -> None
+
+ let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds =
+ fun prtac symb arg -> match symb with
+ | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
+ | Extend.Ulist1 s | Extend.Ulist0 s ->
+ begin match get_list arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> pr_sequence (pr_any_arg prtac s) l
+ end
+ | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
+ begin match get_list arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
+ end
+ | Extend.Uopt s ->
+ begin match get_opt arg with
+ | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | Some l -> pr_opt (pr_any_arg prtac s) l
+ end
+ | Extend.Uentry _ | Extend.Uentryl _ ->
+ str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+ let rec pr_targ prtac symb arg = match symb with
+ | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
+ prtac (1, Any) arg
+ | Extend.Uentryl (_, l) -> prtac (l, Any) arg
+ | _ ->
+ match arg with
+ | TacGeneric arg ->
+ let pr l arg = prtac l (TacGeneric arg) in
+ pr_any_arg pr symb arg
+ | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+
+ let pr_raw_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_farg prtac)
+ let pr_glob_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_farg prtac)
+
+ let pr_raw_alias prc prlc prtac prpat lev key args =
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
+ let pr_glob_alias prc prlc prtac prpat lev key args =
+ pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args
(**********************************************************************)
(* The tactic printer *)
@@ -558,9 +550,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
@@ -573,7 +564,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 ()
@@ -706,20 +697,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)
-
- let string_of_debug = function
- | Off -> ""
- | Debug -> "debug "
- | Info -> "info_"
+ | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
let pr_then () = str ";"
@@ -746,7 +730,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;
@@ -755,13 +738,12 @@ module Make
pr_reference : 'ref -> std_ppcmds;
pr_name : 'nam -> std_ppcmds;
pr_generic : 'lev generic_argument -> std_ppcmds;
- pr_extend : int -> ml_tactic_name -> '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 = <
term :'trm;
- utrm :'utrm;
dterm :'dtrm;
pattern :'pat;
constant :'cst;
@@ -771,306 +753,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"
- | 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 ")"
- )
-
- (* 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
- )
- (* 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
- )
+ (* 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
+ )
- (* 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
- )
+ (* 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
+ )
- (* Constructors *)
- | TacSplit (ev,l) ->
- hov 1 (
- primitive (with_evars ev "exists")
- ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l
- )
+ (* 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
+ )
- (* 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
+ (* 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 (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
- (* 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
- )
- | 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
+ 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
@@ -1228,7 +1150,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)) ->
@@ -1251,26 +1173,17 @@ 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
else str"(" ++ strm ++ str")"
and pr_tacarg = function
- | TacDynamic (loc,t) ->
- pr_with_comments loc
- (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
- | 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 ->
@@ -1298,7 +1211,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;
@@ -1306,8 +1218,8 @@ 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_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+ 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
make_pr_tac
@@ -1319,9 +1231,9 @@ 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 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
@@ -1329,7 +1241,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);
@@ -1337,8 +1248,10 @@ 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_extend = pr_glob_extend
+ 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));
pr_alias = pr_glob_alias
@@ -1363,39 +1276,49 @@ 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_pat_and_constr_expr (pr_glob_constr_env env);
- pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
- pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+ pr_pattern = pr_constr_pattern_env env Evd.empty;
+ pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
+ 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
- (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
- let pr_tactic env = pr_tactic_level env ltop
+ let pr_raw_generic env = pr_raw_generic_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference
+
+ let pr_glb_generic env = pr_glb_generic_rec
+ (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_raw_extend env = pr_raw_extend_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+
+ let pr_glob_extend env = pr_glob_extend_rec
+ (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_alias pr lev key args =
+ pr_alias_gen (fun _ arg -> pr arg) lev key args
+
+ let pr_extend pr lev ml args =
+ pr_extend_gen pr lev ml args
+
+ let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
end
@@ -1425,37 +1348,68 @@ 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)
(** Registering *)
+let run_delayed c =
+ Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+
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 Constrarg.wit_ident
+ pr_id pr_id pr_id;
+ Genprint.register_print0 Constrarg.wit_var
+ (pr_located pr_id) (pr_located pr_id) pr_id;
Genprint.register_print0
Constrarg.wit_intro_pattern
(Miscprint.pr_intro_pattern pr_constr_expr)
(Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
- (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty))));
+ (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
Genprint.register_print0
Constrarg.wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) pr_lident)
(pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
;
- Genprint.register_print0 Constrarg.wit_sort
- pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
+ Genprint.register_print0
+ Constrarg.wit_constr
+ Ppconstr.pr_constr_expr
+ (fun (c, _) -> Printer.pr_glob_constr c)
+ Printer.pr_constr
+ ;
Genprint.register_print0
Constrarg.wit_uconstr
Ppconstr.pr_constr_expr
(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))
+ (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+ Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+ 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 it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+ 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 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;
@@ -1466,16 +1420,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
@@ -1490,7 +1438,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 3134656145..86e3ea5484 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -11,11 +11,15 @@
open Pp
open Genarg
+open Geninterp
open Names
open Constrexpr
open Tacexpr
open Ppextend
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
@@ -32,7 +36,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 :
@@ -41,14 +45,13 @@ val declare_extra_genarg_pprule :
'b glob_extra_genarg_printer ->
'c extra_genarg_printer -> unit
-type grammar_terminals = string option list
+type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
type pp_tactic = {
- pptac_args : argument_type list;
- pptac_prods : int * grammar_terminals;
+ pptac_level : int;
+ pptac_prods : grammar_terminals;
}
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> 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 b2323acba1..4ef2ea9189 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -8,11 +8,10 @@
open Pp
open Genarg
-open Constrexpr
+open Geninterp
open Tacexpr
open Ppextend
open Environ
-open Pattern
open Misctypes
module type Pp = sig
@@ -32,46 +31,22 @@ module type Pp = sig
val pr_clauses : bool option ->
('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
- val pr_raw_generic :
- (constr_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
- std_ppcmds
-
- val pr_glb_generic :
- (glob_constr_and_expr -> Pp.std_ppcmds) ->
- (glob_constr_and_expr -> Pp.std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (glob_constr_pattern_and_expr -> std_ppcmds) ->
- glevel generic_argument -> std_ppcmds
-
- val pr_top_generic :
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (Pattern.constr_pattern -> std_ppcmds) ->
- tlevel generic_argument ->
- std_ppcmds
-
- val pr_raw_extend:
- (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) -> int ->
- ml_tactic_name -> raw_generic_argument list -> std_ppcmds
-
- val pr_glob_extend:
- (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
- ml_tactic_name -> glob_generic_argument list -> std_ppcmds
+
+ val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+ val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+ val pr_raw_extend: env -> int ->
+ ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+ val pr_glob_extend: env -> int ->
+ ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
val pr_extend :
- (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (constr_pattern -> std_ppcmds) -> int ->
- ml_tactic_name -> typed_generic_argument list -> std_ppcmds
+ (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
@@ -81,7 +56,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
@@ -91,4 +66,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 38add9d2c8..10b2bda05e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -79,13 +79,7 @@ module Make
| VernacEndSubproof -> str""
| _ -> str"."
- let pr_gen t =
- pr_raw_generic
- pr_constr_expr
- pr_lconstr_expr
- pr_raw_tactic_level
- pr_constr_expr
- pr_reference t
+ let pr_gen t = pr_raw_generic (Global.env ()) t
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
@@ -105,18 +99,6 @@ module Make
| ETBinder false -> str "closed binder"
| ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
- let strip_meta id =
- let s = Id.to_string id in
- 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,Some (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
| CommentConstr c -> pr_c c
| CommentString s -> qs s
@@ -385,17 +367,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 ()
@@ -473,8 +444,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) ->
@@ -493,8 +462,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"
@@ -641,10 +608,10 @@ module Make
else
spc() ++ qs s
)
- | VernacTime v ->
- return (keyword "Time" ++ spc() ++ pr_vernac_list v)
- | VernacRedirect (s, v) ->
- return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
+ | VernacTime (_,v) ->
+ return (keyword "Time" ++ spc() ++ pr_vernac v)
+ | VernacRedirect (s, (_,v)) ->
+ return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v)
| VernacTimeout(n,v) ->
return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
| VernacFail v ->
@@ -653,8 +620,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 ") ++
@@ -672,7 +637,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
@@ -802,8 +767,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
@@ -988,24 +953,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)
@@ -1037,24 +984,6 @@ module Make
return (keyword "Cd" ++ pr_opt qs s)
(* Commands *)
- | VernacDeclareTacticDefinition (rc,l) ->
- let pr_tac_body (id, redef, body) =
- let idl, body =
- match body with
- | Tacexpr.TacFun (idl,b) -> idl,b
- | _ -> [], body in
- pr_ltac_ref 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 () ++
@@ -1231,8 +1160,6 @@ module Make
(keyword "Comments" ++ spc()
++ prlist_with_sep sep (pr_comment pr_constr) l)
)
- | VernacNop ->
- mt()
(* Toplevel control *)
| VernacToplevelControl exn ->
@@ -1269,33 +1196,21 @@ module Make
| VernacEndSubproof ->
return (str "}")
- and pr_vernac_list l =
- hov 2 (str"[" ++ spc() ++
- prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l
- ++ spc() ++ str"]")
-
and pr_extend s cl =
let pr_arg a =
try pr_gen a
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 4d9d40ae08..9745a79250 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,7 +35,7 @@ type object_pr = {
print_syntactic_def : kernel_name -> std_ppcmds;
print_module : bool -> Names.module_path -> std_ppcmds;
print_modtype : module_path -> std_ppcmds;
- print_named_decl : Id.t * constr option * types -> std_ppcmds;
+ print_named_decl : Context.Named.Declaration.t -> std_ppcmds;
print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
@@ -132,7 +132,8 @@ 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 open Context.Rel.Declaration in
+ let nprods = List.count is_local_assum ctx in
not (List.is_empty impl) && List.length impl >= nprods &&
let _,lastimpl = List.chop nprods impl in
List.exists is_status_implicit lastimpl
@@ -168,8 +169,10 @@ type opacity =
| FullyOpaque
| TransparentMaybeOpacified of Conv_oracle.level
-let opacity env = function
- | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) ->
+let opacity env =
+ let open Context.Named.Declaration in
+ function
+ | VarRef v when is_local_def (Environ.lookup_named v env) ->
Some(TransparentMaybeOpacified
(Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
| ConstRef cst ->
@@ -440,11 +443,13 @@ let print_named_def name body typ =
let print_named_assum name typ =
str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
-let gallina_print_named_decl (id,c,typ) =
- let s = Id.to_string id in
- match c with
- | Some body -> print_named_def s body typ
- | None -> print_named_assum s typ
+let gallina_print_named_decl =
+ let open Context.Named.Declaration in
+ function
+ | LocalAssum (id, typ) ->
+ print_named_assum (Id.to_string id) typ
+ | LocalDef (id, body, typ) ->
+ print_named_def (Id.to_string id) body typ
let assumptions_for_print lna =
List.fold_right (fun na env -> add_name na env) lna empty_names_context
@@ -721,8 +726,8 @@ let print_any_name = function
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,str = repr_qualid qid in
if not (DirPath.is_empty dir) then raise Not_found;
- let (_,c,typ) = Global.lookup_named str in
- (print_named_decl (str,c,typ))
+ let open Context.Named.Declaration in
+ str |> Global.lookup_named |> set_id str |> print_named_decl
with Not_found ->
errorlabstrm
"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
@@ -750,8 +755,8 @@ let print_opaque_name qid =
let ty = Universes.unsafe_type_of_global gr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
- let (_,c,ty) = lookup_named id env in
- print_named_decl (id,c,ty)
+ let open Context.Named.Declaration in
+ lookup_named id env |> set_id id |> print_named_decl
let print_about_any loc k =
match k with
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 6f3556adba..0eab155796 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -66,7 +66,7 @@ type object_pr = {
print_syntactic_def : kernel_name -> std_ppcmds;
print_module : bool -> Names.module_path -> std_ppcmds;
print_modtype : module_path -> std_ppcmds;
- print_named_decl : Id.t * constr option * types -> std_ppcmds;
+ print_named_decl : Context.Named.Declaration.t -> std_ppcmds;
print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds;
diff --git a/printing/printer.ml b/printing/printer.ml
index ac20eeb6f5..cc8da4097d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -48,7 +48,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
@@ -260,16 +260,19 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) =
let ptyp = (str" : " ++ pt) in
(pr_id id ++ hov 0 (pbody ++ ptyp))
-let pr_var_decl env sigma (id,c,typ) =
- pr_var_decl_skel pr_id env sigma (id,c,typ)
+let pr_var_decl env sigma d =
+ pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d)
let pr_var_list_decl env sigma (l,c,typ) =
hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ))
-let pr_rel_decl env sigma (na,c,typ) =
- let pbody = match c with
- | None -> mt ()
- | Some c ->
+let pr_rel_decl env sigma decl =
+ let open Context.Rel.Declaration in
+ let na = get_name decl in
+ let typ = get_type decl in
+ let pbody = match decl with
+ | LocalAssum _ -> mt ()
+ | LocalDef (_,c,_) ->
(* Force evaluation *)
let pb = pr_lconstr_env env sigma c in
let pb = if isCast c then surround pb else pb in
@@ -291,7 +294,7 @@ let pr_named_context_of env sigma =
hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
let pr_named_context env sigma ne_context =
- hv 0 (Context.fold_named_context
+ hv 0 (Context.Named.fold_outside
(fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
ne_context ~init:(mt ()))
@@ -304,7 +307,7 @@ let pr_rel_context_of env sigma =
(* Prints an env (variables and de Bruijn). Separator: newline *)
let pr_context_unlimited env sigma =
let sign_env =
- Context.fold_named_list_context
+ Context.NamedList.fold
(fun d pps ->
let pidt = pr_var_list_decl env sigma d in
(pps ++ fnl () ++ pidt))
@@ -331,7 +334,7 @@ let pr_context_limit n env sigma =
else
let k = lgsign-n in
let _,sign_env =
- Context.fold_named_list_context
+ Context.NamedList.fold
(fun d (i,pps) ->
if i < k then
(i+1, (pps ++str "."))
@@ -414,7 +417,8 @@ let pr_evgl_sign sigma evi =
| None -> [], []
| Some f -> List.filter2 (fun b c -> not b) f (evar_context evi)
in
- let ids = List.rev_map pi1 l in
+ let open Context.Named.Declaration in
+ let ids = List.rev_map get_id l in
let warn =
if List.is_empty ids then mt () else
(str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
@@ -544,7 +548,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
(* Side effect! This has to be made more robust *)
let () =
match close_cmd with
- | Some cmd -> msg_info cmd
+ | Some cmd -> Feedback.msg_info cmd
| None -> ()
in
match goals with
@@ -622,19 +626,19 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
begin match bgoals,shelf,given_up with
| [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
| [] , [] , _ ->
- msg_info (str "No more subgoals, but there are some goals you gave up:");
+ Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
++ fnl () ++ str "You need to go back and solve them."
| [] , _ , _ ->
- msg_info (str "All the remaining goals are on the shelf.");
+ Feedback.msg_info (str "All the remaining goals are on the shelf.");
fnl ()
++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
| _ , _, _ ->
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
@@ -678,35 +682,10 @@ let pr_prim_rule = function
(str"cut " ++ pr_constr t ++
str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
- | FixRule (f,n,[],_) ->
- (str"fix " ++ pr_id f ++ str"/" ++ int n)
-
- | FixRule (f,n,others,j) ->
- if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
- let rec print_mut = function
- | (f,n,ar)::oth ->
- pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
- | [] -> mt () in
- (str"fix " ++ pr_id f ++ str"/" ++ int n ++
- str" with " ++ print_mut others)
-
- | Cofix (f,[],_) ->
- (str"cofix " ++ pr_id f)
-
- | Cofix (f,others,j) ->
- if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
- let rec print_mut = function
- | (f,ar)::oth ->
- (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
- | [] -> mt () in
- (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
| Refine c ->
str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
- | Thin ids ->
- (str"clear " ++ pr_sequence pr_id ids)
-
| Move (id1,id2) ->
(str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
@@ -720,7 +699,7 @@ let prterm = pr_lconstr
type context_object =
| Variable of Id.t (* A section variable or a Let definition *)
- | Axiom of constant * (Label.t * Context.rel_context * types) list
+ | Axiom of constant * (Label.t * Context.Rel.t * types) list
| Opaque of constant (* An opaque constant. *)
| Transparent of constant
@@ -729,18 +708,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)
@@ -771,7 +749,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
@@ -780,7 +758,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/printer.mli b/printing/printer.mli
index 3424c41dc7..70993bb727 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -10,7 +10,6 @@ open Pp
open Names
open Globnames
open Term
-open Context
open Environ
open Pattern
open Evd
@@ -109,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds
val pr_context_unlimited : env -> evar_map -> std_ppcmds
val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds
-val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds
-val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds
+val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
-val pr_named_context : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds
val pr_named_context_of : env -> evar_map -> std_ppcmds
-val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds
val pr_rel_context_of : env -> evar_map -> std_ppcmds
val pr_context_of : env -> evar_map -> std_ppcmds
@@ -165,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *)
type context_object =
| Variable of Id.t (** A section variable or a Let definition *)
(** An axiom and the type it inhabits (if an axiom of the empty type) *)
- | Axiom of constant * (Label.t * Context.rel_context * types) list
+ | Axiom of constant * (Label.t * Context.Rel.t * types) list
| Opaque of constant (** An opaque constant. *)
| Transparent of constant (** A transparent constant *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c154b0aaa0..5f98eeeab9 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -65,7 +65,6 @@ let get_new_id locals id =
(** Inductive declarations *)
-open Termops
open Reduction
let print_params env sigma params =
@@ -89,7 +88,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = extended_rel_list 0 params in
+ let args = Context.Rel.to_extended_list 0 params in
let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args 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
@@ -143,7 +142,7 @@ let print_record env mind mib =
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = extended_rel_list 0 params in
+ let args = Context.Rel.to_extended_list 0 params in
let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
@@ -263,7 +262,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
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-05-03 10:29:32 +0000