(* fol.grm
 *
 * COPYRIGHT (c) 1992 by AT&T Bell Laboratories.  See COPYRIGHT file for details.
 *
 * 
 *)

%%
%term     IDENT of string
	| NUM of int 
	| TIMES 
	| PLUS 
	| QUOTE
	| MINUS 
	| DIVIDE
	| NEG 
	| EQUAL 
	| AND 
	| OR 
	| IMPLIES 
	| DOT 
	| FORALL 
	| EXISTS 
	| COLON 
	| LPAREN 
	| RPAREN 
	| COMMA
	| LANGLE
	| RANGLE 
        | LEQ 
	| GEQ 
	| FORMPREFIX
	| TERMPREFIX
	| EOF
                            
%nonterm  START of Fol.form_or_term
	| FORM of Fol.form 
	| ATOMICFORM of Fol.form 
	| TERM of Fol.term 
	| TERMLIST of Fol.term list 

%eop EOF
%pos int
%name fol
%noshift EOF
%nodefault
%verbose
%left PLUS 
%right AND OR 
%right IMPLIES 
%pure 
%%

START : FORMPREFIX FORM (Fol.Form FORM) 	
      | TERMPREFIX TERM (Fol.Term TERM) 

TERM : IDENT (Fol.Var IDENT) 
     | NUM (Fol.IntTerm NUM)
     | LPAREN TERM RPAREN (TERM) 
     | TERM PLUS TERM (Fol.Fun(Fol.Constant "+",[TERM1,TERM2]))
     | TERM MINUS TERM (Fol.Fun(Fol.Constant "-",[TERM1,TERM2]))
     | TERM TIMES TERM (Fol.Fun(Fol.Constant "*",[TERM1,TERM2]))
     | TERM DIVIDE TERM (Fol.Fun(Fol.Constant "/",[TERM1,TERM2]))


TERMLIST : TERM ([TERM]) 
         | TERM COMMA TERMLIST (TERM :: TERMLIST)

FORM : ATOMICFORM (ATOMICFORM)
     | NEG ATOMICFORM (Fol.Conn("~",[ATOMICFORM]))
     | FORM AND FORM (Fol.Conn("&",[FORM1,FORM2])) 
     | FORM OR FORM (Fol.Conn("|",[FORM1,FORM2])) 
     | ATOMICFORM IMPLIES FORM (Fol.Conn("->",[ATOMICFORM,FORM])) 
     | EXISTS IDENT DOT FORM 
		(Fol.Quant("exists",[(IDENT1,Fol.IntType)],FORM)) 
     | FORALL IDENT DOT FORM 
		(Fol.Quant("forall",[(IDENT1,Fol.IntType)],FORM)) 


ATOMICFORM  
            : TERM EQUAL TERM (Fol.Pred("=",[TERM1,TERM2]) ) 
            | TERM LANGLE TERM (Fol.Pred("<",[TERM1,TERM2]) ) 
            | TERM RANGLE TERM (Fol.Pred(">",[TERM1,TERM2]) ) 
            | TERM GEQ TERM (Fol.Pred(">=",[TERM1,TERM2]) ) 
            | TERM LEQ TERM (Fol.Pred("<=",[TERM1,TERM2]) ) 
            | IDENT LPAREN TERMLIST RPAREN (Fol.Pred(IDENT,TERMLIST) )
            | LPAREN FORM RPAREN (FORM) 
     	    | IDENT QUOTE (Fol.Pred(IDENT ^ "'",[]) )

