%%
%header (functor FolLrValsFun (structure Token : TOKEN
			       structure Absyn : ABSYN ) : Fol_LRVALS)

%term
    EOF | DOT | COMMA | SEMICOLON
  | LPAREN | RPAREN
  | BACKARROW | DOUBLEARROW
  | ARROW | BAR
  | TRUE | FORALL | EXISTS
  | PARSEPROG | PARSEQUERY
  | LCID of string | UCID of string | INT of string

(* gform: goal formula
   dform: definite clause *)

%nonterm 
    start of Absyn.absyn
  | clause | query | gform | dform
  | atom | termlist | term  | varbd | id

%start start
%eop EOF DOT
%pos int
%verbose
%pure

%right FORALL EXISTS
%left BACKARROW
%right SEMICOLON
%right COMMA
%right DOUBLEARROW
%right ARROW
%left BAR

%name Fol

%prefer DOT
%%

start : PARSEPROG clause (Absyn.null)
      | PARSEQUERY query (Absyn.null)

clause : dform 			()
       |			()

query : gform			()
      |				()

gform : TRUE			()
      | gform COMMA gform	()      (* and *)
      | gform SEMICOLON gform   ()      (* disjunction *)
      | gform BACKARROW dform   ()      (* implication: dform implies gform *)
      | gform ARROW gform BAR gform ()  (* if-then-else *)
      | FORALL varbd gform	()	(* universal quantification *)
      | EXISTS varbd gform	()      (* existential quantification *)
      | atom			()	(* atomic formula *)
      | LPAREN gform RPAREN     ()      

dform : TRUE		        ()
      | dform COMMA dform	()      (* and *)
      | dform BACKARROW gform   ()	(* gform implies dform *)
      | FORALL varbd dform	()
      | atom			()
      | LPAREN dform RPAREN	()

atom : LCID			()
     | LCID LPAREN termlist RPAREN  ()

termlist : term		()
	 | term COMMA termlist  ()

term : id		()
     | INT		()
     | LCID LPAREN termlist RPAREN ()

varbd : LCID DOT	()
      | UCID DOT	()

id : LCID		()
   | UCID		()

