// 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 Thu Apr 05 20:52:24 2007 by hak

/**
 * This the root symbol of the core grammar dealing with only
 * <a href="http://www.w3.org/2005/rules/wg/wiki/A.1_Basis%3A_Positive_Conditions">
 * positive conditions</a>. 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.
     */
  // XML serialization info:
  [ NS:"rcl" LO:"and" CH:(3) ]
  ;

////////////////////////////////////////////////////////////////////////
// Rules for DISJ:
////////////////////////////////////////////////////////////////////////

// DISJ     ::= 'Or' '(' CONDIT* ')'

DISJ
  : 'Or' '(' CONDIT_star ')'
    /**
     * $DISJ$ represents disjunctions as prefixed '$Or$' with zero or more
     * $CONDIT$ arguments.
     */
  // XML serialization info:
  [ NS:"rcl" LO:"or" CH:(3) ]
  ;

////////////////////////////////////////////////////////////////////////
// Rules for QUANTIF:
////////////////////////////////////////////////////////////////////////

// QUANTIF  ::= 'Exists' Var+ '(' CONDIT ')'

QUANTIF
  : 'Exists' Var_plus '(' CONDIT ')'
    /**
     * This represents an existentially quantified formula using the
     * quantifier prefix '$Exists$' followed by one or more $Var$s and a
     * $CONDIT$ between parentheses.
     */
  // XML serialization info:
  [ NS:"rcl" LO:"quantifier" AT:{kind="existential"} CH:(2 4) ]
  ;

////////////////////////////////////////////////////////////////////////
// Rules for LITFORM:
////////////////////////////////////////////////////////////////////////

// LITFORM  ::= Atom

LITFORM
  : Atom
    /**
     * An $Atom$ is a positive literal (<i>i.e.</i>, 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.
     */
  // XML serialization info:
  [ NS:"rcl" LO:"atom" CH:(1 3) ]

  | TERM '=' TERM
    /**
     * Equality is a special $Atom$ represented with infix '$=$' between
     * two $TERM$s.
     */
  // XML serialization info:
  [ NS:"rcl" LO:"equal" CH:(1 3) ]
  ;

////////////////////////////////////////////////////////////////////////
// Rules for TERM:
////////////////////////////////////////////////////////////////////////

// TERM     ::= Var | Con | Expr

/**
 * A $TERM$ is one of:
 * <dl>
 *
 * <dt>$Var$</dt>
 * <dd>denoting a logical variable,</dd>
 *
 * <dt>$Con$</dt> <dd>denoting a constant as numbers, characters,
 * strings, IRIs, etc., ...,</dd>
 *
 * <dt>$Expr$</dt>
 * <dd>denoting an complex expression.</dd>
 *
 * </dl>
 */

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.
     */
  // XML serialization info:
  [ NS:"rcl" LO:"expression" CH:(1 3) ]
  ;

////////////////////////////////////////////////////////////////////////
// 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'
  ;

////////////////////////////////////////////////////////////////////////