/* Generated By:JavaCC: Do not edit this line. CCParser.java */
package us.softoption.parser;

import static us.softoption.infrastructure.Symbols.chNeg;
import static us.softoption.infrastructure.Symbols.chSlash;
import static us.softoption.infrastructure.Symbols.strEmptySet;
import static us.softoption.infrastructure.Symbols.strExiquant;
import static us.softoption.infrastructure.Symbols.strMemberOf;
import static us.softoption.infrastructure.Symbols.strNotMemberOf;
import static us.softoption.infrastructure.Symbols.strUniquant;

import java.io.Reader;
import java.util.ArrayList;


public class CCParser implements CCParserConstants {

static boolean ILLFORMED=false;
static boolean WELLFORMED=true;
String strUnique= "\u2203!";// needs to be same as token UNIQUE
byte fParseType=0; //for slight differences in grammar
public static byte DEFAULT=0;
public static byte BRACKETFREEQUANTS=1;
public static byte BRACKETEDPREDS=2;

public CCParser(Reader r, byte type)
{
  this(r);
  fParseType=type;
}

public void reInit(Reader r, byte type)
{
  this.ReInit(r);
  fParseType=type;
}

  /** Main entry point. */
  public static void main(String args[]) throws ParseException {

java.io.StringReader sr = new java.io.StringReader( "c" );
java.io.Reader r = new java.io.BufferedReader( sr );




    CCParser parser = new CCParser(r);
    TFormula term=null;
    term=parser.term();

    System.out.println(term.fInfo);
  }

boolean isAndStr(String connective)
{
return
(connective.equals("\u2227")||
  connective.equals("&")||
  connective.equals("."));
}

boolean isEquivStr(String connective)
{
return
(connective.equals("\u2261")||
  connective.equals("\u2194"));
}

boolean isImplicStr(String connective)
{
return
(connective.equals("\u2283")||
  connective.equals("\u2192"));
}

boolean isMemberOfStr(String connective)
{
return
(connective.equals("\u2208")||
  connective.equals("\u03b5")||
  connective.equals("\u0395"));
}

boolean isNegationStr(String connective)
{
return
(connective.equals("\u223c")||
  connective.equals("\u00ac")||
  connective.equals("~")||
  connective.equals("\u02dc"));
}

boolean isOrStr(String connective)
{
return
(connective.equals("\u2228"));
}

/*Keep next in Synch with tokens and parser writing routines*/
public String toInternalForm(String connective){
/*we have only one internal 'canonical' form for each connective but translate
back and forth when reading or writing*/

if (isAndStr(connective))
 return
     "\u2227";
if (isEquivStr(connective))      //accepts variations
 return
     "\u2261";                   //standard form
if (isImplicStr(connective))
 return
     "\u2283";
if (isNegationStr(connective))
 return
     "\u223c";

if (isOrStr(connective))         //accepts variations
    return
     "\u2228";    //standard form


if (isMemberOfStr(connective))         //accepts variations
          return
          "\u2208";    //standard form


  return
      connective;
       }

/****************** formulas ******************************/
  final public TFormula wffCheck() throws ParseException {
 TFormula wff;
    wff=top();
    if (wff==null)
        {if (true) return
                null;}
    label_1:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case 0:
        ;
        break;
      default:
        jj_la1[0] = jj_gen;
        break label_1;
      }
      jj_consume_token(0);
    {if (true) return
        wff;}
    }
   {if (true) throw new ParseException("Unwanted extra characters on end.");}
     {if (true) return
        null;}   //extra characters following

    throw new Error("Missing return statement in function");
  }

  final public TFormula wffCheckWithValuation(ArrayList<TFormula> valuation) throws ParseException {
 TFormula wff;
    wff=top();
    if (wff==null)
        {if (true) return
                null;}
    label_2:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case 0:
      case LEFTSQUARE:
        ;
        break;
      default:
        jj_la1[1] = jj_gen;
        break label_2;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case 0:
        jj_consume_token(0);
    {if (true) return
        wff;}
        break;
      case LEFTSQUARE:
        jj_consume_token(LEFTSQUARE);
      System.out.println("Interpretation entered");
     if (getValuation(valuation))
        {if (true) return
                wff;}
    else
        {if (true) return
                null;}
        break;
      default:
        jj_la1[2] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
   {if (true) throw new ParseException("Unwanted extra characters on end.");}
     {if (true) return
        null;}   //extra characters following

    throw new Error("Missing return statement in function");
  }

  final public boolean valuationHelper(ArrayList<TFormula> valuation) throws ParseException {
 String term,vari;
  Token t,v;
    t = jj_consume_token(FUNCTOR);
         term=toInternalForm(t.image);
    jj_consume_token(SLASH);
    v = jj_consume_token(VARIABLE);
         vari=toInternalForm(v.image);
           TFormula aFormula=new TFormula(TFormula.kons,
                                                term+String.valueOf(chSlash)+vari,null,null);
                valuation.add(aFormula);
    label_3:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[3] = jj_gen;
        break label_3;
      }
      jj_consume_token(COMMA);
    }
    label_4:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RIGHTSQUARE:
        ;
        break;
      default:
        jj_la1[4] = jj_gen;
        break label_4;
      }
      jj_consume_token(RIGHTSQUARE);
                         {if (true) return WELLFORMED;}
    }
         {if (true) return
                valuationHelper(valuation);}
    throw new Error("Missing return statement in function");
  }

  final public boolean getValuation(ArrayList<TFormula> valuation) throws ParseException {
   String term,vari;
  Token t,v;
      if (valuation==null)
      {if (true) return
        (!WELLFORMED);}

    valuation.clear();
    {if (true) return
     valuationHelper(valuation);}
    throw new Error("Missing return statement in function");
  }

  final private TFormula top() throws ParseException {
 TFormula tertiary,top;
Token t;
   tertiary=tertiary();
        if (tertiary==null)    //illformed
        {if (true) return
                null;}
        Token nextToken=getToken(1); // we need to look ahead 1 without consuming
                                                            // can be terms following
        if (nextToken!=null&&
                (
                  (nextToken.kind==EQUIV)
                ))
                {
                  t=getNextToken();         //advance to connective
                  String cachedInfo=toInternalForm(t.image);
                  top=top();
                  if (top==null)    //illformed
                        {if (true) return
                                null;}

                  {if (true) return
                  new TFormula(TFormula.binary,
                        cachedInfo,tertiary,top);}
                }

  {
  {if (true) return
        tertiary;}  // no connective
 }
    throw new Error("Missing return statement in function");
  }

  final public TFormula tertiary() throws ParseException {
 TFormula secondary,tertiary;
Token t;
   secondary=secondary();
        if (secondary==null)    //illformed
        {if (true) return
                null;}
        Token nextToken=getToken(1); // we need to look ahead 1 without consuming
                                                            // can be terms following
        if (nextToken!=null&&
                (
                  (nextToken.kind==AND)||
                  (nextToken.kind==INFIX2)||  // "." for and is also "." for multiply
                  (nextToken.kind==OR)||
                  (nextToken.kind==IMPLIC)
                ))
                {
                  t=getNextToken();         //advance to connective
                  String cachedInfo=toInternalForm(t.image);
                  tertiary=tertiary();
                  if (tertiary==null)    //illformed
                        {if (true) return
                                null;}
                  {if (true) return
                  new TFormula(TFormula.binary,
                        cachedInfo,secondary,tertiary);}
                }
  {
  {if (true) return
        secondary;}  // no connective
 }
    throw new Error("Missing return statement in function");
  }

/*********************** SECONDARY *****************************/
  final public TFormula secondary() throws ParseException {
    Token oneAhead=getToken(1);
Token twoAhead=getToken(2);
Token threeAhead=getToken(3);

if (oneAhead.kind==LEFTPAREN)
{
  if (twoAhead.kind!=EXIQUANT&&
                twoAhead.kind!=UNIQUE&&
                twoAhead.kind!=UNIQUANT&&
                !((twoAhead.kind==VARIABLE)&&((threeAhead.kind==RIGHTPAREN)||
                                              (threeAhead.kind==COLON)))
  )
  {if (true) return
     awkwardCase();}
}
  if ((fParseType&BRACKETFREEQUANTS)!=0)
    {if (true) return
          secondaryTypeOne();}
  else
        {if (true) return
          secondaryTypeZero();}
    throw new Error("Missing return statement in function");
  }

  final public TFormula secondaryTypeZero() throws ParseException {
 TFormula newnode,term,rLink;
Token t=null,termToken=null,q,c=null,v;
    label_5:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case NEGATION:
      case MODALPOSSIBLE:
      case MODALNECESSARY:
      case MODALKAPPA:
      case MODALRHO:
      case LEFTPAREN:
        ;
        break;
      default:
        jj_la1[5] = jj_gen;
        break label_5;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case NEGATION:
      case MODALPOSSIBLE:
      case MODALNECESSARY:
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case NEGATION:
          t = jj_consume_token(NEGATION);
          break;
        case MODALPOSSIBLE:
          t = jj_consume_token(MODALPOSSIBLE);
          break;
        case MODALNECESSARY:
          t = jj_consume_token(MODALNECESSARY);
          break;
        default:
          jj_la1[6] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
  rLink=secondary();
  if (rLink!=null){
    newnode= new TFormula(TFormula.unary,toInternalForm(t.image),null,rLink);
    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
        break;
      case MODALKAPPA:
        t = jj_consume_token(MODALKAPPA);
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case FUNCTOR:
          termToken = jj_consume_token(FUNCTOR);
           term =new TFormula(TFormula.functor, toInternalForm(termToken.image), null, null);
          break;
        case VARIABLE:
          termToken = jj_consume_token(VARIABLE);
           term =new TFormula(TFormula.variable, toInternalForm(termToken.image), null, null);
          break;
        default:
          jj_la1[7] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
        rLink=secondary();
  if (rLink!=null){
    newnode= new TFormula(TFormula.modalKappa,toInternalForm(t.image),term,rLink);
    {if (true) return
                newnode;}
        }
        else

                {if (true) return
                   null;}
        break;
      case MODALRHO:
        t = jj_consume_token(MODALRHO);
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case FUNCTOR:
          termToken = jj_consume_token(FUNCTOR);
           term =new TFormula(TFormula.functor, toInternalForm(termToken.image), null, null);
          break;
        case VARIABLE:
          termToken = jj_consume_token(VARIABLE);
           term =new TFormula(TFormula.variable, toInternalForm(termToken.image), null, null);
          break;
        default:
          jj_la1[8] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
 rLink=secondary();
  if (rLink!=null){
    newnode= new TFormula(TFormula.modalRho,toInternalForm(t.image),term,rLink);
    {if (true) return
                newnode;}
        }
        else

                {if (true) return
                   null;}
        break;
      default:
        jj_la1[10] = jj_gen;
        if (jj_2_1(2)) {
          jj_consume_token(LEFTPAREN);
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case EXIQUANT:
            q = jj_consume_token(EXIQUANT);
            break;
          case UNIQUE:
            q = jj_consume_token(UNIQUE);
            break;
          default:
            jj_la1[9] = jj_gen;
            jj_consume_token(-1);
            throw new ParseException();
          }
          t = jj_consume_token(VARIABLE);
     {if (true) return
        exiQuantHelper(q,t);}
        } else if (jj_2_2(2)) {
          jj_consume_token(LEFTPAREN);
          q = jj_consume_token(UNIQUANT);
          t = jj_consume_token(VARIABLE);
   {if (true) return
        uniQuantHelper(q,t);}
        } else if (jj_2_3(3)) {
          jj_consume_token(LEFTPAREN);
          v = jj_consume_token(VARIABLE);
          jj_consume_token(RIGHTPAREN);
 {if (true) return
        copiQuantHelper(v, c);}
        } else if (jj_2_4(3)) {
          jj_consume_token(LEFTPAREN);
          v = jj_consume_token(VARIABLE);
          jj_consume_token(COLON);
 {if (true) return
        copiQuantHelperColon(v, c);}
        } else {
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case LEFTPAREN:
            jj_consume_token(LEFTPAREN);
 TFormula wff;
Token next;
int result =testBracketContents();

if (result==1)  // we know it is a wff (must end with right paren)
        {
  wff=top(); // now parse original;
                 next= getNextToken();
                 if(next.kind==RIGHTPAREN) //closing bracket
                        {if (true) return
                        wff;}
                 else
                        {if (true) return
                         null;}
        }

if (result==2) // we know it is an infix predicate starting with
                           // a bracketed term eg (1+2)=3
                           // now! the term must end with bracket, but the whole lot not
        {
        boolean skipBracket=true;
    {if (true) return
                infixPredicate(skipBracket);} // now parse original;
        }
if (result==0)
        {if (true) return
                null;}
            break;
          default:
            jj_la1[11] = jj_gen;
            jj_consume_token(-1);
            throw new ParseException();
          }
        }
      }
    }
  {if (true) return
        primary();}
    throw new Error("Missing return statement in function");
  }

/******************/
  final public TFormula secondaryTypeOne() throws ParseException {
 TFormula newnode,term,rLink;
Token t=null,termToken=null,q,c=null,v;
    label_6:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case NEGATION:
      case MODALPOSSIBLE:
      case MODALNECESSARY:
      case MODALKAPPA:
      case MODALRHO:
      case UNIQUANT:
      case EXIQUANT:
      case UNIQUE:
      case LEFTPAREN:
        ;
        break;
      default:
        jj_la1[12] = jj_gen;
        break label_6;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case NEGATION:
      case MODALPOSSIBLE:
      case MODALNECESSARY:
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case NEGATION:
          t = jj_consume_token(NEGATION);
          break;
        case MODALPOSSIBLE:
          t = jj_consume_token(MODALPOSSIBLE);
          break;
        case MODALNECESSARY:
          t = jj_consume_token(MODALNECESSARY);
          break;
        default:
          jj_la1[13] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
  rLink=secondary();
  if (rLink!=null){
    newnode= new TFormula(TFormula.unary,toInternalForm(t.image),null,rLink);
    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
        break;
      case MODALKAPPA:
        t = jj_consume_token(MODALKAPPA);
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case FUNCTOR:
          termToken = jj_consume_token(FUNCTOR);
           term =new TFormula(TFormula.functor, toInternalForm(termToken.image), null, null);
          break;
        case VARIABLE:
          termToken = jj_consume_token(VARIABLE);
           term =new TFormula(TFormula.variable, toInternalForm(termToken.image), null, null);
          break;
        default:
          jj_la1[14] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
        rLink=secondary();
  if (rLink!=null){
    newnode= new TFormula(TFormula.modalKappa,toInternalForm(t.image),term,rLink);
    {if (true) return
                newnode;}
        }
        else

                {if (true) return
                   null;}
        break;
      case MODALRHO:
        t = jj_consume_token(MODALRHO);
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case FUNCTOR:
          termToken = jj_consume_token(FUNCTOR);
           term =new TFormula(TFormula.functor, toInternalForm(termToken.image), null, null);
          break;
        case VARIABLE:
          termToken = jj_consume_token(VARIABLE);
           term =new TFormula(TFormula.variable, toInternalForm(termToken.image), null, null);
          break;
        default:
          jj_la1[15] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
 rLink=secondary();
  if (rLink!=null){
    newnode= new TFormula(TFormula.modalRho,toInternalForm(t.image),term,rLink);
    {if (true) return
                newnode;}
        }
        else

                {if (true) return
                   null;}
        break;
      case EXIQUANT:
      case UNIQUE:
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case EXIQUANT:
          t = jj_consume_token(EXIQUANT);
          break;
        case UNIQUE:
          t = jj_consume_token(UNIQUE);
          break;
        default:
          jj_la1[16] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
        v = jj_consume_token(VARIABLE);
     {if (true) return
        exiQuantHelperTypeOne(t,v);}
        break;
      case UNIQUANT:
        t = jj_consume_token(UNIQUANT);
        v = jj_consume_token(VARIABLE);
     {if (true) return
        uniQuantHelperTypeOne(t,v);}
        break;
      case LEFTPAREN:
        jj_consume_token(LEFTPAREN);
 TFormula wff;
Token next;
int result =testBracketContents();

if (result==1)  // we know it is a wff (must end with right paren)
        {
  wff=top(); // now parse original;
                 next= getNextToken();
                 if(next.kind==RIGHTPAREN) //closing bracket
                        {if (true) return
                        wff;}
                 else
                        {if (true) return
                         null;}
        }

if (result==2) // we know it is an infix predicate starting with
                           // a bracketed term eg (1+2)=3
                           // now! the term must end with bracket, but the whole lot not
        {
        boolean skipBracket=true;
    {if (true) return
                infixPredicate(skipBracket);} // now parse original;
        }
if (result==0)
        {if (true) return
                null;}
        break;
      default:
        jj_la1[17] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
  {if (true) return
        primary();}
    throw new Error("Missing return statement in function");
  }

/*****************/
  final public TFormula copiQuantHelperColon(Token v, Token colon) throws ParseException {
 Token type;
boolean typed=true;
TFormula typeNode=null;
    type = jj_consume_token(FUNCTOR);
 typeNode = new TFormula(TFormula.functor, toInternalForm(type.image), null, null);
    jj_consume_token(RIGHTPAREN);
   {if (true) return
        copiScope(v,colon,typeNode,typed);}
    throw new Error("Missing return statement in function");
  }

  final public TFormula copiQuantHelper(Token v, Token colon) throws ParseException {
TFormula typeNode=null;
boolean typed=true;

{{if (true) return
        copiScope(v,colon,typeNode,!typed);}
}
    throw new Error("Missing return statement in function");
  }

  final public TFormula copiScope(Token v, Token colon,TFormula typeNode, boolean typed) throws ParseException {
 TFormula variable,scope,newnode;
   scope=secondary();
        if (scope!=null){
                variable =new TFormula(TFormula.variable,
                                                                toInternalForm(v.image), null, null);
                if(!typed){
                newnode= new TFormula(TFormula.quantifier,
                                                                strUniquant,
                                                        variable,
                                                        scope);
                }
                else
                {TFormula link = new TFormula(TFormula.kons,  //make a link to variable
                                       "",
                                       variable,
                                       null);
            link.appendToFormulaList(typeNode); //attach type to it
        newnode= new TFormula(TFormula.typedQuantifier, //make root
                                                        strUniquant,
                                                        link,
                                                        scope);
                }

    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula exiQuantHelper(Token q, Token t) throws ParseException {
 Token type;
TFormula newnode,rLink,variable,scope,typeNode=null;
boolean typed=false;

          if ((getToken(1).kind)==COLON){// . peep ahead, typed variable
                getNextToken();  //advance to colon
                type=getNextToken();  //advance to type
            if (type.kind==FUNCTOR){
                        typed=true;
                        typeNode = new TFormula(TFormula.functor, toInternalForm(type.image), null, null);
                        //getNextToken();  // go past functor
                }



         else
         if (type.kind==LEFTCURLY){ //comprehension
            typed=true;
                typeNode =new TFormula(TFormula.comprehension, strEmptySet, null, null);
                if (!termAbstraction(typeNode))
                        {if (true) return
                                null;}  //not a well formed comprehension
        }

                else
                        {if (true) return
                                null;}
          }
    jj_consume_token(RIGHTPAREN);
      scope=secondary();
        if (scope!=null){
                variable =new TFormula(TFormula.variable,
                                                                toInternalForm(t.image), null, null);
                if(!typed){
                newnode= new TFormula(TFormula.quantifier,

                                                                toInternalForm(q.image).equals(strUnique)?
                                                                        "!":strExiquant,
                                                        variable,
                                                        scope);
                }
                else
                {TFormula link = new TFormula(TFormula.kons,  //make a link to variable
                                       "",
                                       variable,
                                       null);
            link.appendToFormulaList(typeNode); //attach type to it
        newnode= new TFormula(TFormula.typedQuantifier, //make root
                                                        toInternalForm(q.image).equals(strUnique)?
                                                                        "!":strExiquant,
                                                        link,
                                                        scope);

                }

    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula exiQuantHelperTypeOne(Token q, Token t) throws ParseException {
 Token type;
TFormula newnode,rLink,variable,scope,typeNode=null;
boolean typed=false;

          if ((getToken(1).kind)==COLON){// . peep ahead, typed variable
                getNextToken();  //advance to colon
                type=getNextToken();  //advance to type
            if (type.kind==FUNCTOR){
                        typed=true;
                        typeNode = new TFormula(TFormula.functor, toInternalForm(type.image), null, null);
                        //getNextToken();  // go past functor
                }


//mfmfmfm Dec 13 09
         else
         if (type.kind==LEFTCURLY){ //comprehension
            typed=true;
                typeNode =new TFormula(TFormula.comprehension, strEmptySet, null, null);
                if (!termAbstraction(typeNode))
                        {if (true) return
                                null;}  //not a well formed comprehension
        }
//mfmfmfm		
                else
                        {if (true) return
                                null;}
          }
      scope=secondary();
        if (scope!=null){
                variable =new TFormula(TFormula.variable,
                                                                toInternalForm(t.image), null, null);
                if(!typed){
                newnode= new TFormula(TFormula.quantifier,

                                                                toInternalForm(q.image).equals(strUnique)?
                                                                        "!":strExiquant,
                                                        variable,
                                                        scope);
                }
                else
                {TFormula link = new TFormula(TFormula.kons,  //make a link to variable
                                       "",
                                       variable,
                                       null);
            link.appendToFormulaList(typeNode); //attach type to it
        newnode= new TFormula(TFormula.typedQuantifier, //make root
                                                        toInternalForm(q.image).equals(strUnique)?
                                                                        "!":strExiquant,
                                                        link,
                                                        scope);

                }

    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula uniQuantHelper(Token q, Token t) throws ParseException {
 Token type;
TFormula newnode,rLink,variable,scope,typeNode=null;
boolean typed=false;

          if ((getToken(1).kind)==COLON){// . peep ahead, typed variable
                getNextToken();  //advance to colon
                type=getNextToken();  //advance to type
            if (type.kind==FUNCTOR){
                        typed=true;
                        typeNode = new TFormula(TFormula.functor, toInternalForm(type.image), null, null);
                        //getNextToken();  // go past functor
                }



//mfmfmfm Dec 13 09
         else
         if (type.kind==LEFTCURLY){ //comprehension
            typed=true;
                typeNode =new TFormula(TFormula.comprehension, strEmptySet, null, null);
                if (!termAbstraction(typeNode))
                        {if (true) return
                                null;}  //not a well formed comprehension
        }
//mfmfmfm		
                else
                        {if (true) return
                                null;}
          }
    jj_consume_token(RIGHTPAREN);
      scope=secondary();
        if (scope!=null){
                variable =new TFormula(TFormula.variable,
                                                                toInternalForm(t.image), null, null);
                if(!typed){
                newnode= new TFormula(TFormula.quantifier,

                                                                strUniquant,
                                                        variable,
                                                        scope);
                }
                else
                {TFormula link = new TFormula(TFormula.kons,  //make a link to variable
                                       "",
                                       variable,
                                       null);
            link.appendToFormulaList(typeNode); //attach type to it
        newnode= new TFormula(TFormula.typedQuantifier, //make root
                                                        strUniquant,
                                                        link,
                                                        scope);

                }

    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula uniQuantHelperTypeOne(Token q, Token t) throws ParseException {
 Token type;
TFormula newnode,rLink,variable,scope,typeNode=null;
boolean typed=false;

          if ((getToken(1).kind)==COLON){// . peep ahead, typed variable
                getNextToken();  //advance to colon
                type=getNextToken();  //advance to type
            if (type.kind==FUNCTOR){
                        typed=true;
                        typeNode = new TFormula(TFormula.functor, toInternalForm(type.image), null, null);
                        //getNextToken();  // go past functor
                }



//mfmfmfm Dec 13 09
         else
         if (type.kind==LEFTCURLY){ //comprehension
            typed=true;
                typeNode =new TFormula(TFormula.comprehension, strEmptySet, null, null);
                if (!termAbstraction(typeNode))
                        {if (true) return
                                null;}  //not a well formed comprehension
        }
//mfmfmfm		
                else
                        {if (true) return
                                null;}
          }
      scope=secondary();
        if (scope!=null){
                variable =new TFormula(TFormula.variable,
                                                                toInternalForm(t.image), null, null);
                if(!typed){
                newnode= new TFormula(TFormula.quantifier,

                                                                strUniquant,
                                                        variable,
                                                        scope);
                }
                else
                {TFormula link = new TFormula(TFormula.kons,  //make a link to variable
                                       "",
                                       variable,
                                       null);
            link.appendToFormulaList(typeNode); //attach type to it
        newnode= new TFormula(TFormula.typedQuantifier, //make root
                                                        strUniquant,
                                                        link,
                                                        scope);

                }

    {if (true) return
                newnode;}
        }
        else
                {if (true) return
                   null;}
    throw new Error("Missing return statement in function");
  }

  final public int testBracketContents() throws ParseException {
 int index=1;
int indent=1;
TFormula wff;
String contents="";
java.io.StringReader sr;
java.io.Reader r;
CCParser aCCParser;
Token next= getToken(index);

while ((next.kind!=EOF)&&indent > 0){
  if (next.kind==RIGHTPAREN) indent-=1;
  if (next.kind==LEFTPAREN) indent+=1;
  if (indent >0)
        {contents+=next.image;
        index++;
        next= getToken(index);
        if (next.kind==EOF)
                contents="";   //duplicate contents of brackets
  }                    // without advancing original
}

        if (contents.length()< 1)
                {if (true) return
                        0;}

        TFormula wffTry=null;
        sr = new java.io.StringReader( contents );
        r = new java.io.BufferedReader( sr );
        aCCParser = new CCParser(sr,fParseType);

        try {
                wffTry= aCCParser.top();   //trying for wff
    } catch (ParseException e) {
        wffTry=null;
        System.out.println("Not parsed");
    }
    if (wffTry!=null)
        {if (true) return
                1;}
//////////////////
        TFormula termTry=null;
        sr = new java.io.StringReader( contents );
        r = new java.io.BufferedReader( sr );
        aCCParser = new CCParser(sr,fParseType);

        try {
                termTry= aCCParser.term();   //trying for term
    } catch (ParseException e) {
        termTry=null;
        System.out.println("Not parsed");
    }
        if (termTry!=null)
        {if (true) return
                2;}
////////////////
    {if (true) return
        0;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula primary() throws ParseException {
  {if (true) return
  atomic();}
    throw new Error("Missing return statement in function");
  }

  final public TFormula atomic() throws ParseException {
 TFormula proposition;
Token t;
    label_7:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case PREDICATE:
      case TOPBOTTOM:
        ;
        break;
      default:
        jj_la1[18] = jj_gen;
        break label_7;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case TOPBOTTOM:
        // (
        t = jj_consume_token(TOPBOTTOM);
 proposition=new TFormula(TFormula.predicator,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
{if (true) return
        proposition;}
        break;
      case PREDICATE:
        //(
        t = jj_consume_token(PREDICATE);
 {if (true) return
        predicate(t);}
        break;
      default:
        jj_la1[19] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
 boolean skipBracket=false;
  {if (true) return
        infixPredicate(false);}
    throw new Error("Missing return statement in function");
  }

  final public TFormula predicate(Token t) throws ParseException {
  if ((fParseType&BRACKETEDPREDS)!=0)
    {if (true) return
          predicateTypeOne(t);}
  else
        {if (true) return
          predicateTypeZero(t);}
    throw new Error("Missing return statement in function");
  }

  final public TFormula predicateTypeZero(Token t) throws ParseException {
 TFormula proposition;
  proposition=new TFormula(TFormula.predicator,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);

        Token nextToken=getToken(1); // we need to look ahead 1 without consuming
                                                            // can be terms following
// good looks like Pabd or P(1+1)c bad is PaF

        if ((nextToken!=null)&&

                  (
                  (nextToken.kind==FUNCTOR)||
                  (nextToken.kind==VARIABLE)||
                  (nextToken.kind==CONSTANT)||
                  (nextToken.kind==LEFTPAREN)||
                  (nextToken.kind==LEFTANGLE)||
                  (nextToken.kind==POWERSET)||
                  (nextToken.kind==LEFTCURLY)
                        )
                        )
                        {
                        if (predHelper(proposition)) //terms following
                                {if (true) return
                                        proposition;}
                        else
                                {if (true) return
                                        null;}
                        }

        {if (true) return
                proposition;}  // no terms is ok

    throw new Error("Missing return statement in function");
  }

  final public TFormula predicateTypeOne(Token t) throws ParseException {
 TFormula proposition;
  proposition=new TFormula(TFormula.predicator,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);

        Token nextToken=getToken(1); // we need to look ahead 1 without consuming
                                                            // can be terms following
// we've looked ahead-- has to be bracket if terms

        if (nextToken.kind!=LEFTPAREN)
                {if (true) return
                        proposition;}
    jj_consume_token(LEFTPAREN);
          if (!predHelper(proposition)) //terms following
                                {if (true) return
                                        null;}
    jj_consume_token(RIGHTPAREN);
                {if (true) return
                        proposition;}
    throw new Error("Missing return statement in function");
  }

  final public boolean predHelper(TFormula root) throws ParseException {
 TFormula term;
Token nextToken;
         term=term();
        if (term==null)
                {if (true) return ILLFORMED;}  //has to be one

    label_8:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[20] = jj_gen;
        break label_8;
      }
      jj_consume_token(COMMA);
    }
                root.appendToFormulaList(term);

                nextToken=getToken(1); //generated token manager call

                if (nextToken!=null&&
                        (
                  (nextToken.kind==FUNCTOR)||
                  (nextToken.kind==VARIABLE)||
                  (nextToken.kind==CONSTANT)||
                  (nextToken.kind==LEFTPAREN)||
                  (nextToken.kind==LEFTANGLE)||
                  (nextToken.kind==POWERSET)||
                  (nextToken.kind==LEFTCURLY)
                )
                        )
                        {if (true) return
                                predHelper(root);}  // do next one
                else
                        {if (true) return
                                WELLFORMED;}        // finished

    throw new Error("Missing return statement in function");
  }

  final public TFormula infixPredicate(boolean skipBracket) throws ParseException {
 TFormula leftTerm,rightTerm,infix;
Token t;
short kind;
        leftTerm= term();
        if (leftTerm==null)
                {if (true) return null;}
 if(skipBracket){
        t= getNextToken();
        if(t.kind!=RIGHTPAREN)
                {if (true) return
                        null;}
        }
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case INFIXPREDICATE:
      t = jj_consume_token(INFIXPREDICATE);
      break;
    case EQUALITY:
      t = jj_consume_token(EQUALITY);
      break;
    case LEFTANGLE:
      t = jj_consume_token(LEFTANGLE);
      break;
    case RIGHTANGLE:
      t = jj_consume_token(RIGHTANGLE);
      break;
    default:
      jj_la1[21] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
     if (t.kind==EQUALITY)
      kind=TFormula.equality;
   else
      kind=TFormula.predicator;

        infix=new TFormula(kind,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
        rightTerm= term();
        if (rightTerm==null)
                {if (true) return null;}

  infix.appendToFormulaList(leftTerm);
  infix.appendToFormulaList(rightTerm);

  /*special case*/

  if (infix.fInfo.equals(strNotMemberOf)){ // special case, in set theory not member is abbreviation
                                                            // we make it into negation to get proper semantics for rules
                        infix.fInfo=toInternalForm(strMemberOf);
                        TFormula rLink= infix.copyFormula();
                        TFormula negation= new TFormula(TFormula.unary,String.valueOf(chNeg),null,rLink);

                        infix.assignFieldsToMe(negation);   //surgery 		
                }
  {if (true) return
        infix;}
    throw new Error("Missing return statement in function");
  }

/******************  terms *******************************/
  final public TFormula term() throws ParseException {
  {if (true) return
        term5ary();}
    throw new Error("Missing return statement in function");
  }

  final public TFormula term5ary() throws ParseException {
 TFormula term4ary;
Token t;
   term4ary= term4ary();
        if (term4ary==null)
                {if (true) return term4ary;}
    label_9:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case INFIX5:
        ;
        break;
      default:
        jj_la1[22] = jj_gen;
        break label_9;
      }
      t = jj_consume_token(INFIX5);
   TFormula prefix=new TFormula(TFormula.functor,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
   TFormula term5ary=term5ary();

   if (term4ary==null) {if (true) return null;}

   TFormula oldRoot = new TFormula(term4ary.getKind(),
                                term4ary.getInfo(),
                                term4ary.getLLink(),
                                term4ary.getRLink());
   prefix.appendToFormulaList(oldRoot);
   prefix.appendToFormulaList(term5ary);
   term4ary.assignFieldsToMe(prefix); //surgery
        {if (true) return
                term4ary;}    // bale to ensure 0 or 1                                

    }
  {if (true) return
        term4ary;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula term4ary() throws ParseException {
 TFormula tertiary;
Token t;
   tertiary= term3ary();
        if (tertiary==null)
                {if (true) return tertiary;}
    label_10:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case INFIX4:
        ;
        break;
      default:
        jj_la1[23] = jj_gen;
        break label_10;
      }
      t = jj_consume_token(INFIX4);
   TFormula prefix=new TFormula(TFormula.functor,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
   TFormula term4ary=term4ary();

   if (term4ary==null) {if (true) return null;}

   TFormula oldRoot = new TFormula(tertiary.getKind(),
                                tertiary.getInfo(),
                                tertiary.getLLink(),
                                tertiary.getRLink());
   prefix.appendToFormulaList(oldRoot);
   prefix.appendToFormulaList(term4ary);
   tertiary.assignFieldsToMe(prefix); //surgery

        {if (true) return
                tertiary;}    // bale to ensure 0 or 1                                

    }
  {if (true) return
        tertiary;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula term3ary() throws ParseException {
 TFormula secondary;
Token t;
   secondary= term2ary();
        if (secondary==null)
                {if (true) return secondary;}
    label_11:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case INFIX3:
        ;
        break;
      default:
        jj_la1[24] = jj_gen;
        break label_11;
      }
      t = jj_consume_token(INFIX3);
   TFormula prefix=new TFormula(TFormula.functor,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
   TFormula tertiary=term3ary();

   if (tertiary==null) {if (true) return null;}

   TFormula oldRoot = new TFormula(secondary.getKind(),
                                secondary.getInfo(),
                                secondary.getLLink(),
                                secondary.getRLink());
   prefix.appendToFormulaList(oldRoot);
   prefix.appendToFormulaList(tertiary);
   secondary.assignFieldsToMe(prefix); //surgery

        {if (true) return
                secondary;}    // bale to ensure 0 or 1                                 

    }
  {if (true) return
        secondary;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula term2ary() throws ParseException {
 TFormula root;
Token t, lookAhead;
        root= term1ary();
        if (root==null)
                {if (true) return root;}


/*there is an issue at this point. If what is next is a period there is
ambiguity in some systems between 'and' and 'multiply'. Between Hf.Gb and Hf.g
So we look to see if it
is a period (without advancing). It is made worse in Copi systems which use
(x) for the Universal Quantifier eg (x)Fx.(y)Fy the (y) could be part of the term
x.(y) */

   lookAhead=getToken(1);

   if (lookAhead.kind==INFIX2) //it's a period
          {boolean meansMultiply=testForSecondaryTerm();
          if (!meansMultiply)
                 {if (true) return
                   root;}            //the period means 'and' not 'mulitply'
          }
    label_12:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case SUCCESSOR:
        ;
        break;
      default:
        jj_la1[25] = jj_gen;
        break label_12;
      }
      t = jj_consume_token(SUCCESSOR);
   TFormula prefix=new TFormula(TFormula.functor,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
   TFormula oldRoot = new TFormula(root.getKind(),
                                root.getInfo(),
                                root.getLLink(),
                                root.getRLink());
   prefix.appendToFormulaList(oldRoot);
   root.assignFieldsToMe(prefix); //surgery                             

    }
    label_13:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case INFIX2:
        ;
        break;
      default:
        jj_la1[26] = jj_gen;
        break label_13;
      }
      t = jj_consume_token(INFIX2);
   TFormula prefix=new TFormula(TFormula.functor,
                                                                t.image,
        // NOTE not toInternalForm(t.image), because "." is ambiguous for and
                                                                null,
                                                                null);
   TFormula secondary=term2ary();

   if (secondary==null) {if (true) return null;}

   TFormula oldRoot = new TFormula(root.getKind(),
                                root.getInfo(),
                                root.getLLink(),
                                root.getRLink());
   prefix.appendToFormulaList(oldRoot);
   prefix.appendToFormulaList(secondary);
   root.assignFieldsToMe(prefix); //surgery

   {if (true) return
        root;}    // bale to ensure 0 or 1                            

    }
  {if (true) return
        root;}
    throw new Error("Missing return statement in function");
  }

  final public boolean testForSecondaryTerm() throws ParseException {
 int index=2;

TFormula wff;
String contents="";
java.io.StringReader sr;
java.io.Reader r;
CCParser aCCParser;
//Token next= getToken(index);
//index++;
Token next= getToken(index);   //skip the period

// looking for uniquant in (x) form  11/28/11

if (next.kind==LEFTPAREN){
        Token next1= getToken(index+1);
        if (next1.kind==VARIABLE){
                Token next2= getToken(index+2);
                if (next2.kind==RIGHTPAREN)
                        {if (true) return
                           false;} //ie not a term
        }
}
// end of looking for uniquant  11/28/11


while ((next.kind!=EOF)&&
           (next.kind!=PREDICATE)&&
           (next.kind!=INFIXPREDICATE)&&
           (next.kind!=UNIQUANT)&&
           (next.kind!=EXIQUANT)&&
           (next.kind!=NEGATION)&&
           (next.kind!=AND)&&
           (next.kind!=OR)&&
           (next.kind!=IMPLIC)&&
           (next.kind!=EQUIV)
           )

           {
        contents+=next.image;
        index++;
        next= getToken(index);
        }

        if (contents.length()< 1)
                {if (true) return
                        false;}

        TFormula termTry=null;
        sr = new java.io.StringReader( contents );
        r = new java.io.BufferedReader( sr );
        aCCParser = new CCParser(sr,fParseType);

        try {
                termTry= aCCParser.term2ary();   //trying for wff
    } catch (ParseException e) {
        termTry=null;
        System.out.println("Following term not parsed");
    }
    if (termTry!=null)
        {if (true) return
                true;}
    {if (true) return
        false;}
    throw new Error("Missing return statement in function");
  }

//	{<termprimary>::={}|{termlist}|{var: scope}|{var| scope} }  //ie a comprehensino
//	{<termprimary>::= <powerset(one element termlist>)
//	{<termprimary>::= < <a,b> ie ordered pair >}
//	{<termprimary>::=(<term>)}
//	{<termprimary>::=<functor>|<functor(<nonempty termlist>)}
  final public TFormula term1ary() throws ParseException {
  Token t ;
  TFormula termForm,subterm;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LEFTCURLY:
      t = jj_consume_token(LEFTCURLY);
         termForm =new TFormula(TFormula.comprehension, strEmptySet, null, null);
        if (termComprehension(termForm))
                {if (true) return
                        termForm;}
        else
                {if (true) return
                        null;}
      break;
    case POWERSET:
      t = jj_consume_token(POWERSET);
         termForm =new TFormula(TFormula.functor, toInternalForm(t.image), null, null);
        if (termPowerSet(termForm))
                {if (true) return
                        termForm;}
        else
                {if (true) return
                        null;}
      break;
    case LEFTANGLE:
      jj_consume_token(LEFTANGLE);
         termForm =new TFormula(TFormula.pair, "", null, null);
        if (termOrderedPair(termForm))
                {if (true) return
                        termForm;}
        else {if (true) return
                        null;}
      break;
    case LEFTPAREN:
      jj_consume_token(LEFTPAREN);
         TFormula innerTerm=term();
      jj_consume_token(RIGHTPAREN);
         {if (true) return innerTerm;}
      break;
    case CONSTANT:
      t = jj_consume_token(CONSTANT);
         termForm =new TFormula(TFormula.functor, toInternalForm(t.image), null, null);
                {if (true) return termForm;}
      break;
    case VARIABLE:
      t = jj_consume_token(VARIABLE);
         termForm =new TFormula(TFormula.variable, toInternalForm(t.image), null, null);
                {if (true) return termForm;}
      break;
    case FUNCTOR:
      if (jj_2_5(2)) {
        t = jj_consume_token(FUNCTOR);
        jj_consume_token(LEFTPAREN);
         termForm =new TFormula(TFormula.functor, toInternalForm(t.image), null, null);
        if (termList(termForm))
                {if (true) return termForm;}
        else {if (true) return null;}
      } else {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case FUNCTOR:
          t = jj_consume_token(FUNCTOR);
         termForm =new TFormula(TFormula.functor, toInternalForm(t.image), null, null);
                {if (true) return termForm;}
          break;
        default:
          jj_la1[27] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
      }
      break;
    default:
      jj_la1[28] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    throw new Error("Missing return statement in function");
  }

  final public boolean termList(TFormula root) throws ParseException {
 TFormula subterm;
         subterm=term();  // must be at least one
        if (subterm!=null)
                root.appendToFormulaList(subterm);
        else
                {if (true) return false;}
    label_14:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[29] = jj_gen;
        break label_14;
      }
      jj_consume_token(COMMA);
    }
    label_15:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RIGHTPAREN:
        ;
        break;
      default:
        jj_la1[30] = jj_gen;
        break label_15;
      }
      jj_consume_token(RIGHTPAREN);
                       {if (true) return true;}
    }
         {if (true) return
                termList(root);}
    throw new Error("Missing return statement in function");
  }

  final public boolean termListAngle(TFormula root) throws ParseException {
 TFormula subterm;
         subterm=term();  // must be at least one
        if (subterm!=null)
                root.appendToFormulaList(subterm);
        else
                {if (true) return false;}
    label_16:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[31] = jj_gen;
        break label_16;
      }
      jj_consume_token(COMMA);
    }
    label_17:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RIGHTANGLE:
        ;
        break;
      default:
        jj_la1[32] = jj_gen;
        break label_17;
      }
      jj_consume_token(RIGHTANGLE);
                        {if (true) return true;}
    }
         {if (true) return
                termListAngle(root);}
    throw new Error("Missing return statement in function");
  }

  final public boolean comprehensionHelper(TFormula root) throws ParseException {
 TFormula subterm;
         subterm=term();  // second and subsequent
        if (subterm!=null)
                root.appendToFormulaList(subterm);
        else
                {if (true) return ILLFORMED;}
    label_18:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[33] = jj_gen;
        break label_18;
      }
      jj_consume_token(COMMA);
    }
    label_19:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RIGHTCURLY:
        ;
        break;
      default:
        jj_la1[34] = jj_gen;
        break label_19;
      }
      jj_consume_token(RIGHTCURLY);
                        {if (true) return WELLFORMED;}
    }
         {if (true) return
                comprehensionHelper(root);}
    throw new Error("Missing return statement in function");
  }

  final public boolean termComprehension(TFormula root) throws ParseException {
 TFormula firstTerm,scope=null;
Token t;
    label_20:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RIGHTCURLY:
        ;
        break;
      default:
        jj_la1[35] = jj_gen;
        break label_20;
      }
      jj_consume_token(RIGHTCURLY);
                  {if (true) return WELLFORMED;}
    }
         firstTerm=term();  // must be at least one

 //System.out.println("COMPREHENSION");

                if (firstTerm==null)
                {if (true) return ILLFORMED;}
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case COMMA:
      jj_consume_token(COMMA);
         root.appendToFormulaList(firstTerm); // attach first
         {if (true) return
                comprehensionHelper(root);}       // attach rest  		 

      break;
    case COLON:
    case VERTLINE:
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COLON:
        t = jj_consume_token(COLON);
        break;
      case VERTLINE:
        t = jj_consume_token(VERTLINE);
        break;
      default:
        jj_la1[36] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
 scope=secondary();
        if (scope!=null){
           root.fInfo=toInternalForm(t.image);
       root.fLLink=firstTerm;
       root.fRLink=scope;
                }
      jj_consume_token(RIGHTCURLY);
                 {if (true) return
                WELLFORMED;}
      break;
    case RIGHTCURLY:
      jj_consume_token(RIGHTCURLY);
  root.appendToFormulaList(firstTerm); // attach first and only
        {if (true) return
                WELLFORMED;}
      break;
    default:
      jj_la1[37] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
  {if (true) return
        ILLFORMED;}
    throw new Error("Missing return statement in function");
  }

  final public boolean termAbstraction(TFormula root) throws ParseException {
 TFormula firstTerm,scope=null;
Token t;
         firstTerm=term();  // must be at least one

 //System.out.println("COMPREHENSION");

                if (firstTerm==null)
                {if (true) return ILLFORMED;}
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case COLON:
      t = jj_consume_token(COLON);
      break;
    case VERTLINE:
      t = jj_consume_token(VERTLINE);
      break;
    default:
      jj_la1[38] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
 scope=secondary();
        if (scope!=null){
           root.fInfo=toInternalForm(t.image);
       root.fLLink=firstTerm;
       root.fRLink=scope;
                }
    label_21:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RIGHTCURLY:
        ;
        break;
      default:
        jj_la1[39] = jj_gen;
        break label_21;
      }
      jj_consume_token(RIGHTCURLY);
                {if (true) return WELLFORMED;}
    }
    {if (true) return
                ILLFORMED;}
  {if (true) return
        ILLFORMED;}
    throw new Error("Missing return statement in function");
  }

  final public boolean termOrderedPair(TFormula root) throws ParseException {
                 if (!(termListAngle(root)&&
                root.firstTerm()!=null&&
                root.secondTerm()!=null&&
                root.nthTopLevelTerm(3)==null))//exactly two terms
                        {if (true) return
                                ILLFORMED;}
                 {if (true) return
                        WELLFORMED;}
    throw new Error("Missing return statement in function");
  }

  final public boolean termPowerSet(TFormula root) throws ParseException {
    jj_consume_token(LEFTPAREN);
         if (!(termList(root)&&
                root.firstTerm()!=null&&
                root.secondTerm()==null))//exactly ONE term
                        {if (true) return
                                ILLFORMED;}
                 {if (true) return
                        WELLFORMED;}
    throw new Error("Missing return statement in function");
  }

/******************* Awkward ******************************/
  final public TFormula awkwardCase() throws ParseException {
 TFormula wff;
    Token next;
int result =testAwkwardBracketContents();

if (result==1)  // we know it is a wff (must end with right paren)
        {
          next= getNextToken();  // advances to opening left bracket
                wff=top(); // now parse original;
                 next= getNextToken();
                 if(next.kind==RIGHTPAREN) //closing bracket
                        {if (true) return
                        wff;}
                 else
                        {if (true) return
                         null;}
        }

if (result==2) // we know it is an infix predicate starting with
                           // a bracketed term eg (1+2)=3

        {
    {if (true) return
                infixAwkwardPredicate();} // now parse original;
        }
if (result==0)
        {if (true) return
                null;}
    {if (true) return
     null;}
    throw new Error("Missing return statement in function");
  }

  final public TFormula infixAwkwardPredicate() throws ParseException {
 TFormula leftTerm,rightTerm,infix;
Token t;
short kind;
        leftTerm= term();
        if (leftTerm==null)
                {if (true) return null;}
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case INFIXPREDICATE:
      t = jj_consume_token(INFIXPREDICATE);
      break;
    case EQUALITY:
      t = jj_consume_token(EQUALITY);
      break;
    case LEFTANGLE:
      t = jj_consume_token(LEFTANGLE);
      break;
    case RIGHTANGLE:
      t = jj_consume_token(RIGHTANGLE);
      break;
    default:
      jj_la1[40] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
     if (t.kind==EQUALITY)
      kind=TFormula.equality;
   else
      kind=TFormula.predicator;

        infix=new TFormula(kind,
                                                                toInternalForm(t.image),
                                                                null,
                                                                null);
        rightTerm= term();
        if (rightTerm==null)
                {if (true) return null;}

  infix.appendToFormulaList(leftTerm);
  infix.appendToFormulaList(rightTerm);

  /*special case*/

  if (infix.fInfo.equals(strNotMemberOf)){ // special case, in set theory not member is abbreviation
                                                            // we make it into negation to get proper semantics for rules
                        infix.fInfo=toInternalForm(strMemberOf);
                        TFormula rLink= infix.copyFormula();
                        TFormula negation= new TFormula(TFormula.unary,String.valueOf(chNeg),null,rLink);

                        infix.assignFieldsToMe(negation);   //surgery 		
                }
  {if (true) return
        infix;}
    throw new Error("Missing return statement in function");
  }

  final public int testAwkwardBracketContents() throws ParseException {
 int index=2;  // we start at 2 to miss the opening (
int indent=1;
TFormula wff;
String contents="";
java.io.StringReader sr;
java.io.Reader r;
CCParser aCCParser;
Token next= getToken(index);

while ((next.kind!=EOF)&&indent > 0){
  if (next.kind==RIGHTPAREN) indent-=1;
  if (next.kind==LEFTPAREN) indent+=1;
  if (indent >0)
        {contents+=next.image;
        index++;
        next= getToken(index);
        if (next.kind==EOF)
                contents="";   //duplicate contents of brackets
  }                    // without advancing original
}

        if (contents.length()< 1)
                {if (true) return
                        0;}

        TFormula wffTry=null;
        sr = new java.io.StringReader( contents );
        r = new java.io.BufferedReader( sr );
        aCCParser = new CCParser(sr,fParseType);

        try {
                wffTry= aCCParser.top();   //trying for wff
    } catch (ParseException e) {
        wffTry=null;
        System.out.println("Not parsed");
    }
    if (wffTry!=null)
        {if (true) return
                1;}
//////////////////
        TFormula termTry=null;
        sr = new java.io.StringReader( contents );
        r = new java.io.BufferedReader( sr );
        aCCParser = new CCParser(sr,fParseType);

        try {
                termTry= aCCParser.term();   //trying for term
    } catch (ParseException e) {
        termTry=null;
        System.out.println("Not parsed");
    }
        if (termTry!=null)
        {if (true) return
                2;}
////////////////
    {if (true) return
        0;}
    throw new Error("Missing return statement in function");
  }

  private boolean jj_2_1(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_1(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(0, xla); }
  }

  private boolean jj_2_2(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_2(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(1, xla); }
  }

  private boolean jj_2_3(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_3(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(2, xla); }
  }

  private boolean jj_2_4(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_4(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(3, xla); }
  }

  private boolean jj_2_5(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_5(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(4, xla); }
  }

  private boolean jj_3_4() {
    if (jj_scan_token(LEFTPAREN)) return true;
    if (jj_scan_token(VARIABLE)) return true;
    if (jj_scan_token(COLON)) return true;
    return false;
  }

  private boolean jj_3_3() {
    if (jj_scan_token(LEFTPAREN)) return true;
    if (jj_scan_token(VARIABLE)) return true;
    if (jj_scan_token(RIGHTPAREN)) return true;
    return false;
  }

  private boolean jj_3_5() {
    if (jj_scan_token(FUNCTOR)) return true;
    if (jj_scan_token(LEFTPAREN)) return true;
    return false;
  }

  private boolean jj_3_1() {
    if (jj_scan_token(LEFTPAREN)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_scan_token(18)) {
    jj_scanpos = xsp;
    if (jj_scan_token(19)) return true;
    }
    return false;
  }

  private boolean jj_3_2() {
    if (jj_scan_token(LEFTPAREN)) return true;
    if (jj_scan_token(UNIQUANT)) return true;
    return false;
  }

  /** Generated Token Manager. */
  public CCParserTokenManager token_source;
  JavaCharStream jj_input_stream;
  /** Current token. */
  public Token token;
  /** Next token. */
  public Token jj_nt;
  private int jj_ntk;
  private Token jj_scanpos, jj_lastpos;
  private int jj_la;
  private int jj_gen;
  final private int[] jj_la1 = new int[41];
  static private int[] jj_la1_0;
  static private int[] jj_la1_1;
  static {
      jj_la1_init_0();
      jj_la1_init_1();
   }
   private static void jj_la1_init_0() {
      jj_la1_0 = new int[] {0x1,0x4000001,0x4000001,0x0,0x8000000,0x101f000,0x7000,0xc0,0xc0,0xc0000,0x1f000,0x1000000,0x10ff000,0x7000,0xc0,0xc0,0xc0000,0x10ff000,0x900,0x900,0x0,0x80000600,0x0,0x0,0x0,0x0,0x0,0x40,0x910000e0,0x0,0x2000000,0x0,0x0,0x0,0x20000000,0x20000000,0x0,0x20000000,0x0,0x20000000,0x80000600,};
   }
   private static void jj_la1_init_1() {
      jj_la1_1 = new int[] {0x0,0x0,0x0,0x2,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x2,0x1,0x200,0x100,0x80,0x20,0x40,0x0,0x10,0x2,0x0,0x2,0x1,0x2,0x0,0x0,0xc,0xe,0xc,0x0,0x1,};
   }
  final private JJCalls[] jj_2_rtns = new JJCalls[5];
  private boolean jj_rescan = false;
  private int jj_gc = 0;

  /** Constructor with InputStream.  12/2/11
  public CCParser(java.io.InputStream stream) {
     this(stream, null);
  }
  /** Constructor with InputStream and supplied encoding 
  public CCParser(java.io.InputStream stream, String encoding) {
    try { jj_input_stream = new JavaCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
    token_source = new CCParserTokenManager(jj_input_stream);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 41; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  /** Reinitialise.
  public void ReInit(java.io.InputStream stream) {
     ReInit(stream, null);
  }
  /** Reinitialise. 
  public void ReInit(java.io.InputStream stream, String encoding) {
    try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
    token_source.ReInit(jj_input_stream);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 41; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }
  
  */

  /** Constructor. */
  public CCParser(java.io.Reader stream) {
    jj_input_stream = new JavaCharStream(stream, 1, 1);
    token_source = new CCParserTokenManager(jj_input_stream);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 41; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  /** Reinitialise. */
  public void ReInit(java.io.Reader stream) {
    jj_input_stream.ReInit(stream, 1, 1);
    token_source.ReInit(jj_input_stream);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 41; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  /** Constructor with generated Token Manager. */
  public CCParser(CCParserTokenManager tm) {
    token_source = tm;
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 41; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  /** Reinitialise. */
  public void ReInit(CCParserTokenManager tm) {
    token_source = tm;
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 41; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  private Token jj_consume_token(int kind) throws ParseException {
    Token oldToken;
    if ((oldToken = token).next != null) token = token.next;
    else token = token.next = token_source.getNextToken();
    jj_ntk = -1;
    if (token.kind == kind) {
      jj_gen++;
      if (++jj_gc > 100) {
        jj_gc = 0;
        for (int i = 0; i < jj_2_rtns.length; i++) {
          JJCalls c = jj_2_rtns[i];
          while (c != null) {
            if (c.gen < jj_gen) c.first = null;
            c = c.next;
          }
        }
      }
      return token;
    }
    token = oldToken;
    jj_kind = kind;
    throw generateParseException();
  }

  static private final class LookaheadSuccess extends java.lang.Error { }
  final private LookaheadSuccess jj_ls = new LookaheadSuccess();
  private boolean jj_scan_token(int kind) {
    if (jj_scanpos == jj_lastpos) {
      jj_la--;
      if (jj_scanpos.next == null) {
        jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
      } else {
        jj_lastpos = jj_scanpos = jj_scanpos.next;
      }
    } else {
      jj_scanpos = jj_scanpos.next;
    }
    if (jj_rescan) {
      int i = 0; Token tok = token;
      while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
      if (tok != null) jj_add_error_token(kind, i);
    }
    if (jj_scanpos.kind != kind) return true;
    if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
    return false;
  }


/** Get the next Token. */
  final public Token getNextToken() {
    if (token.next != null) token = token.next;
    else token = token.next = token_source.getNextToken();
    jj_ntk = -1;
    jj_gen++;
    return token;
  }

/** Get the specific Token. */
  final public Token getToken(int index) {
    Token t = token;
    for (int i = 0; i < index; i++) {
      if (t.next != null) t = t.next;
      else t = t.next = token_source.getNextToken();
    }
    return t;
  }

  private int jj_ntk() {
    if ((jj_nt=token.next) == null)
      return (jj_ntk = (token.next=token_source.getNextToken()).kind);
    else
      return (jj_ntk = jj_nt.kind);
  }

  private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>();
  private int[] jj_expentry;
  private int jj_kind = -1;
  private int[] jj_lasttokens = new int[100];
  private int jj_endpos;

  private void jj_add_error_token(int kind, int pos) {
    if (pos >= 100) return;
    if (pos == jj_endpos + 1) {
      jj_lasttokens[jj_endpos++] = kind;
    } else if (jj_endpos != 0) {
      jj_expentry = new int[jj_endpos];
      for (int i = 0; i < jj_endpos; i++) {
        jj_expentry[i] = jj_lasttokens[i];
      }
      jj_entries_loop: for (java.util.Iterator<?> it = jj_expentries.iterator(); it.hasNext();) {
        int[] oldentry = (int[])(it.next());
        if (oldentry.length == jj_expentry.length) {
          for (int i = 0; i < jj_expentry.length; i++) {
            if (oldentry[i] != jj_expentry[i]) {
              continue jj_entries_loop;
            }
          }
          jj_expentries.add(jj_expentry);
          break jj_entries_loop;
        }
      }
      if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind;
    }
  }

  /** Generate ParseException. */
  public ParseException generateParseException() {
    jj_expentries.clear();
    boolean[] la1tokens = new boolean[44];
    if (jj_kind >= 0) {
      la1tokens[jj_kind] = true;
      jj_kind = -1;
    }
    for (int i = 0; i < 41; i++) {
      if (jj_la1[i] == jj_gen) {
        for (int j = 0; j < 32; j++) {
          if ((jj_la1_0[i] & (1<<j)) != 0) {
            la1tokens[j] = true;
          }
          if ((jj_la1_1[i] & (1<<j)) != 0) {
            la1tokens[32+j] = true;
          }
        }
      }
    }
    for (int i = 0; i < 44; i++) {
      if (la1tokens[i]) {
        jj_expentry = new int[1];
        jj_expentry[0] = i;
        jj_expentries.add(jj_expentry);
      }
    }
    jj_endpos = 0;
    jj_rescan_token();
    jj_add_error_token(0, 0);
    int[][] exptokseq = new int[jj_expentries.size()][];
    for (int i = 0; i < jj_expentries.size(); i++) {
      exptokseq[i] = jj_expentries.get(i);
    }
    return new ParseException(token, exptokseq, tokenImage);
  }

  /** Enable tracing. */
  final public void enable_tracing() {
  }

  /** Disable tracing. */
  final public void disable_tracing() {
  }

  private void jj_rescan_token() {
    jj_rescan = true;
    for (int i = 0; i < 5; i++) {
    try {
      JJCalls p = jj_2_rtns[i];
      do {
        if (p.gen > jj_gen) {
          jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
          switch (i) {
            case 0: jj_3_1(); break;
            case 1: jj_3_2(); break;
            case 2: jj_3_3(); break;
            case 3: jj_3_4(); break;
            case 4: jj_3_5(); break;
          }
        }
        p = p.next;
      } while (p != null);
      } catch(LookaheadSuccess ls) { }
    }
    jj_rescan = false;
  }

  private void jj_save(int index, int xla) {
    JJCalls p = jj_2_rtns[index];
    while (p.gen > jj_gen) {
      if (p.next == null) { p = p.next = new JJCalls(); break; }
      p = p.next;
    }
    p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla;
  }

  static final class JJCalls {
    int gen;
    Token first;
    int arg;
    JJCalls next;
  }

}
