summaryrefslogtreecommitdiff
path: root/contrib/interface/history.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/history.ml')
-rw-r--r--contrib/interface/history.ml373
1 files changed, 373 insertions, 0 deletions
diff --git a/contrib/interface/history.ml b/contrib/interface/history.ml
new file mode 100644
index 00000000..f73c2084
--- /dev/null
+++ b/contrib/interface/history.ml
@@ -0,0 +1,373 @@
+open Paths;;
+
+type tree = {mutable index : int;
+ parent : tree option;
+ path_to_root : int list;
+ mutable is_open : bool;
+ mutable sub_proofs : tree list};;
+
+type prf_info = {
+ mutable prf_length : int;
+ mutable ranks_and_goals : (int * int * tree) list;
+ mutable border : tree list;
+ prf_struct : tree};;
+
+let theorem_proofs = ((Hashtbl.create 17):
+ (string, prf_info) Hashtbl.t);;
+
+
+let rec mk_trees_for_goals path tree rank k n =
+ if k = (n + 1) then
+ []
+ else
+ { index = rank;
+ parent = tree;
+ path_to_root = k::path;
+ is_open = true;
+ sub_proofs = [] } ::(mk_trees_for_goals path tree rank (k+1) n);;
+
+
+let push_command s rank ngoals =
+ let ({prf_length = this_length;
+ ranks_and_goals = these_ranks;
+ border = this_border} as proof_info) =
+ Hashtbl.find theorem_proofs s in
+ let rec push_command_aux n = function
+ [] -> failwith "the given rank was too large"
+ | a::l ->
+ if n = 1 then
+ let {path_to_root = p} = a in
+ let new_trees = mk_trees_for_goals p (Some a) (this_length + 1) 1 ngoals in
+ new_trees,(new_trees@l),a
+ else
+ let new_trees, res, this_tree = push_command_aux (n-1) l in
+ new_trees,(a::res),this_tree in
+ let new_trees, new_border, this_tree =
+ push_command_aux rank this_border in
+ let new_length = this_length + 1 in
+ begin
+ proof_info.border <- new_border;
+ proof_info.prf_length <- new_length;
+ proof_info.ranks_and_goals <- (rank, ngoals, this_tree)::these_ranks;
+ this_tree.index <- new_length;
+ this_tree.is_open <- false;
+ this_tree.sub_proofs <- new_trees
+ end;;
+
+let get_tree_for_rank thm_name rank =
+ let {ranks_and_goals=l;prf_length=n} =
+ Hashtbl.find theorem_proofs thm_name in
+ let rec get_tree_aux = function
+ [] ->
+ failwith
+ "inconsistent values for thm_name and rank in get_tree_for_rank"
+ | (_,_,({index=i} as tree))::tl ->
+ if i = rank then
+ tree
+ else
+ get_tree_aux tl in
+ get_tree_aux l;;
+
+let get_path_for_rank thm_name rank =
+ let {path_to_root=l}=get_tree_for_rank thm_name rank in
+ l;;
+
+let rec list_descendants_aux l tree =
+ let {index = i; is_open = open_status; sub_proofs = tl} = tree in
+ let res = (List.fold_left list_descendants_aux l tl) in
+ if open_status then i::res else res;;
+
+let list_descendants thm_name rank =
+ list_descendants_aux [] (get_tree_for_rank thm_name rank);;
+
+let parent_from_rank thm_name rank =
+ let {parent=mommy} = get_tree_for_rank thm_name rank in
+ match mommy with
+ Some x -> Some x.index
+ | None -> None;;
+
+let first_child_command thm_name rank =
+ let {sub_proofs = l} = get_tree_for_rank thm_name rank in
+ let rec first_child_rec = function
+ [] -> None
+ | {index=i;is_open=b}::l ->
+ if b then
+ (first_child_rec l)
+ else
+ Some i in
+ first_child_rec l;;
+
+type index_or_rank = Is_index of int | Is_rank of int;;
+
+let first_child_command_or_goal thm_name rank =
+ let proof_info = Hashtbl.find theorem_proofs thm_name in
+ let {sub_proofs=l}=get_tree_for_rank thm_name rank in
+ match l with
+ [] -> None
+ | ({index=i;is_open=b} as t)::_ ->
+ if b then
+ let rec get_rank n = function
+ [] -> failwith "A goal is lost in first_child_command_or_goal"
+ | a::l ->
+ if a==t then
+ n
+ else
+ get_rank (n + 1) l in
+ Some(Is_rank(get_rank 1 proof_info.border))
+ else
+ Some(Is_index i);;
+
+let next_sibling thm_name rank =
+ let ({parent=mommy} as t)=get_tree_for_rank thm_name rank in
+ match mommy with
+ None -> None
+ | Some real_mommy ->
+ let {sub_proofs=l}=real_mommy in
+ let rec next_sibling_aux b = function
+ (opt_first, []) ->
+ if b then
+ opt_first
+ else
+ failwith "inconsistency detected in next_sibling"
+ | (opt_first, {is_open=true}::l) ->
+ next_sibling_aux b (opt_first, l)
+ | (Some(first),({index=i; is_open=false} as t')::l) ->
+ if b then
+ Some i
+ else
+ next_sibling_aux (t == t') (Some first,l)
+ | None,({index=i;is_open=false} as t')::l ->
+ next_sibling_aux (t == t') ((Some i), l)
+ in
+ Some (next_sibling_aux false (None, l));;
+
+
+let prefix l1 l2 =
+ let l1rev = List.rev l1 in
+ let l2rev = List.rev l2 in
+ is_prefix l1rev l2rev;;
+
+let rec remove_all_prefixes p = function
+ [] -> []
+ | a::l ->
+ if is_prefix p a then
+ (remove_all_prefixes p l)
+ else
+ a::(remove_all_prefixes p l);;
+
+let recompute_border tree =
+ let rec recompute_border_aux tree acc =
+ let {is_open=b;sub_proofs=l}=tree in
+ if b then
+ tree::acc
+ else
+ List.fold_right recompute_border_aux l acc in
+ recompute_border_aux tree [];;
+
+
+let historical_undo thm_name rank =
+ let ({ranks_and_goals=l} as proof_info)=
+ Hashtbl.find theorem_proofs thm_name in
+ let rec undo_aux acc = function
+ [] -> failwith "bad rank provided for undoing in historical_undo"
+ | (r, n, ({index=i} as tree))::tl ->
+ let this_path_reversed = List.rev tree.path_to_root in
+ let res = remove_all_prefixes this_path_reversed acc in
+ if i = rank then
+ begin
+ proof_info.prf_length <- i-1;
+ proof_info.ranks_and_goals <- tl;
+ tree.is_open <- true;
+ tree.sub_proofs <- [];
+ proof_info.border <- recompute_border proof_info.prf_struct;
+ this_path_reversed::res
+ end
+ else
+ begin
+ tree.is_open <- true;
+ tree.sub_proofs <- [];
+ undo_aux (this_path_reversed::res) tl
+ end
+ in
+ List.map List.rev (undo_aux [] l);;
+
+(* The following function takes a list of trees and compute the
+ number of elements whose path is lexically smaller or a suffixe of
+ the path given as a first argument. This works under the precondition that
+ the list is lexicographically order. *)
+
+let rec logical_undo_on_border the_tree rev_path = function
+ [] -> (0,[the_tree])
+ | ({path_to_root=p}as tree)::tl ->
+ let p_rev = List.rev p in
+ if is_prefix rev_path p_rev then
+ let (k,res) = (logical_undo_on_border the_tree rev_path tl) in
+ (k+1,res)
+ else if lex_smaller p_rev rev_path then
+ let (k,res) = (logical_undo_on_border the_tree rev_path tl) in
+ (k,tree::res)
+ else
+ (0, the_tree::tree::tl);;
+
+
+let logical_undo thm_name rank =
+ let ({ranks_and_goals=l; border=last_border} as proof_info)=
+ Hashtbl.find theorem_proofs thm_name in
+ let ({path_to_root=ref_path} as ref_tree)=get_tree_for_rank thm_name rank in
+ let rev_ref_path = List.rev ref_path in
+ let rec logical_aux lex_smaller_offset family_width = function
+ [] -> failwith "this case should never happen in logical_undo"
+ | (r,n,({index=i;path_to_root=this_path; sub_proofs=these_goals} as tree))::
+ tl ->
+ let this_path_rev = List.rev this_path in
+ let new_rank, new_offset, new_width, kept =
+ if is_prefix rev_ref_path this_path_rev then
+ (r + lex_smaller_offset), lex_smaller_offset,
+ (family_width + 1 - n), false
+ else if lex_smaller this_path_rev rev_ref_path then
+ r, (lex_smaller_offset - 1 + n), family_width, true
+ else
+ (r + 1 - family_width+ lex_smaller_offset),
+ lex_smaller_offset, family_width, true in
+ if i=rank then
+ [i,new_rank],[], tl, rank
+ else
+ let ranks_undone, ranks_kept, ranks_and_goals, current_rank =
+ (logical_aux new_offset new_width tl) in
+ begin
+ if kept then
+ begin
+ tree.index <- current_rank;
+ ranks_undone, ((i,new_rank)::ranks_kept),
+ ((new_rank, n, tree)::ranks_and_goals),
+ (current_rank + 1)
+ end
+ else
+ ((i,new_rank)::ranks_undone), ranks_kept,
+ ranks_and_goals, current_rank
+ end in
+ let number_suffix, new_border =
+ logical_undo_on_border ref_tree rev_ref_path last_border in
+ let changed_ranks_undone, changed_ranks_kept, new_ranks_and_goals,
+ new_length_plus_one = logical_aux 0 number_suffix l in
+ let the_goal_index =
+ let rec compute_goal_index n = function
+ [] -> failwith "this case should never happen in logical undo (2)"
+ | {path_to_root=path}::tl ->
+ if List.rev path = (rev_ref_path) then
+ n
+ else
+ compute_goal_index (n+1) tl in
+ compute_goal_index 1 new_border in
+ begin
+ ref_tree.is_open <- true;
+ ref_tree.sub_proofs <- [];
+ proof_info.border <- new_border;
+ proof_info.ranks_and_goals <- new_ranks_and_goals;
+ proof_info.prf_length <- new_length_plus_one - 1;
+ changed_ranks_undone, changed_ranks_kept, proof_info.prf_length,
+ the_goal_index
+ end;;
+
+let start_proof thm_name =
+ let the_tree =
+ {index=0;parent=None;path_to_root=[];is_open=true;sub_proofs=[]} in
+ Hashtbl.add theorem_proofs thm_name
+ {prf_length=0;
+ ranks_and_goals=[];
+ border=[the_tree];
+ prf_struct=the_tree};;
+
+let dump_sequence chan s =
+ match (Hashtbl.find theorem_proofs s) with
+ {ranks_and_goals=l}->
+ let rec dump_rec = function
+ [] -> ()
+ | (r,n,_)::tl ->
+ dump_rec tl;
+ output_string chan (string_of_int r);
+ output_string chan ",";
+ output_string chan (string_of_int n);
+ output_string chan "\n" in
+ begin
+ dump_rec l;
+ output_string chan "end\n"
+ end;;
+
+
+let proof_info_as_string s =
+ let res = ref "" in
+ match (Hashtbl.find theorem_proofs s) with
+ {prf_struct=tree} ->
+ let open_goal_counter = ref 0 in
+ let rec dump_rec = function
+ {index=i;sub_proofs=trees;parent=the_parent;is_open=op} ->
+ begin
+ (match the_parent with
+ None ->
+ if op then
+ res := !res ^ "\"open goal\"\n"
+ | Some {index=j} ->
+ begin
+ res := !res ^ (string_of_int j);
+ res := !res ^ " -> ";
+ if op then
+ begin
+ res := !res ^ "\"open goal ";
+ open_goal_counter := !open_goal_counter + 1;
+ res := !res ^ (string_of_int !open_goal_counter);
+ res := !res ^ "\"\n";
+ end
+ else
+ begin
+ res := !res ^ (string_of_int i);
+ res := !res ^ "\n"
+ end
+ end);
+ List.iter dump_rec trees
+ end in
+ dump_rec tree;
+ !res;;
+
+
+let dump_proof_info chan s =
+ match (Hashtbl.find theorem_proofs s) with
+ {prf_struct=tree} ->
+ let open_goal_counter = ref 0 in
+ let rec dump_rec = function
+ {index=i;sub_proofs=trees;parent=the_parent;is_open=op} ->
+ begin
+ (match the_parent with
+ None ->
+ if op then
+ output_string chan "\"open goal\"\n"
+ | Some {index=j} ->
+ begin
+ output_string chan (string_of_int j);
+ output_string chan " -> ";
+ if op then
+ begin
+ output_string chan "\"open goal ";
+ open_goal_counter := !open_goal_counter + 1;
+ output_string chan (string_of_int !open_goal_counter);
+ output_string chan "\"\n";
+ end
+ else
+ begin
+ output_string chan (string_of_int i);
+ output_string chan "\n"
+ end
+ end);
+ List.iter dump_rec trees
+ end in
+ dump_rec tree;;
+
+let get_nth_open_path s n =
+ match Hashtbl.find theorem_proofs s with
+ {border=l} ->
+ let {path_to_root=p}=List.nth l (n - 1) in
+ p;;
+
+let border_length s =
+ match Hashtbl.find theorem_proofs s with
+ {border=l} -> List.length l;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 20:00:51 +0000