Nettoyage de l'interface de Pfedit

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

8 files changed, 219 insertions, 82 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 91a83ea9d9..004bc5c474 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -162,3 +162,36 @@ let w_Define sp c wc =
     	in 
 	(ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc)
     | _ -> error "define_evar"
+
+(******************************************)
+(* Instantiation of existential variables *)
+(******************************************)
+
+let instantiate_pf n c pfts = 
+  let gls = top_goal_of_pftreestate pfts in
+  let (wc,_) = startWalk gls in
+  let sigma  = (w_Underlying wc) in 
+  let (sp,_) = 
+    try 
+      List.nth (Evd.non_instantiated sigma) (n-1)
+    with Failure _ -> 
+      error "not so many uninstantiated existential variables"
+  in 
+  let wc' = w_Define sp c wc in 
+  let newgc = ts_mk (w_Underlying wc') in 
+  change_constraints_pftreestate newgc pfts
+
+let instantiate_pf_com n com pfts = 
+  let gls = top_goal_of_pftreestate pfts in
+  let (wc,_) = startWalk gls in
+  let sigma = (w_Underlying wc) in 
+  let (sp,evd) = 
+    try
+      List.nth (Evd.non_instantiated sigma) (n-1) 
+    with Failure _ -> 
+      error "not so many uninstantiated existential variables"
+  in 
+  let c = Astterm.interp_constr sigma evd.evar_env com in     
+  let wc' = w_Define sp c wc in
+  let newgc = ts_mk (w_Underlying wc') in
+  change_constraints_pftreestate newgc pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 1674f2f3ac..ef72c9d35d 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -49,3 +49,6 @@ val w_ORELSE     : w_tactic -> w_tactic -> w_tactic
 val ctxt_type_of : readable_constraints -> constr -> constr
 
 val evars_of     : readable_constraints -> constr -> local_constraints
+
+val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3270177ee1..2d4e8a903b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -123,7 +123,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let indspec =
-    try try_mutind_of env sigma ct
+    try find_inductive env sigma ct
     with Induc -> anomaly "mk_casegoals" in
   let (lbrty,conclty) = type_case_branches env sigma indspec pt p c in
   (acc'',lbrty,conclty)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7ffb408786..44c4fc5fb7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -25,13 +25,14 @@ type proof_topstate = {
 
 let proof_edits = (Edit.empty() : (string,pftreestate,proof_topstate) Edit.t)
 
-let list_proofs () = Edit.dom proof_edits
+let get_all_proof_names () = 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"." ;
+               (prlist_with_sep pr_spc pr_str (get_all_proof_names ())) ;
+	       'sTR"." ;
                (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
               	else [< >])
             >]
@@ -52,6 +53,7 @@ let get_state () =
 let get_topstate ()    = snd(get_state())
 let get_pftreestate () = fst(get_state())
 
+(*
 let get_evmap_sign og =
   let og = match og with
     | Some n ->
@@ -67,22 +69,30 @@ let get_evmap_sign og =
   match og with
     | Some goal -> (project goal, pf_env goal)
     | _ -> (Evd.empty, Global.env())
- 
-let set_proof s = 
+*)
+
+let get_goal_context n =
+  let pftree = get_pftreestate () in
+  let goal = nth_goal_of_pftreestate n pftree in
+  (project goal, pf_env goal)
+
+let get_current_goal_context () = get_goal_context 1
+
+let set_current_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 () =
+let resume_last_proof () =
   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 () =
+let get_current_proof_name () =
   match Edit.read proof_edits with
     | None ->
         errorlabstrm "Pfedit.get_proof"
@@ -108,13 +118,6 @@ let mutate f =
     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)
@@ -127,13 +130,8 @@ let restart () =
     | Some(na,_,ts) -> 
 	del_proof na;
         start (na,ts);
-        set_proof (Some na)
+        set_current_proof (Some na)
 
-let proof_prompt () =
-  match Edit.read proof_edits with
-    | None -> "Coq < "
-    | Some(na,_,_) -> na^" < "
-	  
 let proof_term () =
   extract_pftreestate (get_pftreestate())
     
@@ -153,7 +151,7 @@ let set_undo n =
   else 
     error "Cannot set a negative undo limit"
       
-let unset_undo  () = set_undo undo_default
+let reset_undo  () = set_undo undo_default
 
 let undo n =
   try 
@@ -171,7 +169,7 @@ let undo n =
 
 let save_named opacity =
   let (pfs,ts) = get_state() 
-  and ident = get_proof() in
+  and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
@@ -181,11 +179,11 @@ let save_named opacity =
   del_proof ident;
   if Options.is_verbose() then message (ident ^ " is defined")
     
-let save_anonymous opacity save_ident n =
+let save_anonymous opacity save_ident strength =
   let (pfs,ts) = get_state() 
-  and ident = get_proof() in
-  let {evar_concl=concl} = ts.top_goal 
-  and strength = ts.top_strength in
+  and ident = get_current_proof_name() in
+  let {evar_concl=concl} = ts.top_goal in
+  (* we do not consider default ts.top_strength *)
   let pfterm = extract_pftreestate pfs in 
   if ident = "Unnamed_thm" then
     declare_constant (id_of_string save_ident)
@@ -213,28 +211,23 @@ let save_anonymous_remark opacity id =
  
 let refining () = [] <> (Edit.dom proof_edits)
 
-let abort_goal pn = del_proof pn
-
-let abort_cur_goal () = del_proof (get_proof ())
+let check_no_pending_proofs () =
+  if refining () then 
+    errorlabstrm "check_no_pending_proofs"
+      [< 'sTR"Proof editing in progress" ; (msg_proofs false) ;
+         'sTR"Use \"Abort All\" first or complete proof(s)." >]
 
-let abort_goals () =
-  if refining() then begin
-    init_proofs();
-    message "Current goals aborted"
-  end else 
-    error "No proof-editing in progress"
+let abort_goal pn = del_proof pn
 
-let abort_refine f x = 
-  if refining() then abort_goals(); 
-  f x
-  (* used to be: error "Must save or abort current goal first" *)
+let abort_current_goal () = del_proof (get_current_proof_name ())
 
+let abort_goals = init_proofs
    
 (*********************************************************************)
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof_with_type na str env concl =
+let start_proof na str env concl =
   let top_goal = mk_goal (mt_ctxt Intset.empty) env concl in
   let ts = { 
     top_hyps = (env,empty_env);
@@ -242,19 +235,17 @@ let start_proof_with_type na str env concl =
     top_strength = str }
   in
   start(na,ts);
-  set_proof (Some na)
-
-let start_proof na str concl_com =
-  let sigma = Evd.empty in
-  let env = Global.env() in
-  let concl = interp_type sigma env concl_com in
-  start_proof_with_type na str env concl
+  set_current_proof (Some na)
 
+(*
 let start_proof_constr na str concl =
   let sigma = Evd.empty in
   let env = Global.env() in
+(* Si c'est un constr, il est supposé typable dans le contexte courant
   let _ = execute_type env sigma concl in
+*)
   start_proof_with_type na str env concl
+*)
 
 let solve_nth k tac =
   let pft = get_pftreestate() in
@@ -273,7 +264,9 @@ let solve_nth k tac =
 
 let by tac = mutate (solve_pftreestate tac)
 
-let traverse n = rev_mutate (traverse n)
+let instantiate_nth_evar_com n c = mutate (instantiate_pf_com n c)
+
+let traverse n = mutate (traverse n)
  
 (* [traverse_to path]
 
@@ -338,15 +331,25 @@ let traverse_to path =
     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)
+  mutate (up_and_down path)
 
 (* traverse the proof tree until it reach the nth subgoal *)
 let traverse_nth_goal n = mutate (nth_unproven n)
 
+let traverse_prev_unproven () = mutate prev_unproven
+
+let traverse_next_unproven () = mutate next_unproven
+
+
 (* The goal focused on *)
 let focus_n = ref 0
 let make_focus n = focus_n := n
 let focus () = !focus_n
 let focused_goal () = let n = !focus_n in if n=0 then 1 else n
 
+let reset_top_of_tree () = 
+  let pts = get_pftreestate () in 
+  if not (is_top_pftreestate pts) then mutate top_of_tree
+
+
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 3499f9227b..6d5c56439a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -12,59 +12,152 @@ open Proof_type
 open Tacmach
 (*i*)
 
-val proof_prompt : unit -> string
+(* [refining ()] tells if there is some proof in progress, even if a not
+   focused one *)
+
 val refining : unit -> bool
+
+(* [check_no_pending_proofs ()] fails if there is still some proof in
+   progress *)
+
+val check_no_pending_proofs : unit -> unit
+
+(* [abort_goal name] aborts proof of name [name] or failed if no proof
+has this name *)
+
 val abort_goal : string -> unit
-val abort_cur_goal : unit -> unit
+
+(* [abort_current_goal ()] aborts current focused proof or failed if
+    no proof is focused *)
+
+val abort_current_goal : unit -> unit
+
+(* [abort_goals ()] aborts all open proofs if any *)
+
 val abort_goals : unit -> unit
-val abort_refine : ('a -> 'b) -> 'a -> 'b
-val msg_proofs : bool -> std_ppcmds
 
-val undo_limit : int ref
-val set_undo : int -> unit
-val unset_undo : unit -> unit
+(* [undo n] undoes the effect of the last [n] tactics applied to the
+    current proof; it fails if no proof is focused or if the ``undo''
+    stack is exhausted *)
+
 val undo : int -> unit
-val resume_last : unit -> unit
 
-type proof_topstate = {
-  top_hyps : env * env;
-  top_goal : goal;
-  top_strength : strength }
+(* [set_undo n] sets the size of the ``undo'' stack *)
+
+val set_undo : int -> unit
+
+(* [reset_undo n] sets the size of the ``undo'' stack to the default
+   value (12) *)
+
+val reset_undo : unit -> unit
+
+(* [resume_last_proof ()] focus on the last unfocused proof or fails
+   if there is no suspended proofs *)
+
+val resume_last_proof : unit -> unit
+
+(* [get_pftreestate ()] returns the current focused pending proof or
+   raises [UserError "no focused proof"] *)
 
-val get_state : unit -> pftreestate * proof_topstate
-val get_topstate : unit -> proof_topstate
 val get_pftreestate : unit -> pftreestate
-val get_evmap_sign : int option -> evar_declarations * env
-val set_proof : string option -> unit
-val get_proof : unit -> string
-val list_proofs : unit -> string list
-val add_proof : string * pftreestate * proof_topstate -> unit
-val del_proof : string -> unit
-val init_proofs : unit -> unit
 
-val mutate : (pftreestate -> pftreestate) -> unit
-val rev_mutate : (pftreestate -> pftreestate) -> unit
-val start : string * proof_topstate -> unit
+(* [get_goal_context n] returns the context of the [n]th subgoal of
+   the current focused proof or raises a [UserError] if there is no
+   focused proof or if there is no more subgoals *)
+
+val get_goal_context : int -> evar_declarations * env
+
+(* [get_current_goal_context ()] works as [get_goal_context 1] *)
+
+val get_current_goal_context : unit -> evar_declarations * env
+
+(* [set_current_proof None] unfocuses the current focused proof; [set_proof
+(Some name)] focuses on the proof of name [name] or raises a
+[UserError] if no proof has name [name] *)
+
+val set_current_proof : string option -> unit
+
+(* [get_current_proof_name ()] return the name of the current focused
+    proof or failed if no proof is focused *)
+
+val get_current_proof_name : unit -> string
+
+(* [list_proofs ()] returns the list of all pending proof names *)
+
+val get_all_proof_names : unit -> string list
+
+(* [restart ()] restarts the current focused proof from the beginning
+   or fails if no proof is focused *)
+
 val restart : unit -> unit
-val proof_prompt : unit -> string
-val proof_term : unit -> constr
 
-val start_proof : string -> strength -> Coqast.t -> unit
-val start_proof_constr : string -> strength -> constr -> unit
+(* [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
+
+val start_proof : string -> strength -> env -> constr -> unit
+
+(* [save_named b] saves the current completed proof under the name it
+was started; boolean [b] tells if the theorem is declared opaque; it
+fails if the proof is not completed *)
 
 val save_named : bool -> unit
-val save_anonymous : bool -> string -> 'a -> unit
+
+(* [save_anonymous_thm b name] behaves as [save_named] but declares the
+theorem under the name [name] and gives it the strength of a theorem *)
+
 val save_anonymous_thm : bool -> string -> unit
+
+(* [save_anonymous_remark b name] behaves as [save_named] but declares the
+theorem under the name [name] and gives it the strength of a remark *)
+
 val save_anonymous_remark : bool -> string -> unit
 
+(* [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
+   current focused proof or raises a UserError if no proof is focused or
+   if there is no [n]th subgoal *)
+
 val solve_nth : int -> tactic -> unit
+
+(* [by tac] applies tactic [tac] to the 1st subgoal of the current
+   focused proof or raises a UserError if there is no focused proof or
+   if there is no more subgoals *)
+
 val by : tactic -> unit
-val traverse : int -> unit
-val traverse_nth_goal : int -> unit
-val traverse_to : int list -> unit
+
+(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
+   existential variable of the current focused proof by [c] or raises a
+   UserError if no proof is focused or if there is no such [n]th
+   existential variable *)
+
+val instantiate_nth_evar_com : int -> Coqast.t -> unit
+
+(* To deal with focus *)
 
 val make_focus : int -> unit
 val focus : unit -> int
 val focused_goal : unit -> int
-
 val subtree_solved : unit -> bool
+
+val reset_top_of_tree : unit -> unit
+val traverse : int -> unit
+val traverse_nth_goal : int -> unit
+val traverse_next_unproven : unit -> unit
+val traverse_prev_unproven : unit -> unit
+
+(*i N'ont pas à être exportées
+type proof_topstate
+val msg_proofs : bool -> std_ppcmds
+val undo_limit : int ref
+val get_state : unit -> pftreestate * proof_topstate
+val get_topstate : unit -> proof_topstate
+val add_proof : string * pftreestate * proof_topstate -> unit
+val del_proof : string -> unit
+val init_proofs : unit -> unit
+
+val mutate : (pftreestate -> pftreestate) -> unit
+val rev_mutate : (pftreestate -> pftreestate) -> unit
+val start : string * proof_topstate -> unit
+val proof_term : unit -> constr
+val save_anonymous : bool -> string -> unit
+val traverse_to : int list -> unit
+i*)
+
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d0b3ca33ab..4b821596e4 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -97,6 +97,7 @@ val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 val traverse : int -> pftreestate -> pftreestate
 val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate : tactic -> pftreestate -> pftreestate
+
 (* a weak version of logical undoing, that is really correct only *)
 (* if there are no existential variables.                         *)
 val weak_undo_pftreestate : pftreestate -> pftreestate
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5a69ecf577..c0254a7ca6 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -150,6 +150,8 @@ let prev_unproven           = prev_unproven
 let top_of_tree             = top_of_tree
 let frontier                = frontier
 let change_constraints_pftreestate = change_constraints_pftreestate
+let instantiate_pf     = instantiate_pf
+let instantiate_pf_com = instantiate_pf_com
 
 (***********************************)
 (* Walking constraints re-exported *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 0baa909c99..afb9016ea5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -107,6 +107,8 @@ val prev_unproven           : pftreestate -> pftreestate
 val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   global_constraints -> pftreestate -> pftreestate
+val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
 
 
 (*s Tacticals re-exported from the Refiner module. *)