6. Program Structure and Syntax in Teyjus

Programming in Lambda Prolog is structured around the definition of modules. In Teyjus, there are three files associated with a module. If the name of the module is <modname> then these files are <modname>.mod, <modname>.sig and <modname>.lp, and they correspond, respectively, to the source code, the signature and the bytecode file generated by the compiler for the module. The user of Teyjus is not concerned with the internal structure of the bytecode file and it suffices for him/her to know merely of its existence. It is necessary, however, to understand the structure and purpose of the signature and source code file in order to produce meaningful Lambda Prolog programs that can be compiled and executed under Teyjus. This chapter presents the structure of these two kinds of objects. Before looking at the syntactic aspects, however, it is useful to understand the intended roles of these two kinds of objects in programming.

Signatures are associated with a module to determine an external view for it. In particular, a signature identifies names of sorts, type constructors, constants and operators and also might indicate that certain predicates are to be used in the module without changes in their definitions or that a fixed definition for these predicates is to be exported from that module. Signatures are eventually employed in two ways: (a) when a module is being compiled, the signature is used to determine whether the module is "living up to its promise" and also to qualify some of the declarations in the module and (b) when some other module imports or accumulates this one, the signature determines what is externally visible and hence plays a role in certifying the module interactions.

Two technical terms are used in the above paragraph to describe possibilities for module interactions: importing and accumulating. We pause briefly to explain these kinds of interactions. Importation is a process by which the globally visible procedures defined in a particular module become dynamically available in solving the bodies of procedures in another module. Note that actual interactions of this kind manifest themselves only at loading and execution time. Modules that interact through importation are in fact compiled separately in Teyjus, with signatures being used to ensure compatibility and to determine load-time actions and run-time interactions. Accumulation, on the other hand, is mainly a compile-time process: it calls for the accretion of the code in other independently defined modules into a new, larger, module. The vision that accumulation is intended to evoke is that of static inlining of code. However, the inlining is not entirely naive. In Lambda Prolog it is possible to scope constant names and procedure definitions over modules. For names, this is achieved via the notion of a local constant: any constant that is not defined in the signature form the module is interpreted as being local. For procedures, this is manifest in the scopes of imports (and also in explicit implication goals). The inlining corresponding to accumulation is to be done in a way that respects scopes. In particular, locals in an accumulated module are to be treated as being distinct even if there is a coincidence in names with the constants in another accumulated module or in the accumulating module. Similarly, imports in an accumulated module have only the code originating in that module as their scope.

The precise way in which signatures fulfill their intended roles is manifest in the notions of matching a module declaration with its signature and of certifying interactions via imports and accumulates. These notions are explained in more detail in this chapter after a presentation of the syntax of signatures and modules supported by Teyjus.

6.1 Characterization of Tokens in Teyjus

We describe below the rules for recognizing tokens in the different relevant categories. Two points are relevant to mention prior to this description. First, as is standard, the principle of longest match is used in tokenization. The Teyjus lexical analyzer is in fact generated by flex, based on a regular grammar presentation of the tokens and token categories below. Second, a far fewer set of characters are treated as token separators than is usual. In particular, only the characters identified as punctuation symbols are interpreted in this manner over and above `white space' characters. To take a specific example, a sequence such as X+Y is interpreted as a token as opposed to a sequence of three tokens.

6.1.1 Keywords

The following sequences of characters are recognized as tokens with a special meaning within Teyjus.

module     end          import     accumulate     accum_sig   
local      localkind    closed     sig            
kind       type         exportdef  useonly        infixl 
infixr     infix        prefix     prefixr        postfix 
postfixl   :-           \          ->             !

6.1.2 Other Special Tokens in Teyjus

The following tokens are ones that, in addition to the keywords and punctuation symbols, cannot be redefined by user programs. Some of these symbols--in particular, the symbols pi, sigma, ;, &, =>, =, :: and nil--are constants and are like other identifiers except for the `no redefinition' clause. The remaining symbols are overloaded and so are treated in a special way by the parser. Finally, some symbols, in particular :: and nil, receive a special treatment at the abstract machine level.

pi         sigma        ,          ;              &
=>         +            -          *              /
~          <            >          =<             >=
::         =            nil

6.1.3 Punctuation Symbols

The following symbols serve as delimiters, grouping symbols, etc. Notice that comma appears in the list of pseudo keywords as well; usage is determined by context.

.          ,            (          )              :  
[          ]            | 

6.1.4 Identifier and Variable Names

Any contiguous sequence of alphanumeric or sign characters different from the punctuation characters (i.e. any of the characters +-*/\^<>=`'~?@#$&!_~) that begins with something other than a digit or the sequence /* constitutes a name. A name that begins with anything other than the underscore character may be used as that of a variable bound by an abstraction. Names other than those that begin with the underscore (_) character or an uppercase letter and those included in the special tokens category may be identified as constants through type declarations or sorts or type constructors through kind declarations. Such names are also interpreted as those of (local, undeclared) constants if they are used in clauses without a previous type declaration and they are not bound by enclosing abstractions. A name that begins with the underscore character or with an uppercase letter and that is not bound by an abstraction is considered to be that of a free (implicitly existentially quantified) variable.

Three points should be noted with regard to this definition. First, as already observed and unlike in most other languages, certain characters (like -, *, etc) are not treated as token separators in addition to being tokens. Thus, X-Y is a single token and not a sequence of three tokens. Second, some token sequences such as => and -> appear to be ambiguous, qualifying to be either keywords or names. This ambiguity is resolved by deeming the keyword interpretation to take precedence in all such cases. Finally, some names, such as pi and ::, are treated as special (overloaded or predefined) tokens and these cannot be reinterpreted through type declarations.

6.1.5 Integer Literals

A sequence of digits is recognized as an integer constant. As usual, there are size limitations on integers. In the present implementation, the limitation is that the integer should fit in 25 bits.

6.1.6 Real Literals

A sequence of digits followed by a period and then a sequence of digits is recognized as a real constant. The sequence before the period may be empty but the sequence after the period must be nonempty. There are size and precision restrictions that arise in the present implementation first from the limitations of the implementation language (double in C) and then from those of the abstract machine. The latter are likely to be dominant and are the following: the exponent must fit in 7 bits and the mantissa in 15 bits.

6.1.7 String Literals

These are character sequences enclosed within two double quotes. We permit a mix of SICSTUS and ML syntax for strings. In particular:

A string constant is a sequence enclosed between quotes of zero or more printable characters numbered 33-126, spaces or escape sequences. All escape sequences barring one start with the character \ and stand for a character sequence. The escape sequences are:

     \a       Alert (ASCII 0x07)
     \b       Backspace (ASCII 0x08)
     \t       Horizontal tab (ASCII 0x09)
     \n       Linefeed or newline (ASCII 0x0A)
     \v       Vertical tab (ASCII 0x0B)
     \f       Form feed (ASCII 0x0C)
     \r       Carriage return (ASCII 0x0D)
     \e       Escape (ASCII 0x1B)
     \d       Delete (ASCII 0x7F)
     \\       Backslash
     \"       Double quote
     \^c      A control character whose encoding is C mod 32, where C is the 
              encoding of the character c, with C in the range [64,122].
     \ddd     The character whose encoding is the number ddd, three decimal digits
              denoting an integer in the range [0,255].
     \xhh     The character whose encoding is the number hh, two hexadecimal digits,
              with a-f (A-F) denoting the `digits' 10-15 respectively. 
     \f...f\  This sequence is ignored, where f...f stands for a sequence of one
              or more formatting characters (that are currently restricted to 
              horizontal and vertical tab, whitespace, newline and carriage return).
     \c...    where ... stands for a sequence of formatting characters, ending with
              a non formatting character. 
              This sequence is to be ignored.

In the escape sequences involving decimal or hexadecimal digits, the sequence of digits is taken to be the longest sequence of such characters.

The exceptional escape sequence is ""; this stands for a " included inside the string literal.

6.1.8 The Syntax for Comments

Two styles for writing comments are supported. Multiline comments may be enclosed within a matched pair of /* and */; nesting of comments is legal. Single line comments are preceded by % and extend to the end of the line.

6.2 The Structure of a Signature File

The Teyjus parser for signatures is automatically generated by bison from a context-free grammar and a post processor that manipulates the (pre) abstract syntax structures generated from the grammar. The post processing phase is needed to handle information such as arities of type constructors that is also gleaned through the parse. The grammar below represents the effect of the combined processing and, therefore, differs from the one presented to bison.

6.2.1 A BNF Specification of Signature Syntax

<Signature>    ::=   <SigHeader> <SigPreamble> <Sign-Decls> <SigEnd>

<SigHeader>    ::=   'sig' <NameToken> '.'

<SigEnd>       ::=   'end' | '$'                 % $ stands for eof

<SigPreamble>  ::=   <Empty>
                   | accum_sig <NameTokens> '.' <SigPreamble>

<NameTokens>   ::=   <NameToken>
                   | <NameToken> ',' <NameTokens>

<Sign-Decls>   ::=   <Empty>
                   | <Sign-Decl> <Sign-Decls>

<Sign-Decl>    ::=   'kind'  <Ids>  <Kind> '.'
                   | 'type'  <Ids>  <Type> '.'
                   | <Fixity> <Ids> <SmallInt> '.'
                   | 'exportdef' <Ids> '.' 
                   | 'exportdef' <Ids> <Type> '.'
                   | 'useonly' <Ids> '.' 
                   | 'useonly' <Ids> <Type> '.'

<Ids>          ::=   <Id>
                   | <Id> ',' <Ids>

<Kind>         ::=   'type'
                   | 'type' '->' <Kind>

<Type>         ::=   <CType> '->' <Type>
                   | <CType>

<CType>        ::=   <NameToken>
                   | <TyCIdent> <CTypes>
                   | '(' <Type> ')'

<TyCIdent>     ::= <Id>

<CTypes>       ::=   <CType>
                   | <CType> <CTypes>

<Fixity>       ::=   'infixl' | 'infixr' | 'infix'
                   | 'prefix' | 'prefixr'
                   | 'postfix' | 'postfixl'

<NameToken>    ::=  { Any Teyjus token distinct from keywords,
                        pseudo-keywords, integer, string and real
                        literals }

<Id>           ::=  { Like NameToken, except that the token should 
                       also begin with something different from an 
                       uppercase letter and _ }
                       
<SmallInt>     ::=  { Integer value between 0 and 255; i.e. unsigned 
                     one byte number }

<Empty>        ::=  { empty token sequence }

6.2.2 Commentary on Signature Syntax

The declarations in a signature file must satisfy certain properties in addition to being derivable from the grammar rules:

• Each signature is expected to be presented in a distinct file. This file must have the name <modname>.sig where <modname> is the name of the relevant module and signature. This name should also coincide with the name indicated in the signature header, generated by the rule for <SigHeader>.
• The intended effect of accum_sig declarations is to include the declarations in the named signatures in the signature being generated from the text in the present file. Thus, accum_sig functions in a manner similar to #include in C. The possible interactions between sibling accumulated signatures and the accumulating signature are discussed further below.
• Kind declarations are those expressions in the category <Sign-Decl> that begin with the token kind. The purpose of these declarations is to identify sorts and type constructors that may be used in determining types for constants and variables. Thus a declaration of the form

  kind foo type -> ... -> type

  with n+1 occurrences of type identifies foo as a type constructor of arity n. (If n is 0 the object identified is a sort.) Note that there are restrictions built into the grammar rules on the syntax of tokens that can be identified as sorts and type constructors.

• Type declarations are those expressions in the category <Sign-Decl> that begin with the token type. Type declarations identify term constants with their associated types. Note that the constants for which types can be so declared have a limited syntax. In particular, they should not begin with an uppercase letter or the underscore (_) character.
• Type expressions are constructed, as usual, from type constants (sorts and type constructors), type variables and the arrow type constructor written as ->. Tokens appearing in such expressions are classified as a type variables or a type constants depending on whether or not it begins with an uppercase letter or the underscore (_) character. In understanding the structure of potentially ambiguous type expressions, the following convention is to be used: the application of a type constructor to types is left associative and has higher precedence than the construction of an arrow type; i.e. (tc ty1 ... tyn -> sort) is read as ((...(tc ty1)...tyn) -> sort).
• All sorts and type constructors that appear in type expressions must be either built-in or defined in the signature or defined in an accumulated signature and should have the arity required of them at the point of use. A sort or type constructor that is used in an accumulated signature and that is not defined there but is defined in a sibling accumulated signature may or may not be flagged as an error; the precise behavior is depended on the order of accumulation that is undefined at the language description level.
• Operator declarations are those expressions in the category <Sign-Decl> that are further characterized by the form

  <Fixity> <Ids> <SmallInt> '.'

  Such declarations identify relevant (term) constants as being infix, prefix or postfix operators that are not associative, left associative or right associative and having a specified precedence. Types of constants that are defined as operators must be consistent with their interpretation as such.

• Exportdef and useonly declarations are expressions in the <Sign-Decl> category that begin with the tokens exportdef and useonly, respectively. exportdef and useonly declarations must pertain to predicate constants only, i.e. constants with a target type o. exportdef declarations identify the relevant constants as ones whose definitions emanating from the module associated with the signature must not change. useonly declarations play a complementary role: these identify predicates that might be used in the module associated with the signature but whose definitions cannot be further refined there. exportdef and useonly declarations can also identify types with the relevant constants. In this case, the type expressions must satisfy all the requirements required of them relative to type declarations of the usual form.
• There must be at most one type, one kind and one fixity identification per Id. There might be multiple declarations for this Id but all must agree eventually. Also, no predicate should be defined both useonly and exportdef in any given module.
• The arities of sorts/type constructors in usage must be consistent with that in declaration.
• Fixity declarations must be for constants defined in the signature.

6.3 The Structure of Source Code for a Module

We describe here the structure of declarations constituting the source code for a module that is contained in a file called <modname>.mod. As already explained, this source code file goes hand-in-hand with the signature file for the module and requires the latter to be used in its interpretation.

The Teyjus parser for the source code file consists of a part automatically generated by bison from a context-free grammar and a post processor that manipulates the (pre) abstract syntax structures generated by the bison based parser. The post processing phase is needed to handle information such as arities of type constructors and operator fixities and precedence that is also gleaned through the parse. The grammar below represents the effect of the combined processing and differs for this reason from the one presented to bison.

6.3.1 A BNF Specification of Module Syntax

The rules below describe the syntax of the declarations that may appear in a module file. These grammar rules build on the ones already presented while explaining the syntax of signatures in A BNF Specification of Signature Syntax. Thus, to understand this grammar, it may be necessary to consult also the grammar for signatures.

<Module>        ::=  <ModHeader> <ModPreamble> <ModBody> <ModEnd>

<ModHeader>     ::=  'module' <NameToken> '.'

<ModEnd>        ::=  '$'                        % $ stands for eof
                   | 'end' 

<ModPreamble>   ::=  <Empty>
                   | 'import' <NameTokens> '.' <ModPreamble>
                   | 'accumulate' <NameTokens> '.' <ModPreamble>
                   | 'accum_sig' <NameTokens> '.' <ModPreamble>

<ModBody>       ::=  <Empty> 
                   | <ModSignDecl> <ModBody>
                   | <ModClause> <ModBody>

<ModSignDecl>   ::=  <Sign-Decl>
                   | 'local' <Ids> '.'
                   | 'local' <Ids> <Type> '.'
                   | 'localkind' <Ids> '.'
                   | 'localkind' <Ids> <Kind> '.'
                   | 'closed' <Ids> '.'
                   | 'closed' <Ids> <Type> '.'

<ModClause>     ::=  <Clause> '.'

<Clause>        ::=  <Atom>
                   | <Clause> ':-' <Goal>
                   | <Goal> '=>' <Clause>
                   | <Clause> ',' <Clause>
                   | <Clause> '&' <Clause>
                   | <PiId> <TypedId> '\' <Clause>
                   | <PiId> <CTerm>
                   | '(' <Clause> ')'

<Goal>          ::=  '!'
                   | <PiId> <Term>
                   | <PiId> <TypedId> '\' <Goal>
                   | <SigmaId> <Term>
                   | <SigmaId> <TypedId> '\' <Goal>
                   | <Goal> ';' <Goal>
                   | <Goal> ',' <Goal>
                   | <Goal> '&' <Goal>
                   | <Clause> '=>' <Goal>
                   | <Atom>
                   | <FlexAtom>
                   | '(' <Goal> ')'


<Atom>          ::=  <Term>    { the type of the term must be boolean
                                 and its main functor must be a constant
                                 or a variable bound by an enclosing
                                 essential universal quantifier }

<FlexAtom>      ::=  <TypedVar>
                   | <FlexAtom> <AppTerm>
                   | '(' <FlexAtom> ')'


<CTerm>         ::=  <Term>    { The main functor of the term must be a 
                                 constant or a variable bound by an
                                 enclosing essential universal 
                                 quantifier }

<Term>          ::=  <Term> <TypedCIdent> <Term>   
                   | <Term> <TypedCIdent>          
                   | <TypedCIdent> <Term>          
                   | <Term> <Term>
                   | <TypedId> '\' <Term>
                   | '[' ']'                    % Prolog list notation
                   | '[' TermList '|' Term ']'  % Prolog list notation
                   | <TypedCIdent>
                   | <TypedVar> 
                   | <TypedId>
                   | '(' <Term> ')'

<TermList>      ::=  <Term>
                   | <Term> ',' <TermList>

<PiId>          ::=  'pi'
                   | 'pi' ':' <Type>
                   | '(' <PiId> ')'

<SigmaId>       ::=  'sigma'
                   | 'sigma' ':' <Type>
                   | '(' <SigmaId> ')'

<TypedId>       ::=  <AbsToken>
                   | <AbsToken> ':' <Type>
                   | '(' <TypedId> ')'

<TypedVar>      ::=  <VIdent>
                   | <VIdent> ':' <Type>
                   | '(' <TypedVar> ')'

<TypedCIdent>   ::=  <SpecialOp>
                   | <Id>
                   | <Id> ':' <Type>
                   | '(' <TypedCIdent> ')'

<SpecialOp>     ::=  { A pseudo keyword corresponding to one of the 
                        overloaded operators }

<AbsToken>      ::=  { A <NameToken> that does not begin with _ }

<VIdent>        ::=  { A Teyjus token that begins with an uppercase
                        letter or _ and that is not the variable bound
                        by an enclosing abstraction }

6.3.2 Commentary on Module Syntax

The module declaration must satisfy certain properties in addition to adhering to the syntax rules:

• Each module is expected to be presented in a distinct file. This file must have the name <modname>.mod where <modname> is the name of the relevant module and the associated signature. This name should also coincide with the name indicated in the module header, generated by the rule for <ModHeader>.
• Accumulates, Imports and and AccumSig declarations are those appearing in the module preamble (i.e. generated by the rule for <ModPreamble>) and beginning with the tokens accumulate, import and accum_sig respectively. AccumSig declarations have a similar role in module declarations to the one they have in signature declarations. Accumulates and Imports have been explained informally in the preamble to the presentation of Teyjus syntax. This informal description is further bolstered elsewhere by an explanation of the rules for certifying module interactions.
• Local constant and local kind declarations are those in the category <ModSignDecl> that begin with the tokens local and localkind respectively. These declarations identify constants and kinds that are to be treated as being scoped within the module in which they appear and those that are imported and accumulated by this module.
• Closed constant declarations are those in the category <ModSignDecl> that begin with the token closed. Every closed constant must be of predicate type. From an outward perspective, these constants behave like exportdef constants: their definitions are exported from the module in question and the cannot be changed in the importing or accumulating context. From an inward perspective, these constants are ones for which an assurance can be given of fixity of code. Thus, they should either be defined as useonly or they should not be globals in imported modules reachable through some chain of accumulates.
• There is some redundancy in module syntax. In particular, exportdef, useonly, local and localkind declarations may be left out; the former two must also appear in the explicit signature file and locals can be taken to be the complement of the sorts, type constructors and constants defined in the explicit signature file. However, they are included in the syntax of modules to permit a preprocessing phase that calculates the explicit signature. (This is not the preferred situation though; signature files are intended to be useful in the certification of module interactions and not an obstacle to be surmounted in whichever way possible.)
• The name of a predicate defined by a clause that appears at the top level in the module or in the antecedent of an implication goal must not be identical to that of a logical symbol or a useonly predicate. It must not also be identical to that of a built-in predicate unless the predicate name has been redefined through a type declaration.
• There must be at most one arity and type associated with any given Id. There might be multiple declarations for this Id but all must agree eventually.
• In the form

  <Term> <TypedCIdent> <Term>

  that appears in the rules for <Term>, the identifier must have been declared as an infix operator. Similarly, in the form

  <Term> <TypedCIdent>

  that appears in the rule for <Term>, the identifier must have been declared as a postfix operator and in the form

  <TypedCIdent> <Term>

  the identifier should have been declared as a prefix operator. The rule for <Term> is obviously ambiguous as written. Disambiguation is to be affected using the precedence and associativity of the relevant operators. In this context, it is also to be noted that abstraction and application are treated like (infix) operators, that application is left associative and has higher precedence than all other operators and abstraction is right associative and has lower precedence than all other operators.

• The comma (',') token is overloaded in many different ways. One place where this overloading causes ambiguity is in terms embedded within Prolog style lists: here it can either be interpreted as the (infix) conjunction operator or as a list separator. The intended disambiguation device in this context is the following: if both the left and the right hand side of the comma operator has the ground type o, then this is interpreted as the symbol for conjunction, otherwise it is understood to be the list separator. Of course, the reading of comma as the conjunction operator can be forced by surrounding the expression within parentheses. For example, in

  [ p,(q,r),s]

  the middle comma is forced to be interpreted as conjunction. In the other direction, if p, q and r are of predicate type, we may want to construct a list that has these three as elements. This cannot be forced using the Prolog-style list notation; the list

  [p, q, r]

  will only be read as a singleton list. However, to depict such a list, we can use :: and nil based representation instead.

• The arithmetic operators like +, * and - and the comparison operators <, =<, > and >= are also overloaded. Teyjus requires that one of the operands of these operators must be recognizably of ground type. If this is not the case, an error is signalled. This requirement is a little stringent: particular subexpressions may not have this property but, in the end, it may still be possible to determine a specific type for the overall expression. This treatment will have to be rethought in a new version of the system
• There are the usual typing restrictions on well-formedness.
• The constants representing implication are not permitted to appear embedded inside terms.
• Signature files should exist for accumulated and imported modules and accumulated signatures. Source code files should exist for accumulated modules.
• We can calculate a signature from the source code for a module by taking the type, kind and fixity declarations in a module, adding to these the accumulated signatures and signatures of accumulated and imported modules and removing all the declarations corresponding to local constants and localkind types. The type association for all the constants and the arity association for all the kinds in this signature that are also defined in the signature file for the module must be identical. (All the objects in this calculated signature that do not also appear in the explicitly defined signature are interpreted as local or localkind objects.)
• All exportdef and useonly declarations in the calculated signature must be for global constants and must also appear in the explicit signature. All fixity declarations for global constants in the calculated signature must also appear in the explicit signature. A global constant that is defined to be closed (in the module source) should be exportdef (in the explicit signature).
• Tokens that begin with uppercase letters are to be interpreted as variables. Such variables may be bound or free depending on whether or not they are captured by an enclosing abstraction. Notice in contrast that tokens that begin with _ can only be free variables. Notice also that bound variables may, in addition, begin with lower case letters or sign characters, much like constant tokens. Free variables that appear in clauses are to be understood as being implicitly universally qualified at the head of the clause. All occurrences of a (bound or free) variable in a clause must have the same type.
• In the rule for an <Atom>, the head is permitted to be an essentially universally quantified variable. In determining the interpretation of a quantifier, the assumption is that a Clause appears in a negative context.
• Every sort and type constructor that is used in the type declarations and clauses in a module must be explicitly declared. While this practice is not encouraged, undeclared constants may be used in the clauses in a module. Types are to be inferred for these constants in these cases based on usage. The convention to be used in this inferring such types is that every usage of such a constant is at a type identical to its implicitly declared type and, further, this implicitly declared type is the most general type consistent with all the usages of the constant and this convention. The Teyjus compiler is designed to display the inferred types of these constants in the form of a warning relative to each module that it processes.
• A chain of imports or accumulates from a given module must not lead back to the same module. This violation of syntax for imported modules cannot be detected at compile time without violating the philosophy of separate compilation, but it will be detected at load time.

6.4 Matching a Module with its Signature

The process of matching a signature with the declarations in the source file, i.e. the file with extension .mod, has three essential effects:

• It makes sure that the types for (global) constants and the arities for (global) type constructors that are defined in the module agree with what is expected of them in the signature.
• It identifies the final list of global and local constants, sorts and type constructors corresponding to the module.
• It ensures that the useonly restrictions on predicates are satisfied by the code in the module.

The broad manner of processing is the following. First, all type and kind declarations in a module are processed to extract lists of global and local constant, sort and type constructor declarations. The global lists are enhanced by the declarations in accumulated signatures and in the signatures of imported modules. The global lists are further enhanced by global declarations in accumulated modules. The locally or implicitly declared constants, kinds and type constructors in such modules are added as new objects of these categories distinct from any other symbols that are or will be encountered in processing. The global lists are now filtered by the lists obtained from the signature for this module, with the eliminated objects going to relevant local lists. At each stage in this processing, the declared type and arity of objects in a given category having identical names in any given context must match.

The simplified signature of global and local sorts, type constructors and constants is used to analyze the clauses in the module. In the process, new constants may be encountered and these may be added to the relevant local lists. The inference of types for undeclared constants may also be supported by this process. A check must be made in the course of processing clauses to ensure that useonly predicates do not have defining clauses either at the top-level or in the antecedents of implication goals.

6.5 Using Signatures to Certify Module Interactions

Part of the process of certifying module interactions involves checking for compatibility between symbols that are global to an imported module and the definitions of these symbols in the importing module or in the signatures of sibling imported modules. This aspect is covered under the topic of matching a module with its signature. The other part of the process concerns ensuring that restrictions imposed by closed, exportdef and useonly declarations are satisfied. This is done as follows:

Closed Declarations--Inwards

We assume that we are given a list of closed predicates at the outset; these predicates are ones defined to be closed in some module within whose accumulate structure the present one appears embedded. We prune this list first by eliminating all the predicates that are either not global in the present module or are defined to be useonly. We then add to the list all the predicates defined to be closed within the present module. Modules accumulated into the present context are then to be processed in the same fashion as the one being described, except that the incoming list of closed predicates is the newly derived one. With regard to each imported module, the requirement is that if any of the predicates in the newly derived list is global to it, then it is also defined to be useonly.

Exportdef Declarations

One aspect to check is the compatibility of the `parent' module with those imported or accumulated by it. For this purpose, we (conceptually) collect all the exportdef predicates from the signatures of the imported or accumulated modules. We then check that the resulting list consists of only non-global constants or of global predicates that are also of the exportdef kind in the parent module. Further, none of the predicates in this list should have defining clauses in the parent module.

The other aspect to check is compatibility between sibling imported and accumulated modules. For this purpose, it is necessary to determine that the exportdef declaration of each predicate in one module is complemented by a useonly declaration for that predicate in a sibling module if that predicate is global there.

Closed Declarations--Outwards

The role of closed declarations from an outwards perspective is identical to that of exportdef declarations and processing relevant to it therefore follows the lines described in the preceding item.

Useonly Declarations

Within the main module and each accumulated module, we check that there are no clauses defining useonly predicates as described in the section on matching a module with its signature. Then for each accumulated/imported module and useonly constant we check that the constant is either not global in that module or is defined to be useonly in it.

6.6 Builtin Sorts and Type Constructors, Constants and Predicates

The builtin notions supported by Teyjus are sub-categorized and described by the material below.

6.6.1 Sorts and Type Constructors

Teyjus embodies an understanding of the following primitive types

   int          for integers in an implementation determined range. Teyjus supports
                integers in the range (-2**25,2**25).

   real         for reals in an implementation determined range. Teyjus currently 
                supports a representation based on a 15 bit mantissa and 7 bit 
                exponent representation.

   string       for the type of strings

   in_stream    for input streams

   out_stream   for output streams

   o            for the type of propositions

Teyjus also supports the following type constructors

   list         the unary type constructor for lists

6.6.2 Logical Constants and Primitive Goals

The following constants are recognized by the Teyjus parser as logical constants or primitive goals; the types and interpretations of these symbols are indicated alongside them. Some of the symbols listed are treated as keywords (see section Characterization of Tokens in Teyjus) and so cannot be redefined. Others can be redefined by type declarations in user programs.

   true       of type o, representing the true proposition
   !          of type o, representing the Prolog cut
   fail       of type o, representing the goal that always fails
   halt       of type o, representing a goal that terminates interaction
   stop       of type o, representing a goal that terminates interaction
   ,          of type o -> o -> o, representing conjunction 
   &          of type o -> o -> o, representing conjunction 
   ;          of type o -> o -> o, representing disjunction
   :-         of type o -> o -> o, representing Prolog style implication
   =>         of type o -> o -> o, representing implication written right
   sigma      of type (A -> o) -> o, representing existential quantification
   pi         of type (A -> o) -> o, representing universal quantification
   not        of type o -> o, representing Prolog-style negation-by-failure
   =          of type A -> A -> o, representing (Lambda Prolog) equality

The predicates , (comma), &, ; (semicolon), :- and => are all actually recognized as infix operators with the following characteristics: comma is left associative with precedence level 110, & is right associative with precedence level 120, semicolon is left associative with precedence level 100, :- is non associative with precedence level 0 and => is right associative with precedence level 130.

6.6.3 Pervasive Constants

The following symbols are recognized as constants with the associated attributes. Those of these symbols that are not categorized as keywords (see section Characterization of Tokens in Teyjus) can be redefined by the user.

~

overloaded prefix operator of type (int -> int) and (real -> real). Nonassociative and with higher precedence than everything else except application.

+

overloaded infix left associative operator with precedence level 150 and type either (int -> int -> int) or (real -> real -> real).

-

overloaded infix left associative operator with precedence level 150 and type either (int -> int -> int) or (real -> real -> real).

*

overloaded infix left associative operator with precedence level 160 and type either (int -> int -> int) or (real -> real -> real).

div

infix left associative operator with precedence level 160 and type int -> int -> int.

/

infix left associative operator with precedence level 160 and type real -> real -> real.

mod

infix left associative operator with precedence level 160 and type int -> int -> int.

int_to_real

of type int -> real.

abs

of type int -> int.

sqrt

of type real -> real.

sin

of type real -> real. Argument is in radians.

cos

of type real -> real. Argument is in radians.

arctan

of type real -> real. Result (when evaluation is forced) is in radians.

ln

of type real -> real.

floor

of type real -> int.

ceil

of type real -> int.

truncate

of type real -> int.

rabs

of type real -> real.

^

of type string -> string -> string, representing string concatenation.

size

of type string -> int, representing the length function on strings.

chr

of type int -> string.

string_to_int

of type string -> int representing the usual ord function on characters (encoded as single character strings).

substring

of type string -> int -> int -> string. When evaluated, (substring s i j) returns the string starting at position i (zero indexed) in the string and ending at position (i + j). The result is undefined if i < 0 or the length of s is less than i + j.

int_to_string

of type int -> string. When evaluated, the result returned is a string rendition of the integer value of the first argument.

real_to_string

of type real -> string. When evaluated, the result returned is a string rendition of the real value of the first argument.

std_in

of type in_stream, representing the standard input stream

std_out

of type out_stream, representing the standard output stream

std_err

of type in_stream, representing the standard error stream

nil

of type (list A), representing the (polymorphic) nil list

::

of type (A -> (list A) -> (list A)) representing the usual list constructor.

6.6.4 Builtin Comparison Predicates

The following comparison operators are supported by Teyjus.

   <        >        =<        >=

These operators are overloaded in an ad hoc way. In particular, they each have the type A -> A -> o, where A may be instantiated by the types int, real and string. All these operators are of the infix variety, none is associative and each has the precedence level of 130.

6.6.5 Input/Output and other Side Effecting Predicates

The following additional predicates are treated as builtin ones in Teyjus. Their interpretation is true for the most part to that in Terzo, the ML based interpreter for Lambda Prolog.

is

This is the evaluation predicate familiar from Prolog. It is actually defined as an infix, non associative operator with precedence level 130. This predicate is overloaded in an ad hoc way: it can be used at the types int -> int -> o, real -> real -> o and string -> string -> o. The determination of specific type can be delayed to run-time and an illegal usage may result in a run-time type error.

time

Predicate type: int -> int -> o. Calls the Unix 'gettimeofday' function. Instantiates the first and second arguments to the number of seconds and microseconds respectively, since 00:00 Universal Coordinated Time, Janurary 1, 1970. The arguments must be uninstantiated variables.

getenv

Predicate type: string -> string -> o. Calls the Unix 'getenv' function to return the value of environment variables. The first argument should be instantiated to the name of the environment variable. The second argument will be unified with the value of the variable.

open_in

Predicate type: string -> in_stream -> o. Its first argument must be instantiated to a string literal and its second argument should be an uninstantiated variable. Its effect is to open a file with name given by the string literal as an input stream. It is an error if a file of the relevant name does not exist.

open_out

open_append

Predicate type: string -> out_stream -> o. Its first argument must be instantiated to a string literal and its second argument should be an unbound variable. Its effect is to open a file with name given by the string literal as an output stream and to set the variable argument to this stream. If a file of the given name does not exist, then a new one is created. If such a file exists, then open_out initializes this file before it sets it up for writing whereas open_append begins writing at the end of the file.

open_string

Predicate type: string -> in_stream -> o. Its first argument must be instantiated to a string literal and its second argument must be an unbound variable. Its effect is to bind the variable to a stream containing the text in the string argument.

close_in

Predicate type: in_stream -> o. Its argument must be instantiated to an open input stream. The effect is to close this stream.

close_out

Predicate type: out_stream -> o. Its argument must be instantiated to an open output stream. The effect is to close this stream.

term_to_string

Predicate type: A -> string -> o. A character string representation of the first argument is constructed and is unified with the second argument.

string_to_term

Predicate type: string -> A -> o. The first argument must be instantiated to a string. The effect is to parse the portion of the string up to a period token (that excludes the decimal point) into a term and to try to unify this with the second argument. This predicate may fail because of type disparities as well.

input

Predicate type: in_stream -> int -> string -> o. (input strm i str) inputs at most i characters from strm and unifies this with str. This predicate blocks until i characters are available or EOF is reached. The second argument must be instantiated to a non-negative integer and the first to an open in_stream.

output

Predicate type: out_stream -> string -> o. Outputs the string argument to the stream represented by the first argument. Both arguments must be instantiated, the first to an open output stream and the second to a string literal.

input_line

Predicate type: in_stream -> string -> o. The first argument must be instantiated to an open input stream. The predicate blocks till a newline or EOF is present in the input stream, then reads all the characters up to and including the EOF or newline and unifies this with the string argument.

lookahead

Predicate type: in_stream -> string -> o. The first argument must be instantiated to an open input stream. The next character in the stream is looked up (but not consumed) and the result is unified with the string argument. The predicate blocks till a character or EOF is available.

eof

Predicate type: in_stream -> o. The argument must be instantiated to an open input stream. Succeeds if the end of stream has been reached and fails otherwise.

flush

Predicate type: out_stream -> o. The argument must be instantiated to an open output stream. Any buffered output is written out to the stream.

print

Predicate type: string -> o. This predicate is equivalent to (output std_out).

read

Predicate type: A -> o. This predicate reads in the character sequence up to and including a newline or EOF from std_in, attempts to parse this as a period terminated term, and unifies the result with the argument. Note: This predicate flushes the input beyond the period in the current line.

printterm

Predicate type: out_stream -> A -> o. The term constituting the second argument is written out to the out_stream given by the first argument. The first argument must be instantiated to an open out_stream.

readterm

Predicate type: in_stream -> A -> o. The first argument must be instantiated to an open in_stream. A period terminated string is read in from the in_stream, this is parsed as a term and then unified with the second argument. Note: This predicate does not flush the input from the current line even when the input port is std_in.

open_socket

Predicate type: string -> int -> in_stream -> out_stream -> o. Establishes a TCP socket. The first argument should be instantiated to a host name such as 'tulip.cs.umn.edu' or an IP address such as '128.101.35.21'. The second argument should be instantiated to the port number of the service. The third and fourth arguments should be uninstantiated variables that will be instantiated respectively to input and output streams associated with the socket. This predicate only works under Unix/Linux platforms.

6.7 Special Characteristics of the Teyjus Implementation

Listed below are some special characteristics of the Teyjus system knowledge of which may be relevant to programming:

• The present implementation interprets the restrictions on the occurrences of implications and on the antecedents of implication goals in the definition of higher-order hereditary Harrop formulas strictly. In particular, implications cannot appear within arguments of predicates. Further, the antecedent of an implication goal cannot be a flexible atom. The pragmatic reason for this is that the compilation model does not allow for a program clause whose structure is determined at runtime. These restrictions may be eased when interpretation and compilation are integrated in the implementation.
• The current model takes an interpretive approach towards solving queries. Thus, the query G is actually interpreted as the goal solve G where solve is an internal predicate embodying the treatment of goals whose structure is determined at runtime. A consequence of this treatment is that implication goals at the query level cannot be handled. This restriction can be eased by adopting a compilation scheme for top-level queries as well or by integrating compilation and interpretation approaches to handling program clauses.
• There is an interaction between cut and disjunctive goals that may not follow the lines of older implementations of Lambda Prolog. Specifically, a cut within a disjunctive branch in Teyjus cuts off choices only within that branch, leaving the choices over disjunctive branches unchanged. Thus, in the goal

  G1, !, G2 ; G3; G4

  the crossing of the cut removes alternative solution paths only within G1. If there is a failure in solving G2, the disjunctive goal may still be solved by solving G3 or G4.

This document was generated by Gopalan Nadathur on October, 20 2007 using texi2html 1.76.