module Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@169 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 349 insertions, 0 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
new file mode 100644
index 0000000000..18a9b09a74
--- /dev/null
+++ b/proofs/pfedit.ml
@@ -0,0 +1,349 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Sign
+open Generic
+open Term
+open Constant
+open Evd
+open Declare
+open Tacmach
+open Proof_trees
+open Lib
+
+type proof_topstate = {
+  top_hyps : var_context * var_context;
+  top_goal : goal;
+  top_strength : strength }
+
+let proof_edits = (Edit.empty() : (string,pftreestate,proof_topstate) Edit.t)
+
+let list_proofs () = Edit.dom proof_edits
+
+let msg_proofs use_resume =
+  match Edit.dom proof_edits with
+    | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >]
+    | l ->  [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ;
+               (prlist_with_sep pr_spc pr_str (list_proofs ())) ; 'sTR"." ;
+               (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
+              	else [< >])
+            >]
+
+let undo_default = 12
+let undo_limit = ref undo_default
+
+(*********************************************************************)
+(*    Functions for decomposing and modifying the proof state        *)
+(*********************************************************************)
+
+let get_state () =
+  match Edit.read proof_edits with
+    | None -> errorlabstrm "Pfedit.get_state"
+          [< 'sTR"No focused proof"; msg_proofs true >]
+    | Some(_,pfs,ts) -> (pfs,ts)
+
+let get_topstate ()    = snd(get_state())
+let get_pftreestate () = fst(get_state())
+
+let get_evmap_sign og =
+  let og = match og with
+    | Some n ->
+        let pftree = get_pftreestate () in
+        Some (nth_goal_of_pftreestate n pftree)
+    | None ->
+        try
+          let pftree = get_pftreestate () in
+          Some (nth_goal_of_pftreestate 1 pftree)
+        with UserError _ -> 
+	  None 
+  in
+  match og with
+    | Some goal -> (project goal, pf_hyps goal)
+    | _ -> (Evd.empty, Global.var_context())
+ 
+let set_proof s = 
+  try 
+    Edit.focus proof_edits s
+  with Invalid_argument "Edit.focus" ->
+    errorlabstrm "Pfedit.set_proof"
+      [< 'sTR"No such proof" ; (msg_proofs false) >]
+      
+let resume_last () =
+  match (Edit.last_focused proof_edits) with
+    | None ->
+        errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >]
+    | p -> 
+	Edit.focus proof_edits p
+	  
+let get_proof () =
+  match Edit.read proof_edits with
+    | None ->
+        errorlabstrm "Pfedit.get_proof"
+          [< 'sTR"No focused proof" ; msg_proofs true >]
+    | Some(na,_,_) -> na
+
+let add_proof (na,pfs,ts) =
+  Edit.create proof_edits (na,pfs,ts,Some !undo_limit)
+    
+let del_proof na =
+  try 
+    Edit.delete proof_edits na
+  with (UserError ("Edit.delete",_)) ->
+    errorlabstrm "Pfedit.del_proof"
+      [< 'sTR"No such proof" ; msg_proofs false >]
+      
+let init_proofs () = Edit.clear proof_edits
+		       
+let mutate f =
+  try 
+    Edit.mutate proof_edits (fun _ pfs -> f pfs)
+  with Invalid_argument "Edit.mutate" ->
+    errorlabstrm "Pfedit.mutate"
+      [< 'sTR"No focused proof" ; msg_proofs true >]
+
+let rev_mutate f =
+  try 
+    Edit.mutate proof_edits (fun _ pfs -> f pfs)
+  with Invalid_argument "Edit.rev_mutate" ->
+    errorlabstrm "Pfedit.rev_mutate"
+      [< 'sTR"No focused proof"; msg_proofs true >]
+
+let start (na,ts) =
+  let pfs = mk_pftreestate ts.top_goal in 
+  add_proof(na,pfs,ts)
+    
+let restart () =
+  match Edit.read proof_edits with
+    | None -> 
+	errorlabstrm "Pfedit.restart"
+          [< 'sTR"No focused proof to restart" ; msg_proofs true >]
+    | Some(na,_,ts) -> 
+	del_proof na;
+        start (na,ts);
+        set_proof (Some na)
+
+let proof_prompt () =
+  match Edit.read proof_edits with
+    | None -> "Coq < "
+    | Some(na,_,_) -> na^" < "
+	  
+let proof_term () =
+  extract_pftreestate (get_pftreestate())
+    
+(* Detect is one has completed a subtree of the initial goal *)
+let subtree_solved () = 
+  let pts = get_pftreestate () in
+  is_complete_proof (proof_of_pftreestate pts) & 
+  not (is_top_pftreestate pts)
+
+(*********************************************************************)
+(*                 Undo functions                                    *)
+(*********************************************************************)
+    
+let set_undo n = 
+  if n>=0 then 
+    undo_limit := n+1
+  else 
+    error "Cannot set a negative undo limit"
+      
+let unset_undo  () = set_undo undo_default
+
+let undo n =
+  try 
+    Edit.undo proof_edits n; 
+       (* needed because the resolution of a subtree is done in 2 steps 
+       then a sequence of undo can lead to a focus on a completely solved 
+       subtree - this solution only works properly if undoing one step *)
+    if subtree_solved() then  Edit.undo proof_edits 1
+  with (Invalid_argument "Edit.undo") ->
+    errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >]
+
+(*********************************************************************)
+(*              Saving  functions                                    *)
+(*********************************************************************)
+
+let save_named opacity =
+  let (pfs,ts) = get_state() 
+  and ident = get_proof() in
+  let {evar_concl=concl} = ts.top_goal 
+  and strength = ts.top_strength in
+  let pfterm = extract_pftreestate pfs in 
+  declare_constant (id_of_string ident) (*** opacity strength ***) 
+    { const_entry_body = pfterm; const_entry_type = Some concl };
+  del_proof ident;
+  message(ident ^ " is defined")
+    
+let save_anonymous opacity save_ident n =
+  let (pfs,ts) = get_state() 
+  and ident = get_proof() in
+  let {evar_concl=concl} = ts.top_goal 
+  and strength = ts.top_strength in
+  let pfterm = extract_pftreestate pfs in 
+  if ident = "Unnamed_thm" then
+    declare_constant (id_of_string save_ident) (*** opacity,strength ***)
+      { const_entry_body = pfterm; const_entry_type = Some concl }
+  else begin
+    message("Overriding name " ^ ident ^ " and using " ^ save_ident);
+    declare_constant (id_of_string save_ident) (*** opacity,strength ***)
+      { const_entry_body = pfterm; const_entry_type = Some concl }
+  end;
+  del_proof ident;
+  message(save_ident ^ " is defined")
+    
+let save_anonymous_thm opacity id =
+  save_anonymous opacity id NeverDischarge
+
+let save_anonymous_remark opacity id =
+  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
+  save_anonymous opacity id (make_strength path)
+
+(*********************************************************************)
+(*              Abort   functions                                    *)
+(*********************************************************************)
+ 
+let refining () = [] <> (Edit.dom proof_edits)
+
+let abort_goal pn = del_proof pn
+
+let abort_cur_goal () = del_proof (get_proof ())
+
+let abort_goals () =
+  if refining() then begin
+    init_proofs();
+    message "Current goals aborted"
+  end else 
+    error "No proof-editing in progress"
+
+let abort_refine f x = 
+  if refining() then abort_goals(); 
+  f x
+  (* used to be: error "Must save or abort current goal first" *)
+
+let reset_name = abort_refine reset_to
+(*** TODO 
+and reset_keeping_name = abort_refine reset_keeping
+and reset_section = abort_refine raw_reset_section
+and save_state = abort_refine States.raw_save_state
+and restore_state = abort_refine States.raw_restore_state
+and restore_last_saved_state = abort_refine States.raw_restore_last_saved_state
+***)
+and reset_all = abort_refine Lib.init
+
+(***TODO
+let reset_prelude () = restore_state "Prelude"
+and reset_initial () = restore_state "Initial"
+***)
+   
+(*********************************************************************)
+(*              Modifying the current prooftree                      *)
+(*********************************************************************)
+
+let start_proof_with_type na str sign fsign concl =
+  let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in
+  let ts = { 
+    top_hyps = (sign,fsign);
+    top_goal = top_goal;
+    top_strength = str }
+  in
+  start(na,ts);
+  set_proof (Some na)
+
+let start_proof na str concl_com =
+  let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
+  let concl = fconstruct_type sigma sign concl_com in
+  start_proof_with_type na str sign fsign concl.body
+
+let start_proof_constr na str concl =
+  let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
+  let _ = type_of_type sigma sign concl in
+  start_proof_with_type na str sign fsign concl
+
+let solve_nth k tac =
+  let pft = get_pftreestate() in
+  if not (List.mem (-1) (cursor_of_pftreestate pft)) then 
+    mutate (solve_nth_pftreestate k tac)
+    (* ;
+    let pfs =get_pftreestate() in
+    let pf = proof_of_pftreestate pfs in
+    let (pfterm,metamap) = refiner__extract_open_proof pf.goal.hyps pf
+    in (try typing__control_only_guard empty_evd pfterm
+    with e -> (undo 1; raise e));
+    ()) 
+    *)
+  else 
+    error "cannot apply a tactic when we are descended behind a tactic-node"
+
+let by tac = mutate (solve_pftreestate tac)
+
+let traverse n = rev_mutate (traverse n)
+ 
+(* [traverse_to path]
+
+   Traverses the current proof to get to the location specified by
+   [path].
+
+   ALGORITHM:
+
+   If the cursor is equal to the path, we are done.
+
+   If the cursor is longer than the path, then traverse to the parent
+
+   If the cursor is equal to the tail of the path, then traverse to
+   the head of the path, and we are done.
+
+   Otherwise, traverse to the parent, traverse to the tail of the
+   path, then traverse to the path.
+
+*)
+
+let rec nth_cdr = function
+  | 0 -> (function l -> l)
+  | n -> (comp List.tl (nth_cdr (n - 1)))
+	
+let rec common_ancestor_equal_length = function
+  | ((a::l1), (b::l2)) ->
+      let (prefx,n) as result = (common_ancestor_equal_length (l1,l2)) in
+      if result = ([],0) then    
+        if a = b then 
+	  result
+        else 
+	  (a::prefx),(n + 1)
+      else 
+	(a::prefx),(n + 1)
+  | ([], []) -> [],0
+  | (_, _) -> anomaly "common_ancestor_equal_length"
+	
+let common_ancestor l1 l2 =
+  let diff_lengths = (List.length l1) - (List.length l2) in
+  if diff_lengths > 0 then
+    let head,tail = chop_list diff_lengths l1 in
+    let (prefx,n) = common_ancestor_equal_length (tail,l2) in 
+    (head@prefx),n
+  else if diff_lengths < 0 then
+    let (prefx,n) = common_ancestor_equal_length
+		      (l1, (nth_cdr (- diff_lengths) l2)) in
+    prefx,(n - diff_lengths)
+  else 
+    common_ancestor_equal_length (l1,l2)
+      
+let rec traverse_up = function
+  | 0 -> (function pf -> pf)
+  | n -> (function pf -> Tacmach.traverse 0 (traverse_up (n - 1) pf))
+
+let rec traverse_down = function
+  | [] -> (function pf -> pf)
+  | n::l -> (function pf -> Tacmach.traverse n (traverse_down l pf))
+
+let traverse_to path =
+  let up_and_down path pfs =
+    let cursor = cursor_of_pftreestate pfs in
+    let down_list, up_count = common_ancestor path cursor in
+    traverse_down down_list (traverse_up up_count pfs)
+  in
+  rev_mutate (up_and_down path)
+
+(* traverse the proof tree until it reach the nth subgoal *)
+let traverse_nth_goal n = mutate (nth_unproven n)