package G4ip;

import java.util.*;
import pizza.lang.Pair;
import G4ip.Form.*;
import G4ip.Token.*;

public class Token {
  public static final int AND = 0;
  public static final int OR  = 1;
  public static final int IMP = 2;
  public static final int EQU = 3;

  /** End-of-Input */
  public case EOI();             // end-of-input
  public case LPAREN();
  public case RPAREN();
  public case ID(String id);
  public case FALSE();
  public case BINOP(int op);     // binary operation
  public case COMMA();
}

/** A left-to-right, rightmost-derivation parser.<p> 
  * The following grammar is implemented:<p>
  * <dl>
  * <dd><u>Formula</u> ::= <u>Id</u>                             </dd>
  * <dd><code>| false</code>                                     </dd>
  * <dd><code>|</code> ( <u>Formula</u> )                        </dd>         
  * <dd><code>|</code> <u>Formula</u> <u>Binop</u> <u>Formula</u></dd>  
  * </dl><p>
  * <dl>
  * <dd><u>Id</u> is a string of lower case letters</dd>
  * </dl><p>
  * <dl>
  * <dd><u>Binop</u> is either <code>&, v, -></code> or <code><-></code></dd>
  * </dl><p>
  * <dl>
  * <dd><u>FormulaList</u> ::=  <em>empty</em></dd>
  * <dd><code>|</code> [ <u>FormulaList</u> ,]* <u>Formula</u></dd>
  * <dl><p>
  * The parser uses a stack where two actions are performed:
  * <dl>
  * <dd><b>shift</b> moves the next token to the top of the stack (getNextToken)</dd>
  * <dd><b>reduce</b> chooses a grammar rule, X -> A B C; pops A, B, C from the 
  *                   top of the stack and pushes X onto the stack  
  * </dl>
  * @author      Christian Urban
  */       
public class Parser {
  final Pair<String,Token> keywords[] = 
          { new Pair("(",    LPAREN()),
	    new Pair(")",    RPAREN()),
	    new Pair(",",    COMMA()),
	    new Pair("&",    BINOP(Token.AND)),
	    new Pair("v ",   BINOP(Token.OR)),
	    new Pair("->",   BINOP(Token.IMP)),
            new Pair("<->",  BINOP(Token.EQU)),
	    new Pair("false",FALSE()) };
  String in;     // string to be parsed
  int index;     // position of the current input
  Stack stack;   // stack for the left-to-right parser 'LR(0)'
  
  public Parser(String init_in){
    index = 0;
    in = init_in;
    stack = new Stack();
  }

  /** tokens are: identifiers<code>( ) , & v -> <-> false</code> 
    *             and <code>EOI</code> <em>(end of input)</em> 
    */
  public Token getNextToken() throws Exception {
    while ( index < in.length() && Character.isSpace(in.charAt(index)) ) 
          { index++; }                                //delete  white-spaces  
    if (index == in.length()) { return EOI(); }       //end-of-string  
    for (int i=0;i<keywords.length;i++)               //keywords
      { if (in.startsWith(keywords[i].fst,index)) {
	   index=index+keywords[i].fst.length();
	   return keywords[i].snd;
        }
      }
    if (Character.isLowerCase(in.charAt(index)) || Character.isDigit(in.charAt(index))) 
      {     //reads identifiers
      String s = ""; 
      while ( index < in.length() && 
              (    Character.isLowerCase(in.charAt(index))
                || Character.isDigit(in.charAt(index))
              ) 
            ) 
	{ s=s.concat(in.substring(index,index+1)); 
          index++;
        }
      return ID(s);
    }
    throw new Exception("Syntax error at: '" + in.charAt(index)  + "'");   
               // no match at all: probably an unknown character
    return null;
  }

  /** Implements the grammar rules. */
  public void reduce()
    { boolean again = false;
      /*   ID  -> Atm(string)  */
      if (stack.size() > 0 && 
	 (stack.elementAt(stack.size()-1) instanceof ID))
	    { ID id = (ID)stack.pop();
	      stack.push(Atm(id.id));
	      again = true;
	    } 
      /*  FALSE -> False()   */
      if (stack.size() > 0 && 
	  (stack.elementAt(stack.size()-1) instanceof FALSE))
	    { stack.pop();
	      stack.push(False());
	      again = true;
	    } 
      /*   ( Formula )  -> Formula  */ 
      if (stack.size() > 2 &&
	  (stack.elementAt(stack.size()-3) instanceof LPAREN) &&
	  (stack.elementAt(stack.size()-2) instanceof Form)   &&
	  (stack.elementAt(stack.size()-1) instanceof RPAREN))
	    {  stack.pop();
               Form form = (Form)stack.pop(); 
               stack.pop();
               stack.push(form);
               again = true;
            }   
      /*   Formula BINOP Formula  -> Formula  */
      if (stack.size() > 2 &&
	  (stack.elementAt(stack.size()-3) instanceof Form)  &&
	  (stack.elementAt(stack.size()-2) instanceof BINOP) &&
	  (stack.elementAt(stack.size()-1) instanceof Form))
	    {  Form  c2 = (Form)stack.pop();
               BINOP op = (BINOP)stack.pop();
               Form  c1 = (Form)stack.pop(); 
               switch(op.op) {
	       case Token.AND: stack.push(new And(c1,c2)); again = true;break;
               case Token.OR:  stack.push(new Or(c1,c2));  again = true;break; 
	       case Token.IMP: stack.push(new Imp(c1,c2)); again = true;break;
               case Token.EQU: stack.push(new And(Imp(c1,c2),Imp(c2,c1))); again = true;break;
	       }
            }  
      if (again == true) { reduce(); }  // do as many "reduces" as possible 
    }

  /** parses a single formula
    */
  public Form parseFormula() throws Exception {
    Token tok;
    while (!((tok = getNextToken()) instanceof EOI)) {
      stack.push(tok);
      reduce();
    }
    if (stack.size() == 1 &&
       (stack.elementAt(stack.size()-1) instanceof Form))
       { return (Form)stack.pop(); } 
    else throw new Exception("Grammar error");
    return null;  
  }

  /** parses a list of formulae separated by commas
    */
  public Context parseFormulae() throws Exception {
    Token tok;
    Context erg = new Context();
    while (!((tok = getNextToken()) instanceof EOI)) {
      stack.push(tok);
      reduce();
    }
    if (stack.empty()) return erg;  // LHS can be empty  !!
    stack.push(new COMMA());
    for(int i=0;i<stack.size()-1;i=i+2){
      if (stack.elementAt(i)  instanceof Form)
	{ erg.addElement(stack.elementAt(i));
	}  else throw new Exception("Grammar error");
      if (stack.elementAt(i+1) instanceof COMMA)
        {} else throw new Exception("Grammar error");
    }
    return erg;
  }

}