diff options
Diffstat (limited to 'contrib/interface/history.ml')
| -rw-r--r-- | contrib/interface/history.ml | 373 |
1 files changed, 0 insertions, 373 deletions
diff --git a/contrib/interface/history.ml b/contrib/interface/history.ml deleted file mode 100644 index f73c2084..00000000 --- a/contrib/interface/history.ml +++ /dev/null @@ -1,373 +0,0 @@ -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;; |