3
type tree = {mutable index : int;
5
path_to_root : int list;
6
mutable is_open : bool;
7
mutable sub_proofs : tree list};;
10
mutable prf_length : int;
11
mutable ranks_and_goals : (int * int * tree) list;
12
mutable border : tree list;
15
let theorem_proofs = ((Hashtbl.create 17):
16
(string, prf_info) Hashtbl.t);;
19
let rec mk_trees_for_goals path tree rank k n =
25
path_to_root = k::path;
27
sub_proofs = [] } ::(mk_trees_for_goals path tree rank (k+1) n);;
30
let push_command s rank ngoals =
31
let ({prf_length = this_length;
32
ranks_and_goals = these_ranks;
33
border = this_border} as proof_info) =
34
Hashtbl.find theorem_proofs s in
35
let rec push_command_aux n = function
36
[] -> failwith "the given rank was too large"
39
let {path_to_root = p} = a in
40
let new_trees = mk_trees_for_goals p (Some a) (this_length + 1) 1 ngoals in
41
new_trees,(new_trees@l),a
43
let new_trees, res, this_tree = push_command_aux (n-1) l in
44
new_trees,(a::res),this_tree in
45
let new_trees, new_border, this_tree =
46
push_command_aux rank this_border in
47
let new_length = this_length + 1 in
49
proof_info.border <- new_border;
50
proof_info.prf_length <- new_length;
51
proof_info.ranks_and_goals <- (rank, ngoals, this_tree)::these_ranks;
52
this_tree.index <- new_length;
53
this_tree.is_open <- false;
54
this_tree.sub_proofs <- new_trees
57
let get_tree_for_rank thm_name rank =
58
let {ranks_and_goals=l;prf_length=n} =
59
Hashtbl.find theorem_proofs thm_name in
60
let rec get_tree_aux = function
63
"inconsistent values for thm_name and rank in get_tree_for_rank"
64
| (_,_,({index=i} as tree))::tl ->
71
let get_path_for_rank thm_name rank =
72
let {path_to_root=l}=get_tree_for_rank thm_name rank in
75
let rec list_descendants_aux l tree =
76
let {index = i; is_open = open_status; sub_proofs = tl} = tree in
77
let res = (List.fold_left list_descendants_aux l tl) in
78
if open_status then i::res else res;;
80
let list_descendants thm_name rank =
81
list_descendants_aux [] (get_tree_for_rank thm_name rank);;
83
let parent_from_rank thm_name rank =
84
let {parent=mommy} = get_tree_for_rank thm_name rank in
86
Some x -> Some x.index
89
let first_child_command thm_name rank =
90
let {sub_proofs = l} = get_tree_for_rank thm_name rank in
91
let rec first_child_rec = function
93
| {index=i;is_open=b}::l ->
100
type index_or_rank = Is_index of int | Is_rank of int;;
102
let first_child_command_or_goal thm_name rank =
103
let proof_info = Hashtbl.find theorem_proofs thm_name in
104
let {sub_proofs=l}=get_tree_for_rank thm_name rank in
107
| ({index=i;is_open=b} as t)::_ ->
109
let rec get_rank n = function
110
[] -> failwith "A goal is lost in first_child_command_or_goal"
115
get_rank (n + 1) l in
116
Some(Is_rank(get_rank 1 proof_info.border))
120
let next_sibling thm_name rank =
121
let ({parent=mommy} as t)=get_tree_for_rank thm_name rank in
125
let {sub_proofs=l}=real_mommy in
126
let rec next_sibling_aux b = function
131
failwith "inconsistency detected in next_sibling"
132
| (opt_first, {is_open=true}::l) ->
133
next_sibling_aux b (opt_first, l)
134
| (Some(first),({index=i; is_open=false} as t')::l) ->
138
next_sibling_aux (t == t') (Some first,l)
139
| None,({index=i;is_open=false} as t')::l ->
140
next_sibling_aux (t == t') ((Some i), l)
142
Some (next_sibling_aux false (None, l));;
146
let l1rev = List.rev l1 in
147
let l2rev = List.rev l2 in
148
is_prefix l1rev l2rev;;
150
let rec remove_all_prefixes p = function
153
if is_prefix p a then
154
(remove_all_prefixes p l)
156
a::(remove_all_prefixes p l);;
158
let recompute_border tree =
159
let rec recompute_border_aux tree acc =
160
let {is_open=b;sub_proofs=l}=tree in
164
List.fold_right recompute_border_aux l acc in
165
recompute_border_aux tree [];;
168
let historical_undo thm_name rank =
169
let ({ranks_and_goals=l} as proof_info)=
170
Hashtbl.find theorem_proofs thm_name in
171
let rec undo_aux acc = function
172
[] -> failwith "bad rank provided for undoing in historical_undo"
173
| (r, n, ({index=i} as tree))::tl ->
174
let this_path_reversed = List.rev tree.path_to_root in
175
let res = remove_all_prefixes this_path_reversed acc in
178
proof_info.prf_length <- i-1;
179
proof_info.ranks_and_goals <- tl;
180
tree.is_open <- true;
181
tree.sub_proofs <- [];
182
proof_info.border <- recompute_border proof_info.prf_struct;
183
this_path_reversed::res
187
tree.is_open <- true;
188
tree.sub_proofs <- [];
189
undo_aux (this_path_reversed::res) tl
192
List.map List.rev (undo_aux [] l);;
194
(* The following function takes a list of trees and compute the
195
number of elements whose path is lexically smaller or a suffixe of
196
the path given as a first argument. This works under the precondition that
197
the list is lexicographically order. *)
199
let rec logical_undo_on_border the_tree rev_path = function
201
| ({path_to_root=p}as tree)::tl ->
202
let p_rev = List.rev p in
203
if is_prefix rev_path p_rev then
204
let (k,res) = (logical_undo_on_border the_tree rev_path tl) in
206
else if lex_smaller p_rev rev_path then
207
let (k,res) = (logical_undo_on_border the_tree rev_path tl) in
210
(0, the_tree::tree::tl);;
213
let logical_undo thm_name rank =
214
let ({ranks_and_goals=l; border=last_border} as proof_info)=
215
Hashtbl.find theorem_proofs thm_name in
216
let ({path_to_root=ref_path} as ref_tree)=get_tree_for_rank thm_name rank in
217
let rev_ref_path = List.rev ref_path in
218
let rec logical_aux lex_smaller_offset family_width = function
219
[] -> failwith "this case should never happen in logical_undo"
220
| (r,n,({index=i;path_to_root=this_path; sub_proofs=these_goals} as tree))::
222
let this_path_rev = List.rev this_path in
223
let new_rank, new_offset, new_width, kept =
224
if is_prefix rev_ref_path this_path_rev then
225
(r + lex_smaller_offset), lex_smaller_offset,
226
(family_width + 1 - n), false
227
else if lex_smaller this_path_rev rev_ref_path then
228
r, (lex_smaller_offset - 1 + n), family_width, true
230
(r + 1 - family_width+ lex_smaller_offset),
231
lex_smaller_offset, family_width, true in
233
[i,new_rank],[], tl, rank
235
let ranks_undone, ranks_kept, ranks_and_goals, current_rank =
236
(logical_aux new_offset new_width tl) in
240
tree.index <- current_rank;
241
ranks_undone, ((i,new_rank)::ranks_kept),
242
((new_rank, n, tree)::ranks_and_goals),
246
((i,new_rank)::ranks_undone), ranks_kept,
247
ranks_and_goals, current_rank
249
let number_suffix, new_border =
250
logical_undo_on_border ref_tree rev_ref_path last_border in
251
let changed_ranks_undone, changed_ranks_kept, new_ranks_and_goals,
252
new_length_plus_one = logical_aux 0 number_suffix l in
254
let rec compute_goal_index n = function
255
[] -> failwith "this case should never happen in logical undo (2)"
256
| {path_to_root=path}::tl ->
257
if List.rev path = (rev_ref_path) then
260
compute_goal_index (n+1) tl in
261
compute_goal_index 1 new_border in
263
ref_tree.is_open <- true;
264
ref_tree.sub_proofs <- [];
265
proof_info.border <- new_border;
266
proof_info.ranks_and_goals <- new_ranks_and_goals;
267
proof_info.prf_length <- new_length_plus_one - 1;
268
changed_ranks_undone, changed_ranks_kept, proof_info.prf_length,
272
let start_proof thm_name =
274
{index=0;parent=None;path_to_root=[];is_open=true;sub_proofs=[]} in
275
Hashtbl.add theorem_proofs thm_name
279
prf_struct=the_tree};;
281
let dump_sequence chan s =
282
match (Hashtbl.find theorem_proofs s) with
283
{ranks_and_goals=l}->
284
let rec dump_rec = function
288
output_string chan (string_of_int r);
289
output_string chan ",";
290
output_string chan (string_of_int n);
291
output_string chan "\n" in
294
output_string chan "end\n"
298
let proof_info_as_string s =
300
match (Hashtbl.find theorem_proofs s) with
302
let open_goal_counter = ref 0 in
303
let rec dump_rec = function
304
{index=i;sub_proofs=trees;parent=the_parent;is_open=op} ->
306
(match the_parent with
309
res := !res ^ "\"open goal\"\n"
312
res := !res ^ (string_of_int j);
313
res := !res ^ " -> ";
316
res := !res ^ "\"open goal ";
317
open_goal_counter := !open_goal_counter + 1;
318
res := !res ^ (string_of_int !open_goal_counter);
319
res := !res ^ "\"\n";
323
res := !res ^ (string_of_int i);
327
List.iter dump_rec trees
333
let dump_proof_info chan s =
334
match (Hashtbl.find theorem_proofs s) with
336
let open_goal_counter = ref 0 in
337
let rec dump_rec = function
338
{index=i;sub_proofs=trees;parent=the_parent;is_open=op} ->
340
(match the_parent with
343
output_string chan "\"open goal\"\n"
346
output_string chan (string_of_int j);
347
output_string chan " -> ";
350
output_string chan "\"open goal ";
351
open_goal_counter := !open_goal_counter + 1;
352
output_string chan (string_of_int !open_goal_counter);
353
output_string chan "\"\n";
357
output_string chan (string_of_int i);
358
output_string chan "\n"
361
List.iter dump_rec trees
365
let get_nth_open_path s n =
366
match Hashtbl.find theorem_proofs s with
368
let {path_to_root=p}=List.nth l (n - 1) in
371
let border_length s =
372
match Hashtbl.find theorem_proofs s with
373
{border=l} -> List.length l;;
added
removed
contrib/interface/history.ml
