<!-- ============ User Notation ====================== -->
<chapter id="sec_usernotation">
<title>Extending the syntax</title>
- &TODO;
-</chapter>
+ Introduction: &TODO;
+ <sect1>
+ <title>notation</title>
+ <titleabbrev>notation</titleabbrev>
+ <para><userinput>notation usage "presentation" associativity with precedence p for content</userinput></para>
+ <para id="notation">
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">notation</emphasis>
+ [&usage;] <emphasis role="bold">"</emphasis>¬ation_lhs;<emphasis role="bold">"</emphasis> [&associativity;] <emphasis role="bold">with</emphasis> <emphasis role="bold">precedence</emphasis> &nat;
+ <emphasis role="bold">for</emphasis>
+ ¬ation_rhs;
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Declares a mapping between the presentation
+ AST <command>presentation</command> and the content AST
+ <command>content</command>. The declared presentation AST fragment
+ <command>presentation</command> is at precedence level
+ <command>p</command>. The precedence level is used to determine where
+ parentheses must be inserted. In particular, the content AST fragment
+ <command>content</command> is actually a pattern, since it contains
+ placeholders (variables) for sub-ASTs. Every placeholder for a term
+ is given an expected precedence level. Parentheses must be inserted
+ around sub-ASTs having a precedence level strictly smaller than the
+ expected one.</para>
+ <para>If <command>presentation</command> describes a binary
+ infix operator and if no precedence level is explicitly given for the
+ operator arguments, an <command>associativity</command> declaration
+ can be given to automatically choose the right level for the operands.
+ Otherwise, no <command>associativity</command> can be given.</para>
+ <para>If <command>direction</command> is
+ omitted, the mapping is bi-directional and is used both during
+ parsing and pretty-printing of terms. If <command>direction</command>
+ is <command>></command>, the mapping is used only during parsing;
+ if it is <command><</command>, it is used only during
+ pretty-printing. Thus it is possible to use simple notations to type
+ for writing the term, and nicer ones for rendering it.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Notation arguments:</term>
+ <listitem>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>usage</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.usage">&usage;</entry>
+ <entry>::=</entry>
+ <entry><emphasis role="bold"><</emphasis></entry>
+ <entry>Only for pretty-printing</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">></emphasis></entry>
+ <entry>Only for parsing</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>associativity</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.associativity">&associativity;</entry>
+ <entry>::=</entry>
+ <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
+ <entry>Left associative</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
+ <entry>Right associative</entry>
+ </row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry><emphasis role="bold">non</emphasis> <emphasis role="bold">associative</emphasis></entry>
+ <entry>Non associative (default)</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>notation_rhs</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.notation_rhs">¬ation_rhs;</entry>
+ <entry>::=</entry>
+ <entry>&TODO;</entry>
+ <entry>&TODO;</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>notation_lhs</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.notation_lhs">¬ation_lhs;</entry>
+ <entry>::=</entry>
+ <entry>&TODO;</entry>
+ <entry>&TODO;</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1>
+ <title>interpretation</title>
+ <titleabbrev>interpretation</titleabbrev>
+ <para><userinput>interpretation "description" 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
+ rhs</userinput></para>
+ <para id="interpretation">
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">interpretation</emphasis>
+ &qstring; &csymbol; [&interpretation_argument;]…
+ <emphasis role="bold">=</emphasis>
+ &interpretation_rhs;
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It declares a bi-directional mapping <command>{…}</command> between the content-level AST <command>'symbol t<subscript>1</subscript> … t<subscript>n</subscript></command> and the semantic term <command>rhs[{t<subscript>1</subscript>}/p<subscript>1</subscript>;…;{t<subscript>n</subscript>}/p<subscript>n</subscript>]</command>
+ (the simultaneous substitution in <command>rhs</command> of the
+ interpretation <command>{…}</command> of every content-level
+ actual argument <command>t<subscript>i</subscript></command> for its
+ corresponding formal parameter
+ <command>p<subscript>i</subscript></command>). The
+ <command>description</command> must be a textual description of the
+ meaning associated to <command>'symbol</command> by this
+ interpretation, and is used by the user interface of Matita to
+ provide feedback on the interpretation of ambiguous terms.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Interpretation arguments:</term>
+ <listitem>
+
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>interpretation_argument</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.interpretation_argument">&interpretation_argument;</entry>
+ <entry>::=</entry>
+ <entry>[<emphasis role="bold">η</emphasis><emphasis role="bold">.</emphasis>]… &id;</entry>
+ <entry>A formal parameter. If the name of the formal parameter is
+ prefixed by n symbols "η", then the mapping performs
+ (multiple) η-expansions to grant that the semantic actual
+ parameter begins with at least n λ-abstractions.</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+ <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+ <title>interpretation_rhs</title>
+ <tgroup cols="4">
+ <tbody>
+ <row>
+ <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
+ <entry>::=</entry>
+ <entry>&uri;</entry>
+ <entry>A constant, specified by its URI</entry>
+ </row>
+ <row>
+ <entry></entry>
+ <entry>|</entry>
+ <entry>&id;</entry>
+ <entry>A constant, specified by its name, or a bound variable. If
+ the constant name is ambiguous, the one corresponding to the
+ last implicitly or explicitly specified alias is used.</entry>
+ </row>
+ <row>
+ <entry></entry>
+ <entry>|</entry>
+ <entry><emphasis role="bold">_</emphasis></entry>
+ <entry>An implicit parameter</entry>
+ </row>
+ <row>
+ <entry></entry>
+ <entry>|</entry>
+ <entry><emphasis role="bold">(</emphasis>
+ &interpretation_rhs;
+ [&interpretation_rhs;]…
+ <emphasis role="bold">)</emphasis></entry>
+ <entry>An application</entry>
+ </row>
+ </tbody>
+ </tgroup>
+ </table>
+
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+</chapter>
projects / helm.git / blobdiff