mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 13:09:33 -06:00
1184 lines
40 KiB
HTML
1184 lines
40 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
|
|
<HTML>
|
|
<HEAD>
|
|
<META NAME="generator" CONTENT="http://txt2tags.sf.net">
|
|
<TITLE>The Module System of GF</TITLE>
|
|
</HEAD><BODY BGCOLOR="white" TEXT="black">
|
|
<P ALIGN="center"><CENTER><H1>The Module System of GF</H1>
|
|
<FONT SIZE="4">
|
|
<I>Aarne Ranta</I><BR>
|
|
8/4/2005 - 5/7/2007
|
|
</FONT></CENTER>
|
|
|
|
<P></P>
|
|
<HR NOSHADE SIZE=1>
|
|
<P></P>
|
|
<UL>
|
|
<LI><A HREF="#toc1">The principal module types</A>
|
|
<UL>
|
|
<LI><A HREF="#toc2">Abstract syntax</A>
|
|
<UL>
|
|
<LI><A HREF="#toc3">Compilation of abstract syntax</A>
|
|
</UL>
|
|
<LI><A HREF="#toc4">Concrete syntax</A>
|
|
<LI><A HREF="#toc5">Top-level grammar</A>
|
|
<UL>
|
|
<LI><A HREF="#toc6">Compiling top-level grammars</A>
|
|
<LI><A HREF="#toc7">Using top-level grammars</A>
|
|
</UL>
|
|
<LI><A HREF="#toc8">Multilingual grammar</A>
|
|
<UL>
|
|
<LI><A HREF="#toc9">Using multilingual grammars</A>
|
|
</UL>
|
|
<LI><A HREF="#toc10">Resource modules</A>
|
|
<UL>
|
|
<LI><A HREF="#toc11">Compiling resource modules</A>
|
|
<LI><A HREF="#toc12">Using resource modules</A>
|
|
</UL>
|
|
<LI><A HREF="#toc13">Inheritance</A>
|
|
<UL>
|
|
<LI><A HREF="#toc14">Multiple inheritance</A>
|
|
<LI><A HREF="#toc15">Restricted inheritance</A>
|
|
<LI><A HREF="#toc16">Compiling inheritance</A>
|
|
<LI><A HREF="#toc17">Inspecting grammar hierarchies</A>
|
|
</UL>
|
|
<LI><A HREF="#toc18">Reuse of top-level grammars as resources</A>
|
|
</UL>
|
|
<LI><A HREF="#toc19">Additional module types</A>
|
|
<UL>
|
|
<LI><A HREF="#toc20">Interfaces, instances, and incomplete grammars</A>
|
|
<UL>
|
|
<LI><A HREF="#toc21">Using an interface</A>
|
|
<LI><A HREF="#toc22">Instantiating an interface</A>
|
|
<LI><A HREF="#toc23">Compiling interfaces, instances, and parametrized modules</A>
|
|
</UL>
|
|
</UL>
|
|
<LI><A HREF="#toc24">Summary of module syntax and semantics</A>
|
|
<UL>
|
|
<LI><A HREF="#toc25">Abstract syntax modules</A>
|
|
<LI><A HREF="#toc26">Concrete syntax modules</A>
|
|
<LI><A HREF="#toc27">Resource modules</A>
|
|
<LI><A HREF="#toc28">Interface modules</A>
|
|
<LI><A HREF="#toc29">Instance modules</A>
|
|
<LI><A HREF="#toc30">Instantiated concrete syntax modules</A>
|
|
</UL>
|
|
</UL>
|
|
|
|
<P></P>
|
|
<HR NOSHADE SIZE=1>
|
|
<P></P>
|
|
<P>
|
|
A GF grammar consists of a set of <B>modules</B>, which can be
|
|
combined in different ways to build different grammars.
|
|
There are several different <B>types of modules</B>:
|
|
</P>
|
|
<UL>
|
|
<LI><CODE>abstract</CODE>
|
|
<LI><CODE>concrete</CODE>
|
|
<LI><CODE>resource</CODE>
|
|
<LI><CODE>interface</CODE>
|
|
<LI><CODE>instance</CODE>
|
|
<LI><CODE>incomplete concrete</CODE>
|
|
</UL>
|
|
|
|
<P>
|
|
We will go through the module types in this order, which is also
|
|
their order of "importance" from the most basic to
|
|
the more advanced ones.
|
|
</P>
|
|
<P>
|
|
This document presupposes knowledge of GF judgements and expressions, which can
|
|
be gained from the <A HREF="tutorial/gf-tutorial2.html">GF tutorial</A>. It aims
|
|
to give a systamatic description of the module system;
|
|
some tutorial information is repeated to make the document
|
|
self-contained.
|
|
</P>
|
|
<A NAME="toc1"></A>
|
|
<H1>The principal module types</H1>
|
|
<A NAME="toc2"></A>
|
|
<H2>Abstract syntax</H2>
|
|
<P>
|
|
Any GF grammar that is used in an application
|
|
will probably contain at least one module
|
|
of the <CODE>abstract</CODE> module type. Here is an example of
|
|
such a module, defining a fragment of propositional logic.
|
|
</P>
|
|
<PRE>
|
|
abstract Logic = {
|
|
cat Prop ;
|
|
fun Conj : Prop -> Prop -> Prop ;
|
|
fun Disj : Prop -> Prop -> Prop ;
|
|
fun Impl : Prop -> Prop -> Prop ;
|
|
fun Falsum : Prop ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
The <B>name</B> of this module is <CODE>Logic</CODE>.
|
|
</P>
|
|
<P>
|
|
An <CODE>abstract</CODE> module defines an <B>abstract syntax</B>, which
|
|
is a language-independent representation of a fragment of language.
|
|
It consists of two kinds of <B>judgements</B>:
|
|
</P>
|
|
<UL>
|
|
<LI><CODE>cat</CODE> judgements telling what <B>categories</B> there are
|
|
(types of abstract syntax trees)
|
|
<LI><CODE>fun</CODE> judgements telling what <B>functions</B> there are
|
|
(to build abstract syntax trees)
|
|
</UL>
|
|
|
|
<P>
|
|
There can also be <CODE>def</CODE> and <CODE>data</CODE> judgements in an
|
|
abstract syntax.
|
|
</P>
|
|
<A NAME="toc3"></A>
|
|
<H3>Compilation of abstract syntax</H3>
|
|
<P>
|
|
The GF grammar compiler expects to find the module <CODE>Logic</CODE> in a file named
|
|
<CODE>Logic.gf</CODE>. When the compiler is run, it produces
|
|
another file, named <CODE>Logic.gfc</CODE>. This file is in the
|
|
format called <B>canonical GF</B>, which is the "machine language"
|
|
of GF. Next time that the module <CODE>Logic</CODE> is needed in
|
|
compiling a grammar, it can be read from the compiled (<CODE>gfc</CODE>)
|
|
file instead of the source (<CODE>gf</CODE>) file, unless the source
|
|
has been changed after the compilation.
|
|
</P>
|
|
<A NAME="toc4"></A>
|
|
<H2>Concrete syntax</H2>
|
|
<P>
|
|
In order for a GF grammar to describe a concrete language, the abstract
|
|
syntax must be completed with a <B>concrete syntax</B> of it.
|
|
For this purpose, we use modules of type <CODE>concrete</CODE>: for instance,
|
|
</P>
|
|
<PRE>
|
|
concrete LogicEng of Logic = {
|
|
lincat Prop = {s : Str} ;
|
|
lin Conj a b = {s = a.s ++ "and" ++ b.s} ;
|
|
lin Disj a b = {s = a.s ++ "or" ++ b.s} ;
|
|
lin Impl a b = {s = "if" ++ a.s ++ "then" ++ b.s} ;
|
|
lin Falsum = {s = ["we have a contradiction"]} ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
The module <CODE>LogicEng</CODE> is a concrete syntax <CODE>of</CODE> the
|
|
abstract syntax <CODE>Logic</CODE>. The GF grammar compiler checks that
|
|
the concrete is valid with respect to the abstract syntax <CODE>of</CODE>
|
|
which it is claimed to be. The validity requires that there has to be
|
|
</P>
|
|
<UL>
|
|
<LI>a <CODE>lincat</CODE> judgement for each <CODE>cat</CODE> judgement, telling what the
|
|
<B>linearization types</B> of categories are
|
|
<LI>a <CODE>lin</CODE> judgement for each <CODE>fun</CODE> judgement, telling what the
|
|
<B>linearization functions</B> corresponding to functions are
|
|
</UL>
|
|
|
|
<P>
|
|
Validity also requires that the linearization functions defined by
|
|
<CODE>lin</CODE> judgements are type-correct with respect to the
|
|
linearization types of the arguments and value of the function.
|
|
</P>
|
|
<P>
|
|
There can also be <CODE>lindef</CODE> and <CODE>printname</CODE> judgements in a
|
|
concrete syntax.
|
|
</P>
|
|
<A NAME="toc5"></A>
|
|
<H2>Top-level grammar</H2>
|
|
<P>
|
|
When a <CODE>concrete</CODE> module is successfully compiled, a <CODE>gfc</CODE>
|
|
file is produced in the same way as for <CODE>abstract</CODE> modules. The
|
|
pair of an <CODE>abstract</CODE> and a corresponding <CODE>concrete</CODE> module
|
|
is a <B>top-level grammar</B>, which can be used in the GF system to
|
|
perform various tasks. The most fundamental tasks are
|
|
</P>
|
|
<UL>
|
|
<LI><B>linearization</B>: take an abstract syntax tree and find the corresponding string
|
|
<LI><B>parsing</B>: take a string and find the corresponding abstract syntax
|
|
trees (which can be zero, one, or many)
|
|
</UL>
|
|
|
|
<P>
|
|
In the current grammar, infinitely many trees and strings are recognized, although
|
|
no very interesting ones. For example, the tree
|
|
</P>
|
|
<PRE>
|
|
Impl (Disj Falsum Falsum) Falsum
|
|
</PRE>
|
|
<P>
|
|
has the linearization
|
|
</P>
|
|
<PRE>
|
|
if we have a contradiction or we have a contradiction then we have a contradiction
|
|
</PRE>
|
|
<P>
|
|
which in turn can be parsed uniquely as that tree.
|
|
</P>
|
|
<A NAME="toc6"></A>
|
|
<H3>Compiling top-level grammars</H3>
|
|
<P>
|
|
When GF compiles the module <CODE>LogicEng</CODE> it also has to compile
|
|
all modules that it <B>depends</B> on (in this case, just <CODE>Logic</CODE>).
|
|
The compilation process starts with dependency analysis to find
|
|
all these modules, recursively, starting from the explicitly imported one.
|
|
The compiler then reads either <CODE>gf</CODE> or <CODE>gfc</CODE> files, in
|
|
a dependency order. The decision on which files to read depends on
|
|
time stamps and dependencies in a natural way, so that all and only
|
|
those modules that have to be compiled are compiled. (This behaviour can
|
|
be changed with flags, see below.)
|
|
</P>
|
|
<A NAME="toc7"></A>
|
|
<H3>Using top-level grammars</H3>
|
|
<P>
|
|
To use a top-level grammar in the GF system, one uses the <CODE>import</CODE>
|
|
command (short name <CODE>i</CODE>). For instance,
|
|
</P>
|
|
<PRE>
|
|
i LogicEng.gf
|
|
</PRE>
|
|
<P>
|
|
It is also possible to specify the imported grammar(s) on the command
|
|
line when invoking GF:
|
|
</P>
|
|
<PRE>
|
|
gf LogicEng.gf
|
|
</PRE>
|
|
<P>
|
|
Various <B>compilation flags</B> can be added to both ways of compiling a module:
|
|
</P>
|
|
<UL>
|
|
<LI><CODE>-src</CODE> forces compilation form source files
|
|
<LI><CODE>-v</CODE> gives more verbose information on compilation
|
|
<LI><CODE>-s</CODE> makes compilation silent (except if it fails with an error message)
|
|
</UL>
|
|
|
|
<P>
|
|
A complete list of flags can be obtained in GF by <CODE>help i</CODE>.
|
|
</P>
|
|
<P>
|
|
Importing a grammar makes it visible in GF's <B>internal state</B>. To see
|
|
what modules are available, use the command <CODE>print_options</CODE> (<CODE>po</CODE>).
|
|
You can empty the state with the command <CODE>empty</CODE> (<CODE>e</CODE>); this is
|
|
needed if you want to read in grammars with a different abstract syntax
|
|
than the current one without exiting GF.
|
|
</P>
|
|
<P>
|
|
Grammar modules can reside in different directories. They can then be found
|
|
by means of a <B>search path</B>, which is a flag such as
|
|
</P>
|
|
<PRE>
|
|
-path=.:api/toplevel:prelude
|
|
</PRE>
|
|
<P>
|
|
given to the <CODE>import</CODE> command or the shell command invoking GF.
|
|
(It can also be defined in the grammar file; see below.) The compiler
|
|
writes every <CODE>gfc</CODE> file in the same directory as the corresponding
|
|
<CODE>gf</CODE> file.
|
|
</P>
|
|
<P>
|
|
The <CODE>path</CODE> is relative to the working directory <CODE>pwd</CODE>, so that
|
|
all directories listed are primarily interpreted as subdirectories of
|
|
<CODE>pwd</CODE>. Secondarily, they are searched relative to the value of the
|
|
environment variable <CODE>GF_LIB_PATH</CODE>, which is by default set to
|
|
<CODE>/usr/local/share/GF</CODE>.
|
|
</P>
|
|
<P>
|
|
Parsing and linearization can be performed with the <CODE>parse</CODE>
|
|
(<CODE>p</CODE>) and <CODE>linearize</CODE> (<CODE>l</CODE>) commands, respectively.
|
|
For instance,
|
|
</P>
|
|
<PRE>
|
|
> l Impl (Disj Falsum Falsum) Falsum
|
|
if we have a contradiction or we have a contradiction then we have a contradiction
|
|
|
|
> p -cat=Prop "we have a contradiction"
|
|
Falsum
|
|
</PRE>
|
|
<P>
|
|
Notice that the <CODE>parse</CODE> command needs the parsing category
|
|
as a flag. This necessary since a grammar can have several
|
|
possible parsing categories ("entry points").
|
|
</P>
|
|
<A NAME="toc8"></A>
|
|
<H2>Multilingual grammar</H2>
|
|
<P>
|
|
One <CODE>abstract</CODE> syntax can have several <CODE>concrete</CODE> syntaxes.
|
|
Here are two new ones for <CODE>Logic</CODE>:
|
|
</P>
|
|
<PRE>
|
|
concrete LogicFre of Logic = {
|
|
lincat Prop = {s : Str} ;
|
|
lin Conj a b = {s = a.s ++ "et" ++ b.s} ;
|
|
lin Disj a b = {s = a.s ++ "ou" ++ b.s} ;
|
|
lin Impl a b = {s = "si" ++ a.s ++ "alors" ++ b.s} ;
|
|
lin Falsum = {s = ["nous avons une contradiction"]} ;
|
|
}
|
|
|
|
concrete LogicSymb of Logic = {
|
|
lincat Prop = {s : Str} ;
|
|
lin Conj a b = {s = "(" ++ a.s ++ "&" ++ b.s ++ ")"} ;
|
|
lin Disj a b = {s = "(" ++ a.s ++ "v" ++ b.s ++ ")"} ;
|
|
lin Impl a b = {s = "(" ++ a.s ++ "->" ++ b.s ++ ")"} ;
|
|
lin Falsum = {s = "_|_"} ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
The four modules <CODE>Logic</CODE>, <CODE>LogicEng</CODE>, <CODE>LogicFre</CODE>, and
|
|
<CODE>LogicSymb</CODE> together form a <B>multilingual grammar</B>, in which
|
|
it is possible to perform parsing and linearization with respect to any
|
|
of the concrete syntaxes. As a combination of parsing and linearization,
|
|
one can also perform <B>translation</B> from one language to another.
|
|
(By <B>language</B> we mean the set of expressions generated by one
|
|
concrete syntax.)
|
|
</P>
|
|
<A NAME="toc9"></A>
|
|
<H3>Using multilingual grammars</H3>
|
|
<P>
|
|
Any combination of abstract syntax and corresponding concrete syntaxes
|
|
is thus a multilingual grammar. With many languages and other enrichments
|
|
(as described below), a multilingual grammar easily grows to the size of
|
|
tens of modules. The grammar developer, having finished her job, can
|
|
package the result in a <B>multilingual canonical grammar</B>, a file
|
|
with the suffix <CODE>.gfcm</CODE>. For instance, to compile the set of grammars
|
|
described by now, the following sequence of GF commands can be used:
|
|
</P>
|
|
<PRE>
|
|
i LogicEng.gf
|
|
i LogicFre.gf
|
|
i LogicSymb.gf
|
|
pm | wf logic.gfcm
|
|
</PRE>
|
|
<P>
|
|
The "end user" of the grammar only needs the file <CODE>logic.gfcm</CODE> to
|
|
access all the functionality of the multilingual grammar. It can be
|
|
imported in the GF system in the same way as <CODE>.gf</CODE> files. But
|
|
it can also be used in the
|
|
<A HREF="http://www.cs.chalmers.se/~bringert/gf/gf-java.html">Embedded Java Interpreter for GF</A>
|
|
to build Java programs of which the multilingual grammar functionalities
|
|
(linearization, parsing, translation) form a part.
|
|
</P>
|
|
<P>
|
|
In a multilingual grammar, the concrete syntax module names work as
|
|
names of languages that can be selected for linearization and parsing:
|
|
</P>
|
|
<PRE>
|
|
> l -lang=LogicFre Impl Falsum Falsum
|
|
si nous avons une contradiction alors nous avons une contradiction
|
|
|
|
> l -lang=LogicSymb Impl Falsum Falsum
|
|
( _|_ -> _|_ )
|
|
|
|
> p -cat=Prop -lang=LogicSymb "( _|_ & _|_ )"
|
|
Conj Falsum Falsum
|
|
</PRE>
|
|
<P>
|
|
The option <CODE>-multi</CODE> gives linearization to all languages:
|
|
</P>
|
|
<PRE>
|
|
> l -multi Impl Falsum Falsum
|
|
if we have a contradiction then we have a contradiction
|
|
si nous avons une contradiction alors nous avons une contradiction
|
|
( _|_ -> _|_ )
|
|
</PRE>
|
|
<P>
|
|
Translation can be obtained by using a <B>pipe</B> from a parser
|
|
to a linearizer:
|
|
</P>
|
|
<PRE>
|
|
> p -cat=Prop -lang=LogicSymb "( _|_ & _|_ )" | l -lang=LogicEng
|
|
if we have a contradiction then we have a contradiction
|
|
</PRE>
|
|
<P></P>
|
|
<A NAME="toc10"></A>
|
|
<H2>Resource modules</H2>
|
|
<P>
|
|
The <CODE>concrete</CODE> modules shown above would look much nicer if
|
|
we used the main idea of functional programming: avoid repetitive
|
|
code by using <B>functions</B> that capture repeated patterns of
|
|
expressions. A collection of such functions can be a valuable
|
|
<B>resource</B> for a programmer, reusable in many different
|
|
top-level grammars. Thus we introduce the <CODE>resource</CODE>
|
|
module type, with the first example
|
|
</P>
|
|
<PRE>
|
|
resource Util = {
|
|
oper SS : Type = {s : Str} ;
|
|
oper ss : Str -> SS = \s -> {s = s} ;
|
|
oper paren : Str -> Str = \s -> "(" ++ s ++ ")" ;
|
|
oper infix : Str -> SS -> SS -> SS = \h,x,y ->
|
|
ss (x.s ++ h ++ y.s) ;
|
|
oper infixp : Str -> SS -> SS -> SS = \h,x,y ->
|
|
ss (paren (infix h x y)) ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
Modules of <CODE>resource</CODE> type have two forms of judgement:
|
|
</P>
|
|
<UL>
|
|
<LI><CODE>oper</CODE> defining auxiliary operations
|
|
<LI><CODE>param</CODE> defining parameter types
|
|
</UL>
|
|
|
|
<P>
|
|
A <CODE>resource</CODE> can be used in a <CODE>concrete</CODE> (or another
|
|
<CODE>resource</CODE>) by <CODE>open</CODE>ing it. This means that
|
|
all operations (and parameter types) defined in the resource
|
|
module become usable in module that opens it. For instance,
|
|
we can rewrite the module <CODE>LogicSymb</CODE> much more concisely:
|
|
</P>
|
|
<PRE>
|
|
concrete LogicSymb of Logic = open Util in {
|
|
lincat Prop = SS ;
|
|
lin Conj = infixp "&" ;
|
|
lin Disj = infixp "v" ;
|
|
lin Impl = infixp "->" ;
|
|
lin Falsum = ss "_|_" ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
What happens when this variant of <CODE>LogicSymb</CODE> is
|
|
compiled is that the <CODE>oper</CODE>-defined constants
|
|
of <CODE>Util</CODE> are <B>inlined</B> in the
|
|
right-hand-sides of the judgements of <CODE>LogicSymb</CODE>,
|
|
and these expressions are <B>partially evaluated</B>, i.e.
|
|
computed as far as possible. The generated <CODE>gfc</CODE> file
|
|
will look just like the file generated for the first version
|
|
of <CODE>LogicSymb</CODE> - at least, it will do the same job.
|
|
</P>
|
|
<P>
|
|
Several <CODE>resource</CODE> modules can be <CODE>open</CODE>ed
|
|
at the same time. If the modules contain same names, the
|
|
conflict can be resolved by <B>qualified</B> opening and
|
|
reference. For instance,
|
|
</P>
|
|
<PRE>
|
|
concrete LogicSymb of Logic = open Util, Prelude in { ...
|
|
} ;
|
|
</PRE>
|
|
<P>
|
|
(where <CODE>Prelude</CODE> is a standard library of GF) brings
|
|
into scope two definitions of the constant <CODE>SS</CODE>.
|
|
To specify which one is used, you can write
|
|
<CODE>Util.SS</CODE> or <CODE>Prelude.SS</CODE> instead of just <CODE>SS</CODE>.
|
|
You can also introduce abbreviations to avoid long qualifiers, e.g.
|
|
</P>
|
|
<PRE>
|
|
concrete LogicSymb of Logic = open (U=Util), (P=Prelude) in { ...
|
|
} ;
|
|
</PRE>
|
|
<P>
|
|
which means that you can write <CODE>U.SS</CODE> and <CODE>P.SS</CODE>.
|
|
</P>
|
|
<P>
|
|
Judgements of <CODE>param</CODE> and <CODE>oper</CODE> forms may also be used
|
|
in <CODE>concrete</CODE> modules, and they are then considered local
|
|
to those modules, i.e. they are not exported.
|
|
</P>
|
|
<A NAME="toc11"></A>
|
|
<H3>Compiling resource modules</H3>
|
|
<P>
|
|
The compilation of a <CODE>resource</CODE> module differs
|
|
from the compilation of <CODE>abstract</CODE> and
|
|
<CODE>concrete</CODE> modules because <CODE>oper</CODE> operations
|
|
do not in general have values in <CODE>gfc</CODE>. A <CODE>gfc</CODE>
|
|
file <I>is</I> generated, but it contains only
|
|
<CODE>param</CODE> judgements (also recall that <CODE>oper</CODE>s
|
|
are inlined in their top-level use sites, so it is not
|
|
necessary to save them in the compiled grammar).
|
|
However, since computing the operations over and over
|
|
again can be time comsuming, and since type checking
|
|
<CODE>resource</CODE> modules also takes time, a third kind
|
|
of file is generated for resource modules: a <CODE>.gfr</CODE>
|
|
file. This file is written in the GF source code notation,
|
|
but it is type checked and type annotated, and <CODE>oper</CODE>s
|
|
are computed as far as possible.
|
|
</P>
|
|
<P>
|
|
If you look at any <CODE>gfc</CODE> or <CODE>gfr</CODE> file generated
|
|
by the GF compiler, you see that all names have been replaced by
|
|
their qualified variants. This is an important first step (after parsing)
|
|
the compiler does. As for the commands in the GF shell, some output
|
|
qualified names and some not. The difference does not always result
|
|
from firm principles.
|
|
</P>
|
|
<A NAME="toc12"></A>
|
|
<H3>Using resource modules</H3>
|
|
<P>
|
|
The typical use is through <CODE>open</CODE> in a
|
|
<CODE>concrete</CODE> module, which means that
|
|
<CODE>resource</CODE> modules are not imported on their own.
|
|
However, in the developing and testing phase of grammars, it
|
|
can be useful to evaluate <CODE>oper</CODE>s with different
|
|
arguments. To prevent them from being thrown away after inlining, the
|
|
<CODE>-retain</CODE> option can be used:
|
|
</P>
|
|
<PRE>
|
|
> i -retain Util.gf
|
|
</PRE>
|
|
<P>
|
|
The command <CODE>compute_concrete</CODE> (<CODE>cc</CODE>)
|
|
can now be used for evaluating expressions that may contain
|
|
operations defined in <CODE>Util</CODE>:
|
|
</P>
|
|
<PRE>
|
|
> cc ss (paren "foo")
|
|
{s = "(" ++ "foo" ++ ")"}
|
|
</PRE>
|
|
<P>
|
|
To find out what <CODE>oper</CODE>s are available for a given type,
|
|
the command <CODE>show_operations</CODE> (<CODE>so</CODE>) can be used:
|
|
</P>
|
|
<PRE>
|
|
> so SS
|
|
Util.ss : Str -> SS ;
|
|
Util.infix : Str -> SS -> SS -> SS ;
|
|
Util.infixp : Str -> SS -> SS -> SS ;
|
|
</PRE>
|
|
<P></P>
|
|
<A NAME="toc13"></A>
|
|
<H2>Inheritance</H2>
|
|
<P>
|
|
The most characteristic modularity of GF lies in the division of
|
|
grammars into <CODE>abstract</CODE>, <CODE>concrete</CODE>, and
|
|
<CODE>resource</CODE> modules. This permits writing multilingual
|
|
grammar and sharing the maximum of code between different
|
|
languages.
|
|
</P>
|
|
<P>
|
|
In addition to this special kind of modularity, GF provides <B>inheritance</B>,
|
|
which is familiar from other programming languages (in particular,
|
|
object-oriented ones). Inheritance means that a module inherits all
|
|
judgements from another module; we also say that it <B>extends</B>
|
|
the other module. Inheritance is useful to divide big grammars into
|
|
smaller units, and also to reuse the same units in different bigger
|
|
grammars.
|
|
</P>
|
|
<P>
|
|
The first example of inheritance is for abstract syntax. Let us
|
|
extend the module <CODE>Logic</CODE> to <CODE>Arithmetic</CODE>:
|
|
</P>
|
|
<PRE>
|
|
abstract Arithmetic = Logic ** {
|
|
cat Nat ;
|
|
fun Even : Nat -> Prop ;
|
|
fun Odd : Nat -> Prop ;
|
|
fun Zero : Nat ;
|
|
fun Succ : Nat -> Nat ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
In parallel with the extension of the abstract syntax
|
|
<CODE>Logic</CODE> to <CODE>Arithmetic</CODE>, we can extend
|
|
the concrete syntax <CODE>LogicEng</CODE> to <CODE>ArithmeticEng</CODE>:
|
|
</P>
|
|
<PRE>
|
|
concrete ArithmeticEng of Arithmetic = LogicEng ** open Util in {
|
|
lincat Nat = SS ;
|
|
lin Even x = ss (x.s ++ "is" ++ "even") ;
|
|
lin Odd x = ss (x.s ++ "is" ++ "odd") ;
|
|
lin Zero = ss "zero" ;
|
|
lin Succ x = ss ("the" ++ "successor" ++ "of" ++ x.s) ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
Another extension of <CODE>Logic</CODE> is <CODE>Geometry</CODE>,
|
|
</P>
|
|
<PRE>
|
|
abstract Geometry = Logic ** {
|
|
cat Point ;
|
|
cat Line ;
|
|
fun Incident : Point -> Line -> Prop ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
The corresponding concrete syntax is left as exercise.
|
|
</P>
|
|
<A NAME="toc14"></A>
|
|
<H3>Multiple inheritance</H3>
|
|
<P>
|
|
Inheritance can be <B>multiple</B>, which means that a module
|
|
may extend many modules at the same time. Suppose, for instance,
|
|
that we want to build a module for mathematics covering both
|
|
arithmetic and geometry, and the underlying logic. We then write
|
|
</P>
|
|
<PRE>
|
|
abstract Mathematics = Arithmetic, Geometry ** {
|
|
} ;
|
|
</PRE>
|
|
<P>
|
|
We could of course add some new judgements in this module, but
|
|
it is not necessary to do so. If no new judgements are added, the
|
|
module body can be omitted:
|
|
</P>
|
|
<PRE>
|
|
abstract Mathematics = Arithmetic, Geometry ;
|
|
</PRE>
|
|
<P></P>
|
|
<P>
|
|
The module <CODE>Mathematics</CODE> shows that it is possibe
|
|
to extend a module already built by extension. The correctness
|
|
criterion for extensions is that the same name
|
|
(<CODE>cat</CODE>, <CODE>fun</CODE>, <CODE>oper</CODE>, or <CODE>param</CODE>)
|
|
may not be defined twice in the resulting union of names.
|
|
That the names defined in <CODE>Logic</CODE> are "inherited twice"
|
|
by <CODE>Mathematics</CODE> (via both <CODE>Arithmetic</CODE> and
|
|
<CODE>Geometry</CODE>) is no violation of this rule; the usual
|
|
problems of multiple inheritance do not arise, since
|
|
the definitions of inherited constants cannot be changed.
|
|
</P>
|
|
<A NAME="toc15"></A>
|
|
<H3>Restricted inheritance</H3>
|
|
<P>
|
|
Inheritance can be <B>restricted</B>, which means that only some of
|
|
the constants are inherited. There are two dual notations for this:
|
|
</P>
|
|
<PRE>
|
|
A [f,g]
|
|
</PRE>
|
|
<P>
|
|
meaning that <I>only</I> <CODE>f</CODE> and <CODE>g</CODE> are inherited from <CODE>A</CODE>, and
|
|
</P>
|
|
<PRE>
|
|
A-[f,g]
|
|
</PRE>
|
|
<P>
|
|
meaning that <I>everything except</I> <CODE>f</CODE> is <CODE>g</CODE> are inherited from <CODE>A</CODE>.
|
|
</P>
|
|
<P>
|
|
Constants that are not inherited may be redefined in the inheriting module.
|
|
</P>
|
|
<A NAME="toc16"></A>
|
|
<H3>Compiling inheritance</H3>
|
|
<P>
|
|
Inherited judgements are not copied into the inheriting modules.
|
|
Instead, an <B>indirection</B> is created for each inherited name,
|
|
as can be seen by looking into the generated <CODE>gfc</CODE> (and
|
|
<CODE>gfr</CODE>) files. Thus for instance the names
|
|
</P>
|
|
<PRE>
|
|
Mathematics.Prop Arithmetic.Prop Geometry.Prop Logic.Prop
|
|
</PRE>
|
|
<P>
|
|
all refer to the same category, declared in the module
|
|
<CODE>Logic</CODE>.
|
|
</P>
|
|
<A NAME="toc17"></A>
|
|
<H3>Inspecting grammar hierarchies</H3>
|
|
<P>
|
|
The command <CODE>visualize_graph</CODE> (<CODE>vg</CODE>) shows the
|
|
dependency graph in the current GF shell state. The graph can
|
|
also be saved in a file and used e.g. in documentation, by the
|
|
command <CODE>print_multi -graph</CODE> (<CODE>pm -graph</CODE>).
|
|
</P>
|
|
<P>
|
|
The <CODE>vg</CODE> command uses the free software packages Graphviz (commad <CODE>dot</CODE>)
|
|
and Ghostscript (command <CODE>gv</CODE>).
|
|
</P>
|
|
<A NAME="toc18"></A>
|
|
<H2>Reuse of top-level grammars as resources</H2>
|
|
<P>
|
|
Top-level grammars have a straightforward translation to
|
|
<CODE>resource</CODE> modules. The translation concerns
|
|
pairs of abstract-concrete judgements:
|
|
</P>
|
|
<PRE>
|
|
cat C ; ===> oper C : Type = T ;
|
|
lincat C = T ;
|
|
|
|
fun f : A ; ===> oper f : A = t ;
|
|
lin f = t ;
|
|
</PRE>
|
|
<P>
|
|
Due to this translation, a <CODE>concrete</CODE> module
|
|
can be <CODE>open</CODE>ed in the same way as a
|
|
<CODE>resource</CODE> module; the translation is done
|
|
on the fly (it is computationally very cheap).
|
|
</P>
|
|
<P>
|
|
Modular grammar engineering often means that some grammarians
|
|
focus on the semantics of the domain whereas others take care
|
|
of linguistic details. Thus a typical reuse opens a
|
|
linguistically oriented <B>resource grammar</B>,
|
|
</P>
|
|
<PRE>
|
|
abstract Resource = {
|
|
cat S ; NP ; A ;
|
|
fun PredA : NP -> A -> S ;
|
|
}
|
|
concrete ResourceEng of Resource = {
|
|
lincat S = ... ;
|
|
lin PredA = ... ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
The <B>application grammar</B>, instead of giving linearizations
|
|
explicitly, just reduces them to categories and functions in the
|
|
resource grammar:
|
|
</P>
|
|
<PRE>
|
|
concrete ArithmeticEng of Arithmetic = LogicEng ** open ResourceEng in {
|
|
lincat Nat = NP ;
|
|
lin Even x = PredA x (regA "even") ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
If the resource grammar is only capable of generating grammatically
|
|
correct expressions, then the grammaticality of the application
|
|
grammar is also guaranteed: the type checker of GF is used as
|
|
grammar checker.
|
|
To guarantee distinctions between categories that have
|
|
the same linearization type, the actual translation used
|
|
in GF adds to every linearization type and linearization
|
|
a <B>lock field</B>,
|
|
</P>
|
|
<PRE>
|
|
cat C ; ===> oper C : Type = T ** {lock_C : {}} ;
|
|
lincat C = T ;
|
|
|
|
fun f : C_1 ... C_n -> C ; ===> oper f : C_1 ... C_n -> C = \x_1,...,x_n ->
|
|
lin f = t ; t x_1 ... x_n ** {lock_C = &lt;>};
|
|
</PRE>
|
|
<P>
|
|
(Notice that the latter translation is type-correct because of
|
|
record subtyping, which means that <CODE>t</CODE> can ignore the
|
|
lock fields of its arguments.) An application grammarian who
|
|
only uses resource grammar categories and functions never
|
|
needs to write these lock fields herself. Having to do so
|
|
serves as a warning that the grammaticality guarantee given
|
|
by the resource grammar no longer holds.
|
|
</P>
|
|
<P>
|
|
<B>Note</B>. The lock field mechanism is experimental, and may be changed
|
|
to a stronger abstraction mechnism in the future. This may result in
|
|
hand-written lock fields ceasing to work.
|
|
</P>
|
|
<A NAME="toc19"></A>
|
|
<H1>Additional module types</H1>
|
|
<A NAME="toc20"></A>
|
|
<H2>Interfaces, instances, and incomplete grammars</H2>
|
|
<P>
|
|
One difference between top-level grammars and <CODE>resource</CODE>
|
|
modules is that the former systematically separete the
|
|
declarations of categories and functions from their definitions.
|
|
In the reuse translation creating and <CODE>oper</CODE> judgement,
|
|
the declaration coming from the <CODE>abstract</CODE> module is put
|
|
together with the definition coming from the <CODE>concrete</CODE>
|
|
module.
|
|
</P>
|
|
<P>
|
|
However, the separation of declarations and definitions is so
|
|
useful a notion that GF also has specific modules types that
|
|
<CODE>resource</CODE> modules into two parts. In this splitting,
|
|
an <CODE>interface</CODE> module corresponds to an abstract syntax,
|
|
in giving the declarations of operations (and parameter types).
|
|
For instance, a generic markup interface would look as follows:
|
|
</P>
|
|
<PRE>
|
|
interface Markup = open Util in {
|
|
oper Boldface : Str -> Str ;
|
|
oper Heading : Str -> Str ;
|
|
oper markupSS : (Str -> Str) -> SS -> SS = \f,r ->
|
|
ss (f r.s) ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
The definitions of the constants declared in an <CODE>interface</CODE>
|
|
are given in an <CODE>instance</CODE> module (which is always <CODE>of</CODE>
|
|
an interface, in the same way as a <CODE>concrete</CODE> is always
|
|
<CODE>of</CODE> an abstract). The following <CODE>instance</CODE>s
|
|
define markup in HTML and latex.
|
|
</P>
|
|
<PRE>
|
|
instance MarkupHTML of Markup = open Util in {
|
|
oper Boldface s = "&lt;b>" ++ s ++ "&lt;/b>" ;
|
|
oper Heading s = "&lt;h2>" ++ s ++ "&lt;/h2>" ;
|
|
}
|
|
|
|
instance MarkupLatex of Markup = open Util in {
|
|
oper Boldface s = "\\textbf{" ++ s ++ "}" ;
|
|
oper Heading s = "\\section{" ++ s ++ "}" ;
|
|
}
|
|
</PRE>
|
|
<P>
|
|
Notice that both <CODE>interface</CODE>s and <CODE>instance</CODE>s may
|
|
<CODE>open</CODE> <CODE>resource</CODE>s (and also reused top-level grammars).
|
|
An <CODE>interface</CODE> may moreover define some of the operations it
|
|
declares; these definitions are inherited by all instances and cannot
|
|
be changed in them. Inheritance by module extension
|
|
is possible, as always, between modules of the same type.
|
|
</P>
|
|
<A NAME="toc21"></A>
|
|
<H3>Using an interface</H3>
|
|
<P>
|
|
An <CODE>interface</CODE> or an <CODE>instance</CODE>
|
|
can be <CODE>open</CODE>ed in
|
|
a <CODE>concrete</CODE> using the same syntax as when opening
|
|
a <CODE>resource</CODE>. For an <CODE>instance</CODE>, the semantics
|
|
is the same as when opening the definitions together with
|
|
the type signatures - one can think of an <CODE>interface</CODE>
|
|
and an <CODE>instance</CODE> of it together forming an ordinary
|
|
<CODE>resource</CODE>. Opening an <CODE>interface</CODE>, however,
|
|
is different: functions that are only declared without
|
|
having a definition cannot be compiled (inlined); neither
|
|
can functions whose definitions depend on undefined functions.
|
|
</P>
|
|
<P>
|
|
A module that <CODE>open</CODE>s an <CODE>interface</CODE> is therefore
|
|
<B>incomplete</B>, and has to be <B>completed</B> with an
|
|
<CODE>instance</CODE> of the interface to become complete. To make
|
|
this situation clear, GF requires any module that opens an
|
|
<CODE>interface</CODE> to be marked as <CODE>incomplete</CODE>. Thus
|
|
the module
|
|
</P>
|
|
<PRE>
|
|
incomplete concrete DocMarkup of Doc = open Markup in {
|
|
...
|
|
}
|
|
</PRE>
|
|
<P>
|
|
uses the interface <CODE>Markup</CODE> to place markup in
|
|
chosen places in its linearization rules, but the
|
|
implementation of markup - whether in HTML or in LaTeX - is
|
|
left unspecified. This is a powerful way of sharing
|
|
the code of a whole module with just differences in
|
|
the definitions of some constants.
|
|
</P>
|
|
<P>
|
|
Another terminology for <CODE>incomplete</CODE> modules is
|
|
<B>parametrized modules</B> or <B>functors</B>.
|
|
The <CODE>interface</CODE> gives the list of parameters
|
|
that the functor depends on.
|
|
</P>
|
|
<A NAME="toc22"></A>
|
|
<H3>Instantiating an interface</H3>
|
|
<P>
|
|
To complete an <CODE>incomplete</CODE> module, each <CODE>inteface</CODE>
|
|
that it opens has to be provided an <CODE>instance</CODE>. The following
|
|
syntax is used for this:
|
|
</P>
|
|
<PRE>
|
|
concrete DocHTML of Doc = DocMarkup with (Markup = MarkupHTML) ;
|
|
</PRE>
|
|
<P>
|
|
Instantiation of <CODE>Markup</CODE> with <CODE>MarkupLatex</CODE> is
|
|
another one-liner.
|
|
</P>
|
|
<P>
|
|
If more interfaces than one are instantiated, a comma-separated
|
|
list of equations in parentheses is used, e.g.
|
|
</P>
|
|
<PRE>
|
|
concrete MusicIta = MusicI with
|
|
(Syntax = SyntaxIta), (LexMusic = LexMusicIta) ;
|
|
</PRE>
|
|
<P>
|
|
This example shows a common design pattern for building applications:
|
|
the concrete syntax is a functor on the generic resource grammar library
|
|
interface <CODE>Syntax</CODE> and a domain-specific lexicon interface, here
|
|
<CODE>LexMusic</CODE>.
|
|
</P>
|
|
<P>
|
|
All interfaces that are <CODE>open</CODE>ed in the completed model
|
|
must be completed.
|
|
</P>
|
|
<P>
|
|
Notice that the completion of an <CODE>incomplete</CODE> module
|
|
may at the same time extend modules of the same type (which need
|
|
not be completions). It can also add new judgements in a module body,
|
|
and restrict inheritance from the functor.
|
|
</P>
|
|
<PRE>
|
|
concrete MusicIta = MusicI - [f] with
|
|
(Syntax = SyntaxIta), (LexMusic = LexMusicIta) ** {
|
|
|
|
lin f = ...
|
|
|
|
} ;
|
|
</PRE>
|
|
<P></P>
|
|
<A NAME="toc23"></A>
|
|
<H3>Compiling interfaces, instances, and parametrized modules</H3>
|
|
<P>
|
|
Interfaces, instances, and parametric modules are purely a
|
|
front-end feature of GF: these module types do not exist in
|
|
the <CODE>gfc</CODE> and <CODE>gfr</CODE> formats. The compiler has
|
|
nevertheless to keep track of their dependencies and modification
|
|
times. Here is a summary of how they are compiled:
|
|
</P>
|
|
<UL>
|
|
<LI>an <CODE>interface</CODE> is compiled into a <CODE>resource</CODE> with an empty body
|
|
<LI>an <CODE>instance</CODE> is compiled into a <CODE>resource</CODE> in union with its
|
|
<CODE>interface</CODE>
|
|
<LI>an <CODE>incomplete</CODE> module (<CODE>concrete</CODE> or <CODE>resource</CODE>) is compiled
|
|
into a module of the same type with an empty body
|
|
<LI>a completion module (<CODE>concrete</CODE> or <CODE>resource</CODE>) is compiled
|
|
into a module of the same type by compiling its functor so that, instead of
|
|
each <CODE>interface</CODE>, its given <CODE>instance</CODE> is used
|
|
</UL>
|
|
|
|
<P>
|
|
This means that some generated code is duplicated, because those operations that
|
|
do have complete definitions in an <CODE>interface</CODE> are copied to each of
|
|
the <CODE>instances</CODE>.
|
|
</P>
|
|
<A NAME="toc24"></A>
|
|
<H1>Summary of module syntax and semantics</H1>
|
|
<A NAME="toc25"></A>
|
|
<H2>Abstract syntax modules</H2>
|
|
<P>
|
|
Syntax:
|
|
</P>
|
|
<P>
|
|
<CODE>abstract</CODE> A <CODE>=</CODE> (A<sub>1</sub>,...,A<sub>n</sub> <CODE>**</CODE>)?
|
|
<CODE>{</CODE>J<sub>1</sub> <CODE>;</CODE> ... <CODE>;</CODE> J<sub>m</sub> <CODE>; }</CODE>
|
|
</P>
|
|
<P>
|
|
where
|
|
</P>
|
|
<UL>
|
|
<LI>i >= 0
|
|
<LI>each <I>A<sub>i</sub></I> is itself an abstract module,
|
|
possibly with restrictions on inheritance, i.e. <I>A<sub>i</sub></I><CODE>-[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
or <I>A<sub>i</sub></I><CODE>[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
<LI>each <I>J<sub>i</sub></I> is a judgement of one of the forms
|
|
<CODE>cat, fun, def, data</CODE>
|
|
</UL>
|
|
|
|
<P>
|
|
Semantic conditions:
|
|
</P>
|
|
<UL>
|
|
<LI>all inherited names declared in each <I>A<sub>i</sub></I> and <I>A</I> must be distinct
|
|
<LI>names in restriction lists must be defined in the restricted module
|
|
<LI>inherited constants may not depend on names excluded by restriction
|
|
</UL>
|
|
|
|
<A NAME="toc26"></A>
|
|
<H2>Concrete syntax modules</H2>
|
|
<P>
|
|
Syntax:
|
|
</P>
|
|
<P>
|
|
<CODE>incomplete</CODE>? <CODE>concrete</CODE> C <CODE>of</CODE> A <CODE>=</CODE>
|
|
(C<sub>1</sub>,...,C<sub>n</sub> <CODE>**</CODE>)?
|
|
(<CODE>open</CODE> O<sub>1</sub>,...,O<sub>k</sub> <CODE>in</CODE>)?
|
|
<CODE>{</CODE>J<sub>1</sub> <CODE>;</CODE> ... <CODE>;</CODE> J<sub>m</sub> <CODE>; }</CODE>
|
|
</P>
|
|
<P>
|
|
where
|
|
</P>
|
|
<UL>
|
|
<LI>i >= 0
|
|
<LI><I>A</I> is an abstract module
|
|
<LI>each <I>C<sub>i</sub></I> is a concrete module,
|
|
possibly with restrictions on inheritance, i.e. <I>C<sub>i</sub></I><CODE>-[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
<LI>each <I>O<sub>i</sub></I> is an open specification, of one of the forms
|
|
<UL>
|
|
<LI><I>R</I>
|
|
<LI><CODE>(</CODE><I>Q</I><CODE>=</CODE><I>R</I><CODE>)</CODE>
|
|
</UL>
|
|
</UL>
|
|
|
|
<P>
|
|
where <I>R</I> is a resource, instance, or concrete, and <I>Q</I> is any identifier
|
|
</P>
|
|
<UL>
|
|
<LI>each <I>J<sub>i</sub></I> is a judgement of one of the forms
|
|
<CODE>lincat, lin, lindef, printname</CODE>; also the forms <CODE>oper, param</CODE> are
|
|
allowed, but they cannot be inherited.
|
|
</UL>
|
|
|
|
<P>
|
|
If the modifier <CODE>incomplete</CODE> appears, then any <I>R</I> in
|
|
an open specification may also be an interface or an abstract.
|
|
</P>
|
|
<P>
|
|
Semantic conditions:
|
|
</P>
|
|
<UL>
|
|
<LI>each <CODE>cat</CODE> judgement in <I>A</I>
|
|
must have a corresponding, unique
|
|
<CODE>lincat</CODE> judgement in <I>C</I>
|
|
<LI>each <CODE>fun</CODE> judgement in <I>A</I>
|
|
must have a corresponding, unique
|
|
<CODE>lin</CODE> judgement in <I>C</I>
|
|
<LI>names in restriction lists must be defined in the restricted module
|
|
<LI>inherited constants may not depend on names excluded by restriction
|
|
</UL>
|
|
|
|
<A NAME="toc27"></A>
|
|
<H2>Resource modules</H2>
|
|
<P>
|
|
Syntax:
|
|
</P>
|
|
<P>
|
|
<CODE>resource</CODE> R <CODE>=</CODE>
|
|
(R<sub>1</sub>,...,R<sub>n</sub> <CODE>**</CODE>)?
|
|
(<CODE>open</CODE> O<sub>1</sub>,...,O<sub>k</sub> <CODE>in</CODE>)?
|
|
<CODE>{</CODE>J<sub>1</sub> <CODE>;</CODE> ... <CODE>;</CODE> J<sub>m</sub> <CODE>; }</CODE>
|
|
</P>
|
|
<P>
|
|
where
|
|
</P>
|
|
<UL>
|
|
<LI>i >= 0
|
|
<LI>each <I>R<sub>i</sub></I> is a resource, instance, or concrete module,
|
|
possibly with restrictions on inheritance, i.e. <I>R<sub>i</sub></I><CODE>-[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
<LI>each <I>O<sub>i</sub></I> is an open specification, of one of the forms
|
|
<UL>
|
|
<LI><I>P</I>
|
|
<LI><CODE>(</CODE><I>Q</I><CODE>=</CODE><I>R</I><CODE>)</CODE>
|
|
</UL>
|
|
</UL>
|
|
|
|
<P>
|
|
where <I>P</I> is a resource, instance, or concrete, and <I>Q</I> is any identifier
|
|
</P>
|
|
<UL>
|
|
<LI>each <I>J<sub>i</sub></I> is a judgement of one of the forms <CODE>oper, param</CODE>
|
|
</UL>
|
|
|
|
<P>
|
|
Semantic conditions:
|
|
</P>
|
|
<UL>
|
|
<LI>all names defined in each <I>R<sub>i</sub></I> and <I>R</I> must be distinct
|
|
<LI>all constants declared must have a definition
|
|
<LI>names in restriction lists must be defined in the restricted module
|
|
<LI>inherited constants may not depend on names excluded by restriction
|
|
</UL>
|
|
|
|
<A NAME="toc28"></A>
|
|
<H2>Interface modules</H2>
|
|
<P>
|
|
Syntax:
|
|
</P>
|
|
<P>
|
|
<CODE>interface</CODE> R <CODE>=</CODE>
|
|
(R<sub>1</sub>,...,R<sub>n</sub> <CODE>**</CODE>)?
|
|
(<CODE>open</CODE> O<sub>1</sub>,...,O<sub>k</sub> <CODE>in</CODE>)?
|
|
<CODE>{</CODE>J<sub>1</sub> <CODE>;</CODE> ... <CODE>;</CODE> J<sub>m</sub> <CODE>; }</CODE>
|
|
</P>
|
|
<P>
|
|
where
|
|
</P>
|
|
<UL>
|
|
<LI>i >= 0
|
|
<LI>each <I>R<sub>i</sub></I> is an interface or abstract module,
|
|
possibly with restrictions on inheritance, i.e. <I>R<sub>i</sub></I><CODE>-[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
<LI>each <I>O<sub>i</sub></I> is an open specification, of one of the forms
|
|
<UL>
|
|
<LI><I>P</I>
|
|
<LI><CODE>(</CODE><I>Q</I><CODE>=</CODE><I>R</I><CODE>)</CODE>
|
|
</UL>
|
|
</UL>
|
|
|
|
<P>
|
|
where <I>P</I> is a resource, instance, or concrete, and <I>Q</I> is any identifier
|
|
</P>
|
|
<UL>
|
|
<LI>each <I>J<sub>i</sub></I> is a judgement of one of the forms <CODE>oper, param</CODE>
|
|
</UL>
|
|
|
|
<P>
|
|
Semantic conditions:
|
|
</P>
|
|
<UL>
|
|
<LI>all names declared in each <I>R<sub>i</sub></I> and <I>R</I> must be distinct
|
|
<LI>names in restriction lists must be defined in the restricted module
|
|
<LI>inherited constants may not depend on names excluded by restriction
|
|
</UL>
|
|
|
|
<A NAME="toc29"></A>
|
|
<H2>Instance modules</H2>
|
|
<P>
|
|
Syntax:
|
|
</P>
|
|
<P>
|
|
<CODE>instance</CODE> R <CODE>of</CODE> I <CODE>=</CODE>
|
|
(R<sub>1</sub>,...,R<sub>n</sub> <CODE>**</CODE>)?
|
|
(<CODE>open</CODE> O<sub>1</sub>,...,O<sub>k</sub> <CODE>in</CODE>)?
|
|
<CODE>{</CODE>J<sub>1</sub> <CODE>;</CODE> ... <CODE>;</CODE> J<sub>m</sub> <CODE>; }</CODE>
|
|
</P>
|
|
<P>
|
|
where
|
|
</P>
|
|
<UL>
|
|
<LI>i >= 0
|
|
<LI><I>I</I> is an interface module
|
|
<LI>each <I>R<sub>i</sub></I> is an instance, resource, or concrete module,
|
|
possibly with restrictions on inheritance, i.e. <I>R<sub>i</sub></I><CODE>-[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
<P></P>
|
|
<LI>each <I>O<sub>i</sub></I> is an open specification, of one of the forms
|
|
<UL>
|
|
<LI><I>P</I>
|
|
<LI><CODE>(</CODE><I>Q</I><CODE>=</CODE><I>R</I><CODE>)</CODE>
|
|
</UL>
|
|
</UL>
|
|
|
|
<P>
|
|
where <I>P</I> is a resource, instance, or concrete, and <I>Q</I> is any identifier
|
|
</P>
|
|
<UL>
|
|
<LI>each <I>J<sub>i</sub></I> is a judgement of one of the forms
|
|
<CODE>oper, param</CODE>
|
|
</UL>
|
|
|
|
<P>
|
|
Semantic conditions:
|
|
</P>
|
|
<UL>
|
|
<LI>all names declared in each <I>R<sub>i</sub></I>, <I>I</I>, and <I>R</I> must be distinct
|
|
<LI>all constants declared in <I>I</I> must have a definition either in
|
|
<I>I</I> or <I>R</I>
|
|
<LI>names in restriction lists must be defined in the restricted module
|
|
<LI>inherited constants may not depend on names excluded by restriction
|
|
</UL>
|
|
|
|
<A NAME="toc30"></A>
|
|
<H2>Instantiated concrete syntax modules</H2>
|
|
<P>
|
|
Syntax:
|
|
</P>
|
|
<P>
|
|
<CODE>concrete</CODE> C <CODE>of</CODE> A <CODE>=</CODE>
|
|
(C<sub>1</sub>,...,C<sub>n</sub> <CODE>**</CODE>)?
|
|
B
|
|
<CODE>with</CODE>
|
|
<CODE>(</CODE>I<sub>1</sub> <CODE>=</CODE>J<sub>1</sub><CODE>),</CODE> ...
|
|
<CODE>, (</CODE>I<sub>p</sub> <CODE>=</CODE>J<sub>p</sub><CODE>)</CODE>
|
|
(<CODE>-</CODE>? <CODE>[</CODE>c<sub>1</sub>,...,c<sub>q</sub> <CODE>]</CODE>)?
|
|
(<CODE>**</CODE>?
|
|
(<CODE>open</CODE> O<sub>1</sub>,...,O<sub>k</sub> <CODE>in</CODE>)?
|
|
<CODE>{</CODE>J<sub>1</sub> <CODE>;</CODE> ... <CODE>;</CODE> J<sub>m</sub> <CODE>; }</CODE>)? <CODE>;</CODE>
|
|
</P>
|
|
<P>
|
|
where
|
|
</P>
|
|
<UL>
|
|
<LI>i >= 0
|
|
<LI><I>A</I> is an abstract module
|
|
<LI>each <I>C<sub>i</sub></I> is a concrete module,
|
|
possibly with restrictions on inheritance, i.e. <I>R<sub>i</sub></I><CODE>-[</CODE><I>f,..,g</I><CODE>]</CODE>
|
|
<LI><I>B</I> is an incomplete concrete syntax of <I>A</I>
|
|
<LI>each <I>I<sub>i</sub></I> is an interface or an abstract
|
|
<LI>each <I>J<sub>i</sub></I> is an instance or a concrete of <I>I<sub>i</sub></I>
|
|
<LI>each <I>O<sub>i</sub></I> is an open specification, of one of the forms
|
|
<UL>
|
|
<LI><I>R</I>
|
|
<LI><CODE>(</CODE><I>Q</I><CODE>=</CODE><I>R</I><CODE>)</CODE>
|
|
</UL>
|
|
</UL>
|
|
|
|
<P>
|
|
where <I>R</I> is a resource, instance, or concrete, and <I>Q</I> is any identifier
|
|
</P>
|
|
<UL>
|
|
<LI>each <I>J<sub>i</sub></I> is a judgement of one of the forms
|
|
<CODE>lincat, lin, lindef, printname</CODE>; also the forms <CODE>oper, param</CODE> are
|
|
allowed, but they cannot be inherited.
|
|
</UL>
|
|
|
|
|
|
<!-- html code generated by txt2tags 2.3 (http://txt2tags.sf.net) -->
|
|
<!-- cmdline: txt2tags -\-toc -thtml gf-modules.txt -->
|
|
</BODY></HTML>
|