X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=11b06b21cab7269c8bd3bd2867ed8bc48b31f1c5;hb=aebd5af5c7d3e422813159d81fde05b6a9778765;hp=c50e590b0636ecbdc9132e17da5d2383372e2d26;hpb=9efaf66294d18446b7cd960f9ed4203799073e62;p=helm.git

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index c50e590b0..11b06b21c 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -26,78 +26,90 @@
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
-  <para>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>id</title>
       <tgroup cols="4">
       <tbody>
        <row>
-	<entry id="id">&id;</entry>
+	<entry id="grammar.id">&id;</entry>
 	<entry>::=</entry>
-        <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink> prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉</emphasis></entry>
+        <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink> prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉</emphasis></entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>nat</title>
       <tgroup cols="4">
       <tbody>
        <row>
-	<entry id="nat">&nat;</entry>
+	<entry id="grammar.nat">&nat;</entry>
 	<entry>::=</entry>
-	<entry><emphasis>〈〈any sequence of valid <ulink url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink></emphasis></entry>
+	<entry><emphasis>〈〈any sequence of valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink>〉〉</emphasis></entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>char</title>
       <tgroup cols="4">
       <tbody>
        <row>
-	<entry id="char">&char;</entry>
+	<entry id="grammar.char">&char;</entry>
 	<entry>::=</entry>
 	<entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>uri-step</title>
       <tgroup cols="4">
       <tbody>
        <row>
-	<entry id="uri-step">&uri-step;</entry>
+	<entry id="grammar.uri-step">&uri-step;</entry>
 	<entry>::=</entry>
 	<entry>&char;[&char;]…</entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-    <table frame="all" rowsep="0" colsep="0">
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>uri</title>
       <tgroup cols="4">
       <tbody>
        <row>
-	<entry id="uri">&uri;</entry>
+	<entry id="grammar.uri">&uri;</entry>
 	<entry>::=</entry>
 	<entry>[<emphasis role="bold">cic:/</emphasis>|<emphasis role="bold">theory:/</emphasis>]&uri-step;[<emphasis role="bold">/</emphasis>&uri-step;]…<emphasis role="bold">.</emphasis>&id;[<emphasis role="bold">.</emphasis>&id;]…[<emphasis role="bold">#xpointer(</emphasis>&nat;<emphasis role="bold">/</emphasis>&nat;[<emphasis role="bold">/</emphasis>&nat;]…<emphasis role="bold">)</emphasis>]</entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-  </para>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
+
+  <!-- ZACK: Sample EBNF snippet, see:
+  http://www.docbook.org/tdg/en/html/productionset.html -->
+  <!--
+  <productionset>
+    <title>Terms</title>
+    <production id="grammar.term">
+      <lhs>&term;</lhs>
+      <rhs>&sterm;</rhs>
+      <lineannotation></lineannotation>
+    </production>
+  </productionset>
+  -->
+
   <para>
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Terms</title>
     <tgroup cols="4">
     <tbody>
      <row>
-      <entry id="term">&term;</entry>
+      <entry id="grammar.term">&term;</entry>
       <entry>::=</entry>
       <entry>&sterm;</entry>
       <entry>simple or delimited term</entry>
@@ -141,11 +153,10 @@
      <row>
       <entry/>
       <entry>|</entry>
-      <entry><emphasis role="bold">let</emphasis>
-      [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
-      &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
-      [<emphasis role="bold">:</emphasis> &term;]
-      <emphasis role="bold">≝</emphasis> &term;
+      <entry>
+	<emphasis role="bold">let</emphasis>
+	[<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
+	&rec_def;
       </entry>
       <entry>(co)recursive definitions</entry>
      </row>
@@ -153,10 +164,7 @@
       <entry/>
       <entry/>
       <entry>
-      [<emphasis role="bold">and</emphasis>
-      [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]… [<emphasis role="bold">on</emphasis> &nat;]
-      [<emphasis role="bold">:</emphasis> &term;]
-      <emphasis role="bold">≝</emphasis> &term;]…
+      [<emphasis role="bold">and</emphasis> &rec_def;]…
       </entry>
       <entry/>
      </row>
@@ -174,16 +182,34 @@
       <entry>…</entry>
       <entry>user provided notation</entry>
      </row>
+      <row>
+	<entry id="grammar.rec_def">&rec_def;</entry>
+	<entry>::=</entry>
+	<entry>
+	  &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
+	</entry>
+	<entry />
+      </row>
+      <row>
+	<entry />
+	<entry />
+	<entry>
+	  [<emphasis role="bold">on</emphasis> &nat;]
+	  [<emphasis role="bold">:</emphasis> &term;]
+	  <emphasis role="bold">≝</emphasis> &term;]
+	</entry>
+	<entry />
+      </row>
     </tbody>
    </tgroup>
   </table>
 
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Simple terms</title>
     <tgroup cols="4">
     <tbody>
      <row>
-      <entry id="sterm">&sterm;</entry>
+      <entry id="grammar.sterm">&sterm;</entry>
       <entry>::=</entry>
       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
       <entry/>
@@ -252,11 +278,9 @@
       <entry/>
       <entry>
        <emphasis role="bold">[</emphasis> 
-       &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
-         [
-         <emphasis role="bold">|</emphasis>
-         &match_pattern; <emphasis role="bold"> ⇒ </emphasis> &term;
-         ]…<emphasis role="bold">]</emphasis> </entry>
+       &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
+       <emphasis role="bold">]</emphasis> 
+      </entry>
       <entry/>
      </row>
      <row>
@@ -275,12 +299,12 @@
    </tgroup>
   </table>
 
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Arguments</title>
     <tgroup cols="4">
     <tbody>
      <row>
-      <entry id="args">&args;</entry>
+      <entry id="grammar.args">&args;</entry>
       <entry>::=</entry>
       <entry>
        <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
@@ -307,16 +331,8 @@
       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
       <entry/>
      </row>
-    </tbody>
-   </tgroup>
-  </table>
-
-  <table frame="all" rowsep="0" colsep="0">
-    <title>Miscellaneous arguments</title>
-    <tgroup cols="4">
-    <tbody>
      <row>
-      <entry id="args2">&args2;</entry>
+      <entry id="grammar.args2">&args2;</entry>
       <entry>::=</entry>
       <entry>&id;</entry>
       <entry/>
@@ -331,12 +347,18 @@
    </tgroup>
   </table>
 
-  <table frame="all" rowsep="0" colsep="0">
+  <table frame="topbot" rowsep="0" colsep="0" role="grammar">
     <title>Pattern matching</title>
     <tgroup cols="4">
     <tbody>
+      <row>
+	<entry id="grammar.match_branch">&match_branch;</entry>
+	<entry>::=</entry>
+	<entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
+	<entry />
+      </row>
      <row>
-      <entry id="match_pattern">&match_pattern;</entry>
+      <entry id="grammar.match_pattern">&match_pattern;</entry>
       <entry>::=</entry>
       <entry>&id;</entry>
       <entry>0-ary constructor</entry>
@@ -478,5 +500,95 @@
    </sect2>
   </sect1>
 
+  <sect1 id="tacticargs">
+   <title>Tactic arguments</title>
+   <para>This section documents the syntax of some recurring arguments for
+    tactics.</para>
+
+    <sect2 id="introsspec">
+    <title>intros-spec</title>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>intros-spec</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.intros-spec">&intros-spec;</entry>
+	<entry>::=</entry>
+        <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+        <para>The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.</para>
+    </sect2>
+
+    <sect2 id="pattern">
+    <title>pattern</title>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>pattern</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.pattern">&pattern;</entry>
+	<entry>::=</entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+        <para>&TODO;</para>
+    </sect2>
+
+    <sect2 id="reduction-kind">
+    <title>reduction-kind</title>
+    <para>Reduction kinds are normalization functions that transform a term
+     to a convertible but simpler one. Each reduction kind can be used both
+     as a tactic argument and as a stand-alone tactic.</para>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>reduction-kind</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.reduction-kind">&reduction-kind;</entry>
+	<entry>::=</entry>
+        <entry><emphasis role="bold">demodulate</emphasis></entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">normalize</emphasis></entry>
+        <entry>Computes the βδιζ-normal form</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">reduce</emphasis></entry>
+        <entry>Computes the βδιζ-normal form</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">simplify</emphasis></entry>
+        <entry>Computes a form supposed to be simpler</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
+        <entry>δ-reduces the constant or variable if specified, or that
+         in head position</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">whd</emphasis></entry>
+        <entry>Computes the βδιζ-weak-head normal form</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    </sect2>
+  </sect1>
+
 </chapter>