Syntax and Informal Semantics of CCalc Input Files

A CCalc input file consists of

declarations, rules, queries, directives, and comments.

These elements can appear in any order. Every element except for comments ends with a period.

The syntax of these elements is defined below, mostly using EBNF notation. The following symbols belong to EBNF notation: 

::=, |, [ ], { }.
The vertical bar expresses disjunction, the square brackets mean that what they enclose is optional, and the braces are used for grouping. Nonterminals begin with a capital letter. Many of the parentheses in this grammar can be dropped due to operator precedences.

1. Identifiers and Integers

 An identifier is a sequence of letters, digits and underscores that begins with a letter.

An integer is a whole number in the usual decimal notation, such as 5 or -20. Extended integers are expressions that are evaluated to integers in the process of operation of CCalc. They have the following syntax: 

ExtendedInteger ::= Integer | maxstep | - ExtendedInteger
                    | ( ExtendedInteger { + | - | * | // | mod } ExtendedInteger )
The second operand of // (which stands for integer division) and the second operand of mod must have nonzero values.

2. Declarations

 A declaration assigns an identifier, or each of several identifiers, to one of 6 groups:

sorts, objects, constants, variables, tests, and macros.

If a symbol is declared more than once then all its declarations must put it in the same group. The first declaration of an identifier must occur before its first use. Certain reserved words and predeclared identifiers cannot be declared.

Every declaration begins with :- followed by the name of the group and by a tuple of one of more elements separated by semicolons. If the tuple consists of several elements then the declaration has the same meaning as several declarations, each containing one element. For instance, the declaration 

:- variables
  B,B1				:: block;
  L				:: location.
has the same meaning as two declarations 
:- variables
  B,B1				:: block.
:- variables
  L				:: location.

2.1. Sorts

 A sort represents a set of objects. The expression a >> b expresses that a and b are sorts and that b is a subsort of a. For instance, the declaration 
:- sorts
  index;
  location >> block >> ( smallBlock ; largeBlock ).
expresses that there are five sets of objects -- indices, locations, etc. -- and also that every block is a location, every smallBlock is a block, and every largeBlock is a block.

Sorts are denoted by identifiers, and their declarations have the following syntax: 

SortDeclaration ::= :- sorts SortSpecTuple .
SortSpecTuple ::= SortSpec |
                  ( SortSpecTuple ; SortSpecTuple )
SortSpec ::= SortIdentifier
             | ( SortIdentifier >> SortSpecTuple )
SortIdentifier ::= Identifier
Two sorts are standard in CCalc:
boolean The objects of this sort are false and true.
step The objects of this sort are the nonnegative integers that are less than or equal to maxstep.

2.2. Objects

 An object declaration describes expressions of certain syntactic forms as objects and specifies the sorts of these objects. For instance, the declaration 
:- objects
  table      :: location;
  1..10      :: index;
  box(index) :: block.
expresses that table is an object of sort location, that numbers 1,...,10 are objects of sort index, and that the identifier box followed by an object of sort index enclosed in parentheses is an object of sort block. 
ObjectDeclaration ::= :- objects ObjectSpecTuple .
ObjectSpecTuple ::= ObjectSpec
                    | ( ObjectSpecTuple ; ObjectSpecTuple )
ObjectSpec ::= ( ObjectSchemaList :: SortIdentifier )
ObjectSchemaList ::= ObjectSchema
                     | ( ObjectSchemaList , ObjectSchemaList )
ObjectSchema ::= ExtendedInteger
                 | ( ExtendedInteger .. ExtendedInteger )
                 | ObjectIdentifier [ ( SortIdentifierList ) ]
SortIdentifierList ::= SortIdentifier
                       | ( SortIdentifierList ,  SortIdentifierList )
SortIdentifier ::= Identifier
A set of object declarations and a set of sort declarations characterize the set of objects represented by each of the sorts. For instance, given the object declarations and the sort declarations in the examples above, the set of locations is 
box(1), ..., box(10), table.
The set of object declarations in a CCalc input file must be acyclic. For instance, 
next(index) :: index
is not allowed. The acyclicity condition guarantees that the set of objects of each sort is finite.

2.3. Variables

 A variable declaration describes an identifier, or each of several identifiers, as a schematic variable for objects of a certain sort. Variables are global. If a variable is declared more than once then it should be assigned the same sort in all its declarations. 
VariableDeclaration ::= :- variables VariableSpecTuple .
VariableSpecTuple ::= VariableSpec
                    | ( VariableSpecTuple ; VariableSpecTuple )
VariableSpec ::= ( VariableList :: SortIdentifier )
VariableList ::= VariableIdentifier
                     | ( VariableList , VariableList )
VariableIdentifier ::= Identifier

2.4. Constants

 A constant declaration describes expressions of certain syntactic forms as constants and specifies the domains of these constants. For instance, the declaration 
:- constants
  unlimitedResources  :: boolean;
  loc(block)          :: fluent(location).
expresses that the identifier unlimitedResources is a boolean constant, and that the identifier loc followed by an object of sort block enclosed in parentheses is a simple fluent constant whose domain is the set of locations.

Syntactically, one of the differences between an object declaration and a constant declaration is that the symbol :: in a constant declaration can be followed not only by a sort, such as boolean, but also by a composite sort, such as fluent(location). As another example of the use of composite sorts, we can declare a boolean statically determined fluent constant using the composite sort sdFluent(boolean), or simply sdFluent, because of the convention that the part (boolean) in a composite sort can be dropped. It is convenient to allow such composite sorts as rigid(location); this expression has the same meaning as sort identifier location.

A composite sort can be also used to declare an attribute of an action, for instance: 

:- constants
  destination(block) :: attribute(location) of move(block).
This declaration tells us that identifier destination followed by an object of sort block enclosed in parentheses is an action constant whose domain consists of the locations and the predeclared object na ("not applicable"). Furthermore, it tells us that this action constant is an attribute of the action of moving that block. 
ConstantDeclaration ::= :- constants ConstantSpecTuple .
ConstantSpecTuple ::= ConstantSpec
                      | ( ConstantSpecTuple ; ConstantSpecTuple )
ConstantSpec ::= ( ConstantSchemaList :: { SortIdentifier | CompositeSort } )
ConstantSchemaList ::= ConstantSchema
                       | ( ConstantSchemaList , ConstantSchemaList )
ConstantSchema ::= ConstantIdentifier [ ( SortIdentifierList ) ]
CompositeSort ::= rigid [ ( sortIdentifier ) ]
                  | fluent [ ( sortIdentifier ) ]
		  | sdFluent [ ( sortIdentifier ) ]
                  | inertialFluent [ ( sortIdentifier ) ]
                  | action [ ( sortIdentifier ) ]
                  | attribute [ ( sortIdentifier ) ] of ConstantSchema
In an attribute declaration, the ConstantSchema must satisfy two conditions. First, its ConstantIdentifier must be a boolean action constant. Second, its SortIdentifierList, if any, should be a prefix of the SortIdentifierList in each ConstantSchema that is being declared.

2.5. Tests

 A test declaration describes certain identifiers as "test predicates" and specifies for each of these predicates its arity and the name of the file where the Prolog definition of that predicate can be found. For instance, the declaration 
:- tests
  even/1 :: 'tests.pl'.
expresses that even is a unary predicate defined in file tests.pl. 
TestDeclaration ::= :- tests TestSpecTuple .
TestSpecTuple ::= TestSpec |
                  ( TestSpecTuple ; TestSpecTuple )
TestSpec ::= TestList :: ' Filename '
TestList ::= TestIdentifier / Arity
             | ( TestList , TestList )
TestIdentifier ::= Identifier
Arity ::= Integer

2.6. Macros

3. Rules

4. Queries

5. Directives

 There are 2 kinds of directives: include and show. Every directive begins with :- followed by one of these reserved words.

5.1. Include

The include directive is used to include files during loading. The syntax is as follows.

IncludeDirective ::= :- include PathnameTuple .
PathnameTuple ::= ' Pathname ' | ( PathnameTuple  ; PathnameTuple )
Pathname is the name of a file.

5.2. Show

6. Comments

 A comment is the text appearing on a line following a % or appearing on one or more lines between /* and */.

7. Reserved Words and Predeclared Identifiers

The following identifiers are reserved words in the language of CCalc:
action
after
anyAction
anyFluentValues
anyInitialState
attribute
cause
caused
causes
constants
constraint
cwaActions
default
exogenous
fluent
inertial
inertialFluent
if
include
 label
macros
may
maxstep
mod
never
nonexecutable
objects
of
possibly
query
rigid
sdFluent
show
sort
sorts
tests
variables
where
The following identifiers are predeclared:
boolean sort
false object of sort boolean
maxstep object of sort step
na object
step sort
true object of sort boolean