[hcoop/debian/mlton.git] / mlyacc / examples / fol / fol.grm

%%
%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               ()
Commit	Line	Data
7f918cf1 CE	1	%%
	2	%header (functor FolLrValsFun (structure Token : TOKEN
	3	structure Absyn : ABSYN ) : Fol_LRVALS)
	4
	5	%term
	6	EOF \| DOT \| COMMA \| SEMICOLON
	7	\| LPAREN \| RPAREN
	8	\| BACKARROW \| DOUBLEARROW
	9	\| ARROW \| BAR
	10	\| TRUE \| FORALL \| EXISTS
	11	\| PARSEPROG \| PARSEQUERY
	12	\| LCID of string \| UCID of string \| INT of string
	13
	14	(* gform: goal formula
	15	dform: definite clause *)
	16
	17	%nonterm
	18	start of Absyn.absyn
	19	\| clause \| query \| gform \| dform
	20	\| atom \| termlist \| term \| varbd \| id
	21
	22	%start start
	23	%eop EOF DOT
	24	%pos int
	25	%verbose
	26	%pure
	27
	28	%right FORALL EXISTS
	29	%left BACKARROW
	30	%right SEMICOLON
	31	%right COMMA
	32	%right DOUBLEARROW
	33	%right ARROW
	34	%left BAR
	35
	36	%name Fol
	37
	38	%prefer DOT
	39	%%
	40
	41	start : PARSEPROG clause (Absyn.null)
	42	\| PARSEQUERY query (Absyn.null)
	43
	44	clause : dform ()
	45	\| ()
	46
	47	query : gform ()
	48	\| ()
	49
	50	gform : TRUE ()
	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 ()
	59
	60	dform : TRUE ()
	61	\| dform COMMA dform () (* and *)
	62	\| dform BACKARROW gform () (* gform implies dform *)
	63	\| FORALL varbd dform ()
	64	\| atom ()
65	\| LPAREN dform RPAREN ()
66
67	atom : LCID ()
68	\| LCID LPAREN termlist RPAREN ()
69
70	termlist : term ()
71	\| term COMMA termlist ()
72
73	term : id ()
74	\| INT ()
75	\| LCID LPAREN termlist RPAREN ()
76
77	varbd : LCID DOT ()
78	\| UCID DOT ()
79
80	id : LCID ()
81	\| UCID ()