|
RCL_basis.grm
|
// FILE. . . . . /cygdrive/c/cygwin/home/hak/ilt/src/ilog/rcl/RCL_Basis.grm // EDIT BY . . . Hassan Ait-Kaci // ON MACHINE. . 4j4zn71.Ilog.Biz // STARTED ON. . Mon Sep 18 12:45:58 2006 // Last modified on Tue Sep 19 19:08:22 2006 by hak
| This the root symbol of the core grammar dealing with only positive conditions. This is based on the revised version of Sept.10, 2006, by Harold Boley. |
////////////////////////////////////////////////////////////////////////
// Rules for CONDIT:
////////////////////////////////////////////////////////////////////////
// CONDIT ::= LITFORM | QUANTIF | CONJ | DISJ
CONDIT
: LITFORM
| $LITFORM$ stands for Literal Formula and anticipates the introduction of $Atom$s (or negated $Atom$s if negation is supported). |
| QUANTIF
| $QUANTIF$ stands for Quantified Formula, which for Horn-like conditions can only be '$Exists$' Formulas ($Var_plus$ variables should occur free in the scoped $CONDIT$, so '$Exists$' can quantify them). |
| CONJ
| $CONJ$ is a $CONDIT$ expressing conjunctions of formulae. |
| DISJ
| $DISJ$ is a $CONDIT$ expressing disjunctions of formulae. |
;
////////////////////////////////////////////////////////////////////////
// Rules for CONJ:
////////////////////////////////////////////////////////////////////////
// CONJ ::= 'And' '(' CONDIT* ')'
CONJ
: 'And' '(' CONDIT_star ')'
|
$CONJ$ represents conjunctions as prefixed '$And$' with zero or more
$CONDIT$ arguments.
Its XML serialization form is:
<rcl:And>
(XML serialization of $CONDIT_star$)
</rcl:And>
|
[ rcl:And 3 ] // XML serialization pattern
;
////////////////////////////////////////////////////////////////////////
// Rules for DISJ:
////////////////////////////////////////////////////////////////////////
// DISJ ::= 'Or' '(' CONDIT* ')'
DISJ
: 'Or' '(' CONDIT_star ')'
|
$DISJ$ represents disjunctions as prefixed '$Or$' with zero or more
$CONDIT$ arguments.
Its XML serialization form is:
<rclOr>
(XML serialization of $CONDIT_star$)
</rcl:Or>
|
[ rcl:Or 3 ] // XML serialization pattern
;
////////////////////////////////////////////////////////////////////////
// Rules for QUANTIF:
////////////////////////////////////////////////////////////////////////
// QUANTIF ::= 'Exists' Var+ '(' CONDIT ')'
QUANTIF
: 'Exists' Var_plus '(' CONDIT ')'
|
This represents an existentially quantified formula using
prefixed '$Exists$' followed by zero or more $Var$s and a
$CONDIT$ between parentheses.
Its XML serialization form is:
<rcl:Exists>
(XML serialization of $Var_plus$)
(XML serialization of $CONDIT$)
</rcl:Exists>
|
[ rcl:Exists 2 4 ] // XML serialization pattern
;
////////////////////////////////////////////////////////////////////////
// Rules for LITFORM:
////////////////////////////////////////////////////////////////////////
// LITFORM ::= Atom
LITFORM
: Atom
| An $Atom$ is a positive literal (i.e., a non negative $LITFORM$). |
;
////////////////////////////////////////////////////////////////////////
// Rules for Atom:
////////////////////////////////////////////////////////////////////////
// Atom ::= Rel '(' TERM* ')' | TERM '=' TERM
Atom
: 'Rel' '(' TERM_star ')'
|
An $Atom$ represents an atomic formula using a prefixed '$Rel$'
predicate symbol with zero or more $TERM$ arguments.
Its XML serialization form is:
<rcl:Rel>
(XML serialization of $TERM_star$)
</rcl:Rel>
|
[ rcl:Atom 1 3 ] // XML serialization pattern
| TERM '=' TERM
|
Equality is a special $Atom$ represented with infix '$=$' between
two $TERM$s.
Its XML serialization form is:
<rcl:Equal>
(XML serialization of lhs $TERM$)
(XML serialization of rhs $TERM$)
</rcl:Equal>
|
[ rcl:Equal 1 3 ] // XML serialization pattern ; //////////////////////////////////////////////////////////////////////// // Rules for TERM: //////////////////////////////////////////////////////////////////////// // TERM ::= Var | Con | Expr
A $TERM$ is one of:
|
TERM : 'Var'
| A $Var$ is a $TERM$ . |
| Con
| A $Con$ is a $TERM$ . |
| Expr
| An $Expr$ is a $TERM$ . |
;
////////////////////////////////////////////////////////////////////////
// Rules for Expr:
////////////////////////////////////////////////////////////////////////
// Expr ::= Fun '(' TERM* ')'
Expr
: 'Fun' '(' TERM_star ')'
An $Expr$ represents functional expressions using a prefixed
'$Fun$' function symbol with zero or more $TERM$ arguments. Its
XML serialization form is:
<rcl:Expr>
(XML serialization of $Fun$)
(XML serialization of $TERM_star$)
</rcl:Expr>
|
[ rcl:Expr 1 3 ] // XML serialization pattern ; //////////////////////////////////////////////////////////////////////// // Rules for starred, plussed, and optional non-terminals ... //////////////////////////////////////////////////////////////////////// CONDIT_star : /* empty */ | CONDIT_plus ; CONDIT_plus : CONDIT | CONDIT_plus CONDIT ; TERM_star : /* empty */ | TERM_plus ; TERM_plus : TERM | TERM_plus TERM ; Var_plus : 'Var' | Var_plus 'Var' ; ////////////////////////////////////////////////////////////////////////
This file was generated on Thu Oct 05 10:28:30 CEST 2006 from file RCL_basis.grm
by the ilog.language.tools.Hilite Java tool written by Hassan Aït-Kaci