[teyjus] r992 committed - Edited wiki page through web user interface.
tey...@googlecode.com
Author: gopalan.nadathur
Date: Thu Jun 10 13:09:32 2010
Log: Edited wiki page through web user interface.
http://code.google.com/p/teyjus/source/detail?r=992
Modified:
/wiki/ModSyntax.wiki
=======================================
--- /wiki/ModSyntax.wiki Mon Apr 14 09:29:57 2008
+++ /wiki/ModSyntax.wiki Thu Jun 10 13:09:32 2010
@@ -125,36 +125,36 @@
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>_.
-
- * Accumulate, import, accumsig and usesig declarations are those
appearing in the module preamble (i.e. generated by the rule for
_<ModPreamble>_) and beginning with the tokens _accumulate_, _import_,
_accum`_`sig_ and _use`_`sig_ respectively. The accumsig and usesig
declarations have a role in module declarations that is similar to the one
they have in signature declarations. Accumulates and imports have been
explained informally in the section the [ProgramStructure structure of
programs] in _Teyjus_. This informal description is further bolstered by
the presentation elsewhere of the rules for [SigMatching matching
signatures with modules] and for [SigAnnotation 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 whose scope
is limited to the module in which they appear and to the code obtained from
the modules imported and accumulated by that module.
-
- * 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 and is not one used in the _Teyjus_ system; signature files are
intended to be useful in the certification of module interactions and are
not an obstacle to be surmounted in whichever way possible and, for this
reason, are required to be explicitly provided for every module in the
_Teyjus_ framework.
+ * 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>`.
+
+ * Accumulate, import, accumsig and usesig declarations are those
appearing in the module preamble (i.e. generated by the rule for
`<ModPreamble>`) and beginning with the tokens `accumulate`, `import`,
`accum_sig` and `use_sig` respectively. The accumsig and usesig
declarations have a role in module declarations that is similar to the one
they have in signature declarations. Accumulates and imports have been
explained informally in the section the [ProgramStructure structure of
programs] in Teyjus. This informal description is further bolstered by the
presentation elsewhere of the rules for [SigMatching matching signatures
with modules] and for [SigAnnotation 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 whose scope
is limited to the module in which they appear and to the code obtained from
the modules imported and accumulated by that module.
+
+ * 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 and is not one used in the Teyjus system; signature files are
intended to be useful in the certification of module interactions and are
not an obstacle to be surmounted in whichever way possible and, for this
reason, are required to be explicitly provided for every module in the
Teyjus framework.
* 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.
+ * 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
+ 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
+ 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: it can be read as the symbol
for conjunction or as the separator between list elements in the _Prolog_
style list notation that is supported within the _Teyjus_ system. The rule
for disambiguating this operator is simple. It is read as a list separator
when it appears at the top-level in a list context and is read as the
conjunction operator everywhere else. To illustrate these conventions,
suppose that _p_, _q_ and _r_ are constants of propositional (or, more
precisely, _o_) type. Then the expression
+ 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: it can be read as the symbol
for conjunction or as the separator between list elements in the _Prolog_
style list notation that is supported within the _Teyjus_ system. The rule
for disambiguating this operator is simple. It is read as a list separator
when it appears at the top-level in a list context and is read as the
conjunction operator everywhere else. To illustrate these conventions,
suppose that p, _q_ and _r_ are constants of propositional (or, more
precisely, _o_) type. Then the expression
{{{
[ p,q,s]
}}}