aboutsummaryrefslogtreecommitdiffhomepage
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.ml2
-rw-r--r--printing/ppannotation.ml39
-rw-r--r--printing/ppannotation.mli32
-rw-r--r--printing/ppconstr.ml175
-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.ml133
-rw-r--r--printing/pputils.mli18
-rw-r--r--printing/ppvernac.ml75
-rw-r--r--printing/ppvernac.mli15
-rw-r--r--printing/ppvernacsig.mli20
-rw-r--r--printing/prettyp.ml49
-rw-r--r--printing/prettyp.mli8
-rw-r--r--printing/printer.ml183
-rw-r--r--printing/printer.mli17
-rw-r--r--printing/printing.mllib2
-rw-r--r--printing/printmod.ml46
-rw-r--r--printing/printmod.mli5
-rw-r--r--printing/printmodsig.mli17
24 files changed, 498 insertions, 2170 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 0ec35e07b..6505a8f82 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 6e6626f2f..5381fc5bd 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 7b2c5695f..360843711 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 "<-"
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
deleted file mode 100644
index 511f93569..000000000
--- 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-2016 *)
-(* \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 a0fef1a75..000000000
--- 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-2016 *)
-(* \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 80ddd669f..38eeda9b9 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()
@@ -304,9 +317,9 @@ end) = struct
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)
+ | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc)
+ | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
+ | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc)
| _ -> assert false
let begin_of_binders = function
@@ -347,15 +360,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 +380,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
@@ -382,33 +393,33 @@ end) = struct
let rec extract_prod_binders = 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*)
+ if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
| CProdN (loc,[],c) ->
extract_prod_binders c
| CProdN (loc,[[_,Name id],bk,t],
CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
let bl,c = extract_prod_binders b in
- LocalPattern (loc,p,None) :: bl, c
+ CLocalPattern (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
+ CLocalAssum (nal,bk,t) :: bl, c
| c -> [], c
let rec extract_lam_binders = function
(* | 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*)
+ if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
| CLambdaN (loc,[],c) ->
extract_lam_binders c
| CLambdaN (loc,[[_,Name id],bk,t],
CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
let bl,c = extract_lam_binders b in
- LocalPattern (loc,p,None) :: bl, c
+ CLocalPattern (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
+ CLocalAssum (nal,bk,t) :: bl, c
| c -> [], c
let split_lambda = function
@@ -437,7 +448,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 +465,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"}"
@@ -575,7 +586,7 @@ end) = struct
pr_fun_sep ++ pr spc ltop a),
llambda
)
- | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
+ | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b)
when Id.equal x x' ->
return (
hv 0 (
@@ -585,11 +596,12 @@ 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
@@ -690,7 +702,7 @@ end) = struct
| CEvar (_,n,l) ->
return (pr_evar (pr mt) n l, latom)
| CPatVar (_,p) ->
- return (str "?" ++ pr_patvar p, latom)
+ return (str "@?" ++ pr_patvar p, latom)
| CSort (_,s) ->
return (pr_glob_sort s, latom)
| CCast (_,a,b) ->
@@ -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 0241633c6..f92caf426 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.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 3de0d805c..000000000
--- 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-2016 *)
-(* \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 fcc30d702..000000000
--- 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-2016 *)
-(* \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 86e3ea548..000000000
--- 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-2016 *)
-(* \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 665e055f2..000000000
--- 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-2016 *)
-(* \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 50ce56fb0..50630fb9b 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -6,7 +6,13 @@
(* * 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
@@ -17,3 +23,130 @@ let pr_located pr (loc, x) =
let after = Pp.comment (CLexer.extract_comments e) in
before ++ x ++ after
else 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.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) 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 a0f2c7728..b236fed70 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 5d6d36d56..e4a87739b 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)
@@ -67,7 +60,7 @@ module Make
| (loc,Name id) -> pr_lident (loc,id)
| lna -> pr_located pr_name 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 +74,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 +107,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
@@ -198,7 +191,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)
@@ -504,7 +497,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 +521,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 +534,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 ->
@@ -636,8 +619,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 +687,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
@@ -1153,18 +1134,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 +1187,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 +1221,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 d3d4a5ceb..836b05e0e 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 5e5e4bcf4..000000000
--- 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-2016 *)
-(* \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 e117f1dcb..aa422e36a 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)
(********************************)
@@ -132,7 +137,6 @@ let print_renames_list prefix l =
let need_expansion impl ref =
let typ = Global.type_of_global_unsafe ref in
let ctx = prod_assum typ in
- let 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
@@ -639,6 +648,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,7 +711,7 @@ 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
@@ -733,11 +744,10 @@ 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) ->
@@ -759,11 +769,12 @@ let print_opaque_name qid =
| 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 =
match k with
@@ -831,7 +842,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 +852,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 0eab15579..38e111034 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -27,11 +27,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 +69,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 04337f6be..35ddf2e8c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -22,6 +22,10 @@ open Constrextern
open Ppconstr
open Declarations
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+module CompactedDecl = Context.Compacted.Declaration
+
let emacs_str s =
if !Flags.print_emacs then s else ""
let delayed_emacs_cmd s =
@@ -56,7 +60,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 +74,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 +84,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 +99,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 +109,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 +157,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 " *)"
@@ -209,7 +223,7 @@ 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()
@@ -226,7 +240,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 +262,30 @@ 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
+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 +302,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 +323,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 +342,56 @@ 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)
+let rec bld_sign_env env sigma ctxt pps =
+ match ctxt with
+ | [] -> 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'
+
+
+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 hiden 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)
+
+(* compact printing an env (variables and de Bruijn). Separator: three
+ spaces between simple hyps, and newline otherwise *)
+let pr_context_unlimited_compact env sigma =
+ pr_context_limit_compact env sigma
+
+(* The number of printed hypothesis in a goal *)
+(* If [None], no limit *)
+let print_hyps_limit = ref (None : int option)
+
+let _ =
+ let open Goptions in
+ declare_int_option
+ { optsync = false;
+ 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 Flags.print_hyps_limit () with
- | None -> hv 0 (pr_context_unlimited env sigma)
- | Some n -> hv 0 (pr_context_limit n env sigma)
+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) *)
@@ -417,8 +450,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)")
@@ -487,15 +519,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 +535,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
@@ -713,7 +745,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
let end_cmd =
str "This subproof is complete, but there are some unfocused goals." ++
(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
@@ -758,7 +790,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 *)
@@ -909,4 +942,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 695ab33b2..504392e35 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -38,6 +38,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 +58,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 +68,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
@@ -108,8 +115,8 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds
val pr_context_unlimited : env -> evar_map -> std_ppcmds
val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds
-val pr_var_decl : env -> evar_map -> 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
diff --git a/printing/printing.mllib b/printing/printing.mllib
index bc8f0750e..86b68d8fb 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 dfa66d437..6f4b162d7 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -26,6 +26,18 @@ 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 _ =
@@ -44,14 +56,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 =
@@ -88,7 +94,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = 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
@@ -142,7 +148,7 @@ let print_record env mind mib =
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = 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
@@ -397,11 +403,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 +447,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 7f7d34392..f3079d5b6 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 f71fffdce..000000000
--- 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-2016 *)
-(* \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