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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
|
(* ========================================================================= *)
(* HOL Light subgoal package amended for Proof General's Prooftree. *)
(* *)
(* Mark Adams, School of Informatics, University of Edinburgh *)
(* *)
(* (c) Copyright, University of Edinburgh, 2012 *)
(* ========================================================================= *)
(* This file provides alternatives to HOL Light's subgoal package commands *)
(* that output additional annotations specifically for Prooftree. These *)
(* annotations get intercepted by Proof General, which removes them from the *)
(* output displayed to the Proof General user. Annotation can be switched *)
(* off completely with the 'pg_mode_off' command. *)
(* Note that this assumes the existence of xgoals (see 'xtactics.ml'). *)
(* ------------------------------------------------------------------------- *)
(* Proof General mode, for providing extra annotations for Prooftree. *)
(* ------------------------------------------------------------------------- *)
let pg_mode = ref (false : bool);;
let pg_mode_on () = (pg_mode := true);;
let pg_mode_off () = (pg_mode := false);;
let get_pg_mode () = !pg_mode;;
(* ------------------------------------------------------------------------- *)
(* The Prooftree global state is an ever increasing counter. *)
(* ------------------------------------------------------------------------- *)
let the_pt_global_state = ref 1;;
let inc_pt_global_state () =
(the_pt_global_state := !the_pt_global_state + 1);;
let pt_global_state () = !the_pt_global_state;;
(* ------------------------------------------------------------------------- *)
(* The Prooftree proof state is the length of the goal stack. *)
(* ------------------------------------------------------------------------- *)
let pt_proof_state () = length !current_xgoalstack;;
let pt_back_to_proof_state n : xgoalstack =
let pst = pt_proof_state () in
if (0 <= n) & (n <= pst)
then (current_xgoalstack :=
snd (chop_list (pst-n) !current_xgoalstack);
!current_xgoalstack)
else failwith "Not a valid Prooftree state number";;
(* ------------------------------------------------------------------------- *)
(* Subgoal package commands adjusted to update Prooftree global state. *)
(* ------------------------------------------------------------------------- *)
let the_tactic_flag = ref false;;
let xe tac =
let result = xe tac in
(inc_pt_global_state ();
the_tactic_flag := true; (* So that special info gets displayed *)
result);;
let xr n =
let result = xr n in
(inc_pt_global_state ();
result);;
let xset_goal (asl,w) =
let result = xset_goal (asl,w) in
(inc_pt_global_state ();
result);;
let xg t =
let fvs = sort (<) (map (fst o dest_var) (frees t)) in
(if fvs <> [] then
let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
warn true ("Free variables in goal: "^errmsg)
else ());
xset_goal([],t);;
let xb () =
let result = xb () in
(inc_pt_global_state ();
result);;
(* ------------------------------------------------------------------------- *)
(* Special Prooftree printers for xgoals and xgoalstacks. *)
(* ------------------------------------------------------------------------- *)
let the_new_goal_ids = ref ([] : goalid list);;
let print_prooftree_xgoal ((g,id) : xgoal) : unit =
((if (!pg_mode)
then (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]");
print_newline ()));
print_goal g);;
let (print_prooftree_xgoalstack:xgoalstack->unit) =
let print_prooftree_xgoalstate k gs =
let (_,gl,_) = gs in
let n = length gl in
let s = if n = 0 then "No subgoals" else
(string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
^" ("^(string_of_int n)^" total)" in
print_string s; print_newline();
if gl = [] then () else
(do_list (print_prooftree_xgoal o C el gl) (rev(1--(k-1)));
(if (!pg_mode) then print_string "[*]");
print_prooftree_xgoal (el 0 gl)) in
fun l ->
((if (!pg_mode) & (!the_tactic_flag)
then let xs = map string_of_int (!the_new_goal_ids) in
(the_tactic_flag := false;
print_string "[New Goal IDs: ";
print_string_seplist " " xs;
print_string "]";
print_newline ()));
(if l = [] then print_string "Empty goalstack"
else if tl l = [] then
let (_,gl,_ as gs) = hd l in
print_prooftree_xgoalstate 1 gs
else
let (_,gl,_ as gs) = hd l
and (_,gl0,_) = hd(tl l) in
let p = length gl - length gl0 in
let p' = if p < 1 then 1 else p + 1 in
print_prooftree_xgoalstate p' gs);
(if (!pg_mode) then
let (vs,theta) =
if (l = []) then ([],[])
else let ((vs,(_,theta,_)),_,_) = hd l in
(vs,theta) in
let foo v =
let (x,_) = dest_var v in
x ^ if (can (rev_assoc v) theta) then " using" else " open" in
let xs = map foo vs in
(print_newline();
print_string "(dependent evars: ";
print_string_seplist ", " xs;
print_string ")";
print_newline ())));;
(* ------------------------------------------------------------------------- *)
(* Adjust the OCaml prompt to carry information for Prooftree. *)
(* ------------------------------------------------------------------------- *)
let original_prompt_fn = !Toploop.read_interactive_input in
Toploop.read_interactive_input :=
fun prompt buffer len ->
let basic_prompt = "<" in (* 'prompt' arg is ignored *)
let prompt' =
if (!pg_mode)
then let pst = pt_proof_state () and gst = pt_global_state () in
"<prompt> " ^ basic_prompt ^ " " ^
string_of_int gst ^ " || " ^ string_of_int pst ^
" " ^ basic_prompt ^ " </prompt>"
else prompt in
original_prompt_fn prompt' buffer len;;
(* ------------------------------------------------------------------------- *)
(* Printing the goal of a given Prooftree goal id. *)
(* ------------------------------------------------------------------------- *)
let xgoal_of_id (id:goalid) : xgoal =
let gsts = !current_xgoalstack in
let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in
let xg = tryfind find_goal gsts in
xg;;
(* ------------------------------------------------------------------------- *)
(* Install the new goal-related printers. *)
(* ------------------------------------------------------------------------- *)
#install_printer print_prooftree_xgoal;;
#install_printer print_prooftree_xgoalstack;;
|
