import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import javax.swing.*;
import javax.swing.border.*;

public class LogicEquivApp extends JApplet {
  boolean isStandalone = false;

  Proposition currentProp;
  boolean applyingEquiv;
  Box NorthPanel = new Box(BoxLayout.Y_AXIS);  // NORTH

  String []defaultChoices={"",
         "I want to enter my own",
         "T",
         "F",
         "("+Connectives.NEGATION+"A)",
         "(A"+Connectives.AND+"B)",
         "(T"+Connectives.AND+"B)",
         "(A"+Connectives.AND+"F)",
         "(A"+Connectives.OR+"B)",
         "(C"+Connectives.AND+"(A"+Connectives.OR+"B))",
         "(C"+Connectives.OR+"(A"+Connectives.AND+"B))",
         "(F"+Connectives.OR+"A)",
         "(A"+Connectives.OR+"T)",
         "(A"+Connectives.XOR+"B)",
         "(A"+Connectives.CONDITIONAL+"B)",
         "(A"+Connectives.BICONDITIONAL+"B)",
         "((A"+Connectives.OR+"B)"+Connectives.XOR+"(C"+Connectives.OR+"D))",
         };


  JPanel PropChooser=new JPanel(new FlowLayout());
  JComboBox ComboBoxInput = new JComboBox(defaultChoices);   // for PropChooser
  JButton UseIt=new JButton("Use It");

  JPanel PropEdit = new JPanel(new GridLayout(2,1,1,1));
  JLabel P=new JLabel("P=");
  JPanel PP=new JPanel();
  JTextField PropInField=new JTextField(24);  // for PropEdit
  JPanel SymbolPanel = new JPanel(new GridLayout(1,12,2,2));  //for PropEdit

  JPanel EquivChooser = new JPanel(new FlowLayout());

  JPanel WorkingProp=new JPanel(new FlowLayout());
  JLabel WorkLabel=new JLabel("Current:");
  JTextField WorkArea=new JTextField(40);

  JPanel CenterPane = new JPanel();  // CENTER
  ProofTable theTable=new ProofTable("");

  JPanel Bottom=new JPanel(new FlowLayout());
  JTextArea Message=new JTextArea("",2,45);

  JPanel OutputPanel= new JPanel();           // for CENTER

  JComboBox EquivBox=new JComboBox(Proposition.EquivList);

  String []ReverseList={"=>","<="};
  JComboBox ReverseBox=new JComboBox(ReverseList);

  JButton ApplyEquiv= new JButton("Apply Equivalence");
  JButton BackUp= new JButton("Undo Last Step");

  JButton AndButton= new JButton(""+Connectives.AND);           // for WEST
  JButton OrButton= new JButton(""+Connectives.OR);            // for WEST
  JButton XorButton= new JButton(""+Connectives.XOR);           // for WEST
  JButton NegationButton= new JButton(""+Connectives.NEGATION);      // for WEST
  JButton ConditionalButton= new JButton(""+Connectives.CONDITIONAL);   // for WEST
  JButton BiconditionalButton= new JButton(""+Connectives.BICONDITIONAL); // for WEST

  /**Get a parameter value*/
  public String getParameter(String key, String def) {
    return isStandalone ? System.getProperty(key, def) :
      (getParameter(key) != null ? getParameter(key) : def);
  }

  /**Construct the applet*/
  public LogicEquivApp() {
  }
  /**Initialize the applet*/
  public void init() {
    try { jbInit(); }
    catch(Exception e) { e.printStackTrace();
    }
  }
  /**Component initialization*/
  private void jbInit() throws Exception {
    this.setSize(new Dimension(640,550));

    ComboBoxInput.setBackground(Color.white);
    ComboBoxInput.setBorder(BorderFactory.createLoweredBevelBorder());
    ComboBoxInput.setEditable(false);

    PropChooser.add(ComboBoxInput,null);
    PropChooser.add(UseIt,null);
    UseIt.setEnabled(false);

    SymbolPanel.add(AndButton,null);
    SymbolPanel.add(OrButton,null);
    SymbolPanel.add(XorButton,null);
    SymbolPanel.add(NegationButton,null);
    SymbolPanel.add(ConditionalButton,null);
    SymbolPanel.add(BiconditionalButton,null);
    PP.add(P,null);
    PP.add(PropInField,null);
    PropEdit.add(PP,null);
    PropEdit.add(SymbolPanel,null);
    setPropEditEnabled(false);

    PropChooser.add(PropEdit);
    NorthPanel.add(PropChooser, null);

    EquivChooser.add(EquivBox, null);
    EquivChooser.add(ReverseBox, null);
    EquivChooser.add(ApplyEquiv, null);
    EquivChooser.add(BackUp, null);
    setEquivApplyEnabled(false);

    NorthPanel.add(EquivChooser, null);

    WorkArea.setHorizontalAlignment(JTextField.CENTER);
    WorkArea.setEditable(false); // Nope.
    WorkArea.setSelectionColor(new Color(250,100,100));
    WorkArea.setFont(new Font("Lucida Sans",WorkArea.getFont().getStyle(),14));
    WorkingProp.add(WorkLabel,null);
    WorkingProp.add(WorkArea,null);
    NorthPanel.add(WorkingProp, null);

    CenterPane.add(theTable);
    CenterPane.setPreferredSize(new Dimension(630,400));
    CenterPane.setMinimumSize(new Dimension(630,400));
    CenterPane.setBorder(BorderFactory.createTitledBorder(
          BorderFactory.createEtchedBorder(),"",
          TitledBorder.CENTER, TitledBorder.ABOVE_TOP));

    theTable.setVisible(false);

    Bottom.add(Message,null);
    
    this.getContentPane().add(NorthPanel, BorderLayout.NORTH);
    this.getContentPane().add(CenterPane, BorderLayout.CENTER);
    this.getContentPane().add(Bottom, BorderLayout.SOUTH);

    ComboBoxInput.addActionListener(new ActionListener() {
             public void actionPerformed(ActionEvent e) {
             ComboBoxInput_actionPerformed(e); } });
    UseIt.addActionListener(new ActionListener() {
            public void actionPerformed(ActionEvent e) {
            UseIt_actionPerformed(e); } });
    PropInField.addActionListener(new ActionListener() {
            public void actionPerformed(ActionEvent e) {
            PropInField_actionPerformed(e); } });
    AndButton.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
           AddSymbol(Connectives.AND);
      }});
    OrButton.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
           AddSymbol(Connectives.OR);
      }});
    XorButton.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
           AddSymbol(Connectives.XOR);
      }});
    NegationButton.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
           AddSymbol(Connectives.NEGATION);
      }});
    ConditionalButton.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
           AddSymbol(Connectives.CONDITIONAL);
      }});
    BiconditionalButton.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
           AddSymbol(Connectives.BICONDITIONAL);
      }});
    EquivBox.addActionListener(new ActionListener() {
        public void actionPerformed(ActionEvent e) {
        EquivBox_actionPerformed(e); } });
    ReverseBox.addActionListener(new ActionListener() {
        public void actionPerformed(ActionEvent e) {
        ReverseBox_actionPerformed(e); } });
    ApplyEquiv.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
        ApplyEquiv_actionPerformed(e); } });
    BackUp.addActionListener(new ActionListener() {
      public void actionPerformed(ActionEvent e) {
        BackUp_actionPerformed(e); } });

    Message.setBorder(BorderFactory.createEtchedBorder());
    Message.setEditable(false);
    Message.setRows(2);
    Message.setLineWrap(true);
    Message.setWrapStyleWord(true);
    Message.setText("Select a proposition and hit the 'Use It' key "+
                "to start applying equivalences.");

    applyingEquiv=false;
    FontFixer.setUIFont("Lucida Sans");
    SwingUtilities.updateComponentTreeUI(this);

  }

  void AddSymbol(char A) {
            PropInField.replaceSelection(A+"");
            PropInField.requestFocus();
  }

  void setPropEditEnabled(boolean V) {
    AndButton.setEnabled(V);
    OrButton.setEnabled(V);
    XorButton.setEnabled(V);
    NegationButton.setEnabled(V);
    ConditionalButton.setEnabled(V);
    BiconditionalButton.setEnabled(V);
    PropInField.setEnabled(V);
  }
  void setEquivApplyEnabled(boolean V) {
    EquivBox.setEnabled(V);
    ReverseBox.setEnabled(V);
    ApplyEquiv.setEnabled(V);
    WorkArea.setEnabled(V);
    if(V==false)
      BackUp.setEnabled(V);
  }

  void PropInField_actionPerformed(ActionEvent e) {
       String prop=Connectives.toUnicode(PropInField.getText());
       PropInField.setText(prop);
       Proposition test=new Proposition(prop);
       Message.setText(prop);
       if(test.getProp().equals(prop))  {
           Message.append(" is a valid proposition");
           Message.setBackground(Color.white);
           if(applyingEquiv==false) {
             ComboBoxInput.addItem(PropInField.getText());
             ComboBoxInput.setSelectedItem(PropInField.getText());
           }
           else {
               setEquivApplyEnabled(true);
               setPropEditEnabled(false);
               if(EquivBox.getSelectedIndex()==2 ||
                  EquivBox.getSelectedIndex()==15) {
                  Message.append("\nHiglight the desired 'T'"
                  +" and press the 'Apply Equivalence' key "
                  +" to apply the equivalence with P.");
               }
               else if(EquivBox.getSelectedIndex()==3 ||
                  EquivBox.getSelectedIndex()==16) {
                  Message.append("\nHiglight the desired 'F'"
                  +" and press the 'Apply Equivalence' key "
                  +" to apply the equivalence with P.");
              }
           }
       }
       else {
           Message.append(" is NOT a valid proposition");
           Message.setBackground(Color.red);
           }
  }

  void ComboBoxInput_actionPerformed(ActionEvent e) {
       WorkArea.setText("");
       setPropEditEnabled(false);
       setEquivApplyEnabled(false);
       if(ComboBoxInput.getSelectedIndex()==1) {
          UseIt.setEnabled(false);
          setPropEditEnabled(true);
          PropInField.requestFocus();
          Message.setText("Enter the new proposition P in the area above.  "+
                       "Press the ENTER key when you are done.");
          Message.setBackground(Color.yellow);
          return;
       }
       if(ComboBoxInput.getSelectedIndex()==0) {
           UseIt.setEnabled(false);
           return;
       }
       String prop=(String) ComboBoxInput.getSelectedItem();

       theTable.setVisible(false);
       UseIt.setEnabled(true);
       Message.setText("Press 'Use it' to start applying equivalences.");
       Message.setBackground(Color.green);
       applyingEquiv=false;
  }

  void UseIt_actionPerformed(ActionEvent e) {
       if(UseIt.getText().equals("Use It")) {
           String S=(String) ComboBoxInput.getSelectedItem();
           currentProp=new Proposition(S);
           theTable.initTable(S);
           theTable.setVisible(true);
           setEquivApplyEnabled(true);
           WorkArea.setText(S);
           CenterPane.validate();
           UseIt.setText("Restart");
           ComboBoxInput.setEnabled(false);
           Message.setText("Select an equivalence to apply."+
               " Then highlight the portion of the proposition you wish to"+
               " apply it to.");
       }
       else {
           UseIt.setText("Use It");
           ComboBoxInput.setEnabled(true);
           setEquivApplyEnabled(false);
           theTable.setVisible(false);
           Message.setText("Select a proposition and hit the 'Use It' "+
               "key to start applying equivalences.");
       }
  }

  void NeedInput() {
       int EQ=EquivBox.getSelectedIndex()*2+ReverseBox.getSelectedIndex();
       if(EQ==Proposition.OR_DOMIN_R || EQ==Proposition.AND_DOMIN_R || 
          EQ==Proposition.P_OR_NOT_P_R || EQ==Proposition.P_AND_NOT_P_R) {
         applyingEquiv=true;
         setPropEditEnabled(true);
         Message.setText("Enter the proposition 'P' above.\n");
         Message.append("When you are done, be sure to hit the ENTER key");
         Message.setBackground(Color.yellow);
         setEquivApplyEnabled(false);
         PropInField.setText("");
         PropInField.requestFocus();
       }
       else {
         applyingEquiv=false;
         setPropEditEnabled(false);
         setEquivApplyEnabled(true);
      }
   }
  void EquivBox_actionPerformed(ActionEvent e) {
       ReverseBox.setSelectedIndex(0);
       NeedInput();
  }

  void ReverseBox_actionPerformed(ActionEvent e) {
       NeedInput();
  }

  void ApplyEquiv_actionPerformed(ActionEvent e) {
       int f=WorkArea.getSelectionStart();
       int l=WorkArea.getSelectionEnd();
       String Orig=WorkArea.getText();
       if(l==f && f==Orig.length()) {
          f=0;
          Message.setText("No text marked. Attempting to apply it to the"+
                          " entire proposition.\n");
       }
       else {
          Message.setText("");
       }
       int EQ=EquivBox.getSelectedIndex()*2+ReverseBox.getSelectedIndex();
       int result=Proposition.DNA;
       if(EQ==Proposition.OR_DOMIN_R || EQ==Proposition.AND_DOMIN_R || 
          EQ==Proposition.P_OR_NOT_P_R || EQ==Proposition.P_AND_NOT_P_R) {
          String S=PropInField.getText();
          result=currentProp.applyEquivalence(f,l,EQ,S);
       }
       else 
          result=currentProp.applyEquivalence(f,l,EQ);
       if(result==Proposition.OK) {
           String[]newRow=new String[2];
           newRow[0]="<=> "+currentProp.getProp();
           newRow[1]=Proposition.EquivList2[EQ];
           theTable.addRow(newRow);
           String N=Orig.substring(0,f)+"@"+Orig.substring(f,l)
                     +"@"+Orig.substring(l,Orig.length());
           if(theTable.rowCount()!=2)
             N="<=> "+N;
           theTable.updateCell(N,theTable.rowCount()-2,0);
           WorkArea.setText(currentProp.getProp());
           BackUp.setEnabled(true);
           Message.append(Proposition.EquivNames[EQ/2]+" applied to "
                   +Orig.substring(f,l));
           if(EQ%2==1) Message.append(" in the reverse direction");
           Message.setBackground(Color.green);
           }
       else if(result==Proposition.INVALID_PROP) {
           Message.append("The marked area is not a valid proposition.");
           Message.setBackground(Color.red);
          }
       else {
           Message.append(Proposition.EquivNames[EQ/2]+
                         " does not apply to that proposition.");
           Message.setBackground(Color.red);
   
       }
       setPropEditEnabled(false);
       WorkArea.setSelectionStart(WorkArea.getText().length());
       WorkArea.setSelectionEnd(WorkArea.getText().length());
  }
  void BackUp_actionPerformed(ActionEvent e) {
       String np=theTable.deleteRow();
       currentProp.setProp(np);
       WorkArea.setText(currentProp.getProp());
       Message.setText("The last step has been undone.");
       Message.setBackground(Color.green);
       if (theTable.rowCount()<2) BackUp.setEnabled(false);
  }
}