mlyacc/examples/fol/fol.grm

   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               ()