aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml12
-rw-r--r--printing/genprint.mli10
-rw-r--r--printing/miscprint.ml27
-rw-r--r--printing/miscprint.mli13
-rw-r--r--printing/ppannotation.ml39
-rw-r--r--printing/ppannotation.mli32
-rw-r--r--printing/ppconstr.ml369
-rw-r--r--printing/ppconstr.mli86
-rw-r--r--printing/ppconstrsig.mli95
-rw-r--r--printing/pptactic.ml1479
-rw-r--r--printing/pptactic.mli67
-rw-r--r--printing/pptacticsig.mli83
-rw-r--r--printing/pputils.ml138
-rw-r--r--printing/pputils.mli18
-rw-r--r--printing/ppvernac.ml158
-rw-r--r--printing/ppvernac.mli15
-rw-r--r--printing/ppvernacsig.mli20
-rw-r--r--printing/prettyp.ml87
-rw-r--r--printing/prettyp.mli9
-rw-r--r--printing/printer.ml375
-rw-r--r--printing/printer.mli58
-rw-r--r--printing/printing.mllib2
-rw-r--r--printing/printmod.ml96
-rw-r--r--printing/printmod.mli5
-rw-r--r--printing/printmodsig.mli17
25 files changed, 880 insertions, 2430 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 56e704b1ef..bb9736d731 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -9,15 +9,17 @@
open Pp
open Genarg
-type ('raw, 'glb, 'top) printer = {
- raw : 'raw -> std_ppcmds;
- glb : 'glb -> std_ppcmds;
- top : 'top -> std_ppcmds;
+type 'a printer = 'a -> std_ppcmds
+
+type ('raw, 'glb, 'top) genprinter = {
+ raw : 'raw printer;
+ glb : 'glb printer;
+ top : 'top printer;
}
module PrintObj =
struct
- type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
+ type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) genprinter
let name = "printer"
let default wit = match wit with
| ExtraArg tag ->
diff --git a/printing/genprint.mli b/printing/genprint.mli
index c8cf2a1174..24779a359d 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -11,6 +11,8 @@
open Pp
open Genarg
+type 'a printer = 'a -> std_ppcmds
+
val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds
(** Printer for raw level generic arguments. *)
@@ -20,9 +22,9 @@ val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds
val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds
(** Printer for top level generic arguments. *)
-val generic_raw_print : rlevel generic_argument -> std_ppcmds
-val generic_glb_print : glevel generic_argument -> std_ppcmds
-val generic_top_print : tlevel generic_argument -> std_ppcmds
+val generic_raw_print : rlevel generic_argument printer
+val generic_glb_print : glevel generic_argument printer
+val generic_top_print : tlevel generic_argument printer
val register_print0 : ('raw, 'glb, 'top) genarg_type ->
- ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit
+ 'raw printer -> 'glb printer -> 'top printer -> unit
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index e40a361494..5d37c8a024 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -28,7 +28,7 @@ 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 "<-"
@@ -47,3 +47,28 @@ let pr_move_location pr_id = function
| MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
| MoveFirst -> str " at top"
| MoveLast -> str " at bottom"
+
+(** Printing of bindings *)
+let pr_binding prc = function
+ | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+ | ImplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence prc l
+ | ExplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+ | ImplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc prc l
+ | ExplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+ hov 1 (prc c ++ pr_bindings prc prlc bl)
+
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index ae73410814..21d410c7b0 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -22,3 +22,16 @@ val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
val pr_move_location :
('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+
+val pr_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_bindings_no_with :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_with_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
+
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
deleted file mode 100644
index c9e83319aa..0000000000
--- a/printing/ppannotation.ml
+++ /dev/null
@@ -1,39 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ppextend
-open Constrexpr
-open Vernacexpr
-open Tacexpr
-
-type t =
- | AKeyword
- | AUnparsing of unparsing
- | AConstrExpr of constr_expr
- | AVernac of vernac_expr
- | AGlobTacticExpr of glob_tactic_expr
- | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
- | ARawTacticExpr of raw_tactic_expr
- | ARawAtomicTacticExpr of raw_atomic_tactic_expr
- | AAtomicTacticExpr of atomic_tactic_expr
-
-let tag_of_annotation = function
- | AKeyword -> "keyword"
- | AUnparsing _ -> "unparsing"
- | AConstrExpr _ -> "constr_expr"
- | AVernac _ -> "vernac_expr"
- | AGlobTacticExpr _ -> "glob_tactic_expr"
- | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
- | ARawTacticExpr _ -> "raw_tactic_expr"
- | ARawAtomicTacticExpr _ -> "raw_atomic_tactic_expr"
- | AAtomicTacticExpr _ -> "atomic_tactic_expr"
-
-let attributes_of_annotation a =
- []
-
-let tag = Pp.Tag.create "ppannotation"
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
deleted file mode 100644
index 58a4618dcd..0000000000
--- a/printing/ppannotation.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** This module defines the annotations that are attached to
- semi-structured pretty-printing of Coq syntactic objects. *)
-
-open Ppextend
-open Constrexpr
-open Vernacexpr
-open Tacexpr
-
-type t =
- | AKeyword
- | AUnparsing of unparsing
- | AConstrExpr of constr_expr
- | AVernac of vernac_expr
- | AGlobTacticExpr of glob_tactic_expr
- | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
- | ARawTacticExpr of raw_tactic_expr
- | ARawAtomicTacticExpr of raw_atomic_tactic_expr
- | AAtomicTacticExpr of atomic_tactic_expr
-
-val tag_of_annotation : t -> string
-
-val attributes_of_annotation : t -> (string * string) list
-
-val tag : t Pp.Tag.key
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 5a65bc9d85..cf513321fb 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -21,18 +21,31 @@ open Decl_kinds
open Misctypes
(*i*)
-module Make (Taggers : sig
- val tag_keyword : std_ppcmds -> std_ppcmds
- val tag_evar : std_ppcmds -> std_ppcmds
- val tag_type : std_ppcmds -> std_ppcmds
- val tag_path : std_ppcmds -> std_ppcmds
- val tag_ref : std_ppcmds -> std_ppcmds
- val tag_var : std_ppcmds -> std_ppcmds
- val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds
- val tag_unparsing : unparsing -> std_ppcmds -> std_ppcmds
-end) = struct
-
- open Taggers
+module Tag =
+struct
+ let keyword = "constr.keyword"
+ let evar = "constr.evar"
+ let univ = "constr.type"
+ let notation = "constr.notation"
+ let variable = "constr.variable"
+ let reference = "constr.reference"
+ let path = "constr.path"
+
+end
+
+let do_not_tag _ x = x
+let tag t s = Pp.tag t s
+let tag_keyword = tag Tag.keyword
+let tag_evar = tag Tag.evar
+let tag_type = tag Tag.univ
+let tag_unparsing = function
+| UnpTerminal s -> tag Tag.notation
+| _ -> do_not_tag ()
+let tag_constr_expr = do_not_tag
+let tag_path = tag Tag.path
+let tag_ref = tag Tag.reference
+let tag_var = tag Tag.variable
+
let keyword s = tag_keyword (str s)
let sep_v = fun _ -> str"," ++ spc()
@@ -67,7 +80,7 @@ end) = struct
| Any -> true
let prec_of_prim_token = function
- | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+ | Numeral (_,b) -> if b then lposint else lnegint
| String _ -> latom
open Notation
@@ -132,14 +145,14 @@ end) = struct
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_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp)
- let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
+ let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
let pr_univ l =
match l with
- | [_,x] -> str x
- | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
+ | [_,x] -> Name.print x
+ | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
@@ -153,7 +166,7 @@ end) = struct
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
| GType None -> tag_type (str "Type")
- | GType (Some (_, u)) -> tag_type (str u)
+ | GType (Some (_, u)) -> tag_type (Name.print u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -178,7 +191,7 @@ end) = struct
tag_type (str "Set")
| GType u ->
(match u with
- | Some (_,u) -> str u
+ | Some (_,u) -> Name.print u
| None -> tag_type (str "Type"))
let pr_universe_instance l =
@@ -195,35 +208,30 @@ end) = struct
match expl with
| None -> pr (lapp,L) a
| Some (_,ExplByPos (n,_id)) ->
- anomaly (Pp.str "Explicitation by position not implemented")
+ anomaly (Pp.str "Explicitation by position not implemented.")
| Some (_,ExplByName id) ->
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
- let pr_opt_type pr = function
- | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
- | t -> cut () ++ str ":" ++ pr t
-
let pr_opt_type_spc pr = function
- | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
+ | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
let pr_lident (loc,id) =
- if not (Loc.is_ghost loc) then
- let (b,_) = Loc.unloc loc in
- pr_located pr_id (Loc.make_loc (b,b + String.length (Id.to_string id)), id)
- else
- pr_id id
+ match loc with
+ | None -> pr_id id
+ | Some loc -> let (b,_) = Loc.unloc loc in
+ pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id
let pr_lname = function
| (loc,Name id) -> pr_lident (loc,id)
- | lna -> pr_located pr_name lna
+ | lna -> pr_located Name.print lna
let pr_or_var pr = function
| ArgArg x -> pr x
| ArgVar (loc,s) -> pr_lident (loc,s)
let pr_prim_token = function
- | Numeral n -> str (Bigint.to_string n)
+ | Numeral (n,s) -> str (if s then n else "-"^n)
| String s -> qs s
let pr_evar pr id l =
@@ -240,73 +248,75 @@ end) = struct
let lpatrec = 0
let rec pr_patt sep inh p =
- let (strm,prec) = match p with
- | CPatRecord (_, l) ->
+ let (strm,prec) = match CAst.(p.v) with
+ | CPatRecord l ->
let pp (c, p) =
pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
in
str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
- | CPatAlias (_, p, id) ->
+ | CPatAlias (p, id) ->
pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
- | CPatCstr (_,c, None, []) ->
+ | CPatCstr (c, None, []) ->
pr_reference c, latom
- | CPatCstr (_, c, None, args) ->
+ | CPatCstr (c, None, args) ->
pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, Some args, []) ->
+ | CPatCstr (c, Some args, []) ->
str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
- | CPatCstr (_, c, Some 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
- | CPatAtom (_, None) ->
+ | CPatAtom (None) ->
str "_", latom
- | CPatAtom (_,Some r) ->
+ | CPatAtom (Some r) ->
pr_reference r, latom
- | CPatOr (_,pl) ->
+ | CPatOr pl ->
hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
- | CPatNotation (_,"( _ )",([p],[]),[]) ->
+ | CPatNotation ("( _ )",([p],[]),[]) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
- | CPatNotation (_,s,(l,ll),args) ->
+ | CPatNotation (s,(l,ll),args) ->
let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in
(if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
- | CPatPrim (_,p) ->
+ | CPatPrim p ->
pr_prim_token p, latom
- | CPatDelimiters (_,k,p) ->
+ | 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
+ let loc = p.CAst.loc in
+ pr_with_comments ?loc
(sep() ++ if prec_less prec inh then strm else surround strm)
let pr_patt = pr_patt mt
- let pr_eqn pr (loc,pl,rhs) =
+ let pr_eqn pr (loc,(pl,rhs)) =
let pl = List.map snd pl in
spc() ++ hov 4
- (pr_with_comments loc
+ (pr_with_comments ?loc
(str "| " ++
hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
++ str " =>") ++
pr_sep_com spc (pr ltop) rhs))
- let begin_of_binder = function
- LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
- | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
- | LocalPattern(loc,_,_) -> fst (Loc.unloc loc)
+ let begin_of_binder l_bi =
+ let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in
+ match l_bi with
+ | CLocalDef((loc,_),_,_) -> b_loc loc
+ | CLocalAssum((loc,_)::_,_,_) -> b_loc loc
+ | CLocalPattern(loc,(_,_)) -> b_loc loc
| _ -> assert false
let begin_of_binders = function
@@ -339,7 +349,7 @@ end) = struct
end
| Default b ->
match t with
- | CHole (_,_,Misctypes.IntroAnonymous,_) ->
+ | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } ->
let s = prlist_with_sep spc pr_lname nal in
hov 1 (surround_implicit b s)
| _ ->
@@ -347,15 +357,13 @@ end) = struct
hov 1 (if many then surround_impl b s else surround_implicit b s)
let pr_binder_among_many pr_c = function
- | LocalRawAssum (nal,k,t) ->
+ | CLocalAssum (nal,k,t) ->
pr_binder true pr_c (nal,k,t)
- | LocalRawDef (na,c) ->
- let c,topt = match c with
- | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t
- | _ -> 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) ->
+ | CLocalDef (na,c,topt) ->
+ surround (pr_lname na ++
+ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
+ str" :=" ++ spc() ++ pr_c c)
+ | CLocalPattern (loc,(p,tyo)) ->
let p = pr_patt lsimplepatt p in
match tyo with
| None ->
@@ -369,9 +377,9 @@ end) = struct
let pr_delimited_binders kw sep pr_c bl =
let n = begin_of_binders bl in
match bl with
- | [LocalRawAssum (nal,k,t)] ->
+ | [CLocalAssum (nal,k,t)] ->
kw n ++ pr_binder false pr_c (nal,k,t)
- | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
+ | (CLocalAssum _ | CLocalPattern _) :: _ as bdl ->
kw n ++ pr_undelimited_binders sep pr_c bdl
| _ -> assert false
@@ -379,43 +387,44 @@ end) = struct
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
+ let rec extract_prod_binders = let open CAst in function
(* | CLetIn (loc,na,b,c) as x ->
let bl,c = extract_prod_binders c in
- if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
- | CProdN (loc,[],c) ->
+ if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
+ | { v = CProdN ([],c) } ->
extract_prod_binders c
- | CProdN (loc,[[_,Name id],bk,t],
- CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ | { loc; v = CProdN ([[_,Name id],bk,t],
+ { v = CCases (LetPatternStyle,None, [{ v = 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
+ CLocalPattern (loc, (p,None)) :: bl, c
+ | { loc; v = CProdN ((nal,bk,t)::bl,c) } ->
+ let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in
+ CLocalAssum (nal,bk,t) :: bl, c
| c -> [], c
- let rec extract_lam_binders = function
+ let rec extract_lam_binders ce = let open CAst in match ce.v with
(* | CLetIn (loc,na,b,c) as x ->
let bl,c = extract_lam_binders c in
- if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
- | CLambdaN (loc,[],c) ->
+ if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
+ | CLambdaN ([],c) ->
extract_lam_binders c
- | CLambdaN (loc,[[_,Name id],bk,t],
- CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ | CLambdaN ([[_,Name id],bk,t],
+ { v = CCases (LetPatternStyle,None, [{ v = 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
- | c -> [], c
-
- let split_lambda = function
- | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
- | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
- | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
- | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+ CLocalPattern (ce.loc,(p,None)) :: bl, c
+ | CLambdaN ((nal,bk,t)::bl,c) ->
+ let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in
+ CLocalAssum (nal,bk,t) :: bl, c
+ | _ -> [], ce
+
+ let split_lambda = CAst.with_loc_val (fun ?loc -> function
+ | CLambdaN ([[na],bk,t],c) -> (na,t,c)
+ | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c))
+ | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c))
+ | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
+ )
let rename na na' t c =
match (na,na') with
@@ -424,12 +433,13 @@ end) = struct
| (_,Name id), (_,Anonymous) -> (na,t,c)
| _ -> (na',t,c)
- let split_product na' = function
- | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
- | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
- | CProdN (loc,(na::nal,bk,t)::bl,c) ->
- rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
- | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+ let split_product na' = CAst.with_loc_val (fun ?loc -> function
+ | CProdN ([[na],bk,t],c) -> rename na na' t c
+ | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c))
+ | CProdN ((na::nal,bk,t)::bl,c) ->
+ rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c))
+ | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
+ )
let rec split_fix n typ def =
if Int.equal n 0 then ([],typ,def)
@@ -437,7 +447,7 @@ end) = struct
let (na,_,def) = split_lambda def in
let (na,t,typ) = split_product na typ in
let (bl,typ,def) = split_fix (n-1) typ def in
- (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
+ (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def)
let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
let pr_body =
@@ -454,9 +464,9 @@ end) = struct
match (ro : Constrexpr.recursion_order_expr) with
| CStructRec ->
let names_of_binder = function
- | LocalRawAssum (nal,_,_) -> nal
- | LocalRawDef (_,_) -> []
- | LocalPattern _ -> assert false
+ | CLocalAssum (nal,_,_) -> nal
+ | CLocalDef (_,_,_) -> []
+ | CLocalPattern _ -> 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"}"
@@ -475,7 +485,7 @@ end) = struct
pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
let pr_recursive pr_decl id = function
- | [] -> anomaly (Pp.str "(co)fixpoint with no definition")
+ | [] -> anomaly (Pp.str "(co)fixpoint with no definition.")
| [d1] -> pr_decl false d1
| dl ->
prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ())
@@ -495,7 +505,7 @@ end) = struct
let pr_case_type pr po =
match po with
- | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt()
+ | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt()
| Some p ->
spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p)
@@ -532,25 +542,25 @@ end) = struct
let pr_fun_sep = spc () ++ str "=>"
let pr_dangling_with_for sep pr inherited a =
- match a with
- | (CFix (_,_,[_])|CCoFix(_,_,[_])) ->
+ match a.CAst.v with
+ | (CFix (_,[_])|CCoFix(_,[_])) ->
pr sep (latom,E) a
| _ ->
pr sep inherited a
let pr pr sep inherited a =
let return (cmds, prec) = (tag_constr_expr a cmds, prec) in
- let (strm, prec) = match a with
+ let (strm, prec) = match CAst.(a.v) with
| CRef (r, us) ->
return (pr_cref r us, latom)
- | CFix (_,id,fix) ->
+ | CFix (id,fix) ->
return (
hov 0 (keyword "fix" ++ spc () ++
pr_recursive
(pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
lfix
)
- | CCoFix (_,id,cofix) ->
+ | CCoFix (id,cofix) ->
return (
hov 0 (keyword "cofix" ++ spc () ++
pr_recursive
@@ -575,7 +585,8 @@ end) = struct
pr_fun_sep ++ pr spc ltop a),
llambda
)
- | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
+ | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])}
+ | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b)
when Id.equal x x' ->
return (
hv 0 (
@@ -585,16 +596,17 @@ end) = struct
pr spc ltop b),
lletin
)
- | CLetIn (_,x,a,b) ->
+ | CLetIn (x,a,t,b) ->
return (
hv 0 (
- hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :="
- ++ pr spc ltop a ++ spc ()
+ hov 2 (keyword "let" ++ spc () ++ pr_lname x
+ ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t
+ ++ str " :=" ++ pr spc ltop a ++ spc ()
++ keyword "in") ++
pr spc ltop b),
lletin
)
- | CAppExpl (_,(Some i,f,us),l) ->
+ | CAppExpl ((Some i,f,us),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
@@ -602,16 +614,16 @@ end) = struct
return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
else
return (p, lproj)
- | CAppExpl (_,(None,Ident (_,var),us),[t])
- | CApp (_,(_,CRef(Ident(_,var),us)),[t,None])
+ | CAppExpl ((None,Ident (_,var),us),[t])
+ | CApp ((_, {CAst.v = CRef(Ident(_,var),us)}),[t,None])
when Id.equal var Notation_ops.ldots_var ->
return (
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
larg
)
- | CAppExpl (_,(None,f,us),l) ->
+ | CAppExpl ((None,f,us),l) ->
return (pr_appexpl (pr mt) (f,us) l, lapp)
- | CApp (_,(Some i,f),l) ->
+ | CApp ((Some i,f),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
assert (Option.is_empty (snd c));
@@ -623,14 +635,14 @@ end) = struct
)
else
return (p, lproj)
- | CApp (_,(None,a),l) ->
+ | CApp ((None,a),l) ->
return (pr_app (pr mt) a l, lapp)
- | CRecord (_,l) ->
+ | CRecord l ->
return (
hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
latom
)
- | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
+ | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
@@ -641,7 +653,7 @@ end) = struct
spc () ++ keyword "in" ++ pr spc ltop b)),
lletpattern
)
- | CCases(_,_,rtntypopt,c,eqns) ->
+ | CCases(_,rtntypopt,c,eqns) ->
return (
v 0
(hv 0 (keyword "match" ++ brk (1,2) ++
@@ -654,7 +666,7 @@ end) = struct
++ keyword "end"),
latom
)
- | CLetTuple (_,nal,(na,po),c,b) ->
+ | CLetTuple (nal,(na,po),c,b) ->
return (
hv 0 (
hov 2 (keyword "let" ++ spc () ++
@@ -667,7 +679,7 @@ end) = struct
pr spc ltop b),
lletin
)
- | CIf (_,c,(na,po),b1,b2) ->
+ | CIf (c,(na,po),b1,b2) ->
(* On force les parenthèses autour d'un "if" sous-terme (même si le
parsing est lui plus tolérant) *)
return (
@@ -681,19 +693,19 @@ end) = struct
lif
)
- | CHole (_,_,Misctypes.IntroIdentifier id,_) ->
+ | CHole (_,Misctypes.IntroIdentifier id,_) ->
return (str "?[" ++ pr_id id ++ str "]", latom)
- | CHole (_,_,Misctypes.IntroFresh id,_) ->
+ | CHole (_,Misctypes.IntroFresh id,_) ->
return (str "?[?" ++ pr_id id ++ str "]", latom)
- | CHole (_,_,_,_) ->
+ | CHole (_,_,_) ->
return (str "_", latom)
- | CEvar (_,n,l) ->
+ | CEvar (n,l) ->
return (pr_evar (pr mt) n l, latom)
- | CPatVar (_,p) ->
- return (str "?" ++ pr_patvar p, latom)
- | CSort (_,s) ->
+ | CPatVar p ->
+ return (str "@?" ++ pr_patvar p, latom)
+ | CSort s ->
return (pr_glob_sort s, latom)
- | CCast (_,a,b) ->
+ | CCast (a,b) ->
return (
hv 0 (pr mt (lcast,L) a ++ spc () ++
match b with
@@ -703,19 +715,19 @@ end) = struct
| CastCoerce -> str ":>"),
lcast
)
- | CNotation (_,"( _ )",([t],[],[])) ->
+ | CNotation ("( _ )",([t],[],[])) ->
return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
- | CNotation (_,s,env) ->
+ | CNotation (s,env) ->
pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env
- | CGeneralization (_,bk,ak,c) ->
+ | CGeneralization (bk,ak,c) ->
return (pr_generalization bk ak (pr mt ltop c), latom)
- | CPrim (_,p) ->
+ | CPrim p ->
return (pr_prim_token p, prec_of_prim_token p)
- | CDelimiters (_,sc,a) ->
+ | CDelimiters (sc,a) ->
return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
in
let loc = constr_loc a in
- pr_with_comments loc
+ pr_with_comments ?loc
(sep() ++ if prec_less prec inherited then strm else surround strm)
type term_pr = {
@@ -739,7 +751,7 @@ end) = struct
let pr prec c = pr prec (transf (Global.env()) c)
let pr_simpleconstr = function
- | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us
+ | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
| c -> pr lsimpleconstr c
let default_term_pr = {
@@ -764,86 +776,3 @@ end) = struct
let pr_binders = pr_undelimited_binders spc (pr ltop)
-end
-
-module Tag =
-struct
- let keyword =
- let style = Terminal.make ~bold:true () in
- Ppstyle.make ~style ["constr"; "keyword"]
-
- let evar =
- let style = Terminal.make ~fg_color:`LIGHT_BLUE () in
- Ppstyle.make ~style ["constr"; "evar"]
-
- let univ =
- let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in
- Ppstyle.make ~style ["constr"; "type"]
-
- let notation =
- let style = Terminal.make ~fg_color:`WHITE () in
- Ppstyle.make ~style ["constr"; "notation"]
-
- let variable =
- Ppstyle.make ["constr"; "variable"]
-
- let reference =
- let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
- Ppstyle.make ~style ["constr"; "reference"]
-
- let path =
- let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in
- Ppstyle.make ~style ["constr"; "path"]
-
-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
- let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
- let tag_keyword = tag Tag.keyword
- let tag_evar = tag Tag.evar
- let tag_type = tag Tag.univ
- let tag_unparsing = function
- | 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
- let tag_ref = tag Tag.reference
- let tag_var = tag Tag.variable
-end)
-
-module Richpp = struct
-
- include Make (struct
- open Ppannotation
- let tag_keyword = Pp.tag (Pp.Tag.inj AKeyword tag)
- let tag_type = Pp.tag (Pp.Tag.inj AKeyword tag)
- let tag_evar = do_not_tag ()
- let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag)
- let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag)
- let tag_path = do_not_tag ()
- let tag_ref = do_not_tag ()
- let tag_var = do_not_tag ()
- end)
-
-end
-
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index b0a5844dbb..fd232759ef 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -11,11 +11,85 @@
(** The default pretty-printers produce {!Pp.std_ppcmds} that are
interpreted as raw strings. *)
-include Ppconstrsig.Pp
+open Loc
+open Pp
+open Libnames
+open Constrexpr
+open Names
+open Misctypes
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as annotated strings. The annotations can be
- retrieved using {!RichPp.rich_pp}. Their definitions are
- located in {!Ppannotation.t}. *)
+val extract_lam_binders :
+ constr_expr -> local_binder_expr list * constr_expr
+val extract_prod_binders :
+ constr_expr -> local_binder_expr list * constr_expr
+val split_fix :
+ int -> constr_expr -> constr_expr ->
+ local_binder_expr list * constr_expr * constr_expr
-module Richpp : Ppconstrsig.Pp
+val prec_less : int -> int * Ppextend.parenRelation -> bool
+
+val pr_tight_coma : unit -> std_ppcmds
+
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+
+val pr_lident : Id.t located -> std_ppcmds
+val pr_lname : Name.t located -> std_ppcmds
+
+val pr_with_comments : ?loc:Loc.t -> std_ppcmds -> std_ppcmds
+val pr_com_at : int -> std_ppcmds
+val pr_sep_com :
+ (unit -> std_ppcmds) ->
+ (constr_expr -> std_ppcmds) ->
+ constr_expr -> std_ppcmds
+
+val pr_id : Id.t -> std_ppcmds
+val pr_name : Name.t -> std_ppcmds
+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_expr 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_expr list -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_constr_expr : constr_expr -> std_ppcmds
+val pr_lconstr_expr : constr_expr -> std_ppcmds
+val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+
+type term_pr = {
+ pr_constr_expr : constr_expr -> std_ppcmds;
+ pr_lconstr_expr : constr_expr -> std_ppcmds;
+ pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+}
+
+val set_term_pr : term_pr -> unit
+val default_term_pr : term_pr
+
+(* The modular constr printer.
+ [modular_constr_pr pr s p t] prints the head of the term [t] and calls
+ [pr] on its subterms.
+ [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
+ and [ltop] for "lconstr" printers (spiwack: we might need more
+ specification here).
+ We can make a new modular constr printer by overriding certain branches,
+ for instance if we want to build a printer which prints "Prop" as "Omega"
+ instead we can proceed as follows:
+ let my_modular_constr_pr pr s p = function
+ | CSort (_,GProp Null) -> str "Omega"
+ | t -> modular_constr_pr pr s p t
+ Which has the same type. We can turn a modular printer into a printer by
+ taking its fixpoint. *)
+
+type precedence
+val lsimpleconstr : precedence
+val ltop : precedence
+val modular_constr_pr :
+ ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
+ (unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
deleted file mode 100644
index 48a02db823..0000000000
--- a/printing/ppconstrsig.mli
+++ /dev/null
@@ -1,95 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Loc
-open Pp
-open Libnames
-open Constrexpr
-open Names
-open Misctypes
-
-module type Pp = sig
-
- val extract_lam_binders :
- constr_expr -> local_binder list * constr_expr
- val extract_prod_binders :
- constr_expr -> local_binder list * constr_expr
- val split_fix :
- int -> constr_expr -> constr_expr ->
- local_binder list * constr_expr * constr_expr
-
- val prec_less : int -> int * Ppextend.parenRelation -> bool
-
- val pr_tight_coma : unit -> std_ppcmds
-
- val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-
- val pr_lident : Id.t located -> std_ppcmds
- val pr_lname : Name.t located -> std_ppcmds
-
- val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
- val pr_com_at : int -> std_ppcmds
- val pr_sep_com :
- (unit -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- constr_expr -> std_ppcmds
-
- val pr_id : Id.t -> std_ppcmds
- val pr_name : Name.t -> std_ppcmds
- 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
- val pr_constr_expr : constr_expr -> std_ppcmds
- val pr_lconstr_expr : constr_expr -> std_ppcmds
- val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
-
- type term_pr = {
- pr_constr_expr : constr_expr -> std_ppcmds;
- pr_lconstr_expr : constr_expr -> std_ppcmds;
- pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
- pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
- }
-
- val set_term_pr : term_pr -> unit
- val default_term_pr : term_pr
-
-(** The modular constr printer.
- [modular_constr_pr pr s p t] prints the head of the term [t] and calls
- [pr] on its subterms.
- [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
- and [ltop] for "lconstr" printers (spiwack: we might need more
- specification here).
- We can make a new modular constr printer by overriding certain branches,
- for instance if we want to build a printer which prints "Prop" as "Omega"
- instead we can proceed as follows:
- let my_modular_constr_pr pr s p = function
- | CSort (_,GProp Null) -> str "Omega"
- | t -> modular_constr_pr pr s p t
- Which has the same type. We can turn a modular printer into a printer by
- taking its fixpoint. *)
-
- type precedence
- val lsimpleconstr : precedence
- val ltop : precedence
- val modular_constr_pr :
- ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
- (unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds
-
-end
-
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
deleted file mode 100644
index 086cf7f513..0000000000
--- a/printing/pptactic.ml
+++ /dev/null
@@ -1,1479 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Pp
-open Names
-open Namegen
-open CErrors
-open Util
-open Constrexpr
-open Tacexpr
-open Genarg
-open Geninterp
-open Constrarg
-open Libnames
-open Ppextend
-open Misctypes
-open Locus
-open Decl_kinds
-open Genredexpr
-open Ppconstr
-open Printer
-
-let pr_global x = Nametab.pr_global_env Id.Set.empty x
-
-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_level : int;
- pptac_prods : grammar_terminals;
-}
-
-(* Tactic notations *)
-let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
-
-let declare_notation_tactic_pprule kn pt =
- prnotation_tab := KNmap.add kn pt !prnotation_tab
-
-type 'a raw_extra_genarg_printer =
- (constr_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
-
-type 'a glob_extra_genarg_printer =
- (glob_constr_and_expr -> std_ppcmds) ->
- (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
-
-type 'a extra_genarg_printer =
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> 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 wit with
- | ExtraArg s -> ArgT.repr s
- | _ -> error
- "Can declare a pretty-printing rule only for extra argument types."
- in
- let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in
- let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in
- let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
- genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
-
-module Make
- (Ppconstr : Ppconstrsig.Pp)
- (Taggers : sig
- val tag_keyword
- : std_ppcmds -> std_ppcmds
- val tag_primitive
- : std_ppcmds -> std_ppcmds
- val tag_string
- : std_ppcmds -> std_ppcmds
- val tag_glob_tactic_expr
- : glob_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_glob_atomic_tactic_expr
- : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_raw_tactic_expr
- : raw_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_raw_atomic_tactic_expr
- : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_atomic_tactic_expr
- : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- end)
-= struct
-
- open Taggers
-
- 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 ->
- pr c
- | NoOccurrences ->
- failwith "pr_with_occurrences: no occurrences"
- | OnlyOccurrences nl ->
- hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
- hov 0 (prlist_with_sep spc (pr_or_var int) nl))
- | AllOccurrencesBut nl ->
- hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
- hov 0 (prlist_with_sep spc (pr_or_var int) nl))
-
- exception ComplexRedFlag
-
- let pr_short_red_flag pr r =
- 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 ()) ++
- hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
-
- let pr_red_flag pr r =
- try pr_short_red_flag pr r
- with complexRedFlags ->
- (if r.rBeta then pr_arg str "beta" else mt ()) ++
- (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
- pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
- hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
-
- let pr_union pr1 pr2 = function
- | Inl a -> pr1 a
- | Inr b -> pr2 b
-
- let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
- | Red false -> keyword "red"
- | Hnf -> keyword "hnf"
- | 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.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)
- | Lazy f ->
- hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
- | Cbn f ->
- hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
- | Unfold l ->
- hov 1 (keyword "unfold" ++ spc() ++
- prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
- | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
- | Pattern l ->
- hov 1 (keyword "pattern" ++
- pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)
-
- | Red true ->
- error "Shouldn't be accessible from user."
- | ExtraRedExpr s ->
- str s
- | CbvVm o ->
- keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
- | CbvNative o ->
- keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
-
- let pr_may_eval test prc prlc pr2 pr3 = function
- | ConstrEval (r,c) ->
- hov 0
- (keyword "eval" ++ brk (1,1) ++
- pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
- keyword "in" ++ spc() ++ prc c)
- | ConstrContext ((_,id),c) ->
- hov 0
- (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
- str "[ " ++ prlc c ++ str " ]")
- | ConstrTypeOf c ->
- hov 1 (keyword "type of" ++ spc() ++ prc c)
- | ConstrTerm c when test c ->
- h 0 (str "(" ++ prc c ++ str ")")
- | ConstrTerm c ->
- prc c
-
- let pr_may_eval a =
- pr_may_eval (fun _ -> false) a
-
- let pr_arg pr x = spc () ++ pr x
-
- let pr_or_var pr = function
- | ArgArg x -> pr x
- | ArgVar (_,s) -> pr_id s
-
- let pr_and_short_name pr (c,_) = pr c
-
- let pr_or_by_notation f = function
- | AN v -> f v
- | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
-
- let pr_located pr (loc,x) = pr x
-
- let pr_evaluable_reference = function
- | EvalVarRef id -> pr_id id
- | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
-
- let pr_quantified_hypothesis = function
- | AnonHyp n -> int n
- | NamedHyp id -> pr_id id
-
- let pr_binding prc = function
- | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
- let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ keyword "with" ++ brk (1,1) ++
- hv 0 (prlist_with_sep spc prc l)
- | ExplicitBindings l ->
- brk (1,1) ++ keyword "with" ++ brk (1,1) ++
- hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
- | NoBindings -> mt ()
-
- let pr_bindings_no_with prc prlc = function
- | ImplicitBindings l ->
- brk (0,1) ++
- prlist_with_sep spc prc l
- | ExplicitBindings l ->
- brk (0,1) ++
- prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
- let pr_clear_flag clear_flag 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
-
- let pr_with_bindings_arg prc prlc (clear_flag,c) =
- pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
-
- let pr_with_constr prc = function
- | None -> mt ()
- | Some c -> spc () ++ hov 1 (keyword "with" ++ spc () ++ prc c)
-
- let pr_message_token prid = function
- | MsgString s -> tag_string (qs s)
- | MsgInt n -> int n
- | MsgIdent id -> prid id
-
- let pr_fresh_ids =
- prlist (fun s -> spc() ++ pr_or_var (fun s -> tag_string (qs s)) s)
-
- let with_evars ev s = if ev then "e" ^ s else s
-
- let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
-
- let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
- match wit with
- | ListArg wit ->
- let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
- let ans = pr_sequence map x in
- hov_if_not_empty 0 ans
- | OptArg wit ->
- let ans = match x with
- | None -> mt ()
- | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
- in
- hov_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_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
- in
- 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
- | [] -> []
- | 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
- | 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
- | _ -> tacarg_using_rule_token pr_gen l
- in
- pr_sequence (fun x -> x) l
-
- 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 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 ->
- 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 *)
-
- let strip_prod_binders_expr n ty =
- let rec strip_ty acc n ty =
- match ty with
- Constrexpr.CProdN(_,bll,a) ->
- let nb =
- List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
- let bll = List.map (fun (x, _, y) -> x, y) bll in
- if nb >= n then (List.rev (bll@acc)), a
- else strip_ty (bll@acc) (n-nb) a
- | _ -> error "Cannot translate fix tactic: not enough products" in
- strip_ty [] n ty
-
- let pr_ltac_or_var pr = function
- | ArgArg x -> pr x
- | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
-
- let pr_ltac_constant kn =
- if !Flags.in_debugger then pr_kn kn
- else try
- pr_qualid (Nametab.shortest_qualid_of_tactic kn)
- with Not_found -> (* local tactic not accessible anymore *)
- str "<" ++ pr_kn kn ++ str ">"
-
- let pr_evaluable_reference_env env = function
- | EvalVarRef id -> pr_id id
- | EvalConstRef sp ->
- Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
-
- let pr_esubst prc l =
- let pr_qhyp = function
- (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
- | (_,NamedHyp id,c) ->
- str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
- in
- prlist_with_sep spc pr_qhyp l
-
- let pr_bindings_gen for_ex prc prlc = function
- | ImplicitBindings l ->
- spc () ++
- hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
- prlist_with_sep spc prc l)
- | ExplicitBindings l ->
- spc () ++
- hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
- pr_esubst prlc l)
- | NoBindings -> mt ()
-
- let pr_bindings prc prlc = pr_bindings_gen false prc prlc
-
- let pr_with_bindings prc prlc (c,bl) =
- hov 1 (prc c ++ pr_bindings prc prlc bl)
-
- let pr_as_disjunctive_ipat prc ipatl =
- keyword "as" ++ spc () ++
- pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
-
- let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
-
- let pr_with_induction_names prc = function
- | None, None -> mt ()
- | Some eqpat, None -> hov 1 (pr_eqn_ipat eqpat)
- | None, Some ipat -> hov 1 (pr_as_disjunctive_ipat prc ipat)
- | Some eqpat, Some ipat ->
- hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat)
-
- let pr_as_intro_pattern prc ipat =
- spc () ++ hov 1 (keyword "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat)
-
- let pr_with_inversion_names prc = function
- | None -> mt ()
- | Some ipat -> pr_as_disjunctive_ipat prc ipat
-
- let pr_as_ipat prc = function
- | None -> mt ()
- | Some ipat -> pr_as_intro_pattern prc ipat
-
- let pr_as_name = function
- | Anonymous -> mt ()
- | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id)
-
- let pr_pose_as_style prc na c =
- spc() ++ prc c ++ pr_as_name na
-
- let pr_pose prc prlc na c = match na with
- | Anonymous -> spc() ++ prc c
- | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
-
- let pr_assertion prc prdc _prlc ipat c = match ipat with
- (* Use this "optimisation" or use only the general case ?
- | IntroIdentifier id ->
- spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
- *)
- | ipat ->
- spc() ++ prc c ++ pr_as_ipat prdc ipat
-
- let pr_assumption prc prdc prlc ipat c = match ipat with
- (* Use this "optimisation" or use only the general case ?*)
- (* it seems that this "optimisation" is somehow more natural *)
- | Some (_,IntroNaming (IntroIdentifier id)) ->
- spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
- | ipat ->
- spc() ++ prc c ++ pr_as_ipat prdc ipat
-
- let pr_by_tactic prt = function
- | Some tac -> keyword "by" ++ spc () ++ prt tac
- | None -> mt()
-
- let pr_hyp_location pr_id = function
- | occs, InHyp -> pr_with_occurrences pr_id occs
- | occs, InHypTypeOnly ->
- pr_with_occurrences (fun id ->
- str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
- ) occs
- | occs, InHypValueOnly ->
- pr_with_occurrences (fun id ->
- str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
- ) occs
-
- let pr_in pp = hov 0 (keyword "in" ++ pp)
-
- let pr_simple_hyp_clause pr_id = function
- | [] -> mt ()
- | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
-
- let pr_in_hyp_as prc pr_id = function
- | 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) ->
- pr_with_occurrences mt (occs,())
- | { onhyps=None; concl_occs=AllOccurrences }
- when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
- | { onhyps=None; concl_occs=NoOccurrences } ->
- pr_in (str " * |-")
- | { onhyps=None; concl_occs=occs } ->
- pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
- | { onhyps=Some l; concl_occs=occs } ->
- let pr_occs = match occs with
- | NoOccurrences -> mt ()
- | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
- in
- pr_in
- (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 "<- "
-
- let pr_multi = function
- | Precisely 1 -> mt ()
- | Precisely n -> int n ++ str "!"
- | UpTo n -> int n ++ str "?"
- | RepeatStar -> str "?"
- | RepeatPlus -> str "!"
-
- 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_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"
- | Once -> mt ()
-
- let pr_match_pattern pr_pat = function
- | Term a -> pr_pat a
- | 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 " ]"
- | Subterm (b,Some id,a) ->
- keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
-
- let pr_match_hyps pr_pat = function
- | Hyp (nal,mp) ->
- pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
- | Def (nal,mv,mp) ->
- pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
- ++ str ":" ++ pr_match_pattern pr_pat mp
-
- let pr_match_rule m pr pr_pat = function
- | Pat ([],mp,t) when m ->
- pr_match_pattern pr_pat mp ++
- spc () ++ str "=>" ++ brk (1,4) ++ pr t
- (*
- | Pat (rl,mp,t) ->
- hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++
- (if rl <> [] then spc () else mt ()) ++
- hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
- str "=>" ++ brk (1,4) ++ pr t))
- *)
- | Pat (rl,mp,t) ->
- hov 0 (
- hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
- (if not (List.is_empty rl) then spc () else mt ()) ++
- hov 0 (
- str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
- str "=>" ++ brk (1,4) ++ pr t))
- | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
-
- let pr_funvar = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
-
- let pr_let_clause k pr (id,(bl,t)) =
- hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
- str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t)))
-
- let pr_let_clauses recflag pr = function
- | hd::tl ->
- hv 0
- (pr_let_clause (if recflag then "let rec" else "let") pr hd ++
- prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
- | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
-
- let pr_seq_body pr tl =
- hv 0 (str "[ " ++
- prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
- str " ]")
-
- let pr_dispatch pr tl =
- hv 0 (str "[>" ++
- prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
- str " ]")
-
- let pr_opt_tactic pr = function
- | TacId [] -> mt ()
- | t -> pr t
-
- let pr_tac_extend_gen pr tf tm tl =
- prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
- pr_opt_tactic pr tm ++ str ".." ++
- prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl
-
- let pr_then_gen pr tf tm tl =
- hv 0 (str "[ " ++
- pr_tac_extend_gen pr tf tm tl ++
- str " ]")
-
- let pr_tac_extend pr tf tm tl =
- hv 0 (str "[>" ++
- pr_tac_extend_gen pr tf tm tl ++
- str " ]")
-
- let pr_hintbases = function
- | None -> keyword "with" ++ str" *"
- | Some [] -> mt ()
- | Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
-
- let pr_auto_using prc = function
- | [] -> mt ()
- | l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
-
- let pr_then () = str ";"
-
- let ltop = (5,E)
- let lseq = 4
- let ltactical = 3
- let lorelse = 2
- let llet = 5
- let lfun = 5
- let lcomplete = 1
- let labstract = 3
- let lmatch = 1
- let latom = 0
- let lcall = 1
- let leval = 1
- let ltatom = 1
- let linfo = 5
-
- let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
-
- (** A printer for tactics that polymorphically works on the three
- "raw", "glob" and "typed" levels *)
-
- type 'a printer = {
- pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
- pr_constr : 'trm -> std_ppcmds;
- pr_lconstr : 'trm -> std_ppcmds;
- pr_dconstr : 'dtrm -> std_ppcmds;
- pr_pattern : 'pat -> std_ppcmds;
- pr_lpattern : 'pat -> std_ppcmds;
- pr_constant : 'cst -> std_ppcmds;
- pr_reference : 'ref -> std_ppcmds;
- pr_name : 'nam -> std_ppcmds;
- pr_generic : 'lev generic_argument -> 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;
- dterm :'dtrm;
- pattern :'pat;
- constant :'cst;
- reference :'ref;
- name :'nam;
- tacexpr :'tacexpr;
- level :'lev
- >
-
- 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
- )
-
- (* 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
- )
-
- (* 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
-
- let make_pr_tac pr strip_prod_binders tag_atom tag =
-
- let extract_binders = function
- | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
- | body -> ([],body) in
- let rec pr_tac inherited tac =
- let return (doc, l) = (tag tac doc, l) in
- let (strm, prec) = return (match tac with
- | TacAbstract (t,None) ->
- keyword "abstract " ++ pr_tac (labstract,L) t, labstract
- | TacAbstract (t,Some s) ->
- hov 0 (
- keyword "abstract"
- ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
- ++ keyword "using" ++ spc () ++ pr_id s),
- labstract
- | TacLetIn (recflag,llc,u) ->
- let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
- v 0
- (hv 0 (
- pr_let_clauses recflag (pr_tac ltop) llc
- ++ spc () ++ keyword "in"
- ) ++ fnl () ++ pr_tac (llet,E) u),
- llet
- | TacMatch (lz,t,lrul) ->
- hov 0 (
- pr_lazy lz ++ keyword "match" ++ spc ()
- ++ pr_tac ltop t ++ spc () ++ keyword "with"
- ++ prlist (fun r ->
- fnl () ++ str "| "
- ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r
- ) lrul
- ++ fnl() ++ keyword "end"),
- lmatch
- | TacMatchGoal (lz,lr,lrul) ->
- hov 0 (
- pr_lazy lz
- ++ keyword (if lr then "match reverse goal with" else "match goal with")
- ++ prlist (fun r ->
- fnl () ++ str "| "
- ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r
- ) lrul ++ fnl() ++ keyword "end"),
- lmatch
- | TacFun (lvar,body) ->
- hov 2 (
- keyword "fun"
- ++ prlist pr_funvar lvar ++ str " =>" ++ spc ()
- ++ pr_tac (lfun,E) body),
- lfun
- | TacThens (t,tl) ->
- hov 1 (
- pr_tac (lseq,E) t ++ pr_then () ++ spc ()
- ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl),
- lseq
- | TacThen (t1,t2) ->
- hov 1 (
- pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
- ++ pr_tac (lseq,L) t2),
- lseq
- | TacDispatch tl ->
- pr_dispatch (pr_tac ltop) tl, lseq
- | TacExtendTac (tf,t,tr) ->
- pr_tac_extend (pr_tac ltop) tf t tr , lseq
- | TacThens3parts (t1,tf,t2,tl) ->
- hov 1 (
- pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
- ++ pr_then_gen (pr_tac ltop) tf t2 tl),
- lseq
- | TacTry t ->
- hov 1 (
- keyword "try" ++ spc () ++ pr_tac (ltactical,E) t),
- ltactical
- | TacDo (n,t) ->
- hov 1 (
- str "do" ++ spc ()
- ++ pr_or_var int n ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacTimeout (n,t) ->
- hov 1 (
- keyword "timeout "
- ++ pr_or_var int n ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacTime (s,t) ->
- hov 1 (
- keyword "time"
- ++ pr_opt str s ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacRepeat t ->
- hov 1 (
- keyword "repeat" ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacProgress t ->
- hov 1 (
- keyword "progress" ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacShowHyps t ->
- hov 1 (
- keyword "infoH" ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacInfo t ->
- hov 1 (
- keyword "info" ++ spc ()
- ++ pr_tac (ltactical,E) t),
- linfo
- | TacOr (t1,t2) ->
- hov 1 (
- pr_tac (lorelse,L) t1 ++ spc ()
- ++ str "+" ++ brk (1,1)
- ++ pr_tac (lorelse,E) t2),
- lorelse
- | TacOnce t ->
- hov 1 (
- keyword "once" ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacExactlyOnce t ->
- hov 1 (
- keyword "exactly_once" ++ spc ()
- ++ pr_tac (ltactical,E) t),
- ltactical
- | TacIfThenCatch (t,tt,te) ->
- hov 1 (
- str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++
- str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++
- str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)),
- ltactical
- | TacOrelse (t1,t2) ->
- hov 1 (
- pr_tac (lorelse,L) t1 ++ spc ()
- ++ str "||" ++ brk (1,1)
- ++ pr_tac (lorelse,E) t2),
- lorelse
- | TacFail (g,n,l) ->
- let arg =
- match n with
- | ArgArg 0 -> mt ()
- | _ -> pr_arg (pr_or_var int) n
- in
- let name =
- match g with
- | TacGlobal -> keyword "gfail"
- | TacLocal -> keyword "fail"
- in
- hov 1 (
- name ++ arg
- ++ prlist (pr_arg (pr_message_token pr.pr_name)) l),
- latom
- | TacFirst tl ->
- keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
- | TacSolve tl ->
- 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_atom pr strip_prod_binders tag_atom t)), ltatom
- | TacArg(_,Tacexp e) ->
- pr.pr_tactic (latom,E) e, latom
- | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
- keyword "constr:" ++ pr.pr_constr c, latom
- | TacArg(_,ConstrMayEval c) ->
- pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
- | TacArg(_,TacFreshId l) ->
- primitive "fresh" ++ pr_fresh_ids l, latom
- | TacArg(_,TacGeneric arg) ->
- pr.pr_generic arg, latom
- | TacArg(_,TacCall(loc,f,[])) ->
- pr.pr_reference f, latom
- | TacArg(_,TacCall(loc,f,l)) ->
- pr_with_comments loc (hov 1 (
- pr.pr_reference f ++ spc ()
- ++ prlist_with_sep spc pr_tacarg l)),
- lcall
- | TacArg (_,a) ->
- pr_tacarg a, latom
- | 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 l), latom
- )
- in
- if prec_less prec inherited then strm
- else str"(" ++ strm ++ str")"
-
- and pr_tacarg = function
- | Reference r ->
- pr.pr_reference r
- | ConstrMayEval c ->
- pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
- | TacFreshId l ->
- keyword "fresh" ++ pr_fresh_ids l
- | TacPretype c ->
- keyword "type_term" ++ pr.pr_constr c
- | TacNumgoals ->
- keyword "numgoals"
- | (TacCall _|Tacexp _ | TacGeneric _) as a ->
- hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a))))
-
- in pr_tac
-
- let strip_prod_binders_glob_constr n (ty,_) =
- let rec strip_ty acc n ty =
- if Int.equal n 0 then (List.rev acc, (ty,None)) else
- match ty with
- Glob_term.GProd(loc,na,Explicit,a,b) ->
- strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
- strip_ty [] n ty
-
- let raw_printers =
- (strip_prod_binders_expr)
-
- let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
- let pr = {
- pr_tactic = pr_raw_tactic_level;
- pr_constr = pr_constr_expr;
- pr_dconstr = pr_constr_expr;
- pr_lconstr = pr_lconstr_expr;
- pr_pattern = pr_constr_pattern_expr;
- pr_lpattern = pr_lconstr_pattern_expr;
- pr_constant = pr_or_by_notation pr_reference;
- pr_reference = pr_reference;
- pr_name = pr_lident;
- 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
- pr raw_printers
- tag_raw_atomic_tactic_expr tag_raw_tactic_expr
- n t
-
- let pr_raw_tactic = pr_raw_tactic_level ltop
-
- let pr_and_constr_expr pr (c,_) = pr c
-
- let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c
-
- let pr_glob_tactic_level env n t =
- let glob_printers =
- (strip_prod_binders_glob_constr)
- in
- let rec prtac n (t:glob_tactic_expr) =
- let pr = {
- pr_tactic = prtac;
- pr_constr = 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);
- pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
- 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 = 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
- (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));
- } in
- make_pr_tac
- pr glob_printers
- tag_glob_atomic_tactic_expr tag_glob_tactic_expr
- n t
- in
- prtac n t
-
- let pr_glob_tactic env = pr_glob_tactic_level env ltop
-
- let strip_prod_binders_constr n ty =
- let rec strip_ty acc n ty =
- if n=0 then (List.rev acc, ty) else
- match Term.kind_of_term ty with
- Term.Prod(na,a,b) ->
- strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
- strip_ty [] n ty
-
- let pr_atomic_tactic_level env n t =
- let prtac n (t:atomic_tactic_expr) =
- let pr = {
- pr_tactic = (fun _ _ -> str "<tactic>");
- pr_constr = pr_constr_env env Evd.empty;
- pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
- pr_lconstr = pr_lconstr_env env Evd.empty;
- pr_pattern = pr_constr_pattern_env env Evd.empty;
- 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;
- (** Those are not used by the atomic printer *)
- pr_generic = (fun _ -> assert false);
- pr_extend = (fun _ _ _ -> assert false);
- pr_alias = (fun _ _ _ -> assert false);
- }
- in
- pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
- in
- prtac n t
-
- 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
-
-module Tag =
-struct
- let keyword =
- let style = Terminal.make ~bold:true () in
- Ppstyle.make ~style ["tactic"; "keyword"]
-
- let primitive =
- let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
- Ppstyle.make ~style ["tactic"; "primitive"]
-
- let string =
- let style = Terminal.make ~fg_color:`LIGHT_RED () in
- Ppstyle.make ~style ["tactic"; "string"]
-
-end
-
-include Make (Ppconstr) (struct
- let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
- let do_not_tag _ x = x
- let tag_keyword = tag Tag.keyword
- let tag_primitive = tag Tag.primitive
- let tag_string = tag Tag.string
- let tag_glob_tactic_expr = do_not_tag
- 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_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 (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_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;
- Genprint.register_print0 Stdarg.wit_pre_ident str str str;
- Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
-
-let () =
- let printer _ _ prtac = prtac (0, E) in
- declare_extra_genarg_pprule wit_tactic printer printer printer
-
-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
-
- include Make (Ppconstr.Richpp) (struct
- open Ppannotation
- let do_not_tag _ x = x
- let tag e s = Pp.tag (Pp.Tag.inj e tag) s
- let tag_keyword = tag AKeyword
- let tag_primitive = tag AKeyword
- let tag_string = do_not_tag ()
- let tag_glob_tactic_expr e = tag (AGlobTacticExpr e)
- 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_atomic_tactic_expr a = tag (AAtomicTacticExpr a)
- end)
-
-end
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
deleted file mode 100644
index b7d349af98..0000000000
--- a/printing/pptactic.mli
+++ /dev/null
@@ -1,67 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** This module implements pretty-printers for tactic_expr syntactic
- objects and their subcomponents. *)
-
-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) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
-
-type 'a glob_extra_genarg_printer =
- (glob_constr_and_expr -> std_ppcmds) ->
- (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
-
-type 'a extra_genarg_printer =
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> std_ppcmds) ->
- (tolerability -> Val.t -> std_ppcmds) ->
- 'a -> std_ppcmds
-
-val declare_extra_genarg_pprule :
- ('a, 'b, 'c) genarg_type ->
- 'a raw_extra_genarg_printer ->
- 'b glob_extra_genarg_printer ->
- 'c extra_genarg_printer -> unit
-
-type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
-
-type pp_tactic = {
- pptac_level : int;
- pptac_prods : grammar_terminals;
-}
-
-val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
-
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as raw strings. *)
-include Pptacticsig.Pp
-
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as annotated strings. The annotations can be
- retrieved using {!RichPp.rich_pp}. Their definitions are
- located in {!Ppannotation.t}. *)
-module Richpp : Pptacticsig.Pp
-
-val ltop : tolerability
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
deleted file mode 100644
index 723839bb11..0000000000
--- a/printing/pptacticsig.mli
+++ /dev/null
@@ -1,83 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Pp
-open Genarg
-open Geninterp
-open Tacexpr
-open Ppextend
-open Environ
-open Misctypes
-
-module type Pp = sig
-
- val pr_with_occurrences :
- ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
- val pr_red_expr :
- ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
- ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
- val pr_may_eval :
- ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
- ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
-
- val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
- 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 : 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 :
- (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
-
- val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
-
- val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
-
- val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
-
- val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
-
- val pr_hintbases : string list option -> std_ppcmds
-
- val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
-
- val pr_bindings :
- ('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 5f5f8fcea8..9ef9162aee 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -6,14 +6,148 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Pp
+open Genarg
+open Nameops
+open Misctypes
+open Locus
+open Genredexpr
let pr_located pr (loc, x) =
- if !Flags.beautify && loc <> Loc.ghost then
+ match loc with
+ | Some loc when !Flags.beautify ->
let (b, e) = Loc.unloc loc in
(* 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
+ | _ -> pr x
+
+let pr_or_var pr = function
+ | ArgArg x -> pr x
+ | ArgVar (_,s) -> pr_id s
+
+let pr_with_occurrences pr keyword (occs,c) =
+ match occs with
+ | AllOccurrences ->
+ pr c
+ | NoOccurrences ->
+ failwith "pr_with_occurrences: no occurrences"
+ | OnlyOccurrences nl ->
+ hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+ | AllOccurrencesBut nl ->
+ hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+exception ComplexRedFlag
+
+let pr_short_red_flag pr r =
+ 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 ()) ++
+ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
+let pr_red_flag pr r =
+ try pr_short_red_flag pr r
+ with complexRedFlags ->
+ (if r.rBeta then pr_arg str "beta" else mt ()) ++
+ (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
+ pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+let pr_union pr1 pr2 = function
+ | Inl a -> pr1 a
+ | Inr b -> pr2 b
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
+ | Red false -> keyword "red"
+ | Hnf -> keyword "hnf"
+ | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+ ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+ | Cbv f ->
+ 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)
+ | Lazy f ->
+ hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
+ | Cbn f ->
+ hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
+ | Unfold l ->
+ hov 1 (keyword "unfold" ++ spc() ++
+ prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
+ | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
+ | Pattern l ->
+ hov 1 (keyword "pattern" ++
+ pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
+
+ | Red true ->
+ CErrors.user_err Pp.(str "Shouldn't be accessible from user.")
+ | ExtraRedExpr s ->
+ str s
+ | CbvVm o ->
+ keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+ | CbvNative o ->
+ keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+
+let pr_or_by_notation f = function
+ | AN v -> f v
+ | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+
+let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
+
+let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
+ match wit with
+ | ListArg wit ->
+ let map x = pr_raw_generic env (in_gen (rawwit wit) x) in
+ let ans = pr_sequence map x in
+ hov_if_not_empty 0 ans
+ | OptArg wit ->
+ let ans = match x with
+ | None -> mt ()
+ | Some x -> pr_raw_generic env (in_gen (rawwit wit) x)
+ in
+ 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 env) [p; q])
+ | ExtraArg s ->
+ Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
+
+let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
+ match wit with
+ | ListArg wit ->
+ let map x = pr_glb_generic env (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_glb_generic env (in_gen (glbwit wit) x)
+ in
+ 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 env) [p; q] in
+ hov_if_not_empty 0 ans
+ | ExtraArg s ->
+ Genprint.generic_glb_print (in_gen (glbwit wit) x)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 4447ee2b81..0dee11e0bc 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -7,7 +7,25 @@
(************************************************************************)
open Pp
+open Genarg
+open Misctypes
+open Locus
+open Genredexpr
val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds
(** Prints an object surrounded by its commented location *)
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+val pr_with_occurrences :
+ ('a -> std_ppcmds) -> (string -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
+
+val pr_short_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds
+val pr_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds
+val pr_red_expr :
+ ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+ (string -> std_ppcmds) ->
+ ('a,'b,'c) red_expr_gen -> std_ppcmds
+
+val pr_raw_generic : Environ.env -> rlevel generic_argument -> std_ppcmds
+val pr_glb_generic : Environ.env -> glevel generic_argument -> std_ppcmds
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a9c49bc20d..a15cadfa0b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -19,18 +19,11 @@ open Constrexpr
open Constrexpr_ops
open Decl_kinds
-module Make
- (Ppconstr : Ppconstrsig.Pp)
- (Pptactic : Pptacticsig.Pp)
- (Taggers : sig
- val tag_keyword : std_ppcmds -> std_ppcmds
- val tag_vernac : vernac_expr -> std_ppcmds -> std_ppcmds
- end)
-= struct
-
- open Taggers
open Ppconstr
- open Pptactic
+
+ let do_not_tag _ x = x
+ let tag_keyword = do_not_tag ()
+ let tag_vernac = do_not_tag
let keyword s = tag_keyword (str s)
@@ -39,11 +32,10 @@ module Make
let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
let pr_lident (loc,id) =
- if Loc.is_ghost loc then
- let (b,_) = Loc.unloc loc in
- pr_located pr_id (Loc.make_loc (b,b + String.length(Id.to_string id)),id)
- else
- pr_id id
+ match loc with
+ | None -> pr_id id
+ | Some loc -> let (b,_) = Loc.unloc loc in
+ pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id
let pr_plident (lid, l) =
pr_lident lid ++
@@ -57,17 +49,16 @@ module Make
let pr_fqid fqid = str (string_of_fqid fqid)
let pr_lfqid (loc,fqid) =
- if Loc.is_ghost loc then
- let (b,_) = Loc.unloc loc in
- pr_located pr_fqid (Loc.make_loc (b,b + String.length(string_of_fqid fqid)),fqid)
- else
- pr_fqid fqid
+ match loc with
+ | None -> pr_fqid fqid
+ | Some loc -> let (b,_) = Loc.unloc loc in
+ pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
let pr_lname = function
| (loc,Name id) -> pr_lident (loc,id)
- | lna -> pr_located pr_name lna
+ | lna -> pr_located Name.print lna
- let pr_smart_global = pr_or_by_notation pr_reference
+ let pr_smart_global = Pputils.pr_or_by_notation pr_reference
let pr_ltac_ref = Libnames.pr_reference
@@ -81,7 +72,7 @@ module Make
| VernacEndSubproof -> str""
| _ -> str"."
- let pr_gen t = pr_raw_generic (Global.env ()) t
+ let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
@@ -114,7 +105,7 @@ module Make
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
- pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
++
match a with
| SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -127,7 +118,7 @@ module Make
let pr_explanation (e,b,f) =
let a = match e with
- | ExplByPos (n,_) -> anomaly (Pp.str "No more supported")
+ | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.")
| ExplByName id -> pr_id id in
let a = if f then str"!" ++ a else a in
if b then str "[" ++ a ++ str "]" else a
@@ -198,7 +189,7 @@ module Make
| HintsExtern (n,c,tac) ->
let pat = match c with None -> mt () | Some pat -> pr_pat pat in
keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
- spc() ++ pr_raw_tactic tac
+ spc() ++ Pputils.pr_raw_generic (Global.env ()) tac
in
hov 2 (keyword "Hint "++ pph ++ opth)
@@ -210,19 +201,19 @@ module Make
keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
pr_located pr_qualid qid
- let rec pr_module_ast leading_space pr_c = function
- | CMident qid ->
+ let rec pr_module_ast leading_space pr_c = let open CAst in function
+ | { loc ; v = CMident qid } ->
if leading_space then
- spc () ++ pr_located pr_qualid qid
+ spc () ++ pr_located pr_qualid (loc, qid)
else
- pr_located pr_qualid qid
- | CMwith (_,mty,decl) ->
+ pr_located pr_qualid (loc,qid)
+ | { v = CMwith (mty,decl) } ->
let m = pr_module_ast leading_space pr_c mty in
let p = pr_with_declaration pr_c decl in
m ++ spc() ++ keyword "with" ++ spc() ++ p
- | CMapply (_,me1,(CMident _ as me2)) ->
+ | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } ->
pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
- | CMapply (_,me1,me2) ->
+ | { v = CMapply (me1,me2) } ->
pr_module_ast leading_space pr_c me1 ++ spc() ++
hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
@@ -261,7 +252,7 @@ module Make
prlist_strict (pr_module_vardecls pr_c) l
let pr_type_option pr_c = function
- | CHole (loc, k, Misctypes.IntroAnonymous, _) -> mt()
+ | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
| _ as c -> brk(0,2) ++ str" :" ++ pr_c c
let pr_decl_notation prc ((loc,ntn),c,scopt) =
@@ -303,7 +294,7 @@ module Make
let begin_of_inductive = function
| [] -> 0
- | (_,((loc,_),_))::_ -> fst (Loc.unloc loc)
+ | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
let pr_class_rawexpr = function
| FunClass -> keyword "Funclass"
@@ -327,7 +318,7 @@ module Make
keyword (if many then "Local Parameters" else "Local Parameter")
| (Global,Conjectural) -> str"Conjecture"
| ((Discharge | Local),Conjectural) ->
- anomaly (Pp.str "Don't know how to beautify a local conjecture")
+ anomaly (Pp.str "Don't know how to beautify a local conjecture.")
let pr_params pr_c (xl,(c,t)) =
hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -393,19 +384,14 @@ module Make
++ 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)) =
+ let pr_statement head (idpl,(bl,c)) =
assert (not (Option.is_empty idpl));
let id, pl = Option.get idpl in
hov 2
(head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
- pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
str":" ++ pr_spc_lconstr c)
- let pr_priority = function
- | None -> mt ()
- | Some i -> spc () ++ str "|" ++ spc () ++ int i
-
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
@@ -504,7 +490,7 @@ module Make
| PrintVisibility s ->
keyword "Print Visibility" ++ pr_opt str s
| PrintAbout (qid,gopt) ->
- pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt
++ keyword "About" ++ spc() ++ pr_smart_global qid
| PrintImplicit qid ->
keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
@@ -528,7 +514,7 @@ module Make
let pr_using e = str (Proof_using.to_string e)
let rec pr_vernac_body v =
- let return = Taggers.tag_vernac v in
+ let return = tag_vernac v in
match v with
| VernacPolymorphic (poly, v) ->
let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
@@ -541,18 +527,8 @@ module Make
(* 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 ->
@@ -585,17 +561,13 @@ module Make
| 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
return (pr_showable s)
| VernacCheckGuard ->
@@ -636,8 +608,6 @@ module Make
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)) ->
@@ -706,7 +676,7 @@ module Make
| None -> mt()
| Some r ->
keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
+ pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
keyword " in" ++ spc()
in
let pr_def_body = function
@@ -728,7 +698,7 @@ module Make
| Some cc -> str" :=" ++ spc() ++ cc))
)
- | VernacStartTheoremProof (ki,l,_) ->
+ | VernacStartTheoremProof (ki,l) ->
return (
hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
@@ -745,9 +715,7 @@ module Make
| 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)
+ | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
)
| VernacExactProof c ->
return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
@@ -759,7 +727,7 @@ module Make
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) ->
+ | VernacInductive (cum, p,f,l) ->
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
@@ -786,13 +754,19 @@ module Make
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"
+ let kind =
+ match k with Record -> "Record" | Structure -> "Structure"
+ | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+ | Class _ -> "Class" | Variant -> "Variant"
+ in
+ if p then
+ let cm = if cum then "Cumulative" else "NonCumulative" in
+ cm ^ " " ^ kind
+ else kind
in
return (
hov 1 (pr_oneind key (List.hd l)) ++
- (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
)
| VernacFixpoint (local, recs) ->
@@ -904,7 +878,7 @@ module Make
(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, { CAst.v = 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()))
@@ -1050,13 +1024,13 @@ module Make
| 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) ++
+ spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print 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
+ spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
in
print_arguments nargs args ++
if not (List.is_empty more_implicits) then
@@ -1103,7 +1077,7 @@ module Make
)
| VernacSetOpacity _ ->
return (
- CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
)
| VernacSetStrategy l ->
let pr_lev = function
@@ -1153,18 +1127,19 @@ module Make
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 ++
+ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword 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
+ let pr_i = match io with None -> mt ()
+ | Some i -> Proof_global.pr_goal_selector 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
+ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
)
| VernacPrint p ->
return (pr_printable p)
@@ -1205,12 +1180,12 @@ module Make
return (keyword "Proof " ++ spc () ++
keyword "using" ++ spc() ++ pr_using e)
| VernacProof (Some te, None) ->
- return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te)
+ return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te)
| VernacProof (Some te, Some e) ->
return (
keyword "Proof" ++ spc () ++
keyword "using" ++ spc() ++ pr_using e ++ spc() ++
- keyword "with" ++ spc() ++pr_raw_tactic te
+ keyword "with" ++ spc() ++ Pputils.pr_raw_generic (Global.env ()) te
)
| VernacProofMode s ->
return (keyword "Proof Mode" ++ str s)
@@ -1239,31 +1214,10 @@ module Make
| Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
| [], [] -> []
| _ -> assert false in
- hov 1 (pr_sequence (fun x -> x) (aux rl cl))
+ hov 1 (pr_sequence identity (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
-
-include Make (Ppconstr) (Pptactic) (struct
- let do_not_tag _ x = x
- let tag_keyword = do_not_tag ()
- let tag_vernac = do_not_tag
-end)
-
-module Richpp = struct
-
- include Make
- (Ppconstr.Richpp)
- (Pptactic.Richpp)
- (struct
- open Ppannotation
- let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s
- let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s
- end)
-
-end
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 6145d6648b..ed5585b309 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,12 +9,11 @@
(** This module implements pretty-printers for vernac_expr syntactic
objects and their subcomponents. *)
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as raw strings. *)
-include Ppvernacsig.Pp
+(** Prints a fixpoint body *)
+val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as annotated strings. The annotations can be
- retrieved using {!RichPp.rich_pp}. Their definitions are
- located in {!Ppannotation.t}. *)
-module Richpp : Ppvernacsig.Pp
+(** Prints a vernac expression *)
+val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+
+(** Prints a vernac expression and closes it with a dot. *)
+val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
deleted file mode 100644
index f23192aff4..0000000000
--- a/printing/ppvernacsig.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-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
-
- (** Prints a vernac expression and closes it with a dot. *)
- val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
-
-end
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index c6825d42ed..faa69f41e5 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -27,6 +27,10 @@ open Recordops
open Misctypes
open Printer
open Printmod
+open Context.Rel.Declaration
+
+(* module RelDecl = Context.Rel.Declaration *)
+module NamedDecl = Context.Named.Declaration
type object_pr = {
print_inductive : mutual_inductive -> std_ppcmds;
@@ -38,8 +42,8 @@ type object_pr = {
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;
- print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds;
+ print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds;
+ print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds;
}
let gallina_print_module = print_module
@@ -67,10 +71,11 @@ let print_basename sp = pr_global (ConstRef sp)
let print_ref reduce ref =
let typ = Global.type_of_global_unsafe ref in
+ let typ = EConstr.of_constr typ in
let typ =
if reduce then
let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
- in it_mkProd_or_LetIn ccl ctx
+ in EConstr.it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref in
let env = Global.env () in
@@ -80,7 +85,7 @@ let print_ref reduce ref =
if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
else mt ()
in
- hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++
+ hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
Printer.pr_universe_ctx sigma univs)
(********************************)
@@ -127,12 +132,11 @@ let print_impargs_list prefix l =
let print_renames_list prefix l =
if List.is_empty l then [] else
[add_colon prefix ++ str "Arguments are renamed to " ++
- hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
+ hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
let need_expansion impl ref =
let typ = Global.type_of_global_unsafe ref in
let ctx = prod_assum typ 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
@@ -170,9 +174,8 @@ type opacity =
| TransparentMaybeOpacified of Conv_oracle.level
let opacity env =
- let open Context.Named.Declaration in
function
- | VarRef v when is_local_def (Environ.lookup_named v env) ->
+ | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) ->
Some(TransparentMaybeOpacified
(Conv_oracle.get_strategy (Environ.oracle env) (VarKey v)))
| ConstRef cst ->
@@ -202,6 +205,11 @@ let print_opacity ref =
str "transparent (with minimal expansion weight)"]
(*******************)
+
+let print_if_is_coercion ref =
+ if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+
+(*******************)
(* *)
let print_polymorphism ref =
@@ -255,7 +263,8 @@ let print_name_infos ref =
type_info_for_implicit @
print_renames_list (mt()) renames @
print_impargs_list (mt()) impls @
- print_argument_scopes (mt()) scopes
+ print_argument_scopes (mt()) scopes @
+ print_if_is_coercion ref
let print_id_args_data test pr id l =
if List.exists test l then
@@ -430,8 +439,8 @@ let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MOD
(**** Gallina layer *****)
let gallina_print_typed_value_in_env env sigma (trm,typ) =
- (pr_lconstr_env env sigma trm ++ fnl () ++
- str " : " ++ pr_ltype_env env sigma typ)
+ (pr_leconstr_env env sigma trm ++ fnl () ++
+ str " : " ++ pr_letype_env env sigma typ)
(* To be improved; the type should be used to provide the types in the
abstractions. This should be done recursively inside pr_lconstr, so that
@@ -493,8 +502,8 @@ let ungeneralized_type_of_constant_type t =
Typeops.type_of_constant_type (Global.env ()) t
let print_instance sigma cb =
- if cb.const_polymorphic then
- pr_universe_instance sigma cb.const_universes
+ if Declareops.constant_is_polymorphic cb then
+ pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
else mt()
let print_constant with_values sep sp =
@@ -502,16 +511,14 @@ let print_constant with_values sep sp =
let val_0 = Global.body_of_constant_body cb in
let typ = Declareops.type_of_constant cb in
let typ = ungeneralized_type_of_constant_type typ in
- let univs = Univ.instantiate_univ_context
- (Global.universes_of_constant_body cb)
- in
+ let univs = Global.universes_of_constant_body cb in
let ctx =
Evd.evar_universe_context_of_binders
(Universes.universe_binders_of_global (ConstRef sp))
in
let env = Global.env () and sigma = Evd.from_ctx ctx in
let pr_ltype = pr_ltype_env env sigma in
- hov 0 (pr_polymorphic cb.const_polymorphic ++
+ hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++
match val_0 with
| None ->
str"*** [ " ++
@@ -530,7 +537,7 @@ let gallina_print_constant_with_infos sp =
let gallina_print_syntactic_def kn =
let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn
and (vars,a) = Syntax_def.search_syntactic_definition kn in
- let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in
+ let c = Notation_ops.glob_constr_of_notation_constr a in
hov 2
(hov 4
(str "Notation " ++ pr_qualid qid ++
@@ -578,8 +585,6 @@ let gallina_print_library_entry with_values ent =
Some (str " >>>>>>> Module " ++ pr_name oname)
| (oname,Lib.ClosedModule _) ->
Some (str " >>>>>>> Closed Module " ++ pr_name oname)
- | (_,Lib.FrozenState _) ->
- None
let gallina_print_context with_values =
let rec prec n = function
@@ -639,6 +644,8 @@ let print_judgment env sigma {uj_val=trm;uj_type=typ} =
let print_safe_judgment env sigma j =
let trm = Safe_typing.j_val j in
let typ = Safe_typing.j_type j in
+ let trm = EConstr.of_constr trm in
+ let typ = EConstr.of_constr typ in
print_typed_value_in_env env sigma (trm, typ)
(*********************)
@@ -700,12 +707,12 @@ let read_sec_context r =
let dir =
try Nametab.locate_section qid
with Not_found ->
- user_err_loc (loc,"read_sec_context", str "Unknown section.") in
+ user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| (_,Lib.ClosedSection _)::rest ->
- error "Cannot print the contents of a closed section."
+ user_err Pp.(str "Cannot print the contents of a closed section.")
(* LEM: Actually, we could if we wanted to. *)
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
@@ -733,16 +740,15 @@ 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 open Context.Named.Declaration in
- str |> Global.lookup_named |> set_id str |> print_named_decl
+ str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl
with Not_found ->
- errorlabstrm
- "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
+ user_err
+ ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
let print_name = function
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
print_any_name
- (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
+ (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
ntn sc))
| AN ref ->
print_any_name (locate_any_name ref)
@@ -755,21 +761,22 @@ let print_opaque_name qid =
if Declareops.constant_has_body cb then
print_constant_with_infos cst
else
- error "Not a defined constant."
+ user_err Pp.(str "Not a defined constant.")
| IndRef (sp,_) ->
print_inductive sp
| ConstructRef cstr as gr ->
+ let open EConstr in
let ty = Universes.unsafe_type_of_global gr in
+ let ty = EConstr.of_constr ty in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
- let open Context.Named.Declaration in
- lookup_named id env |> set_id id |> print_named_decl
+ env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
-let print_about_any loc k =
+let print_about_any ?loc k =
match k with
| Term ref ->
let rb = Reductionops.ReductionBehaviour.print ref in
- Dumpglob.add_glob loc ref;
+ Dumpglob.add_glob ?loc ref;
pr_infos_list
(print_ref false ref :: blankline ::
print_name_infos ref @
@@ -778,7 +785,7 @@ let print_about_any loc k =
[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
| Syntactic kn ->
let () = match Syntax_def.search_syntactic_definition kn with
- | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref
+ | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
| _ -> () in
v 0 (
print_syntactic_def kn ++ fnl () ++
@@ -787,12 +794,12 @@ let print_about_any loc k =
hov 0 (pr_located_qualid k)
let print_about = function
- | ByNotation (loc,ntn,sc) ->
- print_about_any loc
- (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
+ | ByNotation (loc,(ntn,sc)) ->
+ print_about_any ?loc
+ (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
ntn sc))
| AN ref ->
- print_about_any (loc_of_reference ref) (locate_any_name ref)
+ print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref)
(* for debug *)
let inspect depth =
@@ -831,7 +838,7 @@ let index_of_class cl =
try
fst (class_info cl)
with Not_found ->
- errorlabstrm "index_of_class"
+ user_err ~hdr:"index_of_class"
(pr_class cl ++ spc() ++ str "not a defined class.")
let print_path_between cls clt =
@@ -841,7 +848,7 @@ let print_path_between cls clt =
try
lookup_path_between_class (i,j)
with Not_found ->
- errorlabstrm "index_cl_of_id"
+ user_err ~hdr:"index_cl_of_id"
(str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
++ str ".")
in
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 8c8cfcbc27..4add21fa7b 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -8,7 +8,6 @@
open Pp
open Names
-open Term
open Environ
open Reductionops
open Libnames
@@ -27,11 +26,11 @@ val print_full_context_typ : unit -> std_ppcmds
val print_full_pure_context : unit -> std_ppcmds
val print_sec_context : reference -> std_ppcmds
val print_sec_context_typ : reference -> std_ppcmds
-val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds
+val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds
val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds
val print_eval :
reduction_function -> env -> Evd.evar_map ->
- Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+ Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds
val print_name : reference or_by_notation -> std_ppcmds
val print_opaque_name : reference -> std_ppcmds
@@ -69,8 +68,8 @@ type object_pr = {
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;
- print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds
+ print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds;
+ print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds
}
val set_object_pr : object_pr -> unit
diff --git a/printing/printer.ml b/printing/printer.ml
index 069f1570e1..2a198d4564 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -17,19 +17,57 @@ open Nametab
open Evd
open Proof_type
open Refiner
-open Pfedit
open Constrextern
open Ppconstr
open Declarations
-let emacs_str s =
- if !Flags.print_emacs then s else ""
-let delayed_emacs_cmd s =
- if !Flags.print_emacs then s () else str ""
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+module CompactedDecl = Context.Compacted.Declaration
let get_current_context () =
Pfedit.get_current_context ()
+let enable_unfocused_goal_printing = ref false
+let enable_goal_tags_printing = ref false
+let enable_goal_names_printing = ref false
+
+let should_tag() = !enable_goal_tags_printing
+let should_unfoc() = !enable_unfocused_goal_printing
+let should_gname() = !enable_goal_names_printing
+
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "printing of unfocused goal";
+ optkey = ["Printing";"Unfocused"];
+ optread = (fun () -> !enable_unfocused_goal_printing);
+ optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
+
+(* This is set on by proofgeneral proof-tree mode. But may be used for
+ other purposes *)
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "printing of goal tags";
+ optkey = ["Printing";"Goal";"Tags"];
+ optread = (fun () -> !enable_goal_tags_printing);
+ optwrite = (fun b -> enable_goal_tags_printing:=b) }
+
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "printing of goal names";
+ optkey = ["Printing";"Goal";"Names"];
+ optread = (fun () -> !enable_goal_names_printing);
+ optwrite = (fun b -> enable_goal_names_printing:=b) }
+
+
(**********************************************************************)
(** Terms *)
@@ -56,7 +94,10 @@ let pr_constr_goal_style_env env = pr_constr_core true env
let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
- (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let pr_leconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.to_constr sigma c)
+let pr_econstr_env env sigma c = pr_constr_env env sigma (EConstr.to_constr sigma c)
+
+(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
let pr_lconstr t =
let (sigma, env) = get_current_context () in
pr_lconstr_env env sigma t
@@ -67,6 +108,9 @@ let pr_constr t =
let pr_open_lconstr (_,c) = pr_lconstr c
let pr_open_constr (_,c) = pr_constr c
+let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c)
+let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c)
+
let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
(* Warning: clashes can occur with variables of same name in env but *)
(* we also need to preserve the actual names of the patterns *)
@@ -74,8 +118,8 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
pr (Termops.push_rels_assum assums env) sigma c
-let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
-let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
let pr_constr_under_binders c =
let (sigma, env) = get_current_context () in
@@ -89,7 +133,6 @@ let pr_type_core goal_concl_style env sigma t =
let pr_ltype_core goal_concl_style env sigma t =
pr_lconstr_expr (extern_type goal_concl_style env sigma t)
-let pr_goal_concl_style_env env = pr_ltype_core true env
let pr_ltype_env env = pr_ltype_core false env
let pr_type_env env = pr_type_core false env
@@ -100,8 +143,13 @@ let pr_type t =
let (sigma, env) = get_current_context () in
pr_type_env env sigma t
+let pr_etype_env env sigma c = pr_type_env env sigma (EConstr.to_constr sigma c)
+let pr_letype_env env sigma c = pr_ltype_env env sigma (EConstr.to_constr sigma c)
+let pr_goal_concl_style_env env sigma c =
+ pr_ltype_core true env sigma (EConstr.to_constr sigma c)
+
let pr_ljudge_env env sigma j =
- (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type)
+ (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
let pr_ljudge j =
let (sigma, env) = get_current_context () in
@@ -143,7 +191,7 @@ let pr_constr_pattern t =
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
let _ = Termops.set_print_constr
- (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t))
+ (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma (EConstr.Unsafe.to_constr t)))
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
@@ -182,10 +230,10 @@ let qualid_of_global env r =
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
+ let extern_ref ?loc vars r =
+ try orig_extern_ref ?loc vars r
with e when CErrors.noncritical e ->
- Libnames.Qualid (loc, qualid_of_global env r)
+ Libnames.Qualid (Loc.tag ?loc @@ qualid_of_global env r)
in
Constrextern.set_extern_reference extern_ref;
try
@@ -209,7 +257,15 @@ let safe_pr_constr t =
let pr_universe_ctx sigma c =
if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
fnl()++pr_in_comment (fun c -> v 0
- (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c
+ (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c
+ else
+ mt()
+
+let pr_cumulativity_info sigma cumi =
+ if !Detyping.print_universes
+ && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
+ fnl()++pr_in_comment (fun uii -> v 0
+ (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
else
mt()
@@ -226,7 +282,7 @@ let pr_puniverses f env (c,u) =
else mt ())
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
-let pr_existential_key = Evd.pr_existential_key
+let pr_existential_key = Termops.pr_existential_key
let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
@@ -248,31 +304,37 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
(**********************************************************************)
(* Contexts and declarations *)
-let pr_var_decl_skel pr_id env sigma (id,c,typ) =
- let pbody = match c with
- | None -> (mt ())
- | Some c ->
- (* Force evaluation *)
- let pb = pr_lconstr_env env sigma c in
- let pb = if isCast c then surround pb else pb in
- (str" := " ++ pb ++ cut () ) in
+
+(* Flag for compact display of goals *)
+
+let get_compact_context,set_compact_context =
+ let compact_context = ref false in
+ (fun () -> !compact_context),(fun b -> compact_context := b)
+
+let pr_compacted_decl env sigma decl =
+ let ids, pbody, typ = match decl with
+ | CompactedDecl.LocalAssum (ids, typ) ->
+ ids, mt (), typ
+ | CompactedDecl.LocalDef (ids,c,typ) ->
+ (* Force evaluation *)
+ let pb = pr_lconstr_env env sigma c in
+ let pb = if isCast c then surround pb else pb in
+ ids, (str" := " ++ pb ++ cut ()), typ
+ in
+ let pids = prlist_with_sep pr_comma pr_id ids in
let pt = pr_ltype_env env sigma typ in
let ptyp = (str" : " ++ pt) in
- (pr_id id ++ hov 0 (pbody ++ ptyp))
-
-let pr_var_decl env sigma d =
- pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d)
+ hov 0 (pids ++ pbody ++ ptyp)
-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_named_decl env sigma decl =
+ decl |> CompactedDecl.of_named_decl |> pr_compacted_decl env sigma
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 na = RelDecl.get_name decl in
+ let typ = RelDecl.get_type decl in
let pbody = match decl with
- | LocalAssum _ -> mt ()
- | LocalDef (_,c,_) ->
+ | RelDecl.LocalAssum _ -> mt ()
+ | RelDecl.LocalDef (_,c,_) ->
(* Force evaluation *)
let pb = pr_lconstr_env env sigma c in
let pb = if isCast c then surround pb else pb in
@@ -289,13 +351,16 @@ let pr_rel_decl env sigma decl =
(* Prints a signature, all declarations on the same line if possible *)
let pr_named_context_of env sigma =
- let make_decl_list env d pps = pr_var_decl env sigma d :: pps in
+ let make_decl_list env d pps = pr_named_decl env sigma d :: pps in
let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
+let pr_var_list_decl env sigma decl =
+ hov 0 (pr_compacted_decl env sigma decl)
+
let pr_named_context env sigma ne_context =
hv 0 (Context.Named.fold_outside
- (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
+ (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d)
ne_context ~init:(mt ()))
let pr_rel_context env sigma rel_context =
@@ -307,9 +372,9 @@ 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.NamedList.fold
+ Context.Compacted.fold
(fun d pps ->
- let pidt = pr_var_list_decl env sigma d in
+ let pidt = pr_compacted_decl env sigma d in
(pps ++ fnl () ++ pidt))
(Termops.compact_named_context (named_context env)) ~init:(mt ())
in
@@ -326,39 +391,74 @@ let pr_ne_context_of header env sigma =
List.is_empty (Environ.named_context env) then (mt ())
else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ())
-let pr_context_limit n env sigma =
- let named_context = Environ.named_context env in
- let lgsign = List.length named_context in
- if n >= lgsign then
- pr_context_unlimited env sigma
- else
- let k = lgsign-n in
- let _,sign_env =
- Context.NamedList.fold
- (fun d (i,pps) ->
- if i < k then
- (i+1, (pps ++str "."))
- else
- let pidt = pr_var_list_decl env sigma d in
- (i+1, (pps ++ fnl () ++
- str (emacs_str "") ++
- pidt)))
- (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ()))
- in
- let db_env =
- fold_rel_context
- (fun env d pps ->
- let pnat = pr_rel_decl env sigma d in
- (pps ++ fnl () ++
- str (emacs_str "") ++
- pnat))
- env ~init:(mt ())
- in
- (sign_env ++ db_env)
+(* Heuristic for horizontalizing hypothesis that the user probably
+ considers as "variables": An hypothesis H:T where T:S and S<>Prop. *)
+let should_compact env sigma typ =
+ get_compact_context() &&
+ let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in
+ not (is_Prop (EConstr.to_constr sigma type_of_typ))
+
+
+(* If option Compact Contexts is set, we pack "simple" hypothesis in a
+ hov box (with three sapaces as a separator), the global box being a
+ v box *)
+let rec bld_sign_env env sigma ctxt pps =
+ match ctxt with
+ | [] -> pps
+ | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ ->
+ let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in
+ (* putting simple hyps in a more horizontal flavor *)
+ bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps')
+ | d:: ctxt' ->
+ let pidt = pr_var_list_decl env sigma d in
+ let pps' = pps ++ brk (0,0) ++ pidt in
+ bld_sign_env env sigma ctxt' pps'
+and bld_sign_env_id env sigma ctxt pps is_start =
+ match ctxt with
+ | [] -> pps,ctxt
+ | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+ let pidt = pr_var_list_decl env sigma d in
+ let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
+ bld_sign_env_id env sigma ctxt' pps' false
+ | _ -> pps,ctxt
+
+
+(* compact printing an env (variables and de Bruijn). Separator: three
+ spaces between simple hyps, and newline otherwise *)
+let pr_context_limit_compact ?n env sigma =
+ let ctxt = Termops.compact_named_context (named_context env) in
+ let lgth = List.length ctxt in
+ let n_capped =
+ match n with
+ | None -> lgth
+ | Some n when n > lgth -> lgth
+ | Some n -> n in
+ let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in
+ (* a dot line hinting the number of hidden hyps. *)
+ let hidden_dots = String.make (List.length ctxt_hidden) '.' in
+ let sign_env = v 0 (str hidden_dots ++ (mt ())
+ ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in
+ let db_env =
+ fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
+ env ~init:(mt ()) in
+ sign_env ++ db_env
+
+(* The number of printed hypothesis in a goal *)
+(* If [None], no limit *)
+let print_hyps_limit = ref (None : int option)
-let pr_context_of env sigma = match Flags.print_hyps_limit () with
- | None -> hv 0 (pr_context_unlimited env sigma)
- | Some n -> hv 0 (pr_context_limit n env sigma)
+let _ =
+ let open Goptions in
+ declare_int_option
+ { optdepr = false;
+ optname = "the hypotheses limit";
+ optkey = ["Hyps";"Limit"];
+ optread = (fun () -> !print_hyps_limit);
+ optwrite = (fun x -> print_hyps_limit := x) }
+
+let pr_context_of env sigma = match !print_hyps_limit with
+ | None -> hv 0 (pr_context_limit_compact env sigma)
+ | Some n -> hv 0 (pr_context_limit_compact ~n env sigma)
(* display goal parts (Proof mode) *)
@@ -391,23 +491,25 @@ let default_pr_goal gs =
(* display a goal tag *)
let pr_goal_tag g =
let s = " (ID " ^ Goal.uid g ^ ")" in
- str (emacs_str s)
-
-let display_name = false
+ str s
(* display a goal name *)
let pr_goal_name sigma g =
- if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
+ if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g)
else mt ()
+let pr_goal_header nme sigma g =
+ let (g,sigma) = Goal.V82.nf_evar sigma g in
+ str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
+ ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
+
(* display the conclusion of a goal *)
let pr_concl n sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
let env = Goal.V82.env sigma g in
let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
- str (emacs_str "") ++
- str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++
- str " is:" ++ cut () ++ str" " ++ pc
+ let header = pr_goal_header (int n) sigma g in
+ header ++ str " is:" ++ cut () ++ str" " ++ pc
(* display evar type: a context and a type *)
let pr_evgl_sign sigma evi =
@@ -417,8 +519,7 @@ let pr_evgl_sign sigma evi =
| None -> [], []
| Some f -> List.filter2 (fun b c -> not b) f (evar_context evi)
in
- let open Context.Named.Declaration in
- let ids = List.rev_map get_id l in
+ let ids = List.rev_map NamedDecl.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)")
@@ -464,12 +565,12 @@ let pr_ne_evar_set hd tl sigma l =
let pr_selected_subgoal name sigma g =
let pg = default_pr_goal { sigma=sigma ; it=g; } in
- v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g
- ++ str " is:" ++ cut () ++ pg)
+ let header = pr_goal_header name sigma g in
+ v 0 (header ++ str " is:" ++ cut () ++ pg)
let default_pr_subgoal n sigma =
let rec prrec p = function
- | [] -> error "No such goal."
+ | [] -> user_err Pp.(str "No such goal.")
| g::rest ->
if Int.equal p 1 then
pr_selected_subgoal (int n) sigma g
@@ -487,15 +588,15 @@ let print_evar_constraints gl 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 ()
+ if Context.Named.equal Constr.equal (named_context env) (named_context e') then
+ if Context.Rel.equal Constr.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 t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1)
+ and t2 = Evarutil.nf_evar sigma (EConstr.of_constr 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
@@ -503,13 +604,13 @@ let print_evar_constraints gl sigma =
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
+ Namegen.make_all_name_different env sigma in
str" " ++
- hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++
+ hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc () ++ pr_lconstr_env env sigma t2)
+ spc () ++ pr_leconstr_env env sigma t2)
in
let pr_candidate ev evi (candidates,acc) =
if Option.has_some evi.evar_candidates then
@@ -534,8 +635,7 @@ let should_print_dependent_evars = ref false
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Printing Dependent Evars Line";
optkey = ["Printing";"Dependent";"Evars";"Line"];
optread = (fun () -> !should_print_dependent_evars);
@@ -558,27 +658,24 @@ let print_dependent_evars gl sigma seeds =
end i (str ",")
end evars (str "")
in
- fnl () ++
- str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
- else
- fnl () ++
- str "(dependent evars: (printing disabled) )" ++ fnl ()
+ cut () ++ cut () ++
+ str "(dependent evars:" ++ evars ++ str ")"
+ else mt ()
in
- constraints ++ delayed_emacs_cmd evars
+ constraints ++ evars ()
(* Print open subgoals. Checks for uninstantiated existential variables *)
(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
(* spiwack: [pr_first] is true when the first goal must be singled out
and printed in its entirety. *)
-(* courtieu: in emacs mode, even less cases where the first goal is printed
- in its entirety *)
-let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals =
+let default_pr_subgoals ?(pr_first=true)
+ close_cmd sigma seeds shelf stack unfocused goals =
(** Printing functions for the extra informations. *)
let rec print_stack a = function
| [] -> Pp.int a
| b::l -> Pp.int a ++ str"-" ++ print_stack b l
in
- let print_unfocused l =
+ let print_unfocused_nums l =
match l with
| [] -> None
| a::l -> Some (str"unfocused: " ++ print_stack a l)
@@ -598,7 +695,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
| [] -> Pp.mt ()
| a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")"
in
- let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in
+ let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in
let print_extra = print_extra_list extra in
let focused_if_needed =
let needed = not (CList.is_empty extra) && pr_first in
@@ -615,8 +712,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
in
let print_multiple_goals g l =
if pr_first then
- default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++
- pr_rec 2 l
+ default_pr_goal { it = g ; sigma = sigma; }
+ ++ (if l=[] then mt () else cut ())
+ ++ pr_rec 2 l
else
pr_rec 1 (g::l)
in
@@ -631,32 +729,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
begin
let exl = Evarutil.non_instantiated sigma in
if Evar.Map.is_empty exl then
- (str"No more subgoals."
- ++ print_dependent_evars None sigma seeds)
+ (str"No more subgoals." ++ 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)
- ++ print_dependent_evars None sigma seeds ++ fnl () ++
- str "You can use Grab Existential Variables.")
+ v 0 ((str "No more subgoals,"
+ ++ str " but there are non-instantiated existential variables:"
+ ++ cut () ++ (hov 0 pei)
+ ++ print_dependent_evars None sigma seeds
+ ++ cut () ++ str "You can use Grab Existential Variables."))
end
- | [g] when not !Flags.print_emacs && pr_first ->
- let pg = default_pr_goal { it = g ; sigma = sigma; } in
- v 0 (
- str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
- ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg
- ++ print_dependent_evars (Some g) sigma seeds
- )
| g1::rest ->
let goals = print_multiple_goals g1 rest in
let ngoals = List.length rest+1 in
v 0 (
- int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++
- print_extra ++
- str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1")
- ++ pr_goal_tag g1
- ++ pr_goal_name sigma g1 ++ cut ()
- ++ goals
+ int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
+ ++ print_extra
+ ++ str (if (should_gname()) then ", subgoal 1" else "")
+ ++ (if should_tag() then pr_goal_tag g1 else str"")
+ ++ pr_goal_name sigma g1 ++ cut () ++ goals
+ ++ (if unfocused=[] then str ""
+ else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
+ ++ pr_rec (List.length rest + 2) unfocused))
++ print_dependent_evars (Some g1) sigma seeds
)
@@ -665,7 +758,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
type printer_pr = {
- pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
pr_goal : goal sigma -> std_ppcmds;
}
@@ -699,30 +792,34 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
begin match goals with
| [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
begin match bgoals,shelf,given_up with
- | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
+ | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals
| [] , [] , _ ->
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
+ ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up
++ fnl () ++ str "You need to go back and solve them."
| [] , _ , _ ->
Feedback.msg_info (str "All the remaining goals are on the shelf.");
fnl ()
- ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
+ ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf
| _ , _, _ ->
let end_cmd =
str "This subproof is complete, but there are some unfocused goals." ++
(let s = Proof_global.Bullet.suggest p in
- if Pp.is_empty s then s else fnl () ++ s) ++
+ if Pp.ismt s then s else fnl () ++ s) ++
fnl ()
in
- pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
+ pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals
end
- | _ -> pr_subgoals None sigma seeds shelf stack goals
+ | _ ->
+ let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+ let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
+ let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
+ pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused
end
let pr_nth_open_subgoal n =
- let pf = get_pftreestate () in
+ let pf = Proof_global.give_me_the_proof () in
let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
pr_subgoal n sigma gls
@@ -732,7 +829,7 @@ let pr_goal_by_id id =
Proof.in_proof p (fun sigma ->
let g = Evd.evar_key id sigma in
pr_selected_subgoal (pr_id id) sigma g)
- with Not_found -> error "No such goal."
+ with Not_found -> user_err Pp.(str "No such goal.")
let pr_goal_by_uid uid =
let p = Proof_global.give_me_the_proof () in
@@ -743,7 +840,7 @@ let pr_goal_by_uid uid =
in
try
Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;})
- with Not_found -> error "Invalid goal identifier."
+ with Not_found -> user_err Pp.(str "Invalid goal identifier.")
(* Elementary tactics *)
@@ -758,7 +855,8 @@ let pr_prim_rule = function
str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
| Refine c ->
- str(if Termops.occur_meta c then "refine " else "exact ") ++
+ (** FIXME *)
+ str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
(* Backwards compatibility *)
@@ -901,6 +999,11 @@ let pr_assumptionset env s =
let xor a b =
(a && not b) || (not a && b)
+let pr_cumulative poly cum =
+ if poly then
+ if cum then str "Cumulative " else str "NonCumulative "
+ else mt ()
+
let pr_polymorphic b =
let print = xor (Flags.is_universe_polymorphism ()) b in
if print then
@@ -909,4 +1012,4 @@ 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"}"
+ str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
diff --git a/printing/printer.mli b/printing/printer.mli
index 0080bda069..f8685b0895 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -18,6 +18,11 @@ open Glob_term
(** These are the entry points for printing terms, context, tac, ... *)
+
+val enable_unfocused_goal_printing: bool ref
+val enable_goal_tags_printing : bool ref
+val enable_goal_names_printing : bool ref
+
(** Terms *)
val pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds
@@ -38,6 +43,13 @@ val safe_pr_lconstr : constr -> std_ppcmds
val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds
val safe_pr_constr : constr -> std_ppcmds
+val pr_econstr_env : env -> evar_map -> EConstr.t -> std_ppcmds
+val pr_econstr : EConstr.t -> std_ppcmds
+val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds
+val pr_leconstr : EConstr.t -> std_ppcmds
+
+val pr_etype_env : env -> evar_map -> EConstr.types -> std_ppcmds
+val pr_letype_env : env -> evar_map -> EConstr.types -> std_ppcmds
val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds
val pr_open_constr : open_constr -> std_ppcmds
@@ -51,7 +63,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds
-val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds
val pr_ltype_env : env -> evar_map -> types -> std_ppcmds
val pr_ltype : types -> std_ppcmds
@@ -61,8 +73,8 @@ val pr_type : types -> std_ppcmds
val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds
val pr_closed_glob : closed_glob_constr -> std_ppcmds
-val pr_ljudge_env : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds
-val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds
val pr_lglob_constr : glob_constr -> std_ppcmds
@@ -83,8 +95,10 @@ val pr_sort : evar_map -> sorts -> std_ppcmds
(** Universe constraints *)
val pr_polymorphic : bool -> std_ppcmds
+val pr_cumulative : bool -> bool -> std_ppcmds
val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds
val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> std_ppcmds
(** Printing global references using names as short as possible *)
@@ -104,12 +118,15 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds
(** Contexts *)
+(** Display compact contexts of goals (simple hyps on the same line) *)
+val set_compact_context : bool -> unit
+val get_compact_context : unit -> bool
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 -> Context.Named.Declaration.t -> std_ppcmds
-val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds
val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds
@@ -125,10 +142,22 @@ val pr_cpred : Cpred.t -> std_ppcmds
val pr_idpred : Id.Pred.t -> std_ppcmds
val pr_transparent_state : transparent_state -> std_ppcmds
-(** Proofs *)
+(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
val pr_goal : goal sigma -> std_ppcmds
-val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
+
+(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
+ prints the goals of the list [goals] followed by the goals in
+ [unfocused], in a short way (typically only the conclusion) except
+ for the first goal if [pr_first] is true. This function can be
+ replaced by another one by calling [set_printer_pr] (see below),
+ typically by plugin writers. The default printer prints only the
+ focused goals unless the conrresponding option
+ [enable_unfocused_goal_printing] is set. [seeds] is for printing
+ dependent evars (mainly for emacs proof tree mode). *)
+val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list
+ -> goal list -> goal list -> std_ppcmds
+
val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds
val pr_concl : int -> evar_map -> goal -> std_ppcmds
@@ -142,19 +171,6 @@ val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map ->
val pr_prim_rule : prim_rule -> std_ppcmds
-(** Emacs/proof general support
- (emacs_str s) outputs
- - s if emacs mode,
- - nothing otherwise.
- This function was previously used to insert special chars like
- [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the
- proof context for proof by pointing. This part of the code is
- removed for now because it interacted badly with utf8. We may put
- it back some day using some xml-like tags instead of special
- chars. See for example the <prompt> tag in the prompt when in
- emacs mode. *)
-val emacs_str : string -> string
-
(** Backwards compatibility *)
val prterm : constr -> std_ppcmds (** = pr_lconstr *)
@@ -183,7 +199,7 @@ val pr_goal_by_id : Id.t -> std_ppcmds
val pr_goal_by_uid : string -> std_ppcmds
type printer_pr = {
- pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
pr_goal : goal sigma -> std_ppcmds;
};;
diff --git a/printing/printing.mllib b/printing/printing.mllib
index bc8f0750e1..86b68d8fb0 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,9 +1,7 @@
Genprint
Pputils
-Ppannotation
Ppconstr
Printer
-Pptactic
Printmod
Prettyp
Ppvernac
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb8a1d97df..10b791e37f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -26,12 +26,23 @@ open Goptions
the "short" mode or (Some env) in the "rich" one.
*)
+module Tag =
+struct
+
+ let definition = "module.definition"
+ let keyword = "module.keyword"
+
+end
+
+let tag t s = Pp.tag t s
+let tag_definition s = tag Tag.definition s
+let tag_keyword s = tag Tag.keyword s
+
let short = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "short module printing";
optkey = ["Short";"Module";"Printing"];
optread = (fun () -> !short) ;
@@ -44,14 +55,8 @@ let mk_fake_top =
let r = ref 0 in
fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
-module Make (Taggers : sig
- val tag_definition : std_ppcmds -> std_ppcmds
- val tag_keyword : std_ppcmds -> std_ppcmds
-end) =
-struct
-
-let def s = Taggers.tag_definition (str s)
-let keyword s = Taggers.tag_keyword (str s)
+let def s = tag_definition (str s)
+let keyword s = tag_keyword (str s)
let get_new_id locals id =
let rec get_id l id =
@@ -83,19 +88,19 @@ let build_ind_type env mip =
Inductive.type_of_inductive env mip
let print_one_inductive env sigma mib ((_,i) as ind) =
- let u = if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ let u = if Declareops.inductive_is_polymorphic mib then
+ Declareops.inductive_polymorphic_instance mib
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = Context.Rel.to_extended_list 0 params in
+ let args = Context.Rel.to_extended_list mkRel 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
let envpar = push_rel_context params env in
let inst =
- if mib.mind_polymorphic then
- Printer.pr_universe_instance sigma mib.mind_universes
+ if Declareops.inductive_is_polymorphic mib then
+ Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
else mt ()
in
hov 0 (
@@ -115,11 +120,18 @@ let print_mutual_inductive env mind mib =
in
let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
- hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
- def keyword ++ spc () ++
- prlist_with_sep (fun () -> fnl () ++ str" with ")
- (print_one_inductive env sigma mib) inds ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+ hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
+ Printer.pr_cumulative
+ (Declareops.inductive_is_polymorphic mib)
+ (Declareops.inductive_is_cumulative mib) ++
+ def keyword ++ spc () ++
+ prlist_with_sep (fun () -> fnl () ++ str" with ")
+ (print_one_inductive env sigma mib) inds ++
+ match mib.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+ | Cumulative_ind cumi ->
+ Printer.pr_cumulativity_info
+ sigma (Univ.instantiate_cumulativity_info cumi))
let get_fields =
let rec prodec_rec l subst c =
@@ -136,13 +148,13 @@ let get_fields =
let print_record env mind mib =
let u =
- if mib.mind_polymorphic then
- Univ.UContext.instance mib.mind_universes
+ if Declareops.inductive_is_polymorphic mib then
+ Declareops.inductive_polymorphic_instance mib
else Univ.Instance.empty
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = Context.Rel.to_extended_list 0 params in
+ let args = Context.Rel.to_extended_list mkRel 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
@@ -159,7 +171,10 @@ let print_record env mind mib =
in
hov 0 (
hov 0 (
- Printer.pr_polymorphic mib.mind_polymorphic ++
+ Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
+ Printer.pr_cumulative
+ (Declareops.inductive_is_polymorphic mib)
+ (Declareops.inductive_is_cumulative mib) ++
def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
print_params env sigma params ++
str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
@@ -170,7 +185,12 @@ let print_record env mind mib =
(fun (id,b,c) ->
pr_id id ++ str (if b then " : " else " := ") ++
Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
+ match mib.mind_universes with
+ | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
+ | Cumulative_ind cumi ->
+ Printer.pr_cumulativity_info
+ sigma (Univ.instantiate_cumulativity_info cumi)
+ )
let pr_mutual_inductive_body env mind mib =
if mib.mind_record <> None && not !Flags.raw_print then
@@ -273,7 +293,8 @@ let print_body is_impl env mp (l,body) =
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
| SFBconst cb ->
let u =
- if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+ if Declareops.constant_is_polymorphic cb then
+ Declareops.constant_polymorphic_instance cb
else Univ.Instance.empty
in
let sigma = Evd.empty in
@@ -295,7 +316,8 @@ let print_body is_impl env mp (l,body) =
Printer.pr_lconstr_env env sigma
(Vars.subst_instance_constr u (Mod_subst.force_constr l)))
| _ -> mt ()) ++ str "." ++
- Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
+ Printer.pr_universe_ctx sigma
+ (Declareops.constant_polymorphic_context cb))
| SFBmind mib ->
try
let env = Option.get env in
@@ -397,11 +419,11 @@ let rec printable_body dir =
let print_expression' is_type env mp me =
States.with_state_protection
- (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
+ (fun e -> print_expression is_type env mp [] e) me
let print_signature' is_type env mp me =
States.with_state_protection
- (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
+ (fun e -> print_signature is_type env mp [] e) me
let unsafe_print_module env mp with_body mb =
let name = print_modpath [] mp in
@@ -441,20 +463,4 @@ let print_modtype kn =
with e when CErrors.noncritical e ->
print_signature' true None kn mtb.mod_type))
-end
-
-module Tag =
-struct
- let definition =
- let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
- Ppstyle.make ~style ["module"; "definition"]
- let keyword =
- let style = Terminal.make ~bold:true () in
- Ppstyle.make ~style ["module"; "keyword"]
-end
-include Make(struct
- let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
- let tag_definition s = tag Tag.definition s
- let tag_keyword s = tag Tag.keyword s
-end)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 2d0eab0cd0..81b5774537 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -6,9 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Pp
open Names
(** false iff the module is an element of an open module type *)
val printable_body : DirPath.t -> bool
-include Printmodsig.Pp
+val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
+val print_module : bool -> module_path -> std_ppcmds
+val print_modtype : module_path -> std_ppcmds
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
deleted file mode 100644
index 8dcea426ab..0000000000
--- a/printing/printmodsig.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Pp
-open Names
-
-module type Pp =
-sig
- val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
- val print_module : bool -> module_path -> std_ppcmds
- val print_modtype : module_path -> std_ppcmds
-end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:51:10 +0000