package G4ip;


import pizza.util.Hashtable;
import java.util.Vector;
import G4ip.Form.*;
import G4ip.ProofDisplay.*;
import G4ip.Sequent.*;


/** The Gi4p prover.<p>
  * The prover is a thread in order to suspend the proof search
  * after one proof is found and to let the user make a choice 
  * of whether to stop or to continue with the proof search.
  * @author Christian Urban
  */
public class Prover extends Thread
{ ProverApplet  parent;  // the parent of the prover;
  boolean once;          // if true then at least one proof was found
  Sequent sequ;          // the root sequent to be proved
  Vector  frames;        // to record all frames which have been opened
  int index ;
  Hashtable<int,Sequent> proof;      // keeps a record of the proof
             
 
  /** The constructor creates a prover which proves a specific sequent.<p>
    * The parameter parent is for access to the applet buttons.
    */
  public Prover(Sequent init_sequ, ProverApplet init_parent) {
    super("Prover");
    parent = init_parent;
    once   = false;
    sequ   = new Sequent(init_sequ);
    frames = new Vector();
    index  = 1;
    proof  = new Hashtable();
  }
   
  /** Starts the thread; calls prove and stops the thread when 
    * the proof search is finished.
    */
  public void run()
    { prove(1,sequ,initial_sc); 
      if (once == true) { 
	parent.messages.setText("No more proofs.");
	parent.messages.repaint();
	parent.repaint();
      }
      else { 
	parent.messages.setText("Not provable.");
	parent.messages.repaint();
        parent.repaint();	
      }
      parent.switch_into_input_mode();
      this.stop();     // everything is done, stop the thread
    } 

  /** Closes all frames which have been opened.
    */
  public void finalize() { 
    for (int i=0; i<frames.size();i++) { 
      if (frames.elementAt != null) 
	{ ((ProofDisplay)frames.elementAt(i)).dispose(); }
    }
  }

  /** The tactic of the proof search.<p>
    * Method prove first enumerates all formulae on the LHS        
    * as being the principal formula and attempts to apply left-rules,  
    * subsequently it analyses the goal formula.                     
    */ 
  public void prove(int index, Sequent is,(() -> void) sc)  {
    Form principal;
    proof.put(index,new Sequent(is));      // add sequence to proof
    rightrules(index,is,sc);
    for (int i=0;i<is.Gamma.size();i++) {
      principal = (Form)is.Gamma.elementAt(i);
      is.Gamma.removeElement(principal);       // Gamma minus principal formula
      leftrules(index,principal,is,sc);
      is.Gamma.insertElementAt(principal,i);   // put principal formula
    }                                          // back into Gamma 
    //rightrules(index,is,sc);
    proof.remove(index);                   // remove sequence from proof
  }

  /** Analyses the goal formula. 
    */
  public void rightrules(int index, Sequent sequ,(()  -> void) sc)  {
    Context Gamma = sequ.Gamma;
    switch(sequ.G) { 
                          /** And-R
			    *  Gamma => A    Gamma => B  
			    * --------------------------   
			    *      Gamma => A and B     
			    */
    case And(Form A,Form B): 
      prove(2*index,new Sequent(Gamma,A),
            fun() -> void { prove(2*index+1,new Sequent(Gamma,B),sc); }  ); 
      break;

                          /** Imp-R  
			    *   Gamma,A => B   
			    * ----------------- 
			    *  Gamma => A imp B     
			    */ 
    case Imp(Form A,Form B):
      prove(2*index,new Sequent(Gamma.add(A),B),sc); break;
                           
                           /** Or-R 
			     *   Gamma  => A           Gamma => B   
			     * ----------------- or -----------------  
			     *  Gamma => A or B      Gamma => A or B   
			     */
    case Or(Form A,Form B):
      prove(2*index,new Sequent(Gamma,A),sc);
      prove(2*index,new Sequent(Gamma,B),sc); break;
                           
                           /** Equ-R
			     *  Gamma => A -> B  Gamma => B -> A 
			     * -------------------------------- 
			     *          Gamma => A <-> B         
			     */ 
    }
  }

  /** Analyses the principal formula on the LHS. 
    */
  public void leftrules(int index,Form principal,Sequent sequ,(() -> void) sc){
    Context Gamma = sequ.Gamma;
    Form    G     = sequ.G;
    switch(principal) {
                          /** false-L
			    * --------------------  
                            *  false, Gamma => G     
			    */
    case False():  sc(); break;

                           /** Axiom
      			     *  ---------------                  
      			     *   Gamma, G => G     G being atomic 
      			     */
    case Atm(String c):
      if (G instanceof Atm) {
	if (((Atm)G).c.compareTo(c) == 0) { sc(); }
      }
      break;

                          /** And-L
			    *   Gamma, A, B => G    
                            * -------------------- 
                            *  Gamma, A and B => G     
			    */
      
    case And(Form A, Form B): 
      prove(2*index,new Sequent(Gamma.add(A,B),G),sc); break;

                          /** Or-R
			    *  Gamma, A => G   Gamma, B => G 
                            * ------------------------------- 
                            *      Gamma, A or B => G      
			    */ 
    case Or(Form A, Form B):
      prove(2*index,new Sequent(Gamma.add(A),G),
	    fun() -> void {prove(2*index+1,new Sequent(Gamma.add(B),G),sc);});
      break;

                          /** Imp-L 2         
			    *  Gamma, A imp (B imp C) => G  
                            * ------------------------------
                            *  Gamma, (A and B) imp C => G    
                            */
    case Imp(And(Form A, Form B), Form C):
      prove(2*index,new Sequent(Gamma.add(Imp(A,Imp(B,C))),G),sc); break; 


                          /** Imp-L 3       
                            *  Gamma, (A imp C), (B imp C) => G 
                            * ----------------------------------
                            *   Gamma, (A or B) imp C => G       
			    */
    case Imp(Or(Form A, Form B), Form C):  
      prove(2*index,new Sequent(Gamma.add(Imp(A,C),Imp(B,C)),G),sc); break; 

                          /** Imp-L 4 
			    *  Gamma, (B imp C) => (A imp B)    Gamma, C => G 
                            * ------------------------------------------------
                            *         Gamma, (A imp B) imp C => G                
			    */
    case Imp(Imp(Form A, Form B), Form C): 
      prove(2*index,new Sequent(Gamma.add(Imp(B,C)),Imp(A,B)),
	    fun() -> void { prove(2*index+1,new Sequent(Gamma.add(C),G),sc);});
      break;  
                          /** Imp-L 1         
			    *   Gamma(A), B => G          A being atomic       
                            * ------------------------    Gamma(A) means:
                            *  Gamma(A), A imp B => G     Gamma contains A
			    */ 
    case Imp(Form A, Form B):
      if (A instanceof Atm) { 
	if (Gamma.includes(A)) {
	  { prove(2*index,new Sequent(Gamma.add(B),G),sc); }
	}
      }
      break;    
    }

  }


  /** The initial success continuation. 
    * Suspends the thread when a proof is found. 
    */
  public void initial_sc()  {  
    once = true;
    ProofDisplay p = new ProofDisplay(proof);
    frames.addElement(p);       // keep a record for later disposal
    try {                       // suspend the proof search, 
    suspend(); }           // it might be resumed later on  by the user
    catch(SecurityException sec_exc)
      { /* this catch is neccessary for Netscape 3.0 (Linux) */ }
  }  
  
}