2 %header (functor FolLrValsFun (structure Token : TOKEN
3 structure Absyn : ABSYN ) : Fol_LRVALS)
6 EOF | DOT | COMMA | SEMICOLON
8 | BACKARROW | DOUBLEARROW
10 | TRUE | FORALL | EXISTS
11 | PARSEPROG | PARSEQUERY
12 | LCID of string | UCID of string | INT of string
14 (* gform: goal formula
15 dform: definite clause *)
19 | clause | query | gform | dform
20 | atom | termlist | term | varbd | id
41 start : PARSEPROG clause (Absyn.null)
42 | PARSEQUERY query (Absyn.null)
51 | gform COMMA gform () (* and *)
52 | gform SEMICOLON gform () (* disjunction *)
53 | gform BACKARROW dform () (* implication: dform implies gform *)
54 | gform ARROW gform BAR gform () (* if-then-else *)
55 | FORALL varbd gform () (* universal quantification *)
56 | EXISTS varbd gform () (* existential quantification *)
57 | atom () (* atomic formula *)
58 | LPAREN gform RPAREN ()
61 | dform COMMA dform () (* and *)
62 | dform BACKARROW gform () (* gform implies dform *)
63 | FORALL varbd dform ()
65 | LPAREN dform RPAREN ()
68 | LCID LPAREN termlist RPAREN ()
71 | term COMMA termlist ()
75 | LCID LPAREN termlist RPAREN ()