E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
<listitem><para>Alternatives are put in square brakets and they are
separated by vertical bars. E.g.: [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>]</para></listitem>
- <listitem><para>Repetition of sequences of elements are given by putting the
- first sequence in square brackets, that are followed by three dots.
+ <listitem><para>Repetitions of a sequence of elements are given by putting the
+ sequence in square brackets, that are followed by three dots. The empty
+ sequence is a valid repetition.
E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
+ <listitem><para>Characters belonging to a set of characters are given
+ by listing the set elements in square brackets. Hyphens are used to
+ specify ranges of characters in the set.
+ E.g.: [<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</para></listitem>
</orderedlist>
<sect1 id="terms_and_co">
<title>Terms & 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>〈〈&TODO;〉〉</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 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="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>char</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.char">&char;</entry>
<entry>::=</entry>
- <entry><emphasis>〈〈&TODO;〉〉</emphasis></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="grammar.uri-step">&uri-step;</entry>
+ <entry>::=</entry>
+ <entry>&char;[&char;]…</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <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>〈〈&TODO;〉〉</emphasis></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>
<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>
<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>
<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/>
<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>
</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;]
<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/>
</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>
</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>
projects / helm.git / blobdiff