/* Generated By:JavaCC: Do not edit this line. CCParser.java */

/*
Copyright (C) 2014 Martin Frické (mfricke@u.arizona.edu http://softoption.us mfricke@softoption.us)

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation 
files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, 
modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the 
Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE 
WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 
COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR 
OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/

/*
Copyright (C) 2015 Martin Frické (mfricke@email.arizona.edu https://softoption.us mfricke@softoption.us mfricke1947@gmail.com)

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation 
files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, 
modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the 
Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE 
WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR 
COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR 
OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/

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;
  }

}
