DTC

Identifiers (denoted below as ID) are composed of letters, digits and underscores and have to begin with a letter.

Preprocessor

The preprocessor understands a subset of Prolog described with the following grammar:

      <program> ::= <program> <clause>
                  | <clause>
      <clause> ::= <predicate> "."
                 | <predicate> ":-" <predicate-alt> "."
      <predicate-alt> ::= <predicate-alt> ";" <predicate-con>
                        | <predicate-con>
      <predicate-con> ::= <predicate-con> "," <predicate-simple>
                        | <predicate-simple>
      <predicate-simple> ::= <predicate>
                           | "(" <predicate-alt> ")"
      <predicate> ::= ID "(" <term-list> ")"
                    | ID 
                    | "!"
                    | <term-relation>
      <term-relation> ::= VAR "is" <term>
                        | VAR "=" <term>
                        | VAR ">" <term>
                        | VAR "<" <term>
                        | VAR "<=" <term>
                        | VAR ">=" <term>
      <term-list> ::= <term-list> "," <term> | <term>
      <compound-term> ::= <term>
                        | <term> "+" <term>
                        | <term> "-" <term>
      <term> ::= VAR
               | "_"
               | ID
               | ID "(" <term-list> ")"
               | <list>
               | STRING
               | NUMBER
               | "(" <term-list> ")"
      <list> ::= "[" <term-list> "|" <term> "]" |
                 "[" <term-list> "]"

The preprocessor performs the following substitutions:

Replaces list syntactic sugar with cons and nil constructors.
Replaces numbers with the term number.
Replaces strings with the term string.
Adds tupleX constructors at the top of every predicate argument.
Replaces underscores with fresh variables.
Unfolds alternatives.
Replaces infix operators with constructors:
- a + b with plus(a,b)
- a - b with minus(a,b)
Replaces comparators with predicates:
- a = b with opeq(tuple2(a,b))
- a < b with opsm(tuple2(a,b))
- a > b with opgr(tuple2(a,b))
- a <= b with opse(tuple2(a,b))
- a >= b with opge(tuple2(a,b))
Ignores exclamations.

It is important to notice that type definitions may only use the core language, not the language understood by the preprocessor.

Type Definitions

Directional types are defined by tree automata. A file with type definitions contains only a list of transitions in the following format:

    f(s₁, s₂,...,s_n) is s₀.

where f is an n-ary function symbol and s₀,...,s_n are states of the automaton. The following grammar has to be obeyed:

     <transition-list> ::= <transition-list> <transition> | <transition>
     <transition> ::= <body> "is" ID "."
     <body> ::= ID "(" <state-list> ")" | ID
     <state-list> ::= <state-list> "," ID | ID

The set of states of the automaton is derived implicitly from the list of transitions. Additionally, the special state top is recognized by the parser as the sink-state. Formally speaking: if there exists no transition for some n-ary function symbol f and some states s₁,...,s_n, then the automaton gets extended with the following transition:

    f(s₁,...,s_n) is top.

Example

An example of a type definition:

     nil is list.
     cons (top, list) is list.

The above definition describes a tree automaton with the states top and list. The following terms are examples of terms recognized by the tree automaton with the accepting state list:

     nil
     cons (nil, nil)
     cons (zero, cons (zero, nil))
     cons (nil, cons (zero, nil))

One of the most important aspects of regular types is that there is no possibility of encoding parametric polymorphism.

Type Annotations

Type annotations need to be given in a separate file so you do not have to modify your source files. They have to respect the following grammar:

     <type-list> ::= <type-list> <type>
     <type> ::= ID ":" ID "->" ID "."

Type annotations define the accepting states of the automata for input and output types of the predicate.

Reference Manual

Preprocessor

Type Definitions

Example

Type Annotations