1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: tactic_printer.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
open Pp
open Util
open Sign
open Evd
open Tacexpr
open Proof_type
open Proof_trees
open Logic
open Printer
let pr_tactic = function
| TacArg (Tacexp t) ->
(*top tactic from tacinterp*)
Pptactic.pr_glob_tactic (Global.env()) t
| t ->
Pptactic.pr_tactic (Global.env()) t
let pr_rule = function
| Prim r -> hov 0 (pr_prim_rule r)
| Tactic (texp,_) -> hov 0 (pr_tactic texp)
| Change_evars ->
(* This is internal tactic and cannot be replayed at user-level.
Function pr_rule_dot below is used when we want to hide
Change_evars *)
str "Evar change"
(* Does not print change of evars *)
let pr_rule_dot = function
| Change_evars -> mt ()
| r -> pr_rule r ++ str"."
exception Different
(* We remove from the var context of env what is already in osign *)
let thin_sign osign sign =
Sign.fold_named_context
(fun (id,c,ty as d) sign ->
try
if Sign.lookup_named id osign = (id,c,ty) then sign
else raise Different
with Not_found | Different -> Environ.push_named_context_val d sign)
sign ~init:Environ.empty_named_context_val
let rec print_proof sigma osign pf =
let {evar_hyps=hyps; evar_concl=cl;
evar_body=body} = pf.goal in
let hyps = Environ.named_context_of_val hyps in
let hyps' = thin_sign osign hyps in
match pf.ref with
| None ->
hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body})
| Some(r,spfl) ->
hov 0
(hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++
spc () ++ str" BY " ++
hov 0 (pr_rule r) ++ fnl () ++
str" " ++
hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
)
let pr_change gl =
str"Change " ++
pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
let rec print_script nochange sigma osign pf =
let {evar_hyps=sign; evar_concl=cl} = pf.goal in
let sign = Environ.named_context_of_val sign in
match pf.ref with
| None ->
(if nochange then
(str"<Your Tactic Text here>")
else
pr_change pf.goal)
++ fnl ()
| Some(r,spfl) ->
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
pr_rule_dot r ++ fnl () ++
prlist_with_sep pr_fnl
(print_script nochange sigma sign) spfl)
(* printed by Show Script command *)
let print_treescript nochange sigma _osign pf =
let rec aux top pf =
match pf.ref with
| None ->
if nochange then
(str"<Your Tactic Text here>")
else
(pr_change pf.goal)
| Some(r,spfl) ->
(if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
pr_rule_dot r ++
match spfl with
| [] -> mt ()
| [spf] -> fnl () ++ (if top then mt () else str " ") ++ aux top spf
| _ -> fnl () ++ str " " ++
hov 0 (prlist_with_sep fnl (aux false) spfl)
in hov 0 (aux true pf)
let rec print_info_script sigma osign pf =
let {evar_hyps=sign; evar_concl=cl} = pf.goal in
match pf.ref with
| None -> (mt ())
| Some(Change_evars,[spf]) ->
print_info_script sigma osign spf
| Some(r,spfl) ->
(pr_rule r ++
match spfl with
| [pf1] ->
if pf1.ref = None then
(str "." ++ fnl ())
else
(str";" ++ brk(1,3) ++
print_info_script sigma
(Environ.named_context_of_val sign) pf1)
| _ -> (str"." ++ fnl () ++
prlist_with_sep pr_fnl
(print_info_script sigma
(Environ.named_context_of_val sign)) spfl))
let format_print_info_script sigma osign pf =
hov 0 (print_info_script sigma osign pf)
let print_subscript sigma sign pf =
if is_tactic_proof pf then
format_print_info_script sigma sign (subproof_of_proof pf)
else
format_print_info_script sigma sign pf
let _ = Refiner.set_info_printer print_subscript
|
