summaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml11
-rw-r--r--printing/miscprint.ml6
-rw-r--r--printing/ppannotation.ml2
-rw-r--r--printing/ppannotation.mli1
-rw-r--r--printing/ppconstr.ml109
-rw-r--r--printing/ppconstrsig.mli2
-rw-r--r--printing/pptactic.ml1106
-rw-r--r--printing/pptactic.mli13
-rw-r--r--printing/pptacticsig.mli71
-rw-r--r--printing/pputils.ml8
-rw-r--r--printing/ppvernac.ml1783
-rw-r--r--printing/ppvernacsig.mli3
-rw-r--r--printing/prettyp.ml54
-rw-r--r--printing/prettyp.mli2
-rw-r--r--printing/printer.ml276
-rw-r--r--printing/printer.mli25
-rw-r--r--printing/printing.mllib4
-rw-r--r--printing/printmod.ml32
-rw-r--r--printing/richprinter.ml25
-rw-r--r--printing/richprinter.mli39
20 files changed, 1776 insertions, 1796 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index d4f792b7..0ec35e07 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 22db3d0b..7b2c5695 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -28,14 +28,14 @@ and pr_intro_pattern_action prc = function
| IntroInjection pl ->
str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
str "]"
- | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "/" ++ prc c
+ | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
| IntroRewrite true -> str "->"
| 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 df7f925b..511f9356 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 84724053..a0fef1a7 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 e21bfa00..aa94fb7b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -129,15 +129,13 @@ end) = struct
str "`" ++ str hd ++ c ++ str tl
let pr_com_at n =
- if Flags.do_beautify() && not (Int.equal n 0) then comment n
+ if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
else mt()
let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
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
@@ -151,13 +149,19 @@ end) = struct
| GType [] -> tag_type (str "Type")
| GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
+ let pr_glob_level = function
+ | GProp -> tag_type (str "Prop")
+ | GSet -> tag_type (str "Set")
+ | GType None -> tag_type (str "Type")
+ | GType (Some (_, u)) -> tag_type (str u)
+
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 +186,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 +250,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
@@ -281,6 +285,8 @@ end) = struct
| CPatDelimiters (_,k,p) ->
pr_delimiters k (pr_patt mt lsimplepatt p), 1
+ | CPatCast _ ->
+ assert false
in
let loc = cases_pattern_expr_loc p in
pr_with_comments loc
@@ -300,6 +306,7 @@ end) = struct
let begin_of_binder = function
LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
| LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
+ | LocalPattern(loc,_,_) -> fst (Loc.unloc loc)
| _ -> assert false
let begin_of_binders = function
@@ -348,6 +355,13 @@ end) = struct
| _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
surround (pr_lname na ++ pr_opt_type pr_c topt ++
str":=" ++ cut() ++ pr_c c)
+ | LocalPattern (loc,p,tyo) ->
+ let p = pr_patt lsimplepatt p in
+ match tyo with
+ | None ->
+ str "'" ++ p
+ | Some ty ->
+ str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
let pr_undelimited_binders sep pr_c =
prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -356,13 +370,13 @@ end) = struct
let n = begin_of_binders bl in
match bl with
| [LocalRawAssum (nal,k,t)] ->
- pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
- | LocalRawAssum _ :: _ as bdl ->
- pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
+ kw n ++ pr_binder false pr_c (nal,k,t)
+ | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
+ kw n ++ pr_undelimited_binders sep pr_c bdl
| _ -> assert false
let pr_binders_gen pr_c sep is_open =
- if is_open then pr_delimited_binders mt sep pr_c
+ if is_open then pr_delimited_binders pr_com_at sep pr_c
else pr_undelimited_binders sep pr_c
let rec extract_prod_binders = function
@@ -371,6 +385,11 @@ end) = struct
if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
| CProdN (loc,[],c) ->
extract_prod_binders c
+ | CProdN (loc,[[_,Name id],bk,t],
+ CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+ let bl,c = extract_prod_binders b in
+ LocalPattern (loc,p,None) :: bl, c
| CProdN (loc,(nal,bk,t)::bl,c) ->
let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
LocalRawAssum (nal,bk,t) :: bl, c
@@ -382,6 +401,11 @@ end) = struct
if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
| CLambdaN (loc,[],c) ->
extract_lam_binders c
+ | CLambdaN (loc,[[_,Name id],bk,t],
+ CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+ let bl,c = extract_lam_binders b in
+ LocalPattern (loc,p,None) :: bl, c
| CLambdaN (loc,(nal,bk,t)::bl,c) ->
let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
LocalRawAssum (nal,bk,t) :: bl, c
@@ -432,6 +456,7 @@ end) = struct
let names_of_binder = function
| LocalRawAssum (nal,_,_) -> nal
| LocalRawDef (_,_) -> []
+ | LocalPattern _ -> assert false
in let ids = List.flatten (List.map names_of_binder bl) in
if List.length ids > 1 then
spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
@@ -457,7 +482,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 +490,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
@@ -495,9 +520,14 @@ end) = struct
pr (lapp,L) a ++
prlist (fun a -> spc () ++ pr_expl_args pr a) l)
- let pr_forall () = keyword "forall" ++ spc ()
+ let pr_record_body_gen pr l =
+ spc () ++
+ prlist_with_sep pr_semicolon
+ (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l
- let pr_fun () = keyword "fun" ++ spc ()
+ let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
+
+ let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc ()
let pr_fun_sep = spc () ++ str "=>"
@@ -595,28 +625,17 @@ 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 ++
- prlist_with_sep pr_semicolon
- (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
- ++ str" |}"),
+ hv 0 (str"{|" ++ pr_record_body_gen (pr spc) 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)),
@@ -741,6 +760,8 @@ end) = struct
let pr_cases_pattern_expr = pr_patt ltop
+ let pr_record_body = pr_record_body_gen pr
+
let pr_binders = pr_undelimited_binders spc (pr ltop)
end
@@ -778,6 +799,22 @@ end
let do_not_tag _ x = x
+let split_token tag s =
+ let len = String.length s in
+ let rec parse_string off i =
+ if Int.equal i len then
+ if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
+ else if s.[i] == ' ' then
+ if Int.equal off i then parse_space 1 (succ i)
+ else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
+ else parse_string off (succ i)
+ and parse_space spc i =
+ if Int.equal i len then str (String.make spc ' ')
+ else if s.[i] == ' ' then parse_space (succ spc) (succ i)
+ else str (String.make spc ' ') ++ parse_string i (succ i)
+ in
+ parse_string 0 0
+
(** Instantiating Make with tagging functions that only add style
information. *)
include Make (struct
@@ -786,7 +823,7 @@ include Make (struct
let tag_evar = tag Tag.evar
let tag_type = tag Tag.univ
let tag_unparsing = function
- | UnpTerminal s -> tag Tag.notation
+ | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
| _ -> do_not_tag ()
let tag_constr_expr = do_not_tag
let tag_path = tag Tag.path
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index c711dd8f..3de0d805 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -44,12 +44,14 @@ module type Pp = sig
val pr_qualid : qualid -> std_ppcmds
val pr_patvar : patvar -> std_ppcmds
+ val pr_glob_level : glob_level -> std_ppcmds
val pr_glob_sort : glob_sort -> std_ppcmds
val pr_guard_annot : (constr_expr -> std_ppcmds) ->
local_binder list ->
('a * Names.Id.t) option * recursion_order_expr ->
std_ppcmds
+ val pr_record_body : (reference * constr_expr) list -> std_ppcmds
val pr_binders : local_binder list -> std_ppcmds
val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7e903d2d..fcc30d70 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -9,11 +9,12 @@
open Pp
open Names
open Namegen
-open Errors
+open CErrors
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 ->
@@ -121,7 +151,8 @@ module Make
exception ComplexRedFlag
let pr_short_red_flag pr r =
- if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag
+ if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
+ raise ComplexRedFlag
else if List.is_empty r.rConst then
if r.rDelta then mt () else raise ComplexRedFlag
else (if r.rDelta then str "-" else mt ()) ++
@@ -131,9 +162,12 @@ module Make
try pr_short_red_flag pr r
with complexRedFlags ->
(if r.rBeta then pr_arg str "beta" else mt ()) ++
- (if r.rIota then pr_arg str "iota" else mt ()) ++
- (if r.rZeta then pr_arg str "zeta" else mt ()) ++
- (if List.is_empty r.rConst then
+ (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
+ (if r.rMatch then pr_arg str "match" else mt ()) ++
+ (if r.rFix then pr_arg str "fix" else mt ()) ++
+ (if r.rCofix then pr_arg str "cofix" else mt ())) ++
+ (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+ (if List.is_empty r.rConst then
if r.rDelta then pr_arg str "delta"
else mt ()
else
@@ -150,7 +184,8 @@ module Make
| Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
| Cbv f ->
- if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
+ if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
+ f.rZeta && f.rDelta && List.is_empty f.rConst then
keyword "compute"
else
hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
@@ -184,7 +219,7 @@ module Make
| ConstrContext ((_,id),c) ->
hov 0
(keyword "context" ++ spc () ++ pr_id id ++ spc () ++
- str "[" ++ prlc c ++ str "]")
+ str "[ " ++ prlc c ++ str " ]")
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc c)
| ConstrTerm c when test c ->
@@ -240,8 +275,10 @@ module Make
| NoBindings -> mt ()
let pr_clear_flag clear_flag pp x =
- (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt())
- ++ pp x
+ match clear_flag with
+ | Some false -> surround (pp x)
+ | Some true -> str ">" ++ pp x
+ | None -> pp x
let pr_with_bindings prc prlc (c,bl) =
prc c ++ pr_bindings prc prlc bl
@@ -263,193 +300,177 @@ 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
- | 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
+ 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_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
+ | Some x -> pr_raw_generic_rec 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 = 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)
- 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)
- 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]
+ | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
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
in
str "<" ++ name ++ str ">" ++ args
+ let rec pr_user_symbol = function
+ | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list"
+ | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt"
+ | Extend.Uentry tag ->
+ let ArgT.Any tag = tag in
+ ArgT.repr tag
+ | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+
+ let pr_alias_key key =
+ try
+ let prods = (KNmap.find key !prnotation_tab).pptac_prods in
+ let rec pr = function
+ | TacTerm s -> primitive s
+ | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
+ in
+ pr_sequence pr prods
+ with Not_found ->
+ KerName.print key
+
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 *)
@@ -514,10 +535,9 @@ module Make
let pr_with_induction_names prc = function
| None, None -> mt ()
- | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
- | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat)
+ | Some eqpat, None -> hov 1 (pr_eqn_ipat eqpat)
+ | None, Some ipat -> hov 1 (pr_as_disjunctive_ipat prc ipat)
| Some eqpat, Some ipat ->
- spc () ++
hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
let pr_as_intro_pattern prc ipat =
@@ -559,21 +579,21 @@ module Make
spc() ++ prc c ++ pr_as_ipat prdc ipat
let pr_by_tactic prt = function
- | TacId [] -> mt ()
- | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac
+ | Some tac -> keyword "by" ++ spc () ++ prt tac
+ | None -> mt()
let pr_hyp_location pr_id = function
- | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+ | occs, InHyp -> pr_with_occurrences pr_id occs
| occs, InHypTypeOnly ->
- spc () ++ pr_with_occurrences (fun id ->
+ pr_with_occurrences (fun id ->
str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
) occs
| occs, InHypValueOnly ->
- spc () ++ pr_with_occurrences (fun id ->
+ pr_with_occurrences (fun id ->
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 ()
@@ -583,6 +603,17 @@ module Make
| None -> mt ()
| Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+ let pr_in_clause pr_id = function
+ | { onhyps=None; concl_occs=NoOccurrences } ->
+ (str "* |-")
+ | { onhyps=None; concl_occs=occs } ->
+ (pr_with_occurrences (fun () -> str "*") (occs,()))
+ | { onhyps=Some l; concl_occs=NoOccurrences } ->
+ prlist_with_sep (fun () -> str ", ") (pr_hyp_location pr_id) l
+ | { onhyps=Some l; concl_occs=occs } ->
+ let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
+ (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+
let pr_clauses default_is_concl pr_id = function
| { onhyps=Some []; concl_occs=occs }
when (match default_is_concl with Some true -> true | _ -> false) ->
@@ -599,7 +630,8 @@ module Make
| _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
in
pr_in
- (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs)
+ (prlist_with_sep (fun () -> str",")
+ (fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs)
let pr_orient b = if b then mt () else str "<- "
@@ -610,16 +642,30 @@ module Make
| RepeatStar -> str "?"
| RepeatPlus -> str "!"
- let pr_induction_arg prc prlc = function
+ let pr_core_destruction_arg prc prlc = function
| ElimOnConstr c -> pr_with_bindings prc prlc c
| ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
| ElimOnAnonHyp n -> int n
- let pr_induction_kind = function
+ let pr_destruction_arg prc prlc (clear_flag,h) =
+ pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
+
+ let pr_inversion_kind = function
| SimpleInversion -> primitive "simple inversion"
| FullInversion -> primitive "inversion"
| FullInversionClear -> primitive "inversion_clear"
+ let pr_range_selector (i, j) =
+ if Int.equal i j then int i
+ else int i ++ str "-" ++ int j
+
+ let pr_goal_selector = function
+ | SelectNth i -> int i ++ str ":"
+ | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
+ str "]" ++ str ":"
+ | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+ | SelectAll -> str "all" ++ str ":"
+
let pr_lazy = function
| General -> keyword "multi"
| Select -> keyword "lazy"
@@ -630,9 +676,9 @@ module Make
| Subterm (b,None,a) ->
(** ppedrot: we don't make difference between [appcontext] and [context]
anymore, and the interpretation is governed by a flag instead. *)
- keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
+ keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
| Subterm (b,Some id,a) ->
- keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+ keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
let pr_match_hyps pr_pat = function
| Hyp (nal,mp) ->
@@ -706,20 +752,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 +785,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 +793,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 +808,216 @@ module Make
level :'lev
>
- let make_pr_tac pr strip_prod_binders tag_atom tag =
+ 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 (false,[]) -> primitive "intros"
+ | TacIntroPattern (true,[]) -> primitive "eintros"
+ | t -> str "(" ++ pr_atom1 t ++ str ")"
+ )
+
+ (* Main tactic printer *)
+ and pr_atom1 a = tag_atom a (match a with
+ (* Basic tactics *)
+ | TacIntroPattern (ev,[]) as t ->
+ pr_atom0 t
+ | TacIntroPattern (ev,(_::_ as p)) ->
+ hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++
+ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+ | 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_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) 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)))
+ *)
+
+ (* 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 (h,ids,cl) ->
+ pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++
+ pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
+ pr_opt (pr_clauses None pr.pr_name) cl) l ++
+ pr_opt pr_eliminator el
+ )
- (* 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
+ (* 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
+ )
- 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
+ (* Equality and inversion *)
+ | TacRewrite (ev,l,cl,tac) ->
+ 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
+ ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+ )
+ | TacInversion (DepInversion (k,c,ids),hyp) ->
+ hov 1 (
+ primitive "dependent " ++ pr_inversion_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_inversion_kind k ++ spc ()
+ ++ pr_quantified_hypothesis hyp
+ ++ pr_non_empty_arg (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
- (* Some printing combinators *)
- let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb 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 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"
- | 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
- )
-
- (* 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
- )
-
- (* 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_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
- )
-
- (* 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 rec pr_tac inherited tac =
let return (doc, l) = (tag tac doc, l) in
let (strm, prec) = return (match tac with
@@ -1225,10 +1172,11 @@ module Make
keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacComplete t ->
pr_tac (lcomplete,E) t, lcomplete
+ | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
| 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 +1199,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 ->
@@ -1278,7 +1217,7 @@ module Make
| TacNumgoals ->
keyword "numgoals"
| (TacCall _|Tacexp _ | TacGeneric _) as a ->
- keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+ hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))))
in pr_tac
@@ -1298,7 +1237,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 +1244,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 +1257,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 +1267,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 +1274,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 +1302,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 +1374,77 @@ 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 run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
+ | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g))
+ | clear_flag,ElimOnAnonHyp n as x -> x
+ | clear_flag,ElimOnIdent id as x -> x
+
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 Constrarg.wit_destruction_arg
+ (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
+ (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg 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 +1455,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 +1473,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 31346561..86e3ea54 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 b2323acb..665e055f 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
@@ -30,48 +29,31 @@ module type Pp = sig
val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+ val pr_in_clause :
+ ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
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_key : Names.KerName.t -> std_ppcmds
+
+ val pr_alias : (Val.t -> std_ppcmds) ->
+ int -> Names.KerName.t -> Val.t list -> std_ppcmds
+
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
@@ -81,7 +63,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 +73,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/pputils.ml b/printing/pputils.ml
index 906b463a..50ce56fb 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -9,7 +9,11 @@
open Pp
let pr_located pr (loc, x) =
- if Flags.do_beautify () && loc <> Loc.ghost then
+ if !Flags.beautify && loc <> Loc.ghost then
let (b, e) = Loc.unloc loc in
- Pp.comment b ++ pr x ++ Pp.comment e
+ (* Side-effect: order matters *)
+ let before = Pp.comment (CLexer.extract_comments b) in
+ let x = pr x in
+ let after = Pp.comment (CLexer.extract_comments e) in
+ before ++ x ++ after
else pr x
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d2f59e7b..5d6d36d5 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -9,7 +9,7 @@
open Pp
open Names
-open Errors
+open CErrors
open Util
open Extend
open Vernacexpr
@@ -34,6 +34,8 @@ module Make
let keyword s = tag_keyword (str s)
+ let pr_constr = pr_constr_expr
+ let pr_lconstr = pr_lconstr_expr
let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
let pr_lident (loc,id) =
@@ -79,21 +81,11 @@ 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()
- let pr_ne_sep sep pr = function
- [] -> mt()
- | l -> sep() ++ pr l
-
let pr_set_entry_type = function
| ETName -> str"ident"
| ETReference -> str"global"
@@ -105,18 +97,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
@@ -181,14 +161,22 @@ module Make
| HintsReference r -> pr_reference r
| HintsConstr c -> pr_c c
+ let pr_hint_mode = function
+ | ModeInput -> str"+"
+ | ModeNoHeadEvar -> str"!"
+ | ModeOutput -> str"-"
+
+ let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+ pr_opt (fun x -> str"|" ++ int x) pri ++
+ pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
+
let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
match h with
| HintsResolve l ->
keyword "Resolve " ++ prlist_with_sep sep
- (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++
- match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+ (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
l
| HintsImmediate l ->
keyword "Immediate" ++ spc() ++
@@ -202,8 +190,8 @@ module Make
| HintsMode (m, l) ->
keyword "Mode"
++ spc ()
- ++ pr_reference m ++ spc() ++ prlist_with_sep spc
- (fun b -> if b then str"+" else str"-") l
+ ++ pr_reference m ++ spc() ++
+ prlist_with_sep spc pr_hint_mode l
| HintsConstructors c ->
keyword "Constructors"
++ spc() ++ prlist_with_sep spc pr_reference c
@@ -243,6 +231,11 @@ module Make
| NoInline -> str "[no inline]"
| InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+ let pr_assumption_inline = function
+ | DefaultInline -> str "Inline"
+ | NoInline -> mt ()
+ | InlineAt i -> str "Inline(" ++ int i ++ str ")"
+
let pr_module_ast_inl leading_space pr_c (mast,inl) =
pr_module_ast leading_space pr_c mast ++ pr_inline inl
@@ -272,11 +265,12 @@ module Make
| _ as c -> brk(0,2) ++ str" :" ++ pr_c c
let pr_decl_notation prc ((loc,ntn),c,scopt) =
- fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ prc c ++
+ fnl () ++ keyword "where " ++ qs ntn ++ str " := "
+ ++ Flags.without_option Flags.beautify prc c ++
pr_opt (fun sc -> str ": " ++ str sc) scopt
let pr_binders_arg =
- pr_ne_sep spc pr_binders
+ pr_non_empty_arg pr_binders
let pr_and_type_binders_arg bl =
pr_binders_arg bl
@@ -375,8 +369,9 @@ module Make
| SetAssoc RightA -> keyword "right associativity"
| SetAssoc NonA -> keyword "no associativity"
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
- | SetOnlyParsing Flags.Current -> keyword "only parsing"
- | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
+ | SetOnlyPrinting -> keyword "only printing"
+ | SetOnlyParsing -> keyword "only parsing"
+ | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
| SetFormat("text",s) -> keyword "format " ++ pr_located qs s
| SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
@@ -385,22 +380,19 @@ 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 ()
| Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
+ let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
+ let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
+ let annot = pr_guard_annot pr_lconstr_expr bl ro in
+ pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
+ ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
+ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
+ ++ prlist (pr_decl_notation pr_constr) ntn
+
let pr_statement head (idpl,(bl,c,guard)) =
assert (not (Option.is_empty idpl));
let id, pl = Option.get idpl in
@@ -417,894 +409,843 @@ module Make
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
- let make_pr_vernac pr_constr pr_lconstr =
- let pr_constrarg c = spc () ++ pr_constr c in
- let pr_lconstrarg c = spc () ++ pr_lconstr c in
- let pr_intarg n = spc () ++ int n in
- let pr_oc = function
- None -> str" :"
- | Some true -> str" :>"
- | Some false -> str" :>>"
- in
- let pr_record_field ((x, pri), ntn) =
- let prx = match x with
- | (oc,AssumExpr (id,t)) ->
- hov 1 (pr_lname id ++
- pr_oc oc ++ spc() ++
- pr_lconstr_expr t)
- | (oc,DefExpr(id,b,opt)) -> (match opt with
- | Some t ->
- hov 1 (pr_lname id ++
- pr_oc oc ++ spc() ++
- pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
- | None ->
- hov 1 (pr_lname id ++ str" :=" ++ spc() ++
- pr_lconstr b)) in
- let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
- prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
- in
- let pr_record_decl b c fs =
- pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
- hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
- in
- let pr_printable = function
- | PrintFullContext ->
- keyword "Print All"
- | PrintSectionContext s ->
- keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
- | PrintGrammar ent ->
- keyword "Print Grammar" ++ spc() ++ str ent
- | PrintLoadPath dir ->
- keyword "Print LoadPath" ++ pr_opt pr_dirpath dir
- | PrintModules ->
- keyword "Print Modules"
- | PrintMLLoadPath ->
- keyword "Print ML Path"
- | PrintMLModules ->
- keyword "Print ML Modules"
- | PrintDebugGC ->
- keyword "Print ML GC"
- | PrintGraph ->
- keyword "Print Graph"
- | PrintClasses ->
- keyword "Print Classes"
- | PrintTypeClasses ->
- 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) ->
- keyword "Print Coercion Paths" ++ spc()
- ++ pr_class_rawexpr s ++ spc()
- ++ pr_class_rawexpr t
- | PrintCanonicalConversions ->
- keyword "Print Canonical Structures"
- | PrintTables ->
- keyword "Print Tables"
- | PrintHintGoal ->
- keyword "Print Hint"
- | PrintHint qid ->
- keyword "Print Hint" ++ spc () ++ pr_smart_global qid
- | PrintHintDb ->
- 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"
- else "Print Universes"
+ let pr_constrarg c = spc () ++ pr_constr c
+ let pr_lconstrarg c = spc () ++ pr_lconstr c
+ let pr_intarg n = spc () ++ int n
+
+ let pr_oc = function
+ | None -> str" :"
+ | Some true -> str" :>"
+ | Some false -> str" :>>"
+
+ let pr_record_field ((x, pri), ntn) =
+ let prx = match x with
+ | (oc,AssumExpr (id,t)) ->
+ hov 1 (pr_lname id ++
+ pr_oc oc ++ spc() ++
+ pr_lconstr_expr t)
+ | (oc,DefExpr(id,b,opt)) -> (match opt with
+ | Some t ->
+ hov 1 (pr_lname id ++
+ pr_oc oc ++ spc() ++
+ pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+ | None ->
+ hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+ pr_lconstr b)) in
+ let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
+ prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
+
+ let pr_record_decl b c fs =
+ pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
+ hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+
+ let pr_printable = function
+ | PrintFullContext ->
+ keyword "Print All"
+ | PrintSectionContext s ->
+ keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
+ | PrintGrammar ent ->
+ keyword "Print Grammar" ++ spc() ++ str ent
+ | PrintLoadPath dir ->
+ keyword "Print LoadPath" ++ pr_opt pr_dirpath dir
+ | PrintModules ->
+ keyword "Print Modules"
+ | PrintMLLoadPath ->
+ keyword "Print ML Path"
+ | PrintMLModules ->
+ keyword "Print ML Modules"
+ | PrintDebugGC ->
+ keyword "Print ML GC"
+ | PrintGraph ->
+ keyword "Print Graph"
+ | PrintClasses ->
+ keyword "Print Classes"
+ | PrintTypeClasses ->
+ keyword "Print TypeClasses"
+ | PrintInstances qid ->
+ keyword "Print Instances" ++ spc () ++ pr_smart_global qid
+ | PrintCoercions ->
+ keyword "Print Coercions"
+ | PrintCoercionPaths (s,t) ->
+ keyword "Print Coercion Paths" ++ spc()
+ ++ pr_class_rawexpr s ++ spc()
+ ++ pr_class_rawexpr t
+ | PrintCanonicalConversions ->
+ keyword "Print Canonical Structures"
+ | PrintTables ->
+ keyword "Print Tables"
+ | PrintHintGoal ->
+ keyword "Print Hint"
+ | PrintHint qid ->
+ keyword "Print Hint" ++ spc () ++ pr_smart_global qid
+ | PrintHintDb ->
+ keyword "Print Hint *"
+ | PrintHintDbName s ->
+ keyword "Print HintDb" ++ spc () ++ str s
+ | PrintUniverses (b, fopt) ->
+ let cmd =
+ if b then "Print Sorted Universes"
+ else "Print Universes"
+ in
+ keyword cmd ++ pr_opt str fopt
+ | PrintName qid ->
+ keyword "Print" ++ spc() ++ pr_smart_global qid
+ | PrintModuleType qid ->
+ keyword "Print Module Type" ++ spc() ++ pr_reference qid
+ | PrintModule qid ->
+ keyword "Print Module" ++ spc() ++ pr_reference qid
+ | PrintInspect n ->
+ keyword "Inspect" ++ spc() ++ int n
+ | PrintScopes ->
+ keyword "Print Scopes"
+ | PrintScope s ->
+ keyword "Print Scope" ++ spc() ++ str s
+ | PrintVisibility s ->
+ keyword "Print Visibility" ++ pr_opt str s
+ | PrintAbout (qid,gopt) ->
+ pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+ ++ keyword "About" ++ spc() ++ pr_smart_global qid
+ | PrintImplicit qid ->
+ keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
+ (* spiwack: command printing all the axioms and section variables used in a
+ term *)
+ | PrintAssumptions (b, t, qid) ->
+ let cmd = match b, t with
+ | true, true -> "Print All Dependencies"
+ | true, false -> "Print Opaque Dependencies"
+ | false, true -> "Print Transparent Dependencies"
+ | false, false -> "Print Assumptions"
+ in
+ keyword cmd ++ spc() ++ pr_smart_global qid
+ | PrintNamespace dp ->
+ keyword "Print Namespace" ++ pr_dirpath dp
+ | PrintStrategy None ->
+ keyword "Print Strategies"
+ | PrintStrategy (Some qid) ->
+ keyword "Print Strategy" ++ pr_smart_global qid
+
+ let pr_using e = str (Proof_using.to_string e)
+
+ let rec pr_vernac_body v =
+ let return = Taggers.tag_vernac v in
+ match v with
+ | VernacPolymorphic (poly, v) ->
+ let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
+ return (s ++ spc () ++ pr_vernac_body v)
+ | VernacProgram v ->
+ return (keyword "Program" ++ spc() ++ pr_vernac_body v)
+ | VernacLocal (local, v) ->
+ return (pr_locality local ++ spc() ++ pr_vernac_body v)
+
+ (* Stm *)
+ | VernacStm JoinDocument ->
+ return (keyword "Stm JoinDocument")
+ | VernacStm PrintDag ->
+ return (keyword "Stm PrintDag")
+ | VernacStm Finish ->
+ return (keyword "Stm Finish")
+ | VernacStm Wait ->
+ return (keyword "Stm Wait")
+ | VernacStm (Observe id) ->
+ return (keyword "Stm Observe " ++ str(Stateid.to_string id))
+ | VernacStm (Command v) ->
+ return (keyword "Stm Command " ++ pr_vernac_body v)
+ | VernacStm (PGLast v) ->
+ return (keyword "Stm PGLast " ++ pr_vernac_body v)
+
+ (* Proof management *)
+ | VernacAbortAll ->
+ return (keyword "Abort All")
+ | VernacRestart ->
+ return (keyword "Restart")
+ | VernacUnfocus ->
+ return (keyword "Unfocus")
+ | VernacUnfocused ->
+ return (keyword "Unfocused")
+ | VernacGoal c ->
+ return (keyword "Goal" ++ pr_lconstrarg c)
+ | VernacAbort id ->
+ return (keyword "Abort" ++ pr_opt pr_lident id)
+ | VernacUndo i ->
+ return (
+ if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
+ )
+ | VernacUndoTo i ->
+ return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
+ | VernacBacktrack (i,j,k) ->
+ return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k])
+ | VernacFocus i ->
+ return (keyword "Focus" ++ pr_opt int i)
+ | VernacShow s ->
+ let pr_goal_reference = function
+ | OpenSubgoals -> mt ()
+ | NthGoal n -> spc () ++ int n
+ | GoalId id -> spc () ++ pr_id id
+ | GoalUid n -> spc () ++ str n in
+ let pr_showable = function
+ | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
+ | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
+ | ShowProof -> keyword "Show Proof"
+ | ShowNode -> keyword "Show Node"
+ | ShowScript -> keyword "Show Script"
+ | ShowExistentials -> keyword "Show Existentials"
+ | ShowUniverses -> keyword "Show Universes"
+ | ShowTree -> keyword "Show Tree"
+ | ShowProofNames -> keyword "Show Conjectures"
+ | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
+ | ShowMatch id -> keyword "Show Match " ++ pr_reference id
+ | ShowThesis -> keyword "Show Thesis"
in
- keyword cmd ++ pr_opt str fopt
- | PrintName qid ->
- keyword "Print" ++ spc() ++ pr_smart_global qid
- | PrintModuleType qid ->
- keyword "Print Module Type" ++ spc() ++ pr_reference qid
- | PrintModule qid ->
- keyword "Print Module" ++ spc() ++ pr_reference qid
- | PrintInspect n ->
- keyword "Inspect" ++ spc() ++ int n
- | PrintScopes ->
- keyword "Print Scopes"
- | PrintScope s ->
- keyword "Print Scope" ++ spc() ++ str s
- | PrintVisibility s ->
- keyword "Print Visibility" ++ pr_opt str s
- | PrintAbout (qid,gopt) ->
- pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
- ++ keyword "About" ++ spc() ++ pr_smart_global qid
- | PrintImplicit qid ->
- keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
- (* spiwack: command printing all the axioms and section variables used in a
- term *)
- | PrintAssumptions (b, t, qid) ->
- let cmd = match b, t with
- | true, true -> "Print All Dependencies"
- | true, false -> "Print Opaque Dependencies"
- | false, true -> "Print Transparent Dependencies"
- | false, false -> "Print Assumptions"
+ return (pr_showable s)
+ | VernacCheckGuard ->
+ return (keyword "Guarded")
+
+ (* Resetting *)
+ | VernacResetName id ->
+ return (keyword "Reset" ++ spc() ++ pr_lident id)
+ | VernacResetInitial ->
+ return (keyword "Reset Initial")
+ | VernacBack i ->
+ return (
+ if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
+ )
+ | VernacBackTo i ->
+ return (keyword "BackTo" ++ pr_intarg i)
+
+ (* State management *)
+ | VernacWriteState s ->
+ return (keyword "Write State" ++ spc () ++ qs s)
+ | VernacRestoreState s ->
+ return (keyword "Restore State" ++ spc() ++ qs s)
+
+ (* Control *)
+ | VernacLoad (f,s) ->
+ return (
+ keyword "Load"
+ ++ if f then
+ (spc() ++ keyword "Verbose" ++ spc())
+ else
+ spc() ++ qs s
+ )
+ | VernacTime (_,v) ->
+ return (keyword "Time" ++ spc() ++ pr_vernac_body v)
+ | VernacRedirect (s, (_,v)) ->
+ return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v)
+ | VernacTimeout(n,v) ->
+ return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v)
+ | VernacFail v ->
+ return (keyword "Fail" ++ spc() ++ pr_vernac_body v)
+ | VernacError _ ->
+ return (keyword "No-parsing-rule for VernacError")
+
+ (* Syntax *)
+ | VernacOpenCloseScope (_,(opening,sc)) ->
+ return (
+ keyword (if opening then "Open " else "Close ") ++
+ keyword "Scope" ++ spc() ++ str sc
+ )
+ | VernacDelimiters (sc,Some key) ->
+ return (
+ keyword "Delimit Scope" ++ spc () ++ str sc ++
+ spc() ++ keyword "with" ++ spc () ++ str key
+ )
+ | VernacDelimiters (sc, None) ->
+ return (
+ keyword "Undelimit Scope" ++ spc () ++ str sc
+ )
+ | VernacBindScope (sc,cll) ->
+ return (
+ keyword "Bind Scope" ++ spc () ++ str sc ++
+ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
+ )
+ | VernacArgumentsScope (q,scl) ->
+ let pr_opt_scope = function
+ | None -> str"_"
+ | Some sc -> str sc
in
- keyword cmd ++ spc() ++ pr_smart_global qid
- | PrintNamespace dp ->
- keyword "Print Namespace" ++ pr_dirpath dp
- | PrintStrategy None ->
- keyword "Print Strategies"
- | PrintStrategy (Some qid) ->
- keyword "Print Strategy" ++ pr_smart_global qid
- in
+ return (
+ keyword "Arguments Scope"
+ ++ spc() ++ pr_smart_global q
+ ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
+ )
+ | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+ return (
+ hov 0 (hov 0 (keyword "Infix "
+ ++ qs s ++ str " :=" ++ pr_constrarg q) ++
+ pr_syntax_modifiers mv ++
+ (match sn with
+ | None -> mt()
+ | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
+ )
+ | VernacNotation (_,c,((_,s),l),opt) ->
+ return (
+ hov 2 (keyword "Notation" ++ spc() ++ qs s ++
+ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
+ (match opt with
+ | None -> mt()
+ | Some sc -> str" :" ++ spc() ++ str sc))
+ )
+ | VernacSyntaxExtension (_,(s,l)) ->
+ return (
+ keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
+ pr_syntax_modifiers l
+ )
+ | VernacNotationAddFormat(s,k,v) ->
+ return (
+ keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
+ )
+
+ (* Gallina *)
+ | VernacDefinition (d,id,b) -> (* A verifier... *)
+ let pr_def_token (l,dk) =
+ let l = match l with Some x -> x | None -> Decl_kinds.Global in
+ keyword (Kindops.string_of_definition_kind (l,false,dk))
+ in
+ let pr_reduce = function
+ | None -> mt()
+ | Some r ->
+ keyword "Eval" ++ spc() ++
+ pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
+ keyword " in" ++ spc()
+ in
+ let pr_def_body = function
+ | DefineBody (bl,red,body,d) ->
+ let ty = match d with
+ | None -> mt()
+ | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
+ in
+ (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
+ | ProveBody (bl,t) ->
+ (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
+ let (binds,typ,c) = pr_def_body b in
+ return (
+ hov 2 (
+ pr_def_token d ++ spc()
+ ++ pr_plident id ++ binds ++ typ
+ ++ (match c with
+ | None -> mt()
+ | Some cc -> str" :=" ++ spc() ++ cc))
+ )
+
+ | VernacStartTheoremProof (ki,l,_) ->
+ return (
+ hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
+ prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
+ )
+
+ | VernacEndProof Admitted ->
+ return (keyword "Admitted")
+
+ | VernacEndProof (Proved (opac,o)) -> return (
+ match o with
+ | None -> (match opac with
+ | Transparent -> keyword "Defined"
+ | Opaque None -> keyword "Qed"
+ | Opaque (Some l) ->
+ keyword "Qed" ++ spc() ++ str"export" ++
+ prlist_with_sep (fun () -> str", ") pr_lident l)
+ | Some (id,th) -> (match th with
+ | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+ | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+ )
+ | VernacExactProof c ->
+ return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
+ | VernacAssumption (stre,t,l) ->
+ let n = List.length (List.flatten (List.map fst (List.map snd l))) in
+ let pr_params (c, (xl, t)) =
+ hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
+ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
+ let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+ return (hov 2 (pr_assumption_token (n > 1) stre ++
+ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
+ | VernacInductive (p,f,l) ->
+ let pr_constructor (coe,(id,c)) =
+ hov 2 (pr_lident id ++ str" " ++
+ (if coe then str":>" else str":") ++
+ Flags.without_option Flags.beautify pr_spc_lconstr c)
+ in
+ let pr_constructor_list b l = match l with
+ | Constructors [] -> mt()
+ | Constructors l ->
+ let fst_sep = match l with [_] -> " " | _ -> " | " in
+ pr_com_at (begin_of_inductive l) ++
+ fnl() ++ str fst_sep ++
+ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
+ | RecordDecl (c,fs) ->
+ pr_record_decl b c fs
+ in
+ let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
+ hov 0 (
+ str key ++ spc() ++
+ (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
+ 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
+ let key =
+ let (_,_,_,k,_),_ = List.hd l in
+ match k with Record -> "Record" | Structure -> "Structure"
+ | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+ | Class _ -> "Class" | Variant -> "Variant"
+ in
+ return (
+ hov 1 (pr_oneind key (List.hd l)) ++
+ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+ )
+
+ | VernacFixpoint (local, recs) ->
+ let local = match local with
+ | Some Discharge -> "Let "
+ | Some Local -> "Local "
+ | None | Some Global -> ""
+ in
+ return (
+ hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
+ prlist_with_sep (fun _ -> fnl () ++ keyword "with"
+ ++ spc ()) pr_rec_definition recs)
+ )
+
+ | VernacCoFixpoint (local, corecs) ->
+ let local = match local with
+ | Some Discharge -> keyword "Let" ++ spc ()
+ | Some Local -> keyword "Local" ++ spc ()
+ | None | Some Global -> str ""
+ in
+ let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
+ pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+ spc() ++ pr_lconstr_expr c ++
+ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
+ prlist (pr_decl_notation pr_constr) ntn
+ in
+ return (
+ hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
+ )
+ | VernacScheme l ->
+ return (
+ hov 2 (keyword "Scheme" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
+ )
+ | VernacCombinedScheme (id, l) ->
+ return (
+ hov 2 (keyword "Combined Scheme" ++ spc() ++
+ pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+ )
+ | VernacUniverse v ->
+ return (
+ hov 2 (keyword "Universe" ++ spc () ++
+ prlist_with_sep (fun _ -> str",") pr_lident v)
+ )
+ | VernacConstraint v ->
+ let pr_uconstraint (l, d, r) =
+ pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+ pr_glob_level r
+ in
+ return (
+ hov 2 (keyword "Constraint" ++ spc () ++
+ prlist_with_sep (fun _ -> str",") pr_uconstraint v)
+ )
+
+ (* Gallina extensions *)
+ | VernacBeginSection id ->
+ return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
+ | VernacEndSegment id ->
+ return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
+ | VernacNameSectionHypSet (id,set) ->
+ return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
+ str ":="++spc()++pr_using set))
+ | VernacRequire (from, exp, l) ->
+ let from = match from with
+ | None -> mt ()
+ | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+ in
+ return (
+ hov 2
+ (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
+ prlist_with_sep sep pr_module l)
+ )
+ | VernacImport (f,l) ->
+ return (
+ (if f then keyword "Export" else keyword "Import") ++ spc() ++
+ prlist_with_sep sep pr_import_module l
+ )
+ | VernacCanonical q ->
+ return (
+ keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
+ )
+ | VernacCoercion (_,id,c1,c2) ->
+ return (
+ hov 1 (
+ keyword "Coercion" ++ spc() ++
+ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
+ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
+ )
+ | VernacIdentityCoercion (_,id,c1,c2) ->
+ return (
+ hov 1 (
+ keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
+ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
+ spc() ++ pr_class_rawexpr c2)
+ )
+
+ | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
+ return (
+ hov 1 (
+ (if abst then keyword "Declare" ++ spc () else mt ()) ++
+ keyword "Instance" ++
+ (match instid with
+ | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc ()
+ | (_, Anonymous), _ -> mt ()) ++
+ pr_and_type_binders_arg sup ++
+ str":" ++ spc () ++
+ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
+ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
+ (match props with
+ | Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+ | Some (true,_) -> assert false
+ | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
+ | None -> mt()))
+ )
+
+ | VernacContext l ->
+ return (
+ hov 1 (
+ keyword "Context" ++ pr_and_type_binders_arg l)
+ )
+
+ | VernacDeclareInstances insts ->
+ let pr_inst (id, info) =
+ pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+ in
+ return (
+ hov 1 (keyword "Existing" ++ spc () ++
+ keyword(String.plural (List.length insts) "Instance") ++
+ spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
+ )
+
+ | VernacDeclareClass id ->
+ return (
+ hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
+ )
+
+ (* Modules and Module Types *)
+ | VernacDefineModule (export,m,bl,tys,bd) ->
+ let b = pr_module_binders bl pr_lconstr in
+ return (
+ hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
+ pr_lident m ++ b ++
+ pr_of_module_type pr_lconstr tys ++
+ (if List.is_empty bd then mt () else str ":= ") ++
+ prlist_with_sep (fun () -> str " <+")
+ (pr_module_ast_inl true pr_lconstr) bd)
+ )
+ | VernacDeclareModule (export,id,bl,m1) ->
+ let b = pr_module_binders bl pr_lconstr in
+ return (
+ hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
+ pr_lident id ++ b ++ str " :" ++
+ pr_module_ast_inl true pr_lconstr m1)
+ )
+ | VernacDeclareModuleType (id,bl,tyl,m) ->
+ let b = pr_module_binders bl pr_lconstr in
+ let pr_mt = pr_module_ast_inl true pr_lconstr in
+ return (
+ hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
+ prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
+ (if List.is_empty m then mt () else str ":= ") ++
+ prlist_with_sep (fun () -> str " <+ ") pr_mt m)
+ )
+ | VernacInclude (mexprs) ->
+ let pr_m = pr_module_ast_inl false pr_lconstr in
+ return (
+ hov 2 (keyword "Include" ++ spc() ++
+ prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
+ )
+ (* Solving *)
+ | VernacSolveExistential (i,c) ->
+ return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
+
+ (* Auxiliary file and library management *)
+ | VernacAddLoadPath (fl,s,d) ->
+ return (
+ hov 2
+ (keyword "Add" ++
+ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+ keyword "LoadPath" ++ spc() ++ qs s ++
+ (match d with
+ | None -> mt()
+ | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir))
+ )
+ | VernacRemoveLoadPath s ->
+ return (keyword "Remove LoadPath" ++ qs s)
+ | VernacAddMLPath (fl,s) ->
+ return (
+ keyword "Add"
+ ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
+ ++ keyword "ML Path"
+ ++ qs s
+ )
+ | VernacDeclareMLModule (l) ->
+ return (
+ hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+ )
+ | VernacChdir s ->
+ return (keyword "Cd" ++ pr_opt qs s)
- let pr_using e = str (Proof_using.to_string e) in
-
- let rec pr_vernac v =
- let return = Taggers.tag_vernac v in
- match v with
- | VernacPolymorphic (poly, v) ->
- let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
- return (s ++ pr_vernac v)
- | VernacProgram v ->
- return (keyword "Program" ++ spc() ++ pr_vernac v)
- | VernacLocal (local, v) ->
- return (pr_locality local ++ spc() ++ pr_vernac v)
-
- (* Stm *)
- | VernacStm JoinDocument ->
- return (keyword "Stm JoinDocument")
- | VernacStm PrintDag ->
- return (keyword "Stm PrintDag")
- | VernacStm Finish ->
- return (keyword "Stm Finish")
- | VernacStm Wait ->
- return (keyword "Stm Wait")
- | VernacStm (Observe id) ->
- return (keyword "Stm Observe " ++ str(Stateid.to_string id))
- | VernacStm (Command v) ->
- return (keyword "Stm Command " ++ pr_vernac v)
- | VernacStm (PGLast v) ->
- return (keyword "Stm PGLast " ++ pr_vernac v)
-
- (* Proof management *)
- | VernacAbortAll ->
- return (keyword "Abort All")
- | VernacRestart ->
- return (keyword "Restart")
- | VernacUnfocus ->
- return (keyword "Unfocus")
- | VernacUnfocused ->
- return (keyword "Unfocused")
- | VernacGoal c ->
- return (keyword "Goal" ++ pr_lconstrarg c)
- | VernacAbort id ->
- return (keyword "Abort" ++ pr_opt pr_lident id)
- | VernacUndo i ->
- return (
- if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
- )
- | VernacUndoTo i ->
- return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
- | VernacBacktrack (i,j,k) ->
- return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k])
- | VernacFocus i ->
- return (keyword "Focus" ++ pr_opt int i)
- | VernacShow s ->
- let pr_goal_reference = function
- | OpenSubgoals -> mt ()
- | NthGoal n -> spc () ++ int n
- | GoalId id -> spc () ++ pr_id id
- | GoalUid n -> spc () ++ str n in
- let pr_showable = function
- | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
- | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
- | ShowProof -> keyword "Show Proof"
- | ShowNode -> keyword "Show Node"
- | ShowScript -> keyword "Show Script"
- | ShowExistentials -> keyword "Show Existentials"
- | ShowUniverses -> keyword "Show Universes"
- | ShowTree -> keyword "Show Tree"
- | ShowProofNames -> keyword "Show Conjectures"
- | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
- | ShowMatch id -> keyword "Show Match " ++ pr_lident id
- | ShowThesis -> keyword "Show Thesis"
- in
- return (pr_showable s)
- | VernacCheckGuard ->
- return (keyword "Guarded")
-
- (* Resetting *)
- | VernacResetName id ->
- return (keyword "Reset" ++ spc() ++ pr_lident id)
- | VernacResetInitial ->
- return (keyword "Reset Initial")
- | VernacBack i ->
- return (
- if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
- )
- | VernacBackTo i ->
- return (keyword "BackTo" ++ pr_intarg i)
-
- (* State management *)
- | VernacWriteState s ->
- return (keyword "Write State" ++ spc () ++ qs s)
- | VernacRestoreState s ->
- return (keyword "Restore State" ++ spc() ++ qs s)
-
- (* Control *)
- | VernacLoad (f,s) ->
- return (
- keyword "Load"
- ++ if f then
- (spc() ++ keyword "Verbose" ++ spc())
- 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)
- | VernacTimeout(n,v) ->
- return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
- | VernacFail v ->
- return (keyword "Fail" ++ spc() ++ pr_vernac v)
- | VernacError _ ->
- 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 ") ++
- keyword "Scope" ++ spc() ++ str sc
- )
- | VernacDelimiters (sc,Some key) ->
- return (
- keyword "Delimit Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ str key
- )
- | VernacDelimiters (sc, None) ->
- return (
- keyword "Undelimit Scope" ++ spc () ++ str sc
- )
- | VernacBindScope (sc,cll) ->
- return (
- keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
- )
- | VernacArgumentsScope (q,scl) ->
- let pr_opt_scope = function
- | None -> str"_"
- | Some sc -> str sc
- in
- return (
- keyword "Arguments Scope"
- ++ spc() ++ pr_smart_global q
- ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
- )
- | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
- return (
- hov 0 (hov 0 (keyword "Infix "
- ++ qs s ++ str " :=" ++ pr_constrarg q) ++
- pr_syntax_modifiers mv ++
- (match sn with
- | None -> mt()
- | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
- )
- | VernacNotation (_,c,((_,s),l),opt) ->
- let ps =
- let n = String.length s in
- if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
- then
- let s' = String.sub s 1 (n-2) in
- if String.contains s' '\'' then qs s else str s'
- else qs s
- in
- return (
- hov 2 (keyword "Notation" ++ spc() ++ ps ++
- str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
- (match opt with
- | None -> mt()
- | Some sc -> str" :" ++ spc() ++ str sc))
- )
- | VernacSyntaxExtension (_,(s,l)) ->
- return (
- keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
- pr_syntax_modifiers l
- )
- | VernacNotationAddFormat(s,k,v) ->
- return (
- keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
- )
-
- (* Gallina *)
- | VernacDefinition (d,id,b) -> (* A verifier... *)
- let pr_def_token (l,dk) =
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- keyword (Kindops.string_of_definition_kind (l,false,dk))
- in
- let pr_reduce = function
- | None -> mt()
- | Some r ->
- keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
- keyword " in" ++ spc()
- in
- let pr_def_body = function
- | DefineBody (bl,red,body,d) ->
- let ty = match d with
- | None -> mt()
- | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
+ (* Commands *)
+ | VernacCreateHintDb (dbname,b) ->
+ return (
+ hov 1 (keyword "Create HintDb" ++ spc () ++
+ str dbname ++ (if b then str" discriminated" else mt ()))
+ )
+ | VernacRemoveHints (dbnames, ids) ->
+ return (
+ hov 1 (keyword "Remove Hints" ++ spc () ++
+ prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
+ pr_opt_hintbases dbnames)
+ )
+ | VernacHints (_, dbnames,h) ->
+ return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
+ | VernacSyntacticDefinition (id,(ids,c),_,compat) ->
+ return (
+ hov 2
+ (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
+ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
+ pr_syntax_modifiers
+ (match compat with
+ | None -> []
+ | Some Flags.Current -> [SetOnlyParsing]
+ | Some v -> [SetCompatVersion v]))
+ )
+ | VernacDeclareImplicits (q,[]) ->
+ return (
+ hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q)
+ )
+ | VernacDeclareImplicits (q,impls) ->
+ return (
+ hov 1 (keyword "Implicit Arguments" ++ spc () ++
+ spc() ++ pr_smart_global q ++ spc() ++
+ prlist_with_sep spc (fun imps ->
+ str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
+ impls)
+ )
+ | VernacArguments (q, args, more_implicits, nargs, mods) ->
+ return (
+ hov 2 (
+ keyword "Arguments" ++ spc() ++
+ pr_smart_global q ++
+ let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+ let pr_if b x = if b then x else str "" in
+ let pr_br imp x = match imp with
+ | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
+ | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
+ | Vernacexpr.NotImplicit -> x in
+ let rec print_arguments n l =
+ match n, l with
+ | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
+ | _, [] -> mt()
+ | n, { name = id; recarg_like = k;
+ notation_scope = s;
+ implicit_status = imp } :: tl ->
+ spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+ print_arguments (Option.map pred n) tl
+ in
+ let rec print_implicits = function
+ | [] -> mt ()
+ | (name, impl) :: rest ->
+ spc() ++ pr_br impl (pr_name name) ++ print_implicits rest
in
- (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
- | ProveBody (bl,t) ->
- (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in
- let (binds,typ,c) = pr_def_body b in
- return (
- hov 2 (
- pr_def_token d ++ spc()
- ++ pr_plident id ++ binds ++ typ
- ++ (match c with
- | None -> mt()
- | Some cc -> str" :=" ++ spc() ++ cc))
- )
-
- | VernacStartTheoremProof (ki,l,_) ->
- return (
- hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
- prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
- )
-
- | VernacEndProof Admitted ->
- return (keyword "Admitted")
-
- | VernacEndProof (Proved (opac,o)) -> return (
- match o with
- | None -> (match opac with
- | Transparent -> keyword "Defined"
- | Opaque None -> keyword "Qed"
- | Opaque (Some l) ->
- keyword "Qed" ++ spc() ++ str"export" ++
- prlist_with_sep (fun () -> str", ") pr_lident l)
- | Some (id,th) -> (match th with
- | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
- | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+ print_arguments nargs args ++
+ if not (List.is_empty more_implicits) then
+ prlist (fun l -> str"," ++ print_implicits l) more_implicits
+ else (mt ()) ++
+ (if not (List.is_empty mods) then str" : " else str"") ++
+ prlist_with_sep (fun () -> str", " ++ spc()) (function
+ | `ReductionDontExposeCase -> keyword "simpl nomatch"
+ | `ReductionNeverUnfold -> keyword "simpl never"
+ | `DefaultImplicits -> keyword "default implicits"
+ | `Rename -> keyword "rename"
+ | `Assert -> keyword "assert"
+ | `ExtraScopes -> keyword "extra scopes"
+ | `ClearImplicits -> keyword "clear implicits"
+ | `ClearScopes -> keyword "clear scopes")
+ mods)
+ )
+ | VernacReserve bl ->
+ let n = List.length (List.flatten (List.map fst bl)) in
+ return (
+ hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
+ ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
+ )
+ | VernacGeneralizable g ->
+ return (
+ hov 1 (tag_keyword (
+ str"Generalizable Variable" ++
+ match g with
+ | None -> str "s none"
+ | Some [] -> str "s all"
+ | Some idl ->
+ str (if List.length idl > 1 then "s " else " ") ++
+ prlist_with_sep spc pr_lident idl)
+ ))
+ | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+ return (
+ hov 1 (keyword "Transparent" ++
+ spc() ++ prlist_with_sep sep pr_smart_global l)
)
- | VernacExactProof c ->
- return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
- | VernacAssumption (stre,_,l) ->
- let n = List.length (List.flatten (List.map fst (List.map snd l))) in
- let pr_params (c, (xl, t)) =
- hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
- (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t))
- in
- let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
- return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions))
- | VernacInductive (p,f,l) ->
- let pr_constructor (coe,(id,c)) =
- hov 2 (pr_lident id ++ str" " ++
- (if coe then str":>" else str":") ++
- pr_spc_lconstr c)
- in
- let pr_constructor_list b l = match l with
- | Constructors [] -> mt()
- | Constructors l ->
- let fst_sep = match l with [_] -> " " | _ -> " | " in
- pr_com_at (begin_of_inductive l) ++
- fnl() ++ str fst_sep ++
- prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
- | RecordDecl (c,fs) ->
- pr_record_decl b c fs
- in
- let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
- 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 ++
- str" :=") ++ pr_constructor_list k lc ++
- prlist (pr_decl_notation pr_constr) ntn
- in
- let key =
- let (_,_,_,k,_),_ = List.hd l in
- match k with Record -> "Record" | Structure -> "Structure"
- | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
- | Class _ -> "Class" | Variant -> "Variant"
- in
- return (
- hov 1 (pr_oneind key (List.hd l)) ++
- (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
- )
-
- | VernacFixpoint (local, recs) ->
- let local = match local with
- | Some Discharge -> "Let "
- | Some Local -> "Local "
- | None | Some Global -> ""
- in
- let pr_onerec = function
- | (((loc,id),pl),ro,bl,type_,def),ntn ->
- let annot = pr_guard_annot pr_lconstr_expr bl ro in
- pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
- ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
- ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
- prlist (pr_decl_notation pr_constr) ntn
- in
- return (
- hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
- prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
- )
-
- | VernacCoFixpoint (local, corecs) ->
- let local = match local with
- | Some Discharge -> keyword "Let" ++ spc ()
- | Some Local -> keyword "Local" ++ spc ()
- | None | Some Global -> str ""
- in
- let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
- pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
- spc() ++ pr_lconstr_expr c ++
- pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
- prlist (pr_decl_notation pr_constr) ntn
- in
- return (
- hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
- )
- | VernacScheme l ->
- return (
- hov 2 (keyword "Scheme" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
- )
- | VernacCombinedScheme (id, l) ->
- return (
- hov 2 (keyword "Combined Scheme" ++ spc() ++
- pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
- )
- | VernacUniverse v ->
- return (
- hov 2 (keyword "Universe" ++ spc () ++
- prlist_with_sep (fun _ -> str",") pr_lident v)
- )
- | VernacConstraint v ->
- let pr_uconstraint (l, d, r) =
- pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
- in
- return (
- hov 2 (keyword "Constraint" ++ spc () ++
- prlist_with_sep (fun _ -> str",") pr_uconstraint v)
- )
-
- (* Gallina extensions *)
- | VernacBeginSection id ->
- return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
- | VernacEndSegment id ->
- return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
- | VernacNameSectionHypSet (id,set) ->
- return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
- str ":="++spc()++pr_using set))
- | VernacRequire (from, exp, l) ->
- let from = match from with
- | None -> mt ()
- | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
- in
- return (
- hov 2
- (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
- prlist_with_sep sep pr_module l)
- )
- | VernacImport (f,l) ->
- return (
- (if f then keyword "Export" else keyword "Import") ++ spc() ++
- prlist_with_sep sep pr_import_module l
- )
- | VernacCanonical q ->
- return (
- keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
- )
- | VernacCoercion (_,id,c1,c2) ->
- return (
- hov 1 (
- keyword "Coercion" ++ spc() ++
- pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
- spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
- )
- | VernacIdentityCoercion (_,id,c1,c2) ->
- return (
- hov 1 (
- keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
- spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
- spc() ++ pr_class_rawexpr c2)
- )
-
- | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
- return (
- hov 1 (
- (if abst then keyword "Declare" ++ spc () else mt ()) ++
- keyword "Instance" ++
- (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
- Anonymous -> mt ()) ++
- pr_and_type_binders_arg sup ++
- str":" ++ spc () ++
- pr_constr cl ++ pr_priority pri ++
- (match props with
- | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
- | None -> mt()))
- )
-
- | VernacContext l ->
- return (
- hov 1 (
- keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
- )
-
- | VernacDeclareInstances (ids, pri) ->
- return (
- hov 1 (keyword "Existing" ++ spc () ++
- keyword(String.plural (List.length ids) "Instance") ++
- spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
- )
-
- | VernacDeclareClass id ->
- return (
- hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
- )
-
- (* Modules and Module Types *)
- | VernacDefineModule (export,m,bl,tys,bd) ->
- let b = pr_module_binders bl pr_lconstr in
- return (
- hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
- pr_lident m ++ b ++
- pr_of_module_type pr_lconstr tys ++
- (if List.is_empty bd then mt () else str ":= ") ++
- prlist_with_sep (fun () -> str " <+ ")
- (pr_module_ast_inl true pr_lconstr) bd)
- )
- | VernacDeclareModule (export,id,bl,m1) ->
- let b = pr_module_binders bl pr_lconstr in
- return (
- hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
- pr_lident id ++ b ++
- pr_module_ast_inl true pr_lconstr m1)
- )
- | VernacDeclareModuleType (id,bl,tyl,m) ->
- let b = pr_module_binders bl pr_lconstr in
- let pr_mt = pr_module_ast_inl true pr_lconstr in
- return (
- hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
- prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
- (if List.is_empty m then mt () else str ":= ") ++
- prlist_with_sep (fun () -> str " <+ ") pr_mt m)
- )
- | VernacInclude (mexprs) ->
- let pr_m = pr_module_ast_inl false pr_lconstr in
- return (
- hov 2 (keyword "Include" ++ spc() ++
- 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"
+ | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+ return (
+ hov 1 (keyword "Opaque" ++
+ spc() ++ prlist_with_sep sep pr_smart_global l)
+ )
+ | VernacSetOpacity _ ->
+ return (
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
+ )
+ | VernacSetStrategy l ->
+ let pr_lev = function
+ | Conv_oracle.Opaque -> keyword "opaque"
+ | Conv_oracle.Expand -> keyword "expand"
+ | l when Conv_oracle.is_transparent l -> keyword "transparent"
+ | Conv_oracle.Level n -> int n
in
- let pr_info =
- match info with
- | None -> mt ()
- | Some i -> str"Info"++spc()++int i++spc()
+ let pr_line (l,q) =
+ hov 2 (pr_lev l ++ spc() ++
+ str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
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 ())
+ hov 1 (keyword "Strategy" ++ spc() ++
+ hv 0 (prlist_with_sep sep pr_line l))
+ )
+ | VernacUnsetOption (na) ->
+ return (
+ hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None)
+ )
+ | VernacSetOption (na,v) ->
+ return (
+ hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
+ )
+ | VernacSetAppendOption (na,v) ->
+ return (
+ hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++
+ spc() ++ keyword "Append" ++ spc() ++ qs v)
+ )
+ | VernacAddOption (na,l) ->
+ return (
+ hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
+ )
+ | VernacRemoveOption (na,l) ->
+ return (
+ hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
+ )
+ | VernacMemOption (na,l) ->
+ return (
+ hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
+ )
+ | VernacPrintOption na ->
+ return (
+ hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
+ )
+ | VernacCheckMayEval (r,io,c) ->
+ let pr_mayeval r c = match r with
+ | Some r0 ->
+ hov 2 (keyword "Eval" ++ spc() ++
+ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
+ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
+ | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
+ in
+ let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
+ return (pr_i ++ pr_mayeval r c)
+ | VernacGlobalCheck c ->
+ return (hov 2 (keyword "Type" ++ pr_constrarg c))
+ | VernacDeclareReduction (s,r) ->
+ return (
+ keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
+ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
+ )
+ | VernacPrint p ->
+ return (pr_printable p)
+ | VernacSearch (sea,g,sea_r) ->
+ return (pr_search sea g sea_r pr_constr_pattern_expr)
+ | VernacLocate loc ->
+ let pr_locate =function
+ | LocateAny qid -> pr_smart_global qid
+ | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
+ | LocateFile f -> keyword "File" ++ spc() ++ qs f
+ | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
+ | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
+ | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid
+ in
+ return (keyword "Locate" ++ spc() ++ pr_locate loc)
+ | VernacRegister (id, RegisterInline) ->
+ return (
+ hov 2
+ (keyword "Register Inline" ++ spc() ++ pr_lident id)
+ )
+ | VernacComments l ->
+ return (
+ hov 2
+ (keyword "Comments" ++ spc()
+ ++ prlist_with_sep sep (pr_comment pr_constr) l)
+ )
+
+ (* Toplevel control *)
+ | VernacToplevelControl exn ->
+ return (pr_topcmd exn)
+
+ (* For extension *)
+ | VernacExtend (s,c) ->
+ return (pr_extend s c)
+ | VernacProof (None, None) ->
+ return (keyword "Proof")
+ | VernacProof (None, Some e) ->
+ return (keyword "Proof " ++ spc () ++
+ keyword "using" ++ spc() ++ pr_using e)
+ | VernacProof (Some te, None) ->
+ return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te)
+ | VernacProof (Some te, Some e) ->
+ return (
+ keyword "Proof" ++ spc () ++
+ keyword "using" ++ spc() ++ pr_using e ++ spc() ++
+ keyword "with" ++ spc() ++pr_raw_tactic te
)
- | VernacSolveExistential (i,c) ->
- return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (fl,s,d) ->
- return (
- hov 2
- (keyword "Add" ++
- (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
- keyword "LoadPath" ++ spc() ++ qs s ++
- (match d with
- | None -> mt()
- | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir))
- )
- | VernacRemoveLoadPath s ->
- return (keyword "Remove LoadPath" ++ qs s)
- | VernacAddMLPath (fl,s) ->
- return (
- keyword "Add"
- ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
- ++ keyword "ML Path"
- ++ qs s
- )
- | VernacDeclareMLModule (l) ->
- return (
- hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
- )
- | VernacChdir s ->
- 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 () ++
- str dbname ++ (if b then str" discriminated" else mt ()))
- )
- | VernacRemoveHints (dbnames, ids) ->
- return (
- hov 1 (keyword "Remove Hints" ++ spc () ++
- prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
- pr_opt_hintbases dbnames)
- )
- | VernacHints (_, dbnames,h) ->
- return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
- | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
- return (
- hov 2
- (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
- prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
- pr_syntax_modifiers
- (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
- )
- | VernacDeclareImplicits (q,[]) ->
- return (
- hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q)
- )
- | VernacDeclareImplicits (q,impls) ->
- return (
- hov 1 (keyword "Implicit Arguments" ++ spc () ++
- spc() ++ pr_smart_global q ++ spc() ++
- prlist_with_sep spc (fun imps ->
- str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
- impls)
- )
- | VernacArguments (q, impl, nargs, mods) ->
- return (
- hov 2 (
- keyword "Arguments" ++ spc() ++
- pr_smart_global q ++
- let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
- let pr_if b x = if b then x else str "" in
- let pr_br imp max x = match imp, max with
- | true, false -> str "[" ++ x ++ str "]"
- | true, true -> str "{" ++ x ++ str "}"
- | _ -> x in
- let rec aux n l =
- match n, l with
- | 0, l -> spc () ++ str"/" ++ aux ~-1 l
- | _, [] -> mt()
- | n, (id,k,s,imp,max) :: tl ->
- spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
- aux (n-1) tl in
- prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
- if not (List.is_empty mods) then str" : " else str"" ++
- prlist_with_sep (fun () -> str", " ++ spc()) (function
- | `ReductionDontExposeCase -> keyword "simpl nomatch"
- | `ReductionNeverUnfold -> keyword "simpl never"
- | `DefaultImplicits -> keyword "default implicits"
- | `Rename -> keyword "rename"
- | `Assert -> keyword "assert"
- | `ExtraScopes -> keyword "extra scopes"
- | `ClearImplicits -> keyword "clear implicits"
- | `ClearScopes -> keyword "clear scopes")
- mods)
- )
- | VernacReserve bl ->
- let n = List.length (List.flatten (List.map fst bl)) in
- return (
- hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
- ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
- )
- | VernacGeneralizable g ->
- return (
- hov 1 (tag_keyword (
- str"Generalizable Variable" ++
- match g with
- | None -> str "s none"
- | Some [] -> str "s all"
- | Some idl ->
- str (if List.length idl > 1 then "s " else " ") ++
- prlist_with_sep spc pr_lident idl)
- ))
- | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
- return (
- hov 1 (keyword "Transparent" ++
- spc() ++ prlist_with_sep sep pr_smart_global l)
- )
- | VernacSetOpacity(Conv_oracle.Opaque,l) ->
- return (
- hov 1 (keyword "Opaque" ++
- spc() ++ prlist_with_sep sep pr_smart_global l)
- )
- | VernacSetOpacity _ ->
- return (
- Errors.anomaly (keyword "VernacSetOpacity used to set something else")
- )
- | VernacSetStrategy l ->
- let pr_lev = function
- | Conv_oracle.Opaque -> keyword "opaque"
- | Conv_oracle.Expand -> keyword "expand"
- | l when Conv_oracle.is_transparent l -> keyword "transparent"
- | Conv_oracle.Level n -> int n
- in
- let pr_line (l,q) =
- hov 2 (pr_lev l ++ spc() ++
- str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
- in
- return (
- hov 1 (keyword "Strategy" ++ spc() ++
- hv 0 (prlist_with_sep sep pr_line l))
- )
- | VernacUnsetOption (na) ->
- return (
- hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None)
- )
- | VernacSetOption (na,v) ->
- return (
- hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
- )
- | VernacAddOption (na,l) ->
- return (
- hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacRemoveOption (na,l) ->
- return (
- hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacMemOption (na,l) ->
- return (
- hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacPrintOption na ->
- return (
- hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
- )
- | VernacCheckMayEval (r,io,c) ->
- let pr_mayeval r c = match r with
- | Some r0 ->
- hov 2 (keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
- spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
- | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
- in
- let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
- return (pr_i ++ pr_mayeval r c)
- | VernacGlobalCheck c ->
- return (hov 2 (keyword "Type" ++ pr_constrarg c))
- | VernacDeclareReduction (s,r) ->
- return (
- keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
- pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
- )
- | VernacPrint p ->
- return (pr_printable p)
- | VernacSearch (sea,g,sea_r) ->
- return (pr_search sea g sea_r pr_constr_pattern_expr)
- | VernacLocate loc ->
- let pr_locate =function
- | LocateAny qid -> pr_smart_global qid
- | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
- | LocateFile f -> keyword "File" ++ spc() ++ qs f
- | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
- | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
- | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid
- in
- return (keyword "Locate" ++ spc() ++ pr_locate loc)
- | VernacRegister (id, RegisterInline) ->
- return (
- hov 2
- (keyword "Register Inline" ++ spc() ++ pr_lident id)
- )
- | VernacComments l ->
- return (
- hov 2
- (keyword "Comments" ++ spc()
- ++ prlist_with_sep sep (pr_comment pr_constr) l)
- )
- | VernacNop ->
- mt()
-
- (* Toplevel control *)
- | VernacToplevelControl exn ->
- return (pr_topcmd exn)
-
- (* For extension *)
- | VernacExtend (s,c) ->
- return (pr_extend s c)
- | VernacProof (None, None) ->
- return (keyword "Proof")
- | VernacProof (None, Some e) ->
- return (keyword "Proof " ++ spc () ++
- keyword "using" ++ spc() ++ pr_using e)
- | VernacProof (Some te, None) ->
- return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te)
- | VernacProof (Some te, Some e) ->
- return (
- keyword "Proof" ++ spc () ++
- keyword "using" ++ spc() ++ pr_using e ++ spc() ++
- keyword "with" ++ spc() ++pr_raw_tactic te
- )
- | VernacProofMode s ->
- return (keyword "Proof Mode" ++ str s)
- | VernacBullet b ->
- return (begin match b with
- | Dash n -> str (String.make n '-')
- | Star n -> str (String.make n '*')
- | Plus n -> str (String.make n '+')
- end ++ spc())
- | VernacSubproof None ->
- return (str "{")
- | VernacSubproof (Some i) ->
- return (keyword "BeginSubproof" ++ spc () ++ int i)
- | 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
- with Not_found ->
- hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
-
- in pr_vernac
-
- let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v
-
- let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v
-
- let pr_vernac x =
- try pr_vernac x
- with e -> Errors.print e
+ | VernacProofMode s ->
+ return (keyword "Proof Mode" ++ str s)
+ | VernacBullet b ->
+ return (begin match b with
+ | Dash n -> str (String.make n '-')
+ | Star n -> str (String.make n '*')
+ | Plus n -> str (String.make n '+')
+ end)
+ | VernacSubproof None ->
+ return (str "{")
+ | VernacSubproof (Some i) ->
+ return (keyword "BeginSubproof" ++ spc () ++ int i)
+ | VernacEndSubproof ->
+ return (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 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) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+ let pr_vernac v =
+ try pr_vernac_body v ++ sep_end v
+ with e -> CErrors.print e
end
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
index 5d1c8933..5e5e4bcf 100644
--- a/printing/ppvernacsig.mli
+++ b/printing/ppvernacsig.mli
@@ -8,6 +8,9 @@
module type Pp = sig
+ (** Prints a fixpoint body *)
+ val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
+
(** Prints a vernac expression *)
val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fd51fd6b..e117f1dc 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -11,7 +11,7 @@
*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -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 ->
@@ -212,15 +215,21 @@ let print_polymorphism ref =
else "not universe polymorphic") ]
else []
+let print_type_in_type ref =
+ let unsafe = Global.is_type_in_type ref in
+ if unsafe then
+ [ pr_global ref ++ str " relies on an unsafe universe hierarchy"]
+ else []
+
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 -> str" without eta conversion"
+ | Decl_kinds.BiFinite -> str " with eta conversion"
in
- [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
+ [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
| _ -> []
-
+
let print_primitive ref =
match ref with
| IndRef ind ->
@@ -232,7 +241,7 @@ let print_name_infos ref =
let impls = implicits_of_global ref in
let scopes = Notation.find_arguments_scope ref in
let renames =
- try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in
+ try Arguments_renaming.arguments_names ref with Not_found -> [] in
let type_info_for_implicit =
if need_expansion (select_impargs_size 0 impls) ref then
(* Need to reduce since implicits are computed with products flattened *)
@@ -241,6 +250,7 @@ let print_name_infos ref =
else
[] in
print_polymorphism ref @
+ print_type_in_type ref @
print_primitive ref @
type_info_for_implicit @
print_renames_list (mt()) renames @
@@ -271,7 +281,7 @@ let print_inductive_implicit_args =
let print_inductive_renames =
print_args_data_of_inductive_ids
(fun r ->
- try List.hd (Arguments_renaming.arguments_names r) with Not_found -> [])
+ try Arguments_renaming.arguments_names r with Not_found -> [])
((!=) Anonymous)
print_renames_list
@@ -440,11 +450,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 +733,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 +762,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
@@ -860,7 +872,7 @@ let pr_instance env i =
(* gallina_print_constant_with_infos i.is_impl *)
(* lighter *)
print_ref false (instance_impl i) ++
- begin match instance_priority i with
+ begin match hint_priority i with
| None -> mt ()
| Some i -> spc () ++ str "|" ++ spc () ++ int i
end
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 6f3556ad..0eab1557 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 5ad0e453..04337f6b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -28,9 +28,7 @@ let delayed_emacs_cmd s =
if !Flags.print_emacs then s () else str ""
let get_current_context () =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e ->
- (Evd.empty, Global.env())
+ Pfedit.get_current_context ()
(**********************************************************************)
(** Terms *)
@@ -50,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
@@ -186,7 +184,7 @@ let safe_gen f env sigma c =
let orig_extern_ref = Constrextern.get_extern_reference () in
let extern_ref loc vars r =
try orig_extern_ref loc vars r
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Libnames.Qualid (loc, qualid_of_global env r)
in
Constrextern.set_extern_reference extern_ref;
@@ -194,7 +192,7 @@ let safe_gen f env sigma c =
let p = f env sigma c in
Constrextern.set_extern_reference orig_extern_ref;
p
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Constrextern.set_extern_reference orig_extern_ref;
str "??"
@@ -262,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
@@ -293,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 ()))
@@ -306,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))
@@ -333,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 "."))
@@ -380,16 +381,12 @@ let pr_transparent_state (ids, csts) =
let default_pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
let env = Goal.V82.env sigma g in
- let preamb,thesis,penv,pc =
- mt (), mt (),
- pr_context_of env sigma,
- pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
- in
- preamb ++
- str" " ++ hv 0 (penv ++ fnl () ++
- str (emacs_str "") ++
- str "============================" ++ fnl () ++
- thesis ++ str " " ++ pc)
+ let concl = Goal.V82.concl sigma g in
+ let goal =
+ pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ pr_goal_concl_style_env env sigma concl in
+ str " " ++ v 0 goal
(* display a goal tag *)
let pr_goal_tag g =
@@ -400,7 +397,7 @@ let display_name = false
(* display a goal name *)
let pr_goal_name sigma g =
- if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+ if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
else mt ()
(* display the conclusion of a goal *)
@@ -420,13 +417,23 @@ 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)")
in
let pc = pr_lconstr_env env sigma evi.evar_concl in
- hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn)
+ let candidates =
+ match evi.evar_body, evi.evar_candidates with
+ | Evar_empty, Some l ->
+ spc () ++ str "= {" ++
+ prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}"
+ | _ ->
+ mt ()
+ in
+ hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++
+ candidates ++ spc () ++ warn)
(* Print an existential variable *)
@@ -473,25 +480,91 @@ let default_pr_subgoal n sigma =
let pr_internal_existential_key ev = str (string_of_existential ev)
-let emacs_print_dependent_evars sigma seeds =
+let print_evar_constraints gl sigma =
+ let pr_env =
+ match gl with
+ | None -> fun e' -> pr_context_of e' sigma
+ | Some g ->
+ let env = Goal.V82.env sigma g in fun e' ->
+ begin
+ if Context.Named.equal (named_context env) (named_context e') then
+ if Context.Rel.equal (rel_context env) (rel_context e') then mt ()
+ else pr_rel_context_of e' sigma ++ str " |-" ++ spc ()
+ else pr_context_of e' sigma ++ str " |-" ++ spc ()
+ end
+ in
+ let pr_evconstr (pbty,env,t1,t2) =
+ let t1 = Evarutil.nf_evar sigma t1
+ and t2 = Evarutil.nf_evar sigma t2 in
+ let env =
+ (** We currently allow evar instances to refer to anonymous de Bruijn
+ indices, so we protect the error printing code in this case by giving
+ names to every de Bruijn variable in the rel_context of the conversion
+ problem. MS: we should rather stop depending on anonymous variables, they
+ can be used to indicate independency. Also, this depends on a strategy for
+ naming/renaming *)
+ Namegen.make_all_name_different env in
+ str" " ++
+ hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++
+ str (match pbty with
+ | Reduction.CONV -> "=="
+ | Reduction.CUMUL -> "<=") ++
+ spc () ++ pr_lconstr_env env sigma t2)
+ in
+ let pr_candidate ev evi (candidates,acc) =
+ if Option.has_some evi.evar_candidates then
+ (succ candidates, acc ++ pr_evar sigma (ev,evi) ++ fnl ())
+ else (candidates, acc)
+ in
+ let constraints =
+ let _, cstrs = Evd.extract_all_conv_pbs sigma in
+ if List.is_empty cstrs then mt ()
+ else fnl () ++ str (String.plural (List.length cstrs) "unification constraint")
+ ++ str":" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_evconstr cstrs)
+ in
+ let candidates, ppcandidates = Evd.fold_undefined pr_candidate sigma (0,mt ()) in
+ constraints ++
+ if candidates > 0 then
+ fnl () ++ str (String.plural candidates "existential") ++
+ str" with candidates:" ++ fnl () ++ hov 0 ppcandidates
+ else mt ()
+
+let should_print_dependent_evars = ref false
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "Printing Dependent Evars Line";
+ optkey = ["Printing";"Dependent";"Evars";"Line"];
+ optread = (fun () -> !should_print_dependent_evars);
+ optwrite = (fun v -> should_print_dependent_evars := v) }
+
+let print_dependent_evars gl sigma seeds =
+ let constraints = print_evar_constraints gl sigma in
let evars () =
- let evars = Evarutil.gather_dependent_evars sigma seeds in
- let evars =
- Evar.Map.fold begin fun e i s ->
- let e' = pr_internal_existential_key e in
- match i with
- | None -> s ++ str" " ++ e' ++ str " open,"
- | Some i ->
- s ++ str " " ++ e' ++ str " using " ++
- Evar.Set.fold begin fun d s ->
- pr_internal_existential_key d ++ str " " ++ s
- end i (str ",")
- end evars (str "")
+ if !should_print_dependent_evars then
+ let evars = Evarutil.gather_dependent_evars sigma seeds in
+ let evars =
+ Evar.Map.fold begin fun e i s ->
+ let e' = pr_internal_existential_key e in
+ match i with
+ | None -> s ++ str" " ++ e' ++ str " open,"
+ | Some i ->
+ s ++ str " " ++ e' ++ str " using " ++
+ Evar.Set.fold begin fun d s ->
+ pr_internal_existential_key d ++ str " " ++ s
+ end i (str ",")
+ end evars (str "")
in
fnl () ++
str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
+ else
+ fnl () ++
+ str "(dependent evars: (printing disabled) )" ++ fnl ()
in
- delayed_emacs_cmd evars
+ constraints ++ delayed_emacs_cmd evars
(* Print open subgoals. Checks for uninstantiated existential variables *)
(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
@@ -550,7 +623,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
@@ -559,12 +632,12 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
let exl = Evarutil.non_instantiated sigma in
if Evar.Map.is_empty exl then
(str"No more subgoals."
- ++ emacs_print_dependent_evars sigma seeds)
+ ++ print_dependent_evars None sigma seeds)
else
let pei = pr_evars_int sigma 1 exl in
(str "No more subgoals, but there are non-instantiated existential variables:"
++ fnl () ++ (hov 0 pei)
- ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
+ ++ print_dependent_evars None sigma seeds ++ fnl () ++
str "You can use Grab Existential Variables.")
end
| [g] when not !Flags.print_emacs && pr_first ->
@@ -572,7 +645,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
v 0 (
str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg
- ++ emacs_print_dependent_evars sigma seeds
+ ++ print_dependent_evars (Some g) sigma seeds
)
| g1::rest ->
let goals = print_multiple_goals g1 rest in
@@ -584,7 +657,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
++ pr_goal_tag g1
++ pr_goal_name sigma g1 ++ cut ()
++ goals
- ++ emacs_print_dependent_evars sigma seeds
+ ++ print_dependent_evars (Some g1) sigma seeds
)
(**********************************************************************)
@@ -628,19 +701,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
@@ -684,38 +757,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)
-
(* Backwards compatibility *)
let prterm = pr_lconstr
@@ -724,9 +769,14 @@ let prterm = pr_lconstr
(* Printer function for sets of Assumptions.assumptions.
It is used primarily by the Print Assumptions command. *)
+type axiom =
+ | Constant of constant (* An axiom or a constant. *)
+ | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+ | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+
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 axiom * (Label.t * Context.Rel.t * types) list
| Opaque of constant (* An opaque constant. *)
| Transparent of constant
@@ -734,19 +784,31 @@ type context_object =
module OrderedContextObject =
struct
type t = context_object
+
+ let compare_axiom x y =
+ match x,y with
+ | Constant k1 , Constant k2 ->
+ con_ord k1 k2
+ | Positive m1 , Positive m2 ->
+ MutInd.CanOrd.compare m1 m2
+ | Guarded k1 , Guarded k2 ->
+ con_ord k1 k2
+ | _ , Constant _ -> 1
+ | _ , Positive _ -> 1
+ | _ -> -1
+
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, _) -> compare_axiom 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)
@@ -754,7 +816,7 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
let pr_assumptionset env s =
if ContextObjectMap.is_empty s &&
- engagement env = (PredicativeSet, StratifiedType) then
+ engagement env = PredicativeSet then
str "Closed under the global context"
else
let safe_pr_constant env kn =
@@ -765,28 +827,37 @@ let pr_assumptionset env s =
in
let safe_pr_ltype typ =
try str " : " ++ pr_ltype typ
- with e when Errors.noncritical e -> mt ()
+ with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
let sigma, env = get_current_context () in
let env = Environ.push_rel_context rctx env in
try str " " ++ pr_ltype_env env sigma typ
- with e when Errors.noncritical e -> mt ()
+ with e when CErrors.noncritical e -> mt ()
+ in
+ let pr_axiom env ax typ =
+ match ax with
+ | Constant kn ->
+ safe_pr_constant env kn ++ safe_pr_ltype typ
+ | Positive m ->
+ hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+ | Guarded kn ->
+ hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
in
let fold t typ accu =
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
+ | Axiom (axiom, []) ->
+ let ax = pr_axiom env axiom typ in
(v, ax :: a, o, tr)
- | Axiom (kn,l) ->
- let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++
+ | Axiom (axiom,l) ->
+ let ax = pr_axiom env axiom 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)
@@ -839,4 +910,3 @@ let pr_polymorphic b =
let pr_universe_instance evd ctx =
let inst = Univ.UContext.instance ctx in
str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
-
diff --git a/printing/printer.mli b/printing/printer.mli
index 3424c41d..695ab33b 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
@@ -162,12 +161,16 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *)
(** Declarations for the "Print Assumption" command *)
+type axiom =
+ | Constant of constant (* An axiom or a constant. *)
+ | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+ | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+
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
- | Opaque of constant (** An opaque constant. *)
- | Transparent of constant (** A transparent constant *)
+ | Variable of Id.t (* A section variable or a Let definition *)
+ | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+ | Opaque of constant (* An opaque constant. *)
+ | Transparent of constant
module ContextObjectSet : Set.S with type elt = context_object
module ContextObjectMap : CMap.ExtS
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 652a34fa..bc8f0750 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -2,12 +2,8 @@ Genprint
Pputils
Ppannotation
Ppconstr
-Ppconstrsig
Printer
Pptactic
-Pptacticsig
Printmod
Prettyp
Ppvernac
-Ppvernacsig
-Richprinter
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c154b0aa..dfa66d43 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
@@ -248,22 +247,27 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with
| _ -> raise Not_found
let nametab_register_modparam mbid mtb =
+ let id = MBId.to_id mbid in
match mtb.mod_type with
- | MoreFunctor _ -> () (* functorial param : nothing to register *)
+ | MoreFunctor _ -> id (* functorial param : nothing to register *)
| NoFunctor struc ->
(* We first try to use the algebraic type expression if any,
via a Declaremods function that converts back to module entries *)
try
- Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
- with e when Errors.noncritical e ->
+ let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in
+ id
+ with e when CErrors.noncritical e ->
(* Otherwise, we try to play with the nametab ourselves *)
let mp = MPbound mbid in
- let dir = DirPath.make [MBId.to_id mbid] in
+ let check id = Nametab.exists_dir (DirPath.make [id]) in
+ let id = Namegen.next_ident_away_from id check in
+ let dir = DirPath.make [id] in
nametab_register_dir mp;
- List.iter (nametab_register_body mp dir) struc
+ List.iter (nametab_register_body mp dir) struc;
+ id
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
@@ -296,7 +300,7 @@ let print_body is_impl env mp (l,body) =
try
let env = Option.get env in
pr_mutual_inductive_body env (MutInd.make2 mp l) mib
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let keyword =
let open Decl_kinds in
match mib.mind_finite with
@@ -354,7 +358,7 @@ let print_mod_expr env mp locals = function
let rec print_functor fty fatom is_type env mp locals = function
|NoFunctor me -> fatom is_type env mp locals me
|MoreFunctor (mbid,mtb1,me2) ->
- nametab_register_modparam mbid mtb1;
+ let id = nametab_register_modparam mbid mtb1 in
let mp1 = MPbound mbid in
let pr_mtb1 = fty env mp1 locals mtb1 in
let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
@@ -362,7 +366,7 @@ let rec print_functor fty fatom is_type env mp locals = function
let kwd = if is_type then "Funsig" else "Functor" in
hov 2
(keyword kwd ++ spc () ++
- str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+ str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++
spc() ++ print_functor fty fatom is_type env' mp locals' me2)
let rec print_expression x =
@@ -423,7 +427,7 @@ let print_module with_body mp =
try
if !short then raise ShortPrinting;
unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
unsafe_print_module None mp with_body me ++ fnl ()
let print_modtype kn =
@@ -434,7 +438,7 @@ let print_modtype kn =
(try
if !short then raise ShortPrinting;
print_signature' true (Some (Global.env ())) kn mtb.mod_type
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
print_signature' true None kn mtb.mod_type))
end
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
deleted file mode 100644
index d95e1907..00000000
--- a/printing/richprinter.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-open Richpp
-
-module RichppConstr = Ppconstr.Richpp
-module RichppVernac = Ppvernac.Richpp
-module RichppTactic = Pptactic.Richpp
-
-type rich_pp =
- Ppannotation.t Richpp.located Xml_datatype.gxml
- * Xml_datatype.xml
-
-let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
-
-let make_richpp pr ast =
- let rich_pp =
- rich_pp get_annotations (pr ast)
- in
- let xml = Ppannotation.(
- xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
- )
- in
- (rich_pp, xml)
-
-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
deleted file mode 100644
index 261d22c4..00000000
--- a/printing/richprinter.mli
+++ /dev/null
@@ -1,39 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** This module provides an entry point to "rich" pretty-printers that
- produce pretty-printing as done by {!Printer} but with additional
- annotations represented as a semi-structured document.
-
- To understand what are these annotations and how they are represented
- as standard XML attributes, please refer to {!Ppannotation}.
-
- In addition to these annotations, each node of the semi-structured
- document contains a [startpos] and an [endpos] attribute that
- relate this node to the raw pretty-printing.
- Please refer to {!Richpp} for more details. *)
-
-(** A rich pretty-print is composed of: *)
-type rich_pp =
-
- (** - a generalized semi-structured document whose attributes are
- annotations ; *)
- Ppannotation.t Richpp.located Xml_datatype.gxml
-
- (** - an XML document, representing annotations as usual textual
- XML attributes. *)
- * Xml_datatype.xml
-
-(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
-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.39.1) at 2024-12-28 05:18:39 +0000