module rules added

doc/gf-modules.html

@@ -12,7 +12,7 @@
 
 <p>
 
-8/4/2005
+8/4/2005 - 10/4
 
 <p>
 
@@ -42,7 +42,7 @@ This document is meant as an appendix to the GF tutorial, and
 presupposes knowledge of GF judgements and expressions. It aims
 just to tell what module system adds to the old functionality;
 some information is repeated to give understanding on how the
-module system related to the already familiar uses of GF grammars.
+module system relates to the already familiar uses of GF grammars.
 
 
 
@@ -758,7 +758,7 @@ the <tt>instances</tt>.
 by non-compositional functions (<b>transfer rules</b>) between the
 source and target languages. They are being introduce to GF as a module
 type of its own, but their development is still in progress. What
-will be available are <i>at least</i> <tt>fun</tt> and <tt>def</tt>
+will be available are at least <tt>fun</tt> and <tt>def</tt>
 judgements, but more is needed. It has not yet been defined how
 transfer modules are integrated in multilingual grammars, i.e.\
 where in the grammar it is specified what transfer to use.
@@ -771,7 +771,198 @@ has not been implemented.)
 <h2>Summary of module syntax and semantics</h2>
 
 
+<h4>Abstract syntax modules</h4>
 
+Syntax: 
+<p>
+<tt>abstract</tt> A <tt>=</tt> (A_1,...,A_n <tt>**</tt>)?
+<tt>{</tt>J_1 <tt>;</tt> ... <tt>;</tt> J_m <tt>; }</tt>
+
+<p>
+
+where
+<ul>
+<li> i >= 0
+<li> each <i>A_i</i> is itself an abstract module
+<li> each <i>J_i</i> is a judgement of one of the forms
+     <tt>cat, fun, def, data</tt>
+</ul>
+Semantic conditions:
+<ul>
+<li> all names declared in each <i>A_i</i> and <i>A</i> must be distinct
+</ul>
+
+<h4>Concrete syntax modules</h4>
+
+Syntax: 
+<p>
+<tt>incomplete</tt>? <tt>concrete</tt> C <tt>of</tt> A <tt>=</tt>
+(C_1,...,C_n <tt>**</tt>)?
+(<tt>open</tt> O_1,...,O_k <tt>in</tt>)?
+<tt>{</tt>J_1 <tt>;</tt> ... <tt>;</tt> J_m <tt>; }</tt>
+
+<p>
+
+where
+<ul>
+<li> i >= 0
+<li> <i>A</i> is an abstract module
+<li> each <i>C_i</i> is a concrete module
+<li> each <i>O_i</i> is an open specification, of one of the forms
+  <ul>
+    <li> <i>R</i> 
+    <li> <tt>(</tt><i>Q</i><tt>=</tt><i>R</i><tt>)</tt> 
+  </ul>
+where <i>R</i> is a resource, instance, or concrete, and
+<i>Q</i> is any identifier
+<li> each <i>J_i</i> is a judgement of one of the forms
+     <tt>lincat, lin, lindef, printname</tt>
+</ul>
+
+<p>
+
+If the modifier <tt>incomplete</tt> appears, then any <i>R</i> in
+an open specification may also be an interface.
+
+<p>
+
+Semantic conditions:
+<ul>
+<li> each <tt>cat</tt> judgement in <i>A</i>
+     must have a corresponding, unique
+     <tt>lincat</tt> judgement in <i>C</i>
+<li> each <tt>fun</tt> judgement in <i>A</i>
+     must have a corresponding, unique
+     <tt>lin</tt> judgement in <i>C</i>
+</ul>
+
+
+<h4>Resource modules</h4>
+
+Syntax: 
+<p>
+<tt>resource</tt> R <tt>=</tt>
+(R_1,...,R_n <tt>**</tt>)?
+(<tt>open</tt> O_1,...,O_k <tt>in</tt>)?
+<tt>{</tt>J_1 <tt>;</tt> ... <tt>;</tt> J_m <tt>; }</tt>
+
+<p>
+where
+<ul>
+<li> i >= 0
+<li> each <i>R_i</i> is a resource module
+<li> each <i>O_i</i> is an open specification, of one of the forms
+  <ul>
+    <li> <i>P</i> 
+    <li> <tt>(</tt><i>Q</i><tt>=</tt><i>R</i><tt>)</tt> 
+  </ul>
+where <i>P</i> is a resource, instance, or concrete, and
+<i>Q</i> is any identifier
+<li> each <i>J_i</i> is a judgement of one of the forms
+     <tt>oper, param</tt>
+</ul>
+
+<p>
+
+Semantic conditions:
+<ul>
+<li> all names declared in each <i>R_i</i> and <i>R</i> must be distinct
+<li> all constants declared must have a definition
+</ul>
+
+
+<h4>Interface modules</h4>
+
+Syntax: 
+<p>
+<tt>interface</tt> R <tt>=</tt>
+(R_1,...,R_n <tt>**</tt>)?
+(<tt>open</tt> O_1,...,O_k <tt>in</tt>)?
+<tt>{</tt>J_1 <tt>;</tt> ... <tt>;</tt> J_m <tt>; }</tt>
+
+<p>
+where
+<ul>
+<li> i >= 0
+<li> each <i>R_i</i> is an interface module
+<li> each <i>O_i</i> is an open specification, of one of the forms
+  <ul>
+    <li> <i>P</i> 
+    <li> <tt>(</tt><i>Q</i><tt>=</tt><i>R</i><tt>)</tt> 
+  </ul>
+where <i>P</i> is a resource, instance, or concrete, and
+<i>Q</i> is any identifier
+<li> each <i>J_i</i> is a judgement of one of the forms
+     <tt>oper, param</tt>
+</ul>
+
+<p>
+
+Semantic conditions:
+<ul>
+<li> all names declared in each <i>R_i</i> and <i>R</i> must be distinct
+</ul>
+
+
+
+<h4>Instance modules</h4>
+
+Syntax: 
+<p>
+<tt>instance</tt> R <tt>of</tt> I <tt>=</tt>
+(R_1,...,R_n <tt>**</tt>)?
+(<tt>open</tt> O_1,...,O_k <tt>in</tt>)?
+<tt>{</tt>J_1 <tt>;</tt> ... <tt>;</tt> J_m <tt>; }</tt>
+
+<p>
+where
+<ul>
+<li> i >= 0
+<li> <i>I</i> is an interface module
+<li> each <i>R_i</i> is an instance module
+<li> each <i>O_i</i> is an open specification, of one of the forms
+  <ul>
+    <li> <i>P</i> 
+    <li> <tt>(</tt><i>Q</i><tt>=</tt><i>R</i><tt>)</tt> 
+  </ul>
+where <i>P</i> is a resource, instance, or concrete, and
+<i>Q</i> is any identifier
+<li> each <i>J_i</i> is a judgement of one of the forms
+     <tt>oper, param</tt>
+</ul>
+
+<p>
+
+Semantic conditions:
+<ul>
+<li> all names declared in each <i>R_i</i>, <i>I</i>, and <i>R</i> must be distinct
+<li> all constants declared in <tt>I</tt> must have a definition either in
+  <tt>I</tt> or <tt>R</tt>
+</ul>
+
+
+<h4>Instantiated concrete syntax modules</h4>
+
+Syntax: 
+<p>
+<tt>concrete</tt> C <tt>of</tt> A <tt>=</tt>
+(C_1,...,C_n <tt>**</tt>)?
+B
+<tt>with</tt>
+<tt>(</tt>I_1 <tt>=</tt>J_1<tt>),</tt> ... 
+<tt>, (</tt>I_m <tt>=</tt>J_m<tt>) ;</tt>
+
+<p>
+
+where
+<ul>
+<li> i >= 0
+<li> <i>A</i> is an abstract module
+<li> each <i>C_i</i> is a concrete module
+<li> <i>B</i> is an incomplete concrete syntax of <i>A</i>
+<li> each <i>I_i</i> is an interface
+<li> each <i>J_i</i> is an instance of <i>I_i</i>
+</ul>
 
 
 </body>