summaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /printing
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml8
-rw-r--r--printing/genprint.mli8
-rw-r--r--printing/ppconstr.ml51
-rw-r--r--printing/ppconstr.mli13
-rw-r--r--printing/pputils.ml5
-rw-r--r--printing/pputils.mli3
-rw-r--r--printing/ppvernac.ml1252
-rw-r--r--printing/ppvernac.mli26
-rw-r--r--printing/prettyp.ml61
-rw-r--r--printing/prettyp.mli34
-rw-r--r--printing/printer.ml217
-rw-r--r--printing/printer.mli97
-rw-r--r--printing/printing.mllib2
-rw-r--r--printing/printmod.ml19
-rw-r--r--printing/printmod.mli2
-rw-r--r--printing/proof_diffs.ml635
-rw-r--r--printing/proof_diffs.mli84
17 files changed, 999 insertions, 1518 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 1bb7838a..fa53a879 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,15 +19,15 @@ open Geninterp
(* Printing generic values *)
type 'a with_level =
- { default_already_surrounded : Notation_term.tolerability;
- default_ensure_surrounded : Notation_term.tolerability;
+ { default_already_surrounded : Notation_gram.tolerability;
+ default_ensure_surrounded : Notation_gram.tolerability;
printer : 'a }
type printer_result =
| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
type top_printer_result =
| TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index fd5dd725..1a31025a 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -13,15 +13,15 @@
open Genarg
type 'a with_level =
- { default_already_surrounded : Notation_term.tolerability;
- default_ensure_surrounded : Notation_term.tolerability;
+ { default_already_surrounded : Notation_gram.tolerability;
+ default_ensure_surrounded : Notation_gram.tolerability;
printer : 'a }
type printer_result =
| PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
type top_printer_result =
| TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4c5d955c..90d2b7ab 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -18,11 +18,12 @@ open Nameops
open Libnames
open Pputils
open Ppextend
-open Notation_term
+open Glob_term
open Constrexpr
open Constrexpr_ops
+open Notation_gram
open Decl_kinds
-open Misctypes
+open Namegen
(*i*)
module Tag =
@@ -87,8 +88,6 @@ let tag_var = tag Tag.variable
| Numeral (_,b) -> if b then lposint else lnegint
| String _ -> latom
- open Notation
-
let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in
let pop r = let a = List.hd !r in r := List.tl !r; a in
@@ -160,7 +159,7 @@ let tag_var = tag Tag.variable
let pr_univ_expr = function
| Some (x,n) ->
- pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+ pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
| None -> str"_"
let pr_univ l =
@@ -170,18 +169,18 @@ let tag_var = tag Tag.variable
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
- let pr_glob_sort = function
+ let pr_glob_sort = let open Glob_term in function
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
| GType [] -> tag_type (str "Type")
| GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
- let pr_glob_level = function
+ let pr_glob_level = let open Glob_term in function
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
| GType UUnknown -> tag_type (str "Type")
| GType UAnonymous -> tag_type (str "_")
- | GType (UNamed u) -> tag_type (pr_reference u)
+ | GType (UNamed u) -> tag_type (pr_qualid u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -199,23 +198,23 @@ let tag_var = tag Tag.variable
let pr_qualid = pr_qualid
let pr_patvar = pr_id
- let pr_glob_sort_instance = function
+ let pr_glob_sort_instance = let open Glob_term in function
| GProp ->
tag_type (str "Prop")
| GSet ->
tag_type (str "Set")
| GType u ->
(match u with
- | UNamed u -> pr_reference u
+ | UNamed u -> pr_qualid u
| UAnonymous -> tag_type (str "Type")
| UUnknown -> tag_type (str "_"))
let pr_universe_instance l =
pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
- let pr_reference = CAst.with_val (function
- | Qualid qid -> pr_qualid qid
- | Ident id -> tag_var (pr_id id))
+ let pr_reference qid =
+ if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
+ else pr_qualid qid
let pr_cref ref us =
pr_reference ref ++ pr_universe_instance us
@@ -229,7 +228,7 @@ let tag_var = tag Tag.variable
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
let pr_opt_type_spc pr = function
- | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt ()
+ | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
let pr_lident {loc; v=id} =
@@ -243,8 +242,8 @@ let tag_var = tag Tag.variable
| x -> pr_ast Name.print x
let pr_or_var pr = function
- | ArgArg x -> pr x
- | ArgVar id -> pr_lident id
+ | Locus.ArgArg x -> pr x
+ | Locus.ArgVar id -> pr_lident id
let pr_prim_token = function
| Numeral (n,s) -> str (if s then n else "-"^n)
@@ -296,7 +295,7 @@ let tag_var = tag Tag.variable
| CPatOr pl ->
hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
- | CPatNotation ("( _ )",([p],[]),[]) ->
+ | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
| CPatNotation (s,(l,ll),args) ->
@@ -364,7 +363,7 @@ let tag_var = tag Tag.variable
end
| Default b ->
match t with
- | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } ->
+ | { CAst.v = CHole (_,IntroAnonymous,_) } ->
let s = prlist_with_sep spc pr_lname nal in
hov 1 (surround_implicit b s)
| _ ->
@@ -458,7 +457,7 @@ let tag_var = tag Tag.variable
let pr_case_type pr po =
match po with
- | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt()
+ | None | Some { CAst.v = CHole (_,IntroAnonymous,_) } -> mt()
| Some p ->
spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p)
@@ -565,9 +564,9 @@ let tag_var = tag Tag.variable
return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
else
return (p, lproj)
- | CAppExpl ((None,{v=Ident var},us),[t])
- | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None])
- when Id.equal var Notation_ops.ldots_var ->
+ | CAppExpl ((None,qid,us),[t])
+ | CApp ((_, {v = CRef(qid,us)}),[t,None])
+ when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
return (
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
larg
@@ -593,7 +592,7 @@ let tag_var = tag Tag.variable
hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
latom
)
- | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
+ | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
@@ -644,9 +643,9 @@ let tag_var = tag Tag.variable
lif
)
- | CHole (_,Misctypes.IntroIdentifier id,_) ->
+ | CHole (_,IntroIdentifier id,_) ->
return (str "?[" ++ pr_id id ++ str "]", latom)
- | CHole (_,Misctypes.IntroFresh id,_) ->
+ | CHole (_,IntroFresh id,_) ->
return (str "?[?" ++ pr_id id ++ str "]", latom)
| CHole (_,_,_) ->
return (str "_", latom)
@@ -666,7 +665,7 @@ let tag_var = tag Tag.variable
| CastCoerce -> str ":>"),
lcast
)
- | CNotation ("( _ )",([t],[],[],[])) ->
+ | CNotation ((_,"( _ )"),([t],[],[],[])) ->
return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
| CNotation (s,env) ->
pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1f1308b0..bca419c9 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,14 +15,13 @@
open Libnames
open Constrexpr
open Names
-open Misctypes
-open Notation_term
+open Notation_gram
val prec_less : precedence -> tolerability -> bool
val pr_tight_coma : unit -> Pp.t
-val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
val pr_lident : lident -> Pp.t
val pr_lname : lname -> Pp.t
@@ -39,16 +38,16 @@ val pr_name : Name.t -> Pp.t
[@@ocaml.deprecated "alias of Names.Name.print"]
val pr_qualid : qualid -> Pp.t
-val pr_patvar : patvar -> Pp.t
+val pr_patvar : Pattern.patvar -> Pp.t
-val pr_glob_level : glob_level -> Pp.t
-val pr_glob_sort : glob_sort -> Pp.t
+val pr_glob_level : Glob_term.glob_level -> Pp.t
+val pr_glob_sort : Glob_term.glob_sort -> Pp.t
val pr_guard_annot : (constr_expr -> Pp.t) ->
local_binder_expr list ->
lident option * recursion_order_expr ->
Pp.t
-val pr_record_body : (reference * constr_expr) list -> Pp.t
+val pr_record_body : (qualid * constr_expr) list -> Pp.t
val pr_binders : local_binder_expr list -> Pp.t
val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
diff --git a/printing/pputils.ml b/printing/pputils.ml
index c14aa318..59e5f68f 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,7 +11,6 @@
open Util
open Pp
open Genarg
-open Misctypes
open Locus
open Genredexpr
@@ -69,7 +68,7 @@ let pr_short_red_flag pr r =
let pr_red_flag pr r =
try pr_short_red_flag pr r
- with complexRedFlags ->
+ with ComplexRedFlag ->
(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 ()) ++
@@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
-let pr_or_by_notation f = function
+let pr_or_by_notation f = let open Constrexpr in function
| {CAst.loc; v=AN v} -> f v
| {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 6039168f..5b1969e2 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Genarg
-open Misctypes
open Locus
open Genredexpr
@@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
(** Prints an object surrounded by its commented location *)
val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
-val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
val pr_with_occurrences :
('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
deleted file mode 100644
index 5c5b7206..00000000
--- a/printing/ppvernac.ml
+++ /dev/null
@@ -1,1252 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Pp
-open Names
-
-open CErrors
-open Util
-open CAst
-
-open Extend
-open Vernacexpr
-open Pputils
-open Libnames
-open Constrexpr
-open Constrexpr_ops
-open Decl_kinds
-
- open Ppconstr
-
- 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)
-
- let pr_constr = pr_constr_expr
- let pr_lconstr = pr_lconstr_expr
- let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
-
- let pr_uconstraint (l, d, r) =
- pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
- pr_glob_level r
-
- let pr_univ_name_list = function
- | None -> mt ()
- | Some l ->
- str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
-
- let pr_univdecl_instance l extensible =
- prlist_with_sep spc pr_lident l ++
- (if extensible then str"+" else mt ())
-
- let pr_univdecl_constraints l extensible =
- if List.is_empty l && extensible then mt ()
- else str"|" ++ spc () ++ prlist_with_sep (fun () -> str",") pr_uconstraint l ++
- (if extensible then str"+" else mt())
-
- let pr_universe_decl l =
- let open Misctypes in
- match l with
- | None -> mt ()
- | Some l ->
- str"@{" ++ pr_univdecl_instance l.univdecl_instance l.univdecl_extensible_instance ++
- pr_univdecl_constraints l.univdecl_constraints l.univdecl_extensible_constraints ++ str "}"
-
- let pr_ident_decl (lid, l) =
- pr_lident lid ++ pr_universe_decl l
-
- let string_of_fqid fqid =
- String.concat "." (List.map Id.to_string fqid)
-
- let pr_fqid fqid = str (string_of_fqid fqid)
-
- let pr_lfqid {CAst.loc;v=fqid} =
- match loc with
- | None -> pr_fqid fqid
- | Some loc -> let (b,_) = Loc.unloc loc in
- pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid
-
- let pr_lname_decl (n, u) =
- pr_lname n ++ pr_universe_decl u
-
- let pr_smart_global = Pputils.pr_or_by_notation pr_reference
-
- let pr_ltac_ref = Libnames.pr_reference
-
- let pr_module = Libnames.pr_reference
-
- let pr_import_module = Libnames.pr_reference
-
- let sep_end = function
- | VernacBullet _
- | VernacSubproof _
- | VernacEndSubproof -> str""
- | _ -> str"."
-
- let pr_gen t = Pputils.pr_raw_generic (Global.env ()) t
-
- let sep = fun _ -> spc()
- let sep_v2 = fun _ -> str"," ++ spc()
-
- let pr_at_level = function
- | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
- | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
-
- let pr_constr_as_binder_kind = function
- | AsIdent -> keyword "as ident"
- | AsIdentOrPattern -> keyword "as pattern"
- | AsStrictPattern -> keyword "as strict pattern"
-
- let pr_strict b = if b then str "strict " else mt ()
-
- let pr_set_entry_type pr = function
- | ETName -> str"ident"
- | ETReference -> str"global"
- | ETPattern (b,None) -> pr_strict b ++ str"pattern"
- | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
- | ETConstr lev -> str"constr" ++ pr lev
- | ETOther (_,e) -> str e
- | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
- | ETBigint -> str "bigint"
- | ETBinder true -> str "binder"
- | ETBinder false -> str "closed binder"
-
- let pr_at_level_opt = function
- | None -> mt ()
- | Some n -> spc () ++ pr_at_level n
-
- let pr_set_simple_entry_type =
- pr_set_entry_type pr_at_level_opt
-
- let pr_comment pr_c = function
- | CommentConstr c -> pr_c c
- | CommentString s -> qs s
- | CommentInt n -> int n
-
- let pr_in_out_modules = function
- | SearchInside l -> spc() ++ keyword "inside" ++ spc() ++ prlist_with_sep sep pr_module l
- | SearchOutside [] -> mt()
- | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
-
- let pr_search_about (b,c) =
- (if b then str "-" else mt()) ++
- match c with
- | SearchSubPattern p -> pr_constr_pattern_expr p
- | 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 -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
- ++
- match a with
- | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
- | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
- | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
- | SearchAbout sl ->
- keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
-
- let pr_locality local = if local then keyword "Local" else keyword "Global"
-
- let pr_explanation (e,b,f) =
- let a = match e with
- | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.")
- | ExplByName id -> pr_id id in
- let a = if f then str"!" ++ a else a in
- if b then str "[" ++ a ++ str "]" else a
-
- let pr_option_ref_value = function
- | QualidRefValue id -> pr_reference id
- | StringRefValue s -> qs s
-
- let pr_printoption table b =
- prlist_with_sep spc str table ++
- pr_opt (prlist_with_sep sep pr_option_ref_value) b
-
- let pr_set_option a b =
- let pr_opt_value = function
- | IntValue None -> assert false
- (* This should not happen because of the grammar *)
- | IntValue (Some n) -> spc() ++ int n
- | StringValue s -> spc() ++ str s
- | StringOptValue None -> mt()
- | StringOptValue (Some s) -> spc() ++ str s
- | BoolValue b -> mt()
- in pr_printoption a None ++ pr_opt_value b
-
- let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)"
-
- let pr_opt_hintbases l = match l with
- | [] -> mt()
- | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
-
- let pr_reference_or_constr pr_c = function
- | HintsReference r -> pr_reference r
- | HintsConstr c -> pr_c c
-
- let pr_hint_mode = function
- | ModeInput -> str"+"
- | ModeNoHeadEvar -> str"!"
- | ModeOutput -> str"-"
-
- let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
- pr_opt (fun x -> str"|" ++ int x) pri ++
- pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
-
- let pr_hints db h pr_c pr_pat =
- let opth = pr_opt_hintbases db in
- let pph =
- match h with
- | HintsResolve l ->
- keyword "Resolve " ++ prlist_with_sep sep
- (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
- l
- | HintsImmediate l ->
- keyword "Immediate" ++ spc() ++
- prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
- | HintsUnfold l ->
- keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l
- | HintsTransparency (l, b) ->
- keyword (if b then "Transparent" else "Opaque")
- ++ spc ()
- ++ prlist_with_sep sep pr_reference l
- | HintsMode (m, l) ->
- keyword "Mode"
- ++ spc ()
- ++ pr_reference m ++ spc() ++
- prlist_with_sep spc pr_hint_mode l
- | HintsConstructors c ->
- keyword "Constructors"
- ++ spc() ++ prlist_with_sep spc pr_reference c
- | 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() ++ Pputils.pr_raw_generic (Global.env ()) tac
- in
- hov 2 (keyword "Hint "++ pph ++ opth)
-
- let pr_with_declaration pr_c = function
- | CWith_Definition (id,udecl,c) ->
- let p = pr_c c in
- keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
- | CWith_Module (id,qid) ->
- keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
- pr_ast pr_qualid qid
-
- let rec pr_module_ast leading_space pr_c = function
- | { loc ; v = CMident qid } ->
- if leading_space then
- spc () ++ pr_located pr_qualid (loc, qid)
- else
- pr_located pr_qualid (loc,qid)
- | { v = CMwith (mty,decl) } ->
- let m = pr_module_ast leading_space pr_c mty in
- let p = pr_with_declaration pr_c decl in
- m ++ spc() ++ keyword "with" ++ spc() ++ p
- | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } ->
- pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
- | { v = CMapply (me1,me2) } ->
- pr_module_ast leading_space pr_c me1 ++ spc() ++
- hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")
-
- let pr_inline = function
- | DefaultInline -> mt ()
- | NoInline -> str "[no inline]"
- | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
-
- let pr_assumption_inline = function
- | DefaultInline -> str "Inline"
- | NoInline -> mt ()
- | InlineAt i -> str "Inline(" ++ int i ++ str ")"
-
- let pr_module_ast_inl leading_space pr_c (mast,inl) =
- pr_module_ast leading_space pr_c mast ++ pr_inline inl
-
- let pr_of_module_type prc = function
- | Enforce mty -> str ":" ++ pr_module_ast_inl true prc mty
- | Check mtys ->
- prlist_strict (fun m -> str "<:" ++ pr_module_ast_inl true prc m) mtys
-
- let pr_require_token = function
- | Some true ->
- keyword "Export" ++ spc ()
- | Some false ->
- keyword "Import" ++ spc ()
- | None -> mt()
-
- let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
- let m = pr_module_ast true pr_c mty in
- spc() ++
- hov 1 (str"(" ++ pr_require_token export ++
- prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
-
- let pr_module_binders l pr_c =
- prlist_strict (pr_module_vardecls pr_c) l
-
- let pr_type_option pr_c = function
- | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
- | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
-
- let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
- fnl () ++ keyword "where " ++ qs ntn ++ str " := "
- ++ Flags.without_option Flags.beautify prc c ++
- pr_opt (fun sc -> str ": " ++ str sc) scopt
-
- let pr_binders_arg =
- pr_non_empty_arg pr_binders
-
- let pr_and_type_binders_arg bl =
- pr_binders_arg bl
-
- let pr_onescheme (idop,schem) =
- match schem with
- | InductionScheme (dep,ind,s) ->
- (match idop with
- | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
- | None -> spc ()
- ) ++
- hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
- ++ spc() ++ pr_smart_global ind) ++ spc() ++
- hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
- | CaseScheme (dep,ind,s) ->
- (match idop with
- | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
- | None -> spc ()
- ) ++
- hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
- ++ spc() ++ pr_smart_global ind) ++ spc() ++
- hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
- | EqualityScheme ind ->
- (match idop with
- | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
- | None -> spc()
- ) ++
- hov 0 (keyword "Equality for")
- ++ spc() ++ pr_smart_global ind
-
- let begin_of_inductive = function
- | [] -> 0
- | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
-
- let pr_class_rawexpr = function
- | FunClass -> keyword "Funclass"
- | SortClass -> keyword "Sortclass"
- | RefClass qid -> pr_smart_global qid
-
- let pr_assumption_token many discharge kind =
- match discharge, kind with
- | (NoDischarge,Logical) ->
- keyword (if many then "Axioms" else "Axiom")
- | (NoDischarge,Definitional) ->
- keyword (if many then "Parameters" else "Parameter")
- | (NoDischarge,Conjectural) -> str"Conjecture"
- | (DoDischarge,Logical) ->
- keyword (if many then "Hypotheses" else "Hypothesis")
- | (DoDischarge,Definitional) ->
- keyword (if many then "Variables" else "Variable")
- | (DoDischarge,Conjectural) ->
- anomaly (Pp.str "Don't know how to beautify a local conjecture.")
-
- let pr_params pr_c (xl,(c,t)) =
- hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
- (if c then str":>" else str":" ++
- spc() ++ pr_c t))
-
- let rec factorize = function
- | [] -> []
- | (c,(idl,t))::l ->
- match factorize l with
- | (xl,((c', t') as r))::l'
- when (c : bool) == c' && Pervasives.(=) t t' ->
- (** FIXME: we need equality on constr_expr *)
- (idl@xl,r)::l'
- | l' -> (idl,(c,t))::l'
-
- let pr_ne_params_list pr_c l =
- match factorize l with
- | [p] -> pr_params pr_c p
- | l ->
- prlist_with_sep spc
- (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
-
-(*
- prlist_with_sep pr_semicolon (pr_params pr_c)
-*)
-
- let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
-
- let pr_syntax_modifier = function
- | SetItemLevel (l,n) ->
- prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
- | SetItemLevelAsBinder (l,bk,n) ->
- prlist_with_sep sep_v2 str l ++
- spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
- | SetLevel n -> pr_at_level (NumLevel n)
- | SetAssoc LeftA -> keyword "left associativity"
- | SetAssoc RightA -> keyword "right associativity"
- | SetAssoc NonA -> keyword "no associativity"
- | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
- | SetOnlyPrinting -> keyword "only printing"
- | SetOnlyParsing -> keyword "only parsing"
- | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
- | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
- | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
-
- let pr_syntax_modifiers = function
- | [] -> mt()
- | l -> spc() ++
- hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
-
- let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) =
- let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
- let annot = pr_guard_annot pr_lconstr_expr bl ro in
- pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot
- ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
- ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
- ++ prlist (pr_decl_notation pr_constr) ntn
-
- let pr_statement head (idpl,(bl,c)) =
- hov 2
- (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
- (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
- str":" ++ pr_spc_lconstr c)
-
-(**************************************)
-(* Pretty printer for vernac commands *)
-(**************************************)
-
- let pr_constrarg c = spc () ++ pr_constr c
- let pr_lconstrarg c = spc () ++ pr_lconstr c
- let pr_intarg n = spc () ++ int n
-
- let pr_oc = function
- | None -> str" :"
- | Some true -> str" :>"
- | Some false -> str" :>>"
-
- let pr_record_field ((x, pri), ntn) =
- let prx = match x with
- | (oc,AssumExpr (id,t)) ->
- hov 1 (pr_lname id ++
- pr_oc oc ++ spc() ++
- pr_lconstr_expr t)
- | (oc,DefExpr(id,b,opt)) -> (match opt with
- | Some t ->
- hov 1 (pr_lname id ++
- pr_oc oc ++ spc() ++
- pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
- | None ->
- hov 1 (pr_lname id ++ str" :=" ++ spc() ++
- pr_lconstr b)) in
- let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
- prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn
-
- let pr_record_decl b c fs =
- pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
- hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
-
- let pr_printable = function
- | PrintFullContext ->
- keyword "Print All"
- | PrintSectionContext s ->
- keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
- | PrintGrammar ent ->
- keyword "Print Grammar" ++ spc() ++ str ent
- | PrintLoadPath dir ->
- keyword "Print LoadPath" ++ pr_opt DirPath.print dir
- | PrintModules ->
- keyword "Print Modules"
- | PrintMLLoadPath ->
- keyword "Print ML Path"
- | PrintMLModules ->
- keyword "Print ML Modules"
- | PrintDebugGC ->
- keyword "Print ML GC"
- | PrintGraph ->
- keyword "Print Graph"
- | PrintClasses ->
- keyword "Print Classes"
- | PrintTypeClasses ->
- keyword "Print TypeClasses"
- | PrintInstances qid ->
- keyword "Print Instances" ++ spc () ++ pr_smart_global qid
- | PrintCoercions ->
- keyword "Print Coercions"
- | PrintCoercionPaths (s,t) ->
- keyword "Print Coercion Paths" ++ spc()
- ++ pr_class_rawexpr s ++ spc()
- ++ pr_class_rawexpr t
- | PrintCanonicalConversions ->
- keyword "Print Canonical Structures"
- | PrintTables ->
- keyword "Print Tables"
- | PrintHintGoal ->
- keyword "Print Hint"
- | PrintHint qid ->
- keyword "Print Hint" ++ spc () ++ pr_smart_global qid
- | PrintHintDb ->
- keyword "Print Hint *"
- | PrintHintDbName s ->
- keyword "Print HintDb" ++ spc () ++ str s
- | PrintUniverses (b, fopt) ->
- let cmd =
- if b then "Print Sorted Universes"
- else "Print Universes"
- in
- keyword cmd ++ pr_opt str fopt
- | PrintName (qid,udecl) ->
- keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl
- | PrintModuleType qid ->
- keyword "Print Module Type" ++ spc() ++ pr_reference qid
- | PrintModule qid ->
- keyword "Print Module" ++ spc() ++ pr_reference qid
- | PrintInspect n ->
- keyword "Inspect" ++ spc() ++ int n
- | PrintScopes ->
- keyword "Print Scopes"
- | PrintScope s ->
- keyword "Print Scope" ++ spc() ++ str s
- | PrintVisibility s ->
- keyword "Print Visibility" ++ pr_opt str s
- | PrintAbout (qid,l,gopt) ->
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
- ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
- | PrintImplicit qid ->
- keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
- (* spiwack: command printing all the axioms and section variables used in a
- term *)
- | PrintAssumptions (b, t, qid) ->
- let cmd = match b, t with
- | true, true -> "Print All Dependencies"
- | true, false -> "Print Opaque Dependencies"
- | false, true -> "Print Transparent Dependencies"
- | false, false -> "Print Assumptions"
- in
- keyword cmd ++ spc() ++ pr_smart_global qid
- | PrintNamespace dp ->
- keyword "Print Namespace" ++ DirPath.print dp
- | PrintStrategy None ->
- keyword "Print Strategies"
- | PrintStrategy (Some qid) ->
- keyword "Print Strategy" ++ pr_smart_global qid
-
- let pr_using e =
- let rec aux = function
- | SsEmpty -> "()"
- | SsType -> "(Type)"
- | SsSingl { v=id } -> "("^Id.to_string id^")"
- | SsCompl e -> "-" ^ aux e^""
- | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
- | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
- | SsFwdClose e -> "("^aux e^")*"
- in Pp.str (aux e)
-
- let pr_extend s cl =
- let pr_arg a =
- try pr_gen a
- with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
- try
- let rl = Egramml.get_extend_vernac_rule s in
- let rec aux rl cl =
- match rl, cl with
- | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
- | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
- | [], [] -> []
- | _ -> assert false in
- hov 1 (pr_sequence 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_expr v =
- let return = tag_vernac v in
- match v with
- | VernacLoad (f,s) ->
- return (
- keyword "Load"
- ++ if f then
- (spc() ++ keyword "Verbose" ++ spc())
- else
- spc() ++ qs s
- )
-
- (* Proof management *)
- | VernacAbortAll ->
- return (keyword "Abort All")
- | VernacRestart ->
- return (keyword "Restart")
- | VernacUnfocus ->
- return (keyword "Unfocus")
- | VernacUnfocused ->
- return (keyword "Unfocused")
- | VernacAbort id ->
- return (keyword "Abort" ++ pr_opt pr_lident id)
- | VernacUndo i ->
- return (
- if Int.equal i 1 then keyword "Undo" else keyword "Undo" ++ pr_intarg i
- )
- | VernacUndoTo i ->
- return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
- | VernacBacktrack (i,j,k) ->
- return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k])
- | VernacFocus i ->
- return (keyword "Focus" ++ pr_opt int i)
- | VernacShow s ->
- let pr_goal_reference = function
- | OpenSubgoals -> mt ()
- | NthGoal n -> spc () ++ int n
- | GoalId id -> spc () ++ pr_id id
- in
- let pr_showable = function
- | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
- | ShowProof -> keyword "Show Proof"
- | ShowScript -> keyword "Show Script"
- | ShowExistentials -> keyword "Show Existentials"
- | ShowUniverses -> keyword "Show Universes"
- | ShowProofNames -> keyword "Show Conjectures"
- | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
- | ShowMatch id -> keyword "Show Match " ++ pr_reference id
- in
- return (pr_showable s)
- | VernacCheckGuard ->
- return (keyword "Guarded")
-
- (* Resetting *)
- | VernacResetName id ->
- return (keyword "Reset" ++ spc() ++ pr_lident id)
- | VernacResetInitial ->
- return (keyword "Reset Initial")
- | VernacBack i ->
- return (
- if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
- )
- | VernacBackTo i ->
- return (keyword "BackTo" ++ pr_intarg i)
-
- (* State management *)
- | VernacWriteState s ->
- return (keyword "Write State" ++ spc () ++ qs s)
- | VernacRestoreState s ->
- return (keyword "Restore State" ++ spc() ++ qs s)
-
- (* Syntax *)
- | VernacOpenCloseScope (opening,sc) ->
- return (
- keyword (if opening then "Open " else "Close ") ++
- keyword "Scope" ++ spc() ++ str sc
- )
- | VernacDelimiters (sc,Some key) ->
- return (
- keyword "Delimit Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ str key
- )
- | VernacDelimiters (sc, None) ->
- return (
- keyword "Undelimit Scope" ++ spc () ++ str sc
- )
- | VernacBindScope (sc,cll) ->
- return (
- keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
- )
- | VernacArgumentsScope (q,scl) ->
- let pr_opt_scope = function
- | None -> str"_"
- | Some sc -> str sc
- in
- return (
- keyword "Arguments Scope"
- ++ spc() ++ pr_smart_global q
- ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
- )
- | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *)
- return (
- hov 0 (hov 0 (keyword "Infix "
- ++ qs s ++ str " :=" ++ pr_constrarg q) ++
- pr_syntax_modifiers mv ++
- (match sn with
- | None -> mt()
- | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
- )
- | VernacNotation (c,({v=s},l),opt) ->
- return (
- hov 2 (keyword "Notation" ++ spc() ++ qs s ++
- str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
- (match opt with
- | None -> mt()
- | Some sc -> str" :" ++ spc() ++ str sc))
- )
- | VernacSyntaxExtension (_, (s, l)) ->
- return (
- keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++
- pr_syntax_modifiers l
- )
- | VernacNotationAddFormat(s,k,v) ->
- return (
- keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v
- )
-
- (* Gallina *)
- | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
- let pr_def_token dk =
- keyword (
- if Name.is_anonymous (fst id).v
- then "Goal"
- else Kindops.string_of_definition_object_kind dk)
- in
- let pr_reduce = function
- | None -> mt()
- | Some r ->
- keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
- keyword " in" ++ spc()
- in
- let pr_def_body = function
- | DefineBody (bl,red,body,d) ->
- let ty = match d with
- | None -> mt()
- | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
- in
- (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
- | ProveBody (bl,t) ->
- let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
- (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
- let (binds,typ,c) = pr_def_body b in
- return (
- hov 2 (
- pr_def_token kind ++ spc()
- ++ pr_lname_decl id ++ binds ++ typ
- ++ (match c with
- | None -> mt()
- | Some cc -> str" :=" ++ spc() ++ cc))
- )
-
- | VernacStartTheoremProof (ki,l) ->
- return (
- hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
- prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
- )
-
- | VernacEndProof Admitted ->
- return (keyword "Admitted")
-
- | VernacEndProof (Proved (opac,o)) -> return (
- match o with
- | None -> (match opac with
- | Transparent -> keyword "Defined"
- | Opaque -> keyword "Qed")
- | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
- )
- | VernacExactProof c ->
- return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
- | VernacAssumption ((discharge,kind),t,l) ->
- let n = List.length (List.flatten (List.map fst (List.map snd l))) in
- let pr_params (c, (xl, t)) =
- hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
- (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
- let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
- return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
- pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
- | VernacInductive (cum, p,f,l) ->
- let pr_constructor (coe,(id,c)) =
- hov 2 (pr_lident id ++ str" " ++
- (if coe then str":>" else str":") ++
- Flags.without_option Flags.beautify pr_spc_lconstr c)
- in
- let pr_constructor_list b l = match l with
- | Constructors [] -> mt()
- | Constructors l ->
- let fst_sep = match l with [_] -> " " | _ -> " | " in
- pr_com_at (begin_of_inductive l) ++
- fnl() ++ str fst_sep ++
- prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
- | RecordDecl (c,fs) ->
- pr_record_decl b c fs
- in
- let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) =
- hov 0 (
- str key ++ spc() ++
- (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
- pr_and_type_binders_arg indpar ++
- pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
- str" :=") ++ pr_constructor_list k lc ++
- prlist (pr_decl_notation pr_constr) ntn
- in
- let key =
- let (_,_,_,k,_),_ = List.hd l in
- let kind =
- match k with Record -> "Record" | Structure -> "Structure"
- | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
- | Class _ -> "Class" | Variant -> "Variant"
- in
- if p then
- let cm =
- match cum with
- | GlobalCumulativity | LocalCumulativity -> "Cumulative"
- | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
- in
- cm ^ " " ^ kind
- else kind
- in
- return (
- hov 1 (pr_oneind key (List.hd l)) ++
- (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
- )
-
- | VernacFixpoint (local, recs) ->
- let local = match local with
- | DoDischarge -> "Let "
- | NoDischarge -> ""
- in
- return (
- hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
- prlist_with_sep (fun _ -> fnl () ++ keyword "with"
- ++ spc ()) pr_rec_definition recs)
- )
-
- | VernacCoFixpoint (local, corecs) ->
- let local = match local with
- | DoDischarge -> keyword "Let" ++ spc ()
- | NoDischarge -> str ""
- in
- let pr_onecorec ((iddecl,bl,c,def),ntn) =
- pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
- spc() ++ pr_lconstr_expr c ++
- pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
- prlist (pr_decl_notation pr_constr) ntn
- in
- return (
- hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
- )
- | VernacScheme l ->
- return (
- hov 2 (keyword "Scheme" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onescheme l)
- )
- | VernacCombinedScheme (id, l) ->
- return (
- hov 2 (keyword "Combined Scheme" ++ spc() ++
- pr_lident id ++ spc() ++ keyword "from" ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
- )
- | VernacUniverse v ->
- return (
- hov 2 (keyword "Universe" ++ spc () ++
- prlist_with_sep (fun _ -> str",") pr_lident v)
- )
- | VernacConstraint v ->
- return (
- hov 2 (keyword "Constraint" ++ spc () ++
- prlist_with_sep (fun _ -> str",") pr_uconstraint v)
- )
-
- (* Gallina extensions *)
- | VernacBeginSection id ->
- return (hov 2 (keyword "Section" ++ spc () ++ pr_lident id))
- | VernacEndSegment id ->
- return (hov 2 (keyword "End" ++ spc() ++ pr_lident id))
- | VernacNameSectionHypSet (id,set) ->
- return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
- str ":="++spc()++pr_using set))
- | VernacRequire (from, exp, l) ->
- let from = match from with
- | None -> mt ()
- | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
- in
- return (
- hov 2
- (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
- prlist_with_sep sep pr_module l)
- )
- | VernacImport (f,l) ->
- return (
- (if f then keyword "Export" else keyword "Import") ++ spc() ++
- prlist_with_sep sep pr_import_module l
- )
- | VernacCanonical q ->
- return (
- keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
- )
- | VernacCoercion (id,c1,c2) ->
- return (
- hov 1 (
- keyword "Coercion" ++ spc() ++
- pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
- spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
- )
- | VernacIdentityCoercion (id,c1,c2) ->
- return (
- hov 1 (
- keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
- spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
- spc() ++ pr_class_rawexpr c2)
- )
-
- | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
- return (
- hov 1 (
- (if abst then keyword "Declare" ++ spc () else mt ()) ++
- keyword "Instance" ++
- (match instid with
- | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
- | { v = Anonymous }, _ -> mt ()) ++
- pr_and_type_binders_arg sup ++
- str":" ++ spc () ++
- (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
- (match props with
- | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
- | Some (true,_) -> assert false
- | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
- | None -> mt()))
- )
-
- | VernacContext l ->
- return (
- hov 1 (
- keyword "Context" ++ pr_and_type_binders_arg l)
- )
-
- | VernacDeclareInstances insts ->
- let pr_inst (id, info) =
- pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
- in
- return (
- hov 1 (keyword "Existing" ++ spc () ++
- keyword(String.plural (List.length insts) "Instance") ++
- spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
- )
-
- | VernacDeclareClass id ->
- return (
- hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
- )
-
- (* Modules and Module Types *)
- | VernacDefineModule (export,m,bl,tys,bd) ->
- let b = pr_module_binders bl pr_lconstr in
- return (
- hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
- pr_lident m ++ b ++
- pr_of_module_type pr_lconstr tys ++
- (if List.is_empty bd then mt () else str ":= ") ++
- prlist_with_sep (fun () -> str " <+")
- (pr_module_ast_inl true pr_lconstr) bd)
- )
- | VernacDeclareModule (export,id,bl,m1) ->
- let b = pr_module_binders bl pr_lconstr in
- return (
- hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
- pr_lident id ++ b ++ str " :" ++
- pr_module_ast_inl true pr_lconstr m1)
- )
- | VernacDeclareModuleType (id,bl,tyl,m) ->
- let b = pr_module_binders bl pr_lconstr in
- let pr_mt = pr_module_ast_inl true pr_lconstr in
- return (
- hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
- prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
- (if List.is_empty m then mt () else str ":= ") ++
- prlist_with_sep (fun () -> str " <+ ") pr_mt m)
- )
- | VernacInclude (mexprs) ->
- let pr_m = pr_module_ast_inl false pr_lconstr in
- return (
- hov 2 (keyword "Include" ++ spc() ++
- prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
- )
- (* Solving *)
- | VernacSolveExistential (i,c) ->
- return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (fl,s,d) ->
- return (
- hov 2
- (keyword "Add" ++
- (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
- keyword "LoadPath" ++ spc() ++ qs s ++
- (match d with
- | None -> mt()
- | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
- )
- | VernacRemoveLoadPath s ->
- return (keyword "Remove LoadPath" ++ qs s)
- | VernacAddMLPath (fl,s) ->
- return (
- keyword "Add"
- ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
- ++ keyword "ML Path"
- ++ qs s
- )
- | VernacDeclareMLModule (l) ->
- return (
- hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
- )
- | VernacChdir s ->
- return (keyword "Cd" ++ pr_opt qs s)
-
- (* Commands *)
- | VernacCreateHintDb (dbname,b) ->
- return (
- hov 1 (keyword "Create HintDb" ++ spc () ++
- str dbname ++ (if b then str" discriminated" else mt ()))
- )
- | VernacRemoveHints (dbnames, ids) ->
- return (
- hov 1 (keyword "Remove Hints" ++ spc () ++
- prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
- pr_opt_hintbases dbnames)
- )
- | VernacHints (dbnames,h) ->
- return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
- | VernacSyntacticDefinition (id,(ids,c),compat) ->
- return (
- hov 2
- (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
- prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
- pr_syntax_modifiers
- (match compat with
- | None -> []
- | Some Flags.Current -> [SetOnlyParsing]
- | Some v -> [SetCompatVersion v]))
- )
- | VernacDeclareImplicits (q,[]) ->
- return (
- hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q)
- )
- | VernacDeclareImplicits (q,impls) ->
- return (
- hov 1 (keyword "Implicit Arguments" ++ spc () ++
- spc() ++ pr_smart_global q ++ spc() ++
- prlist_with_sep spc (fun imps ->
- str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
- impls)
- )
- | VernacArguments (q, args, more_implicits, nargs, mods) ->
- return (
- hov 2 (
- keyword "Arguments" ++ spc() ++
- pr_smart_global q ++
- let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
- let pr_if b x = if b then x else str "" in
- let pr_br imp x = match imp with
- | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
- | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
- | Vernacexpr.NotImplicit -> x in
- let rec print_arguments n l =
- match n, l with
- | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
- | _, [] -> mt()
- | n, { name = id; recarg_like = k;
- notation_scope = s;
- implicit_status = imp } :: tl ->
- spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
- print_arguments (Option.map pred n) tl
- in
- let rec print_implicits = function
- | [] -> mt ()
- | (name, impl) :: rest ->
- spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
- in
- print_arguments nargs args ++
- if not (List.is_empty more_implicits) then
- prlist (fun l -> str"," ++ print_implicits l) more_implicits
- else (mt ()) ++
- (if not (List.is_empty mods) then str" : " else str"") ++
- prlist_with_sep (fun () -> str", " ++ spc()) (function
- | `ReductionDontExposeCase -> keyword "simpl nomatch"
- | `ReductionNeverUnfold -> keyword "simpl never"
- | `DefaultImplicits -> keyword "default implicits"
- | `Rename -> keyword "rename"
- | `Assert -> keyword "assert"
- | `ExtraScopes -> keyword "extra scopes"
- | `ClearImplicits -> keyword "clear implicits"
- | `ClearScopes -> keyword "clear scopes")
- mods)
- )
- | VernacReserve bl ->
- let n = List.length (List.flatten (List.map fst bl)) in
- return (
- hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
- ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
- )
- | VernacGeneralizable g ->
- return (
- hov 1 (tag_keyword (
- str"Generalizable Variable" ++
- match g with
- | None -> str "s none"
- | Some [] -> str "s all"
- | Some idl ->
- str (if List.length idl > 1 then "s " else " ") ++
- prlist_with_sep spc pr_lident idl)
- ))
- | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
- return (
- hov 1 (keyword "Transparent" ++
- spc() ++ prlist_with_sep sep pr_smart_global l)
- )
- | VernacSetOpacity(Conv_oracle.Opaque,l) ->
- return (
- hov 1 (keyword "Opaque" ++
- spc() ++ prlist_with_sep sep pr_smart_global l)
- )
- | VernacSetOpacity _ ->
- return (
- CErrors.anomaly (keyword "VernacSetOpacity used to set something else.")
- )
- | VernacSetStrategy l ->
- let pr_lev = function
- | Conv_oracle.Opaque -> keyword "opaque"
- | Conv_oracle.Expand -> keyword "expand"
- | l when Conv_oracle.is_transparent l -> keyword "transparent"
- | Conv_oracle.Level n -> int n
- in
- let pr_line (l,q) =
- hov 2 (pr_lev l ++ spc() ++
- str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]")
- in
- return (
- hov 1 (keyword "Strategy" ++ spc() ++
- hv 0 (prlist_with_sep sep pr_line l))
- )
- | VernacUnsetOption (export, na) ->
- let export = if export then keyword "Export" ++ spc () else mt () in
- return (
- hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None)
- )
- | VernacSetOption (export, na,v) ->
- let export = if export then keyword "Export" ++ spc () else mt () in
- return (
- hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v)
- )
- | VernacAddOption (na,l) ->
- return (
- hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacRemoveOption (na,l) ->
- return (
- hov 2 (keyword "Remove" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacMemOption (na,l) ->
- return (
- hov 2 (keyword "Test" ++ spc() ++ pr_printoption na (Some l))
- )
- | VernacPrintOption na ->
- return (
- hov 2 (keyword "Test" ++ spc() ++ pr_printoption na None)
- )
- | VernacCheckMayEval (r,io,c) ->
- let pr_mayeval r c = match r with
- | Some r0 ->
- hov 2 (keyword "Eval" ++ spc() ++
- pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) 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 -> Proof_bullet.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) keyword r
- )
- | VernacPrint p ->
- return (pr_printable p)
- | VernacSearch (sea,g,sea_r) ->
- return (pr_search sea g sea_r pr_constr_pattern_expr)
- | VernacLocate loc ->
- let pr_locate =function
- | LocateAny qid -> pr_smart_global qid
- | LocateTerm qid -> keyword "Term" ++ spc() ++ pr_smart_global qid
- | LocateFile f -> keyword "File" ++ spc() ++ qs f
- | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
- | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
- | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
- in
- return (keyword "Locate" ++ spc() ++ pr_locate loc)
- | VernacRegister (id, RegisterInline) ->
- return (
- hov 2
- (keyword "Register Inline" ++ spc() ++ pr_lident id)
- )
- | VernacComments l ->
- return (
- hov 2
- (keyword "Comments" ++ spc()
- ++ prlist_with_sep sep (pr_comment pr_constr) l)
- )
-
- (* Toplevel control *)
- | VernacToplevelControl exn ->
- return (pr_topcmd exn)
-
- (* For extension *)
- | VernacExtend (s,c) ->
- return (pr_extend s c)
- | VernacProof (None, None) ->
- return (keyword "Proof")
- | VernacProof (None, Some e) ->
- return (keyword "Proof " ++ spc () ++
- keyword "using" ++ spc() ++ pr_using e)
- | VernacProof (Some te, None) ->
- return (keyword "Proof with" ++ spc() ++ 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() ++ Pputils.pr_raw_generic (Global.env ()) te
- )
- | VernacProofMode s ->
- return (keyword "Proof Mode" ++ str s)
- | VernacBullet b ->
- return (begin match b with
- | Dash n -> str (String.make n '-')
- | Star n -> str (String.make n '*')
- | Plus n -> str (String.make n '+')
- end)
- | VernacSubproof None ->
- return (str "{")
- | VernacSubproof (Some i) ->
- return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
- | VernacEndSubproof ->
- return (str "}")
-
-let pr_vernac_flag =
- function
- | VernacPolymorphic true -> keyword "Polymorphic"
- | VernacPolymorphic false -> keyword "Monomorphic"
- | VernacProgram -> keyword "Program"
- | VernacLocal local -> pr_locality local
-
- let rec pr_vernac_control v =
- let return = tag_vernac v in
- match v with
- | VernacExpr (f, v') ->
- List.fold_right
- (fun f a -> pr_vernac_flag f ++ spc() ++ a)
- f
- (pr_vernac_expr v' ++ sep_end v')
- | VernacTime (_,{v}) ->
- return (keyword "Time" ++ spc() ++ pr_vernac_control v)
- | VernacRedirect (s, {v}) ->
- return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
- | VernacTimeout(n,v) ->
- return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
- | VernacFail v ->
- return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
-
- let pr_vernac v =
- try pr_vernac_control v
- with e -> CErrors.print e
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
deleted file mode 100644
index 4aa24bf5..00000000
--- a/printing/ppvernac.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** This module implements pretty-printers for vernac_expr syntactic
- objects and their subcomponents. *)
-
-val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
-
-(** Prints a fixpoint body *)
-val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
-
-(** Prints a vernac expression without dot *)
-val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t
-
-(** Prints a "proof using X" clause. *)
-val pr_using : Vernacexpr.section_subset_expr -> Pp.t
-
-(** Prints a vernac expression and closes it with a dot. *)
-val pr_vernac : Vernacexpr.vernac_control -> Pp.t
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f17d844..1810cc65 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -26,7 +26,6 @@ open Libobject
open Libnames
open Globnames
open Recordops
-open Misctypes
open Printer
open Printmod
open Context.Rel.Declaration
@@ -35,13 +34,13 @@ open Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
type object_pr = {
- print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
- print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
print_modtype : ModPath.t -> Pp.t;
- print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t;
+ print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
@@ -77,7 +76,9 @@ let print_ref reduce ref udecl =
let typ = EConstr.of_constr typ in
let typ =
if reduce then
- let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
in EConstr.it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref in
@@ -93,11 +94,12 @@ let print_ref reduce ref udecl =
let inst = Univ.AUContext.instance univs in
let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
let env = Global.env () in
- let bl = Universes.universe_binders_with_opt_names ref
+ let bl = UnivNames.universe_binders_with_opt_names ref
(Array.to_list (Univ.Instance.to_array inst)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let inst =
- if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
+ if Global.is_polymorphic ref
+ then Printer.pr_universe_instance sigma (Univ.UContext.instance univs)
else mt ()
in
hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
@@ -245,13 +247,13 @@ let print_type_in_type ref =
else []
let print_primitive_record recflag mipv = function
- | Some (Some (_, ps,_)) ->
+ | PrimRecord _ ->
let eta = match recflag with
| CoFinite | Finite -> str" without eta conversion"
| BiFinite -> str " with eta conversion"
in
[Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
- | _ -> []
+ | FakeRecord | NotRecord -> []
let print_primitive ref =
match ref with
@@ -328,7 +330,7 @@ type 'a locatable_info = {
type locatable = Locatable : 'a locatable_info -> locatable
type logical_name =
- | Term of global_reference
+ | Term of GlobRef.t
| Dir of global_dir_reference
| Syntactic of KerName.t
| ModuleType of ModPath.t
@@ -343,8 +345,7 @@ let register_locatable name f =
exception ObjFound of logical_name
-let locate_any_name ref =
- let {v=qid} = qualid_of_reference ref in
+let locate_any_name qid =
try Term (Nametab.locate qid)
with Not_found ->
try Syntactic (Nametab.locate_syndef qid)
@@ -376,7 +377,6 @@ let pr_located_qualid = function
| DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
| DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
| DirModule { obj_dir ; _ } -> "Module", obj_dir
- | DirClosedSection dir -> "Closed Section", dir
in
str s ++ spc () ++ DirPath.print dir
| ModuleType mp ->
@@ -452,8 +452,7 @@ type locatable_kind =
| LocOther of string
| LocAny
-let print_located_qualid name flags ref =
- let {v=qid} = qualid_of_reference ref in
+let print_located_qualid name flags qid =
let located = match flags with
| LocTerm -> locate_term qid
| LocModule -> locate_modtype qid @ locate_module qid
@@ -554,8 +553,7 @@ let print_instance sigma cb =
if Declareops.constant_is_polymorphic cb then
let univs = Declareops.constant_polymorphic_context cb in
let inst = Univ.AUContext.instance univs in
- let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
- pr_universe_instance sigma univs
+ pr_universe_instance sigma inst
else mt()
let print_constant with_values sep sp udecl =
@@ -595,7 +593,7 @@ let print_constant with_values sep sp udecl =
in
let ctx =
UState.of_binders
- (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+ (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
in
let env = Global.env () and sigma = Evd.from_ctx ctx in
let pr_ltype = pr_ltype_env env sigma in
@@ -659,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent =
gallina_print_leaf_entry env sigma with_values (oname,lobj)
| (oname,Lib.OpenedSection (dir,_)) ->
Some (str " >>>>>>> Section " ++ pr_name oname)
- | (oname,Lib.ClosedSection _) ->
- Some (str " >>>>>>> Closed Section " ++ pr_name oname)
| (_,Lib.CompilingLibrary { obj_dir; _ }) ->
Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
| (oname,Lib.OpenedModule _) ->
Some (str " >>>>>>> Module " ++ pr_name oname)
- | (oname,Lib.ClosedModule _) ->
- Some (str " >>>>>>> Closed Module " ++ pr_name oname)
let gallina_print_context env sigma with_values =
let rec prec n = function
@@ -718,7 +712,10 @@ let print_eval x = !object_pr.print_eval x
(**** Printing declarations and judgments *)
(**** Abstract layer *****)
-let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x
+let print_typed_value x =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ print_typed_value_in_env env sigma x
let print_judgment env sigma {uj_val=trm;uj_type=typ} =
print_typed_value_in_env env sigma (trm, typ)
@@ -784,18 +781,14 @@ let print_full_pure_context env sigma =
follows the definition of the inductive type *)
(* This is designed to print the contents of an opened section *)
-let read_sec_context r =
- let qid = qualid_of_reference r in
+let read_sec_context qid =
let dir =
- try Nametab.locate_section qid.v
+ try Nametab.locate_section qid
with Not_found ->
user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest ->
if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
- | (_,Lib.ClosedSection _)::rest ->
- user_err Pp.(str "Cannot print the contents of a closed section.")
- (* LEM: Actually, we could if we wanted to. *)
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
in
@@ -839,12 +832,12 @@ let print_any_name env sigma na udecl =
let print_name env sigma na udecl =
match na with
- | {loc; v=ByNotation (ntn,sc)} ->
+ | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
print_any_name env sigma
(Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
ntn sc))
udecl
- | {loc; v=AN ref} ->
+ | {loc; v=Constrexpr.AN ref} ->
print_any_name env sigma (locate_any_name ref) udecl
let print_opaque_name env sigma qid =
@@ -892,11 +885,11 @@ let print_about_any ?loc env sigma k udecl =
let print_about env sigma na udecl =
match na with
- | {loc;v=ByNotation (ntn,sc)} ->
+ | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
print_about_any ?loc env sigma
(Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
ntn sc)) udecl
- | {loc;v=AN ref} ->
+ | {loc;v=Constrexpr.AN ref} ->
print_about_any ?loc env sigma (locate_any_name ref) udecl
(* for debug *)
@@ -909,7 +902,7 @@ let inspect env sigma depth =
open Classops
-let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v)
+let print_coercion_value env sigma v = Printer.pr_global v.coe_value
let print_class i =
let cl,_ = class_info_from_index i in
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 213f0aee..1668bce2 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,8 +12,6 @@ open Names
open Environ
open Reductionops
open Libnames
-open Globnames
-open Misctypes
open Evd
(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
@@ -26,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node
val print_full_context : env -> Evd.evar_map -> Pp.t
val print_full_context_typ : env -> Evd.evar_map -> Pp.t
val print_full_pure_context : env -> Evd.evar_map -> Pp.t
-val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t
-val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t
+val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t
val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
val print_eval :
reduction_function -> env -> Evd.evar_map ->
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
-val print_name : env -> Evd.evar_map -> reference or_by_notation ->
- Universes.univ_name_list option -> Pp.t
-val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation ->
- Universes.univ_name_list option -> Pp.t
-val print_impargs : reference or_by_notation -> Pp.t
+val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
+ UnivNames.univ_name_list option -> Pp.t
+val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t
+val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
+ UnivNames.univ_name_list option -> Pp.t
+val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
val print_graph : env -> evar_map -> Pp.t
@@ -50,7 +48,7 @@ val print_canonical_projections : env -> Evd.evar_map -> Pp.t
(** Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> Pp.t
-val print_instances : global_reference -> Pp.t
+val print_instances : GlobRef.t -> Pp.t
val print_all_instances : unit -> Pp.t
val inspect : env -> Evd.evar_map -> int -> Pp.t
@@ -79,19 +77,19 @@ val register_locatable : string -> 'a locatable_info -> unit
name describing the kind of objects considered and that is added as a
grammar command prefix for vernacular commands Locate. *)
-val print_located_qualid : reference -> Pp.t
-val print_located_term : reference -> Pp.t
-val print_located_module : reference -> Pp.t
-val print_located_other : string -> reference -> Pp.t
+val print_located_qualid : qualid -> Pp.t
+val print_located_term : qualid -> Pp.t
+val print_located_module : qualid -> Pp.t
+val print_located_other : string -> qualid -> Pp.t
type object_pr = {
- print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
- print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
print_modtype : ModPath.t -> Pp.t;
- print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t;
+ print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 199aa79c..b4038e0f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -82,24 +82,23 @@ let pr_econstr_n_core goal_concl_style env sigma n t =
pr_constr_expr_n n (extern_constr goal_concl_style env sigma t)
let pr_econstr_core goal_concl_style env sigma t =
pr_constr_expr (extern_constr goal_concl_style env sigma t)
-let pr_leconstr_core goal_concl_style env sigma t =
- pr_lconstr_expr (extern_constr goal_concl_style env sigma t)
+let pr_leconstr_core = Proof_diffs.pr_leconstr_core
let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
-let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+let pr_lconstr_env = Proof_diffs.pr_lconstr_env
let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
let _ = Hook.set Refine.pr_constr pr_constr_env
let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c)
let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c)
-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
-
let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
+let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c
+let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c
+
(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
let pr_lconstr t =
let (sigma, env) = Pfedit.get_current_context () in
@@ -108,12 +107,12 @@ let pr_constr t =
let (sigma, env) = Pfedit.get_current_context () in
pr_constr_env env sigma 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_open_lconstr (_,c) = pr_leconstr c
+let pr_open_constr (_,c) = pr_econstr 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 *)
@@ -133,8 +132,7 @@ let pr_lconstr_under_binders c =
let pr_etype_core goal_concl_style env sigma t =
pr_constr_expr (extern_type goal_concl_style env sigma t)
-let pr_letype_core goal_concl_style env sigma t =
- pr_lconstr_expr (extern_type goal_concl_style env sigma t)
+let pr_letype_core = Proof_diffs.pr_letype_core
let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
@@ -194,7 +192,7 @@ let pr_constr_pattern t =
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
-let _ = Termops.set_print_constr
+let _ = Termops.Internal.set_print_constr
(fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
@@ -229,15 +227,15 @@ let dirpath_of_global = function
dirpath_of_mp (MutInd.modpath kn)
| VarRef _ -> DirPath.empty
-let qualid_of_global env r =
- Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+let qualid_of_global ?loc env r =
+ Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r)
let safe_gen f env sigma c =
let orig_extern_ref = Constrextern.get_extern_reference () in
let extern_ref ?loc vars r =
try orig_extern_ref vars r
with e when CErrors.noncritical e ->
- CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r)
+ qualid_of_global ?loc env r
in
Constrextern.set_extern_reference extern_ref;
try
@@ -290,17 +288,19 @@ let pr_cumulativity_info sigma cumi =
let pr_global_env = pr_global_env
let pr_global = pr_global_env Id.Set.empty
-let pr_puniverses f env (c,u) =
- f env c ++
- (if !Constrextern.print_universes then
- str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
- else mt ())
+let pr_universe_instance evd inst =
+ str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+
+let pr_puniverses f env sigma (c,u) =
+ if !Constrextern.print_universes
+ then f env c ++ pr_universe_instance sigma u
+ else f env c
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
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)
+let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr)
let pr_pconstant = pr_puniverses pr_constant
let pr_pinductive = pr_puniverses pr_inductive
@@ -493,16 +493,23 @@ let pr_transparent_state (ids, csts) =
hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
-(* display complete goal *)
-let default_pr_goal gs =
- let g = sig_it gs in
- let sigma = project gs in
+(* display complete goal
+ og_s has goal+sigma on the previous proof step for diffs
+ g_s has goal+sigma on the current proof step
+ *)
+let pr_goal ?(diffs=false) ?og_s g_s =
+ let g = sig_it g_s in
+ let sigma = project g_s in
let env = Goal.V82.env sigma g in
let concl = Goal.V82.concl sigma g in
let goal =
- pr_context_of env sigma ++ cut () ++
- str "============================" ++ cut () ++
- pr_goal_concl_style_env env sigma concl in
+ if diffs then
+ Proof_diffs.diff_goal ?og_s g sigma
+ else
+ pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ pr_goal_concl_style_env env sigma concl
+ in
str " " ++ v 0 goal
(* display a goal tag *)
@@ -518,13 +525,18 @@ let pr_goal_name sigma g =
let pr_goal_header nme sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
- ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
+ ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
(* display the conclusion of a goal *)
-let pr_concl n sigma g =
+let pr_concl n ?(diffs=false) ?og_s sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
let env = Goal.V82.env sigma g in
- let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
+ let pc =
+ if diffs then
+ Proof_diffs.diff_concl ?og_s sigma g
+ else
+ pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+ in
let header = pr_goal_header (int n) sigma g in
header ++ str " is:" ++ cut () ++ str" " ++ pc
@@ -541,12 +553,12 @@ let pr_evgl_sign sigma evi =
if List.is_empty ids then mt () else
(str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
- let pc = pr_lconstr_env env sigma evi.evar_concl in
+ let pc = pr_leconstr_env env sigma evi.evar_concl in
let candidates =
match evi.evar_body, evi.evar_candidates with
| Evar_empty, Some l ->
spc () ++ str "= {" ++
- prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}"
+ prlist_with_sep (fun () -> str "|") (pr_leconstr_env env sigma) l ++ str "}"
| _ ->
mt ()
in
@@ -591,11 +603,11 @@ let pr_ne_evar_set hd tl sigma l =
mt ()
let pr_selected_subgoal name sigma g =
- let pg = default_pr_goal { sigma=sigma ; it=g; } in
+ let pg = pr_goal { sigma=sigma ; it=g; } in
let header = pr_goal_header name sigma g in
v 0 (header ++ str " is:" ++ cut () ++ pg)
-let default_pr_subgoal n sigma =
+let pr_subgoal n sigma =
let rec prrec p = function
| [] -> user_err Pp.(str "No such goal.")
| g::rest ->
@@ -622,8 +634,8 @@ let print_evar_constraints gl sigma =
end
in
let pr_evconstr (pbty,env,t1,t2) =
- let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1)
- and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in
+ let t1 = Evarutil.nf_evar sigma t1
+ and t2 = Evarutil.nf_evar sigma t2 in
let env =
(** We currently allow evar instances to refer to anonymous de Bruijn
indices, so we protect the error printing code in this case by giving
@@ -691,12 +703,25 @@ let print_dependent_evars gl sigma seeds =
in
constraints ++ evars ()
+module GoalMap = Evar.Map
+
(* Print open subgoals. Checks for uninstantiated existential variables *)
(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
(* spiwack: [pr_first] is true when the first goal must be singled out
and printed in its entirety. *)
-let default_pr_subgoals ?(pr_first=true)
+(* [os_map] is derived from the previous proof step, used for diffs *)
+let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
+ let diff_goal_map =
+ match os_map with
+ | Some (_, diff_goal_map) -> diff_goal_map
+ | None -> GoalMap.empty
+ in
+
+ let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
+ try GoalMap.find ng diff_goal_map with Not_found -> ng
+ in
+
(** Printing functions for the extra informations. *)
let rec print_stack a = function
| [] -> Pp.int a
@@ -729,17 +754,24 @@ let default_pr_subgoals ?(pr_first=true)
if needed then str" focused "
else str" " (* non-breakable space *)
in
- (** Main function *)
+
+ let get_ogs g =
+ match os_map with
+ | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma }
+ | None -> None
+ in
let rec pr_rec n = function
| [] -> (mt ())
| g::rest ->
- let pc = pr_concl n sigma g in
+ let og_s = get_ogs g in
+ let pc = pr_concl n ~diffs ?og_s sigma g in
let prest = pr_rec (n+1) rest in
(cut () ++ pc ++ prest)
in
let print_multiple_goals g l =
if pr_first then
- default_pr_goal { it = g ; sigma = sigma; }
+ let og_s = get_ogs g in
+ pr_goal ~diffs ?og_s { it = g ; sigma = sigma }
++ (if l=[] then mt () else cut ())
++ pr_rec 2 l
else
@@ -751,6 +783,8 @@ let default_pr_subgoals ?(pr_first=true)
| Some cmd -> Feedback.msg_info cmd
| None -> ()
in
+
+ (** Main function *)
match goals with
| [] ->
begin
@@ -780,34 +814,7 @@ let default_pr_subgoals ?(pr_first=true)
++ print_dependent_evars (Some g1) sigma seeds
)
-(**********************************************************************)
-(* Abstraction layer *)
-
-
-type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t;
- pr_subgoal : int -> evar_map -> goal list -> Pp.t;
- pr_goal : goal sigma -> Pp.t;
-}
-
-let default_printer_pr = {
- pr_subgoals = default_pr_subgoals;
- pr_subgoal = default_pr_subgoal;
- pr_goal = default_pr_goal;
-}
-
-let printer_pr = ref default_printer_pr
-
-let set_printer_pr = (:=) printer_pr
-
-let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x
-let pr_subgoal x = !printer_pr.pr_subgoal x
-let pr_goal x = !printer_pr.pr_goal x
-
-(* End abstraction layer *)
-(**********************************************************************)
-
-let pr_open_subgoals ~proof =
+let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
(* spiwack: it shouldn't be the job of the printer to look up stuff
in the [evar_map], I did stuff that way because it was more
straightforward, but seriously, [Proof.proof] should return
@@ -830,21 +837,33 @@ let pr_open_subgoals ~proof =
fnl ()
++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf
| _ , _, _ ->
- let end_cmd =
- str "This subproof is complete, but there are some unfocused goals." ++
- (let s = Proof_bullet.suggest p in
- if Pp.ismt s then s else fnl () ++ s) ++
- fnl ()
+ let cmd = if quiet then None else
+ Some
+ (str "This subproof is complete, but there are some unfocused goals." ++
+ (let s = Proof_bullet.suggest p in
+ if Pp.ismt s then s else fnl () ++ s) ++
+ fnl ())
in
- pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
+ pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
end
| _ ->
let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
- pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused
+ let os_map = match oproof with
+ | Some op when diffs ->
+ let (_,_,_,_, osigma) = Proof.proof op in
+ let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
+ Some (osigma, diff_goal_map)
+ | _ -> None
+ in
+ pr_subgoals ~pr_first:true ~diffs ?os_map None bsigma ~seeds ~shelf ~stack:[]
+ ~unfocused:unfocused_if_needed ~goals:bgoals_focused
end
+let pr_open_subgoals ~proof =
+ pr_open_subgoals_diff proof
+
let pr_nth_open_subgoal ~proof n =
let gls,_,_,_,sigma = Proof.proof proof in
pr_subgoal n sigma gls
@@ -879,7 +898,7 @@ type axiom =
type context_object =
| Variable of Id.t (* A section variable or a Let definition *)
- | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+ | Axiom of axiom * (Label.t * Constr.rel_context * types) list
| Opaque of Constant.t (* An opaque constant. *)
| Transparent of Constant.t
@@ -925,11 +944,18 @@ let pr_assumptionset env sigma s =
let safe_pr_constant env kn =
try pr_constant env kn
with Not_found ->
+ (* FIXME? *)
let mp,_,lab = Constant.repr3 kn in
str (ModPath.to_string mp) ++ str "." ++ Label.print lab
in
- let safe_pr_ltype typ =
- try str " : " ++ pr_ltype typ
+ let safe_pr_inductive env kn =
+ try pr_inductive env (kn,0)
+ with Not_found ->
+ (* FIXME? *)
+ MutInd.print kn
+ in
+ let safe_pr_ltype env sigma typ =
+ try str " : " ++ pr_ltype_env env sigma typ
with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
@@ -940,9 +966,9 @@ let pr_assumptionset env sigma s =
let pr_axiom env ax typ =
match ax with
| Constant kn ->
- safe_pr_constant env kn ++ safe_pr_ltype typ
+ safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
| Positive m ->
- hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+ hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
| Guarded kn ->
hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
in
@@ -950,7 +976,7 @@ let pr_assumptionset env sigma s =
let (v, a, o, tr) = accu in
match t with
| Variable id ->
- let var = pr_id id ++ str " : " ++ pr_ltype typ in
+ let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in
(var :: v, a, o, tr)
| Axiom (axiom, []) ->
let ax = pr_axiom env axiom typ in
@@ -964,10 +990,10 @@ let pr_assumptionset env sigma s =
l in
(v, ax :: a, o, tr)
| Opaque kn ->
- let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
+ let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
(v, a, opq :: o, tr)
| Transparent kn ->
- let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in
+ let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
(v, a, o, tran :: tr)
in
let (vars, axioms, opaque, trans) =
@@ -1014,6 +1040,21 @@ let pr_polymorphic b =
if b then str"Polymorphic " else str"Monomorphic "
else mt ()
-let pr_universe_instance evd ctx =
- let inst = Univ.UContext.instance ctx in
- str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+(* print the proof step, possibly with diffs highlighted, *)
+let print_and_diff oldp newp =
+ match newp with
+ | None -> ()
+ | Some proof ->
+ let output =
+ if Proof_diffs.show_diffs () then
+ try pr_open_subgoals_diff ~diffs:true ?oproof:oldp proof
+ with Pp_diff.Diff_Failure msg -> begin
+ (* todo: print the unparsable string (if we know it) *)
+ Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
+ ++ str "Showing results without diff highlighting" );
+ pr_open_subgoals ~proof
+ end
+ else
+ pr_open_subgoals ~proof
+ in
+ Feedback.msg_notice output;;
diff --git a/printing/printer.mli b/printing/printer.mli
index 41843680..518c5b93 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Globnames
open Constr
open Environ
open Pattern
@@ -37,7 +36,7 @@ val pr_constr : constr -> Pp.t
[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
-val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
(** Same, but resilient to [Nametab] errors. Prints fully-qualified
names when [shortest_qualid_of_global] has failed. Prints "??"
@@ -58,7 +57,7 @@ val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t
val pr_leconstr : EConstr.t -> Pp.t
[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t
val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t
@@ -88,7 +87,7 @@ val pr_type_env : env -> evar_map -> types -> Pp.t
val pr_type : types -> Pp.t
[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
-val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t
val pr_closed_glob : closed_glob_constr -> Pp.t
[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
@@ -121,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t
val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
-val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t
val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
Univ.UContext.t -> Pp.t
val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
@@ -130,8 +129,8 @@ val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
(** Printing global references using names as short as possible *)
-val pr_global_env : Id.Set.t -> global_reference -> Pp.t
-val pr_global : global_reference -> Pp.t
+val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
+val pr_global : GlobRef.t -> Pp.t
val pr_constant : env -> Constant.t -> Pp.t
val pr_existential_key : evar_map -> Evar.t -> Pp.t
@@ -140,9 +139,9 @@ val pr_constructor : env -> constructor -> Pp.t
val pr_inductive : env -> inductive -> Pp.t
val pr_evaluable_reference : evaluable_global_reference -> Pp.t
-val pr_pconstant : env -> pconstant -> Pp.t
-val pr_pinductive : env -> pinductive -> Pp.t
-val pr_pconstructor : env -> pconstructor -> Pp.t
+val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
+val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
+val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
(** Contexts *)
@@ -153,13 +152,13 @@ val get_compact_context : unit -> bool
val pr_context_unlimited : env -> evar_map -> Pp.t
val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t
-val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> Pp.t
-val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t
-val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t
+val pr_named_decl : env -> evar_map -> Constr.named_declaration -> Pp.t
+val pr_compacted_decl : env -> evar_map -> Constr.compacted_declaration -> Pp.t
+val pr_rel_decl : env -> evar_map -> Constr.rel_declaration -> Pp.t
-val pr_named_context : env -> evar_map -> Context.Named.t -> Pp.t
+val pr_named_context : env -> evar_map -> Constr.named_context -> Pp.t
val pr_named_context_of : env -> evar_map -> Pp.t
-val pr_rel_context : env -> evar_map -> Context.Rel.t -> Pp.t
+val pr_rel_context : env -> evar_map -> Constr.rel_context -> Pp.t
val pr_rel_context_of : env -> evar_map -> Pp.t
val pr_context_of : env -> evar_map -> Pp.t
@@ -172,22 +171,46 @@ val pr_transparent_state : transparent_state -> Pp.t
(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
-val pr_goal : goal sigma -> Pp.t
-
-(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
- prints the goals of the list [goals] followed by the goals in
- [unfocused], in a short way (typically only the conclusion) except
- for the first goal if [pr_first] is true. This function can be
- replaced by another one by calling [set_printer_pr] (see below),
- typically by plugin writers. The default printer prints only the
- focused goals unless the conrresponding option
- [enable_unfocused_goal_printing] is set. [seeds] is for printing
- dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t
+(** [pr_goal ~diffs ~og_s g_s] prints the goal specified by [g_s]. If [diffs] is true,
+ highlight the differences between the old goal, [og_s], and [g_s]. [g_s] and [og_s] are
+ records containing the goal and sigma for, respectively, the new and old proof steps,
+ e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t
+
+(** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals]
+ prints the goals in [goals] followed by the goals in [unfocused] in a compact form
+ (typically only the conclusion). If [pr_first] is true, print the first goal in full.
+ [close_cmd] is printed afterwards verbatim.
+
+ If [diffs] is true, then highlight diffs relative to [os_map] in the output for first goal.
+ [os_map] contains sigma for the old proof step and the goal map created by
+ [Proof_diffs.make_goal_map].
+
+ This function prints only the focused goals unless the corresponding option [enable_unfocused_goal_printing] is set.
+ [seeds] is for printing dependent evars (mainly for emacs proof tree mode). [shelf] is from
+ Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but
+ there are non-instantiated existential variables. [stack] is used to print summary info on unfocused
+ goals.
+*)
+val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map
+ -> seeds:goal list -> shelf:goal list -> stack:int list
+ -> unfocused: goal list -> goals:goal list -> Pp.t
val pr_subgoal : int -> evar_map -> goal list -> Pp.t
-val pr_concl : int -> evar_map -> goal -> Pp.t
+(** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output
+ is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion,
+ [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_concl : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t
+
+(** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop.
+ The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their
+ conclusions. If [diffs] is true, highlight the differences between the old proof, [oproof], and [proof]. [quiet]
+ disables printing messages as Feedback.
+*)
+val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t
val pr_open_subgoals : proof:Proof.t -> Pp.t
val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t
val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t
@@ -197,11 +220,14 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map ->
Evar.Set.t -> Pp.t
val pr_prim_rule : prim_rule -> Pp.t
+[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"]
+
+val print_and_diff : Proof.t option -> Proof.t option -> unit
(** Backwards compatibility *)
val prterm : constr -> Pp.t (** = pr_lconstr *)
-
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
(** Declarations for the "Print Assumption" command *)
type axiom =
@@ -211,7 +237,7 @@ type axiom =
type context_object =
| Variable of Id.t (* A section variable or a Let definition *)
- | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+ | Axiom of axiom * (Label.t * Constr.rel_context * types) list
| Opaque of Constant.t (* An opaque constant. *)
| Transparent of Constant.t
@@ -223,14 +249,3 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
-type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t;
-
- pr_subgoal : int -> evar_map -> goal list -> Pp.t;
- pr_goal : goal sigma -> Pp.t;
-}
-
-val set_printer_pr : printer_pr -> unit
-
-val default_printer_pr : printer_pr
-
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 86b68d8f..deb52ad2 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,7 +1,7 @@
Genprint
Pputils
Ppconstr
+Proof_diffs
Printer
Printmod
Prettyp
-Ppvernac
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e076c10f..e2d9850b 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let envpar = push_rel_context params env in
let inst =
if Declareops.inductive_is_polymorphic mib then
- let ctx = Declareops.inductive_polymorphic_context mib in
- let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- Printer.pr_universe_instance sigma ctx
+ Printer.pr_universe_instance sigma u
else mt ()
in
hov 0 (
@@ -140,7 +138,7 @@ let print_mutual_inductive env mind mib udecl =
(AUContext.instance (Declareops.inductive_polymorphic_context mib)))
else []
in
- let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+ let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
Printer.pr_cumulative
@@ -183,7 +181,7 @@ let print_record env mind mib udecl =
let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
- let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+ let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
(Array.to_list (Univ.Instance.to_array u)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let keyword =
@@ -217,7 +215,7 @@ let print_record env mind mib udecl =
)
let pr_mutual_inductive_body env mind mib udecl =
- if mib.mind_record <> None && not !Flags.raw_print then
+ if mib.mind_record != NotRecord && not !Flags.raw_print then
print_record env mind mib udecl
else
print_mutual_inductive env mind mib udecl
@@ -323,7 +321,6 @@ let print_body is_impl env mp (l,body) =
else Univ.Instance.empty
in
let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- let sigma = Evd.empty in
(match cb.const_body with
| Def _ -> def "Definition" ++ spc ()
| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -332,17 +329,17 @@ let print_body is_impl env mp (l,body) =
| None -> mt ()
| Some env ->
str " :" ++ spc () ++
- hov 0 (Printer.pr_ltype_env env sigma
+ hov 0 (Printer.pr_ltype_env env (Evd.from_env env)
(Vars.subst_instance_constr u
cb.const_type)) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++
hov 2 (str ":= " ++
- Printer.pr_lconstr_env env sigma
+ Printer.pr_lconstr_env env (Evd.from_env env)
(Vars.subst_instance_constr u (Mod_subst.force_constr l)))
| _ -> mt ()) ++ str "." ++
- Printer.pr_universe_ctx sigma ctx)
+ Printer.pr_universe_ctx (Evd.from_env env) ctx)
| SFBmind mib ->
try
let env = Option.get env in
@@ -387,7 +384,7 @@ let rec print_typ_expr env mp locals mty =
let s = String.concat "." (List.map Id.to_string idl) in
(* XXX: What should env and sigma be here? *)
let env = Global.env () in
- let sigma = Evd.empty in
+ let sigma = Evd.from_env env in
hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
++ Printer.pr_lconstr_env env sigma c)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0b0b0a3..48ba866c 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -15,6 +15,6 @@ val printable_body : DirPath.t -> bool
val pr_mutual_inductive_body : Environ.env ->
MutInd.t -> Declarations.mutual_inductive_body ->
- Universes.univ_name_list option -> Pp.t
+ UnivNames.univ_name_list option -> Pp.t
val print_module : bool -> ModPath.t -> Pp.t
val print_modtype : ModPath.t -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
new file mode 100644
index 00000000..0b630b39
--- /dev/null
+++ b/printing/proof_diffs.ml
@@ -0,0 +1,635 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(*
+Displays the differences between successive proof steps in coqtop and CoqIDE.
+Proof General requires minor changes to make the diffs visible, but this code
+shouldn't break the existing version of PG. See pp_diff.ml for details on how
+the diff works.
+
+Diffs are computed for the hypotheses and conclusion of each goal in the new
+proof with its matching goal in the old proof.
+
+Diffs can be enabled in coqtop with 'Set Diffs "on"|"off"|"removed"' or
+'-diffs on|off|removed' on the OS command line. In CoqIDE, they can be enabled
+from the View menu. The "on" option shows only the new item with added text,
+while "removed" shows each modified item twice--once with the old value showing
+removed text and once with the new value showing added text.
+
+In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
+For coqtop, these can be set through the COQ_COLORS environment variable.
+
+Limitations/Possible enhancements:
+
+- coqtop colors were chosen for white text on a black background. They're
+not the greatest. I didn't want to change the existing green highlight.
+Suggestions welcome.
+
+- coqtop underlines removed text because (per Wikipedia) the ANSI escape code
+for strikeout is not commonly supported (it didn't work on my system). CoqIDE
+uses strikeout on removed text.
+*)
+
+open Pp_diff
+
+let diff_option = ref `OFF
+
+let read_diffs_option () = match !diff_option with
+| `OFF -> "off"
+| `ON -> "on"
+| `REMOVED -> "removed"
+
+let write_diffs_option = function
+| "off" -> diff_option := `OFF
+| "on" -> diff_option := `ON
+| "removed" -> diff_option := `REMOVED
+| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
+
+let _ =
+ Goptions.(declare_string_option {
+ optdepr = false;
+ optname = "show diffs in proofs";
+ optkey = ["Diffs"];
+ optread = read_diffs_option;
+ optwrite = write_diffs_option
+ })
+
+let show_diffs () = !diff_option <> `OFF;;
+let show_removed () = !diff_option = `REMOVED;;
+
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+[@@@ocaml.warning "-32"]
+let cprintf s = cfprintf !log_out_ch s
+[@@@ocaml.warning "+32"]
+
+module StringMap = Map.Make(String);;
+
+let tokenize_string s =
+ (* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too.
+ But I don't understand how it's used--it looks like things get appended to it but
+ it never gets cleared. *)
+ let rec stream_tok acc str =
+ let e = Stream.next str in
+ if Tok.(equal e EOI) then
+ List.rev acc
+ else
+ stream_tok ((Tok.extract_string e) :: acc) str
+ in
+ let st = CLexer.get_lexer_state () in
+ try
+ let istr = Stream.of_string s in
+ let lex = CLexer.lexer.Plexing.tok_func istr in
+ let toks = stream_tok [] (fst lex) in
+ CLexer.set_lexer_state st;
+ toks
+ with exn ->
+ CLexer.set_lexer_state st;
+ raise (Diff_Failure "Input string is not lexable");;
+
+
+type hyp_info = {
+ idents: string list;
+ rhs_pp: Pp.t;
+ mutable done_: bool;
+}
+
+(* Generate the diffs between the old and new hyps.
+ This works by matching lines with the hypothesis name and diffing the right-hand side.
+ Lines that have multiple names such as "n, m : nat" are handled specially to account
+ for, say, the addition of m to a pre-existing "n : nat".
+ *)
+let diff_hyps o_line_idents o_map n_line_idents n_map =
+ let rv : Pp.t list ref = ref [] in
+
+ let is_done ident map = (StringMap.find ident map).done_ in
+ let exists ident map =
+ try let _ = StringMap.find ident map in true
+ with Not_found -> false in
+ let contains l ident = try [List.find (fun x -> x = ident) l] with Not_found -> [] in
+
+ let output old_ids_uo new_ids =
+ (* use the order from the old line in case it's changed in the new *)
+ let old_ids = if old_ids_uo = [] then [] else
+ let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in
+ List.concat (List.map (contains orig) old_ids_uo)
+ in
+
+ let setup ids map = if ids = [] then ("", Pp.mt ()) else
+ let open Pp in
+ let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in
+ let pp_ids = List.map (fun x -> str x) ids in
+ let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in
+ (string_of_ppcmds hyp_pp, hyp_pp)
+ in
+
+ let (o_line, o_pp) = setup old_ids o_map in
+ let (n_line, n_pp) = setup new_ids n_map in
+
+ let hyp_diffs = diff_str ~tokenize_string o_line n_line in
+ let (has_added, has_removed) = has_changes hyp_diffs in
+ if show_removed () && has_removed then begin
+ let o_entry = StringMap.find (List.hd old_ids) o_map in
+ o_entry.done_ <- true;
+ rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv;
+ end;
+ if n_line <> "" then begin
+ let n_entry = StringMap.find (List.hd new_ids) n_map in
+ n_entry.done_ <- true;
+ rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv
+ end
+ in
+
+ (* process identifier level diff *)
+ let process_ident_diff diff =
+ let (dtype, ident) = get_dinfo diff in
+ match dtype with
+ | `Removed ->
+ if dtype = `Removed then begin
+ let o_idents = (StringMap.find ident o_map).idents in
+ (* only show lines that have all idents removed here; other removed idents appear later *)
+ if show_removed () &&
+ List.for_all (fun x -> not (exists x n_map)) o_idents then
+ output (List.rev o_idents) []
+ end
+ | _ -> begin (* Added or Common case *)
+ let n_idents = (StringMap.find ident n_map).idents in
+
+ (* Process a new hyp line, possibly splitting it. Duplicates some of
+ process_ident iteration, but easier to understand this way *)
+ let process_line ident2 =
+ if not (is_done ident2 n_map) then begin
+ let n_ids_list : string list ref = ref [] in
+ let o_ids_list : string list ref = ref [] in
+ let fst_omap_idents = ref None in
+ let add ids id map =
+ ids := id :: !ids;
+ (StringMap.find id map).done_ <- true in
+
+ (* get identifiers shared by one old and one new line, plus
+ other Added in new and other Removed in old *)
+ let process_split ident3 =
+ if not (is_done ident3 n_map) then begin
+ let this_omap_idents = try Some (StringMap.find ident3 o_map).idents
+ with Not_found -> None in
+ if !fst_omap_idents = None then
+ fst_omap_idents := this_omap_idents;
+ match (!fst_omap_idents, this_omap_idents) with
+ | (Some fst, Some this) when fst == this -> (* yes, == *)
+ add n_ids_list ident3 n_map;
+ (* include, in old order, all undone Removed idents in old *)
+ List.iter (fun x -> if x = ident3 || not (is_done x o_map) && not (exists x n_map) then
+ (add o_ids_list x o_map)) fst
+ | (_, None) ->
+ add n_ids_list ident3 n_map (* include all undone Added idents in new *)
+ | _ -> ()
+ end in
+ List.iter process_split n_idents;
+ output (List.rev !o_ids_list) (List.rev !n_ids_list)
+ end in
+ List.iter process_line n_idents (* O(n^2), so sue me *)
+ end in
+
+ let cvt s = Array.of_list (List.concat s) in
+ let ident_diffs = diff_strs (cvt o_line_idents) (cvt n_line_idents) in
+ List.iter process_ident_diff ident_diffs;
+ List.rev !rv;;
+
+
+type 'a hyp = (Names.Id.t list * 'a option * 'a)
+type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map }
+
+(* XXX: Port to proofview, one day. *)
+(* open Proofview *)
+module CDC = Context.Compacted.Declaration
+
+let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
+ let open CDC in function
+ | LocalAssum(idl, tm) -> (idl, None, tm)
+ | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);;
+
+(* XXX: Very unfortunately we cannot use the Proofview interface as
+ Proof is still using the "legacy" one. *)
+let process_goal_concl sigma g : Constr.t * Environ.env =
+ let env = Goal.V82.env sigma g in
+ let ty = Goal.V82.concl sigma g in
+ let ty = EConstr.to_constr sigma ty in
+ (ty, env)
+
+let process_goal sigma g : Constr.t reified_goal =
+ let env = Goal.V82.env sigma g in
+ let hyps = Goal.V82.hyps sigma g in
+ let ty = Goal.V82.concl sigma g in
+ let name = Goal.uid g in
+ (* There is a Constr/Econstr mess here... *)
+ let ty = EConstr.to_constr sigma ty in
+ (* compaction is usually desired [eg for better display] *)
+ let hyps = Termops.compact_named_context (Environ.named_context_of_val hyps) in
+ let hyps = List.map to_tuple hyps in
+ { name; ty; hyps; env; sigma };;
+
+let pr_letype_core goal_concl_style env sigma t =
+ Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
+
+let pp_of_type env sigma ty =
+ pr_letype_core true env sigma EConstr.(of_constr ty)
+
+let pr_leconstr_core goal_concl_style env sigma t =
+ Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t)
+
+let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+
+let diff_concl ?og_s nsigma ng =
+ let open Evd in
+ let o_concl_pp = match og_s with
+ | Some { it=og; sigma=osigma } ->
+ let (oty, oenv) = process_goal_concl osigma og in
+ pp_of_type oenv osigma oty
+ | None -> Pp.mt()
+ in
+ let (nty, nenv) = process_goal_concl nsigma ng in
+ let n_concl_pp = pp_of_type nenv nsigma nty in
+
+ let show_removed = Some (show_removed ()) in
+
+ diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp
+
+(* fetch info from a goal, returning (idents, map, concl_pp) where
+idents is a list with one entry for each hypothesis, in which each entry
+is the list of idents on the lhs of the hypothesis. map is a map from
+ident to hyp_info reoords. For example: for the hypotheses:
+ b : bool
+ n, m : nat
+
+idents will be [ ["b"]; ["n"; "m"] ]
+
+map will contain:
+ "b" -> { ["b"], Pp.t for ": bool"; false }
+ "n" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ "m" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ where the last two entries share the idents list.
+
+concl_pp is the conclusion as a Pp.t
+*)
+let goal_info goal sigma =
+ let map = ref StringMap.empty in
+ let line_idents = ref [] in
+ let build_hyp_info env sigma hyp =
+ let (names, body, ty) = hyp in
+ let open Pp in
+ let idents = List.map (fun x -> Names.Id.to_string x) names in
+
+ line_idents := idents :: !line_idents;
+ let mid = match body with
+ | Some c ->
+ let pb = pr_lconstr_env env sigma c in
+ let pb = if Constr.isCast c then surround pb else pb in
+ str " := " ++ pb
+ | None -> mt() in
+ let ts = pp_of_type env sigma ty in
+ let rhs_pp = mid ++ str " : " ++ ts in
+
+ let make_entry () = { idents; rhs_pp; done_ = false } in
+ List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
+ in
+
+ try
+ let { ty=ty; hyps=hyps; env=env } = process_goal sigma goal in
+ List.iter (build_hyp_info env sigma) (List.rev hyps);
+ let concl_pp = pp_of_type env sigma ty in
+ ( List.rev !line_idents, !map, concl_pp )
+ with _ -> ([], !map, Pp.mt ());;
+
+let diff_goal_info o_info n_info =
+ let (o_line_idents, o_hyp_map, o_concl_pp) = o_info in
+ let (n_line_idents, n_hyp_map, n_concl_pp) = n_info in
+ let show_removed = Some (show_removed ()) in
+ let concl_pp = diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp in
+
+ let hyp_diffs_list = diff_hyps o_line_idents o_hyp_map n_line_idents n_hyp_map in
+ (hyp_diffs_list, concl_pp)
+
+let hyp_list_to_pp hyps =
+ let open Pp in
+ match hyps with
+ | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl
+ | [] -> mt ();;
+
+let unwrap g_s =
+ match g_s with
+ | Some g_s ->
+ let goal = Evd.sig_it g_s in
+ let sigma = Refiner.project g_s in
+ goal_info goal sigma
+ | None -> ([], StringMap.empty, Pp.mt ())
+
+let diff_goal_ide og_s ng nsigma =
+ diff_goal_info (unwrap og_s) (goal_info ng nsigma)
+
+let diff_goal ?og_s ng ns =
+ let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap og_s) (goal_info ng ns) in
+ let open Pp in
+ v 0 (
+ (hyp_list_to_pp hyps_pp_list) ++ cut () ++
+ str "============================" ++ cut () ++
+ concl_pp);;
+
+
+(*** Code to determine which calls to compare between the old and new proofs ***)
+
+open Constrexpr
+open Glob_term
+open Names
+open CAst
+
+(* Compare the old and new proof trees to identify the correspondence between
+new and old goals. Returns a map from the new evar name to the old,
+e.g. "Goal2" -> "Goal1". Assumes that proof steps only rewrite CEvar nodes
+and that CEvar nodes cannot contain other CEvar nodes.
+
+The comparison works this way:
+1. Traverse the old and new trees together (ogname = "", ot != nt):
+- if the old and new trees both have CEvar nodes, add an entry to the map from
+ the new evar name to the old evar name. (Position of goals is preserved but
+ evar names may not be--see below.)
+- if the old tree has a CEvar node and the new tree has a different type of node,
+ we've found a changed goal. Set ogname to the evar name of the old goal and
+ go to step 2.
+- any other mismatch violates the assumptions, raise an exception
+2. Traverse the new tree from the point of the difference (ogname <> "", ot = nt).
+- if the node is a CEvar, generate a map entry from the new evar name to ogname.
+
+Goal ids for unchanged goals appear to be preserved across proof steps.
+However, the evar name associated with a goal id may change in a proof step
+even if that goal is not changed by the tactic. You can see this by enabling
+the call to db_goal_map and entering the following:
+
+ Parameter P : nat -> Prop.
+ Goal (P 1 /\ P 2 /\ P 3) /\ P 4.
+ split.
+ Show Proof.
+ split.
+ Show Proof.
+
+ Which gives you this summarized output:
+
+ > split.
+ New Goals: 3 -> Goal 4 -> Goal0 <--- goal 4 is "Goal0"
+ Old Goals: 1 -> Goal
+ Goal map: 3 -> 1 4 -> 1
+ > Show Proof.
+ (conj ?Goal ?Goal0) <--- goal 4 is the rightmost goal in the proof
+ > split.
+ New Goals: 6 -> Goal0 7 -> Goal1 4 -> Goal <--- goal 4 is now "Goal"
+ Old Goals: 3 -> Goal 4 -> Goal0
+ Goal map: 6 -> 3 7 -> 3
+ > Show Proof.
+ (conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof
+ *)
+let match_goals ot nt =
+ let nevar_to_oevar = ref StringMap.empty in
+ (* ogname is "" when there is no difference on the current path.
+ It's set to the old goal's evar name once a rewitten goal is found,
+ at which point the code only searches for the replacing goals
+ (and ot is set to nt). *)
+ let rec match_goals_r ogname ot nt =
+ let constr_expr ogname exp exp2 =
+ match_goals_r ogname exp.v exp2.v
+ in
+ let constr_expr_opt ogname exp exp2 =
+ match exp, exp2 with
+ | Some expa, Some expb -> constr_expr ogname expa expb
+ | None, None -> ()
+ | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)")
+ in
+ let local_binder_expr ogname exp exp2 =
+ match exp, exp2 with
+ | CLocalAssum (nal,bk,ty), CLocalAssum(nal2,bk2,ty2) ->
+ constr_expr ogname ty ty2
+ | CLocalDef (n,c,t), CLocalDef (n2,c2,t2) ->
+ constr_expr ogname c c2;
+ constr_expr_opt ogname t t2
+ | CLocalPattern p, CLocalPattern p2 ->
+ let (p,ty), (p2,ty2) = p.v,p2.v in
+ constr_expr_opt ogname ty ty2
+ | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)")
+ in
+ let recursion_order_expr ogname exp exp2 =
+ match exp, exp2 with
+ | CStructRec, CStructRec -> ()
+ | CWfRec c, CWfRec c2 ->
+ constr_expr ogname c c2
+ | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
+ constr_expr ogname m m2;
+ constr_expr_opt ogname r r2
+ | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)")
+ in
+ let fix_expr ogname exp exp2 =
+ let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
+ recursion_order_expr ogname ro ro2;
+ List.iter2 (local_binder_expr ogname) lb lb2;
+ constr_expr ogname ce1 ce12;
+ constr_expr ogname ce2 ce22
+ in
+ let cofix_expr ogname exp exp2 =
+ let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in
+ List.iter2 (local_binder_expr ogname) lb lb2;
+ constr_expr ogname ce1 ce12;
+ constr_expr ogname ce2 ce22
+ in
+ let case_expr ogname exp exp2 =
+ let (ce,l,cp), (ce2,l2,cp2) = exp,exp2 in
+ constr_expr ogname ce ce2
+ in
+ let branch_expr ogname exp exp2 =
+ let (cpe,ce), (cpe2,ce2) = exp.v,exp2.v in
+ constr_expr ogname ce ce2
+ in
+ let constr_notation_substitution ogname exp exp2 =
+ let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in
+ List.iter2 (constr_expr ogname) ce ce2;
+ List.iter2 (fun a a2 -> List.iter2 (constr_expr ogname) a a2) cel cel2;
+ List.iter2 (fun a a2 -> List.iter2 (local_binder_expr ogname) a a2) lb lb2
+ in
+ begin
+ match ot, nt with
+ | CRef (ref,us), CRef (ref2,us2) -> ()
+ | CFix (id,fl), CFix (id2,fl2) ->
+ List.iter2 (fix_expr ogname) fl fl2
+ | CCoFix (id,cfl), CCoFix (id2,cfl2) ->
+ List.iter2 (cofix_expr ogname) cfl cfl2
+ | CProdN (bl,c2), CProdN (bl2,c22)
+ | CLambdaN (bl,c2), CLambdaN (bl2,c22) ->
+ List.iter2 (local_binder_expr ogname) bl bl2;
+ constr_expr ogname c2 c22
+ | CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) ->
+ constr_expr ogname c1 c12;
+ constr_expr_opt ogname t t2;
+ constr_expr ogname c2 c22
+ | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) ->
+ List.iter2 (constr_expr ogname) args args2
+ | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) ->
+ constr_expr ogname f f2;
+ List.iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
+ constr_expr ogname c c2) args args2
+ | CRecord fs, CRecord fs2 ->
+ List.iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in
+ constr_expr ogname c c2) fs fs2
+ | CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) ->
+ constr_expr_opt ogname rtnpo rtnpo2;
+ List.iter2 (case_expr ogname) tms tms2;
+ List.iter2 (branch_expr ogname) eqns eqns2
+ | CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) ->
+ constr_expr_opt ogname po po2;
+ constr_expr ogname b b2;
+ constr_expr ogname c c2
+ | CIf (c,(na,po),b1,b2), CIf (c2,(na2,po2),b12,b22) ->
+ constr_expr ogname c c2;
+ constr_expr_opt ogname po po2;
+ constr_expr ogname b1 b12;
+ constr_expr ogname b2 b22
+ | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> ()
+ | CPatVar _, CPatVar _ -> ()
+ | CEvar (n,l), CEvar (n2,l2) ->
+ let oevar = if ogname = "" then Id.to_string n else ogname in
+ nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar;
+ List.iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2
+ | CEvar (n,l), nt' ->
+ (* pass down the old goal evar name *)
+ match_goals_r (Id.to_string n) nt' nt'
+ | CSort s, CSort s2 -> ()
+ | CCast (c,c'), CCast (c2,c'2) ->
+ constr_expr ogname c c2;
+ (match c', c'2 with
+ | CastConv a, CastConv a2
+ | CastVM a, CastVM a2
+ | CastNative a, CastNative a2 ->
+ constr_expr ogname a a2
+ | CastCoerce, CastCoerce -> ()
+ | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)"))
+ | CNotation (ntn,args), CNotation (ntn2,args2) ->
+ constr_notation_substitution ogname args args2
+ | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
+ constr_expr ogname c c2
+ | CPrim p, CPrim p2 -> ()
+ | CDelimiters (key,e), CDelimiters (key2,e2) ->
+ constr_expr ogname e e2
+ | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)")
+ end
+ in
+
+ (match ot with
+ | Some ot -> match_goals_r "" ot nt
+ | None -> ());
+ !nevar_to_oevar
+
+
+let to_constr p =
+ let open CAst in
+ let pprf = Proof.partial_proof p in
+ (* pprf generally has only one element, but it may have more in the derive plugin *)
+ let t = List.hd pprf in
+ let sigma, env = Pfedit.get_current_context ~p () in
+ let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *)
+ x.v
+
+
+module GoalMap = Evar.Map
+
+let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma)
+
+[@@@ocaml.warning "-32"]
+let db_goal_map op np ng_to_og =
+ Printf.printf "New Goals: ";
+ let (ngoals,_,_,_,nsigma) = Proof.proof np in
+ List.iter (fun ng -> Printf.printf "%d -> %s " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals;
+ (match op with
+ | Some op ->
+ let (ogoals,_,_,_,osigma) = Proof.proof op in
+ Printf.printf "\nOld Goals: ";
+ List.iter (fun og -> Printf.printf "%d -> %s " (Evar.repr og) (goal_to_evar og osigma)) ogoals
+ | None -> ());
+ Printf.printf "\nGoal map: ";
+ GoalMap.iter (fun og ng -> Printf.printf "%d -> %d " (Evar.repr og) (Evar.repr ng)) ng_to_og;
+ Printf.printf "\n"
+[@@@ocaml.warning "+32"]
+
+(* Create a map from new goals to old goals for proof diff. The map only
+ has entries for new goals that are not the same as the corresponding old
+ goal; there are no entries for unchanged goals.
+
+ It proceeds as follows:
+ 1. Find the goal ids that were removed from the old proof and that were
+ added in the new proof. If the same goal id is present in both proofs
+ then conclude the goal is unchanged (assumption).
+
+ 2. The code assumes that proof changes only take the form of replacing
+ one or more goal symbols (CEvars) with new terms. Therefore:
+ - if there are no removals, the proofs are the same.
+ - if there are removals but no additions, then there are no new goals
+ that aren't the same as their associated old goals. For the both of
+ these cases, the map is empty because there are no new goals that differ
+ from their old goals
+ - if there is only one removal, then any added goals should be mapped to
+ the removed goal.
+ - if there are more than 2 removals and more than one addition, call
+ match_goals to get a map between old and new evar names, then use this
+ to create the map from new goal ids to old goal ids for the differing goals.
+*)
+let make_goal_map_i op np =
+ let ng_to_og = ref GoalMap.empty in
+ match op with
+ | None -> !ng_to_og
+ | Some op ->
+ let open Goal.Set in
+ let ogs = Proof.all_goals op in
+ let ngs = Proof.all_goals np in
+ let rem_gs = diff ogs ngs in
+ let num_rems = cardinal rem_gs in
+ let add_gs = diff ngs ogs in
+ let num_adds = cardinal add_gs in
+
+ if num_rems = 0 then
+ !ng_to_og (* proofs are the same *)
+ else if num_adds = 0 then
+ !ng_to_og (* only removals *)
+ else if num_rems = 1 then begin
+ (* only 1 removal, some additions *)
+ let removed_g = List.hd (elements rem_gs) in
+ Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x removed_g !ng_to_og) add_gs;
+ !ng_to_og
+ end else begin
+ (* >= 2 removals, >= 1 addition, need to match *)
+ let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in
+
+ let oevar_to_og = ref StringMap.empty in
+ let (_,_,_,_,osigma) = Proof.proof op in
+ List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
+ (Goal.Set.elements rem_gs);
+
+ try
+ let (_,_,_,_,nsigma) = Proof.proof np in
+ let get_og ng =
+ let nevar = goal_to_evar ng nsigma in
+ let oevar = StringMap.find nevar nevar_to_oevar in
+ let og = StringMap.find oevar !oevar_to_og in
+ og
+ in
+ Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs;
+ !ng_to_og
+ with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)")
+ end
+
+let make_goal_map op np =
+ let ng_to_og = make_goal_map_i op np in
+ (*db_goal_map op np ng_to_og;*)
+ ng_to_og
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
new file mode 100644
index 00000000..832393e1
--- /dev/null
+++ b/printing/proof_diffs.mli
@@ -0,0 +1,84 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* diff options *)
+
+(** Controls whether to show diffs. Takes values "on", "off", "removed" *)
+val write_diffs_option : string -> unit
+(** Returns true if the diffs option is "on" or "removed" *)
+val show_diffs : unit -> bool
+
+open Evd
+open Proof_type
+open Environ
+open Constr
+
+(** Computes the diff between the goals of two Proofs and returns
+the highlighted lists of hypotheses and conclusions.
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure. This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t
+
+(** Computes the diff between two goals
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure. This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t
+
+(** Convert a string to a list of token strings using the lexer *)
+val tokenize_string : string -> string list
+
+val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
+val pr_lconstr_env : env -> evar_map -> constr -> Pp.t
+
+(** Computes diffs for a single conclusion *)
+val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
+
+(** Generates a map from [np] to [op] that maps changed goals to their prior
+forms. The map doesn't include entries for unchanged goals; unchanged goals
+will have the same goal id in both versions.
+
+[op] and [np] must be from the same proof document and [op] must be for a state
+before [np]. *)
+val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t
+
+(* Exposed for unit test, don't use these otherwise *)
+(* output channel for the test log file *)
+val log_out_ch : out_channel ref
+
+
+type hyp_info = {
+ idents: string list;
+ rhs_pp: Pp.t;
+ mutable done_: bool;
+}
+
+module StringMap :
+sig
+ type +'a t
+ val empty: hyp_info t
+ val add : string -> hyp_info -> hyp_info t -> hyp_info t
+end
+
+val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 13:37:22 +0000