%union {JavaAgent.resource.cdl.Parsable; FormulaSet; ClauseSet; Formula; Clause; Literal; Term; Vector; Variable; Symbol; Integer}

%token <Integer> '(' ')' '='
%token <Integer> CONSTANT VARIABLE 
%token <Integer> NOT IMPLIES IFF XOR AND OR
%token <Integer> FORALL EXISTS
%token <Integer> LIST TERM LITERAL FORMULA CLAUSE CLAUSESET FORMS

%type  <Symbol>   tCONSTANT
%type  <Variable> tVARIABLE FOPLVarSpec

%type  <Term> FOPLTerm
%type  <Literal> FOPLBLiteral SignedLit
%type  <Clause> FOPLClause
%type  <Vector> FOPL0TermList FOPL1TermList FOPL1FormList FOPL1VarSpecList
%type  <Vector> SignedLit0List
%type  <Formula> FOPLFormula FOPLBFormula
%type  <Integer> FOPLbincon FOPLmulticon FOPLquant
%type  <Integer> LVon LVoff
%type  <ClauseSet> FOPLClauseList
%type  <FormulaSet> FOPLFormList

%type  <JavaAgent.resource.cdl.Parsable> FOPLObject

%start FOPLObject

%%

FOPLObject: TERM FOPLTerm
  { parseResult = $2; }
| LITERAL SignedLit
  { parseResult = $2; }
| FORMULA FOPLFormula
  { parseResult = $2; }
| CLAUSE FOPLClause
  { parseResult = $2; }
| CLAUSESET FOPLClauseList
  { parseResult = $2; }
| FORMS FOPLFormList
  { parseResult = $2; }
;

FOPLFormList: /* empty */
  { $$ = new FormulaSet(); }
| FOPLFormula FOPLFormList
  { $2.assert($1); 
    $$ = $2; }
;

FOPLClauseList: /* empty */
  { $$ = new ClauseSet(); }
| FOPLClause FOPLClauseList
  { $2.assert($1); 
    $$ = $2; }
;

FOPLFormula: tCONSTANT
  { $$ = new Proposition($1); }
| '(' FOPLBFormula ')'
  { $$ = $2; }
;

FOPLBFormula: FOPLBLiteral
  { $$ = $1 }
| NOT FOPLFormula
  { $$ = new NegFormula($2); }
| FOPLmulticon FOPLFormula FOPL1FormList
  { $3.insertElementAt($2, 0);
    $$ = new MultiConFormula($1.intValue(), $3); }
| FOPLbincon FOPLFormula FOPLFormula
  { $$ = new BinConFormula($1.intValue(), $2, $3); }
| '(' FOPLquant LVon FOPL1VarSpecList LVoff ')' '(' FOPLBFormula ')'
  { Variable.removeLocals($4.size());
    $$ = new QuantFormula($2.intValue(), $4, $8); }
;

FOPL1FormList: FOPLFormula
  { Vector res = new Vector(7, 4);
    res.addElement($1);
    $$ = res; }
| FOPL1FormList FOPLFormula
  { $1.addElement($2); 
    $$ = $1; }
;

FOPLmulticon: AND
  { $$ = $1; }
| OR
  { $$ = $1; }
;

FOPLbincon: IMPLIES
  { $$ = $1; }
| IFF
  { $$ = $1; }
| XOR
  { $$ = $1; }
;

FOPLquant: FORALL
  { $$ = $1; }
| EXISTS
  { $$ = $1; }
;

LVon: /* empty, action only */
  { Variable.newLocal=true; }
;

LVoff: /* empty, action only */
  { Variable.newLocal=false; }
;

FOPL1VarSpecList: FOPLVarSpec
  { Vector res = new Vector(4, 2);
    res.addElement($1);
    $$ = res; }
| FOPL1VarSpecList FOPLVarSpec
  { $1.addElement($2); 
    $$ = $1; }
;

FOPLVarSpec: tVARIABLE
  { $$ = $1; }
| '(' tVARIABLE tCONSTANT ')'
  { $2.setType($3);
    $$ = $2; }
;

FOPLClause: '(' SignedLit0List ')'
  { $$ = new Clause($2); }
;

SignedLit0List: /* empty */
  { $$ = new Vector(5, 3); }
| SignedLit SignedLit0List
  { $2.insertElementAt($1, 0); 
    $$ = $2; }
;

SignedLit: tCONSTANT
  { $$ = new Proposition($1); }
| '(' NOT tCONSTANT ')'
  { Proposition p = new Proposition($3);
    p.negate(); 
    $$ = p }
| '(' FOPLBLiteral ')'
  { $$ = $2 }
| '(' NOT '(' FOPLBLiteral ')' ')'
  { $4.negate(); 
    $$ = $4 }
;

FOPLBLiteral: tCONSTANT FOPL1TermList
  { $$ = new Literal($1, $2); }
| '=' FOPLTerm FOPLTerm
  { $$ = new Literal(false, EqualSy, $2, $3); }

FOPLTerm: tCONSTANT
  { $$ = new ConstTerm($1); }
| tVARIABLE
  { $$ = new VarTerm($1); }
| '(' tCONSTANT FOPL1TermList ')'
  { $$ = new FunctTerm($2, $3); }
;

FOPL1TermList: FOPLTerm FOPL0TermList
  { $2.insertElementAt($1, 0); 
    $$ = $2; }
;

FOPL0TermList: /* empty */
  { $$ = new Vector(5, 3); }
| FOPL1TermList
  { $$ = $1; }
;

tVARIABLE: VARIABLE
  { $$ = Variable.get(new String(yytext)); }
;

tCONSTANT: CONSTANT
  { $$ = Symbol.get(new String(yytext)); }
;

%%

/** 
** This variable contains the last Object that has been parsed.
*/
public JavaAgent.resource.cdl.Parsable parseResult = null;

/** 
** This constructor simplifies contructing a FOPL parser for a String.
** The given String is the String to be parsed. If a fresh set of global
** Variables should be used for this parse then <tt>Variable.newVars()</tt> 
** should be called before this constructor. Using this constructor will 
** automatically invoke parsing and the result will be stored in the staic
** variable <tt>parseResult</tt> of this class.
** @param FOPLString the String to be parsed
** @exception Exception A number of exceptions can occur during parsing.
*/
public YYparse(String FOPLString) throws IOException, Exception {
  this(new YYlex(new ByteArrayInputStream(
      (FOPLString + ' ').getBytes())));
  yyparse();
}

/** 
** This constructor simplifies contructing a FOPL parser for an InputStream.
** The given InputStream is the String to be parsed. If a fresh set of global
** Variables should be used for this parse then <tt>Variable.newVars()</tt> 
** should be called before this constructor. Using this constructor will 
** automatically invoke parsing and the result will be stored in the staic
** variable <tt>parseResult</tt> of this class.
** @param FOPLIStream the InputStream from which to parse
** @exception Exception A number of exceptions can occur during parsing or
** reading from the Stream.
*/
public YYparse(InputStream FOPLIStream) throws IOException, Exception {
  this(new YYlex(FOPLIStream));
  yyparse();
}

private void yyverror(String s) throws ParseException {
  String errMsg = "FOPL parse error: line " + (yyloc.lineno()+1) + " ; " + 
      yyerror_verbose(s);
  throw new ParseException(errMsg);
}
  
static private Symbol EqualSy = Symbol.get("=");
