helm/software/matita/help/C/sec_usernotation.xml

   1
   2 <!-- ============ User Notation ====================== -->
   3 <chapter id="sec_usernotation">
   4  <title>Extending the syntax</title>
   5   Introduction: &TODO;
   6  <sect1>
   7   <title>notation</title>
   8   <titleabbrev>notation</titleabbrev>
   9    <para><userinput>notation usage &quot;presentation&quot; associativity with precedence p for content</userinput></para>
  10   <para id="notation">
  11     <variablelist>
  12       <varlistentry role="tactic.synopsis">
  13         <term>Synopsis:</term>
  14         <listitem>
  15           <para><emphasis role="bold">notation</emphasis>
  16            [&usage;] <emphasis role="bold">&quot;</emphasis>&notation_lhs;<emphasis role="bold">&quot;</emphasis> [&associativity;] <emphasis role="bold">with</emphasis> <emphasis role="bold">precedence</emphasis> &nat;
  17            <emphasis role="bold">for</emphasis>
  18            &notation_rhs;
  19           </para>
  20         </listitem>
  21       </varlistentry>
  22       <varlistentry>
  23        <term>Action:</term>
  24        <listitem>
  25          <para>Declares a mapping between the presentation
  26           AST <command>presentation</command> and the content AST
  27           <command>content</command>. The declared presentation AST fragment
  28           <command>presentation</command> is at precedence level
  29           <command>p</command>. The precedence level is used to determine where
  30           parentheses must be inserted. In particular, the content AST fragment
  31           <command>content</command> is actually a pattern, since it contains
  32           placeholders (variables) for sub-ASTs. Every placeholder for a term
  33           is given an expected precedence level. Parentheses must be inserted
  34           around sub-ASTs having a precedence level strictly smaller than the
  35           expected one.</para>
  36           <para>If <command>presentation</command> describes a binary
  37           infix operator and if no precedence level is explicitly given for the
  38           operator arguments, an <command>associativity</command> declaration
  39           can be given to automatically choose the right level for the operands.
  40           Otherwise, no <command>associativity</command> can be given.</para>
  41          <para>If <command>direction</command> is
  42           omitted, the mapping is bi-directional and is used both during
  43           parsing and pretty-printing of terms. If <command>direction</command>
  44           is <command>&gt;</command>, the mapping is used only during parsing;
  45           if it is <command>&lt;</command>, it is used only during
  46           pretty-printing. Thus it is possible to use simple notations to type
  47           for writing the term, and nicer ones for rendering it.</para>
  48        </listitem>
  49       </varlistentry>
  50       <varlistentry>
  51         <term>Notation arguments:</term>
  52         <listitem>
  53
  54     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  55       <title>usage</title>
  56       <tgroup cols="4">
  57       <tbody>
  58        <row>
  59         <entry id="grammar.usage">&usage;</entry>
  60         <entry>::=</entry>
  61         <entry><emphasis role="bold">&lt;</emphasis></entry>
  62         <entry>Only for pretty-printing</entry>
  63        </row>
  64        <row>
  65         <entry/>
  66         <entry>|</entry>
  67         <entry><emphasis role="bold">&gt;</emphasis></entry>
  68         <entry>Only for parsing</entry>
  69        </row>
  70       </tbody>
  71       </tgroup>
  72      </table>
  73
  74     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  75       <title>associativity</title>
  76       <tgroup cols="4">
  77       <tbody>
  78        <row>
  79         <entry id="grammar.associativity">&associativity;</entry>
  80         <entry>::=</entry>
  81         <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
  82         <entry>Left associative</entry>
  83        </row>
  84        <row>
  85         <entry/>
  86         <entry>|</entry>
  87         <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
  88         <entry>Right associative</entry>
  89        </row>
  90        <row>
  91         <entry/>
  92         <entry>|</entry>
  93         <entry><emphasis role="bold">non</emphasis> <emphasis role="bold">associative</emphasis></entry>
  94         <entry>Non associative (default)</entry>
  95        </row>
  96       </tbody>
  97       </tgroup>
  98      </table>
  99
 100     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 101       <title>notation_rhs</title>
 102       <tgroup cols="4">
 103       <tbody>
 104        <row>
 105         <entry id="grammar.notation_rhs">&notation_rhs;</entry>
 106         <entry>::=</entry>
 107         <entry>&TODO;</entry>
 108         <entry>&TODO;</entry>
 109        </row>
 110       </tbody>
 111       </tgroup>
 112      </table>
 113
 114     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 115       <title>notation_lhs</title>
 116       <tgroup cols="4">
 117       <tbody>
 118        <row>
 119         <entry id="grammar.notation_lhs">&notation_lhs;</entry>
 120         <entry>::=</entry>
 121         <entry>&TODO;</entry>
 122         <entry>&TODO;</entry>
 123        </row>
 124       </tbody>
 125       </tgroup>
 126      </table>
 127
 128         </listitem>
 129       </varlistentry>
 130     </variablelist>
 131   </para>
 132  </sect1>
 133  <sect1>
 134    <title>interpretation</title>
 135    <titleabbrev>interpretation</titleabbrev>
 136    <para><userinput>interpretation &quot;description&quot; 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
 137          rhs</userinput></para>
 138    <para id="interpretation">
 139     <variablelist>
 140       <varlistentry role="tactic.synopsis">
 141         <term>Synopsis:</term>
 142         <listitem>
 143           <para><emphasis role="bold">interpretation</emphasis>
 144            &qstring; &csymbol; [&interpretation_argument;]…
 145            <emphasis role="bold">=</emphasis>
 146            &interpretation_rhs;
 147           </para>
 148         </listitem>
 149       </varlistentry>
 150       <varlistentry>
 151        <term>Action:</term>
 152        <listitem>
 153          <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>
 154           (the simultaneous substitution in <command>rhs</command> of the
 155           interpretation <command>{…}</command> of every content-level
 156           actual argument <command>t<subscript>i</subscript></command> for its
 157           corresponding formal parameter
 158           <command>p<subscript>i</subscript></command>). The
 159           <command>description</command> must be a textual description of the
 160           meaning associated to <command>'symbol</command> by this
 161           interpretation, and is used by the user interface of Matita to
 162           provide feedback on the interpretation of ambiguous terms.
 163          </para>
 164        </listitem>
 165       </varlistentry>
 166       <varlistentry>
 167         <term>Interpretation arguments:</term>
 168         <listitem>
 169
 170     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 171       <title>interpretation_argument</title>
 172       <tgroup cols="4">
 173       <tbody>
 174        <row>
 175         <entry id="grammar.interpretation_argument">&interpretation_argument;</entry>
 176         <entry>::=</entry>
 177         <entry>[<emphasis role="bold">η</emphasis><emphasis role="bold">.</emphasis>]… &id;</entry>
 178         <entry>A formal parameter. If the name of the formal parameter is
 179          prefixed by n symbols &quot;η&quot;, then the mapping performs
 180          (multiple) η-expansions to grant that the semantic actual
 181          parameter begins with at least n λ-abstractions.</entry>
 182        </row>
 183       </tbody>
 184       </tgroup>
 185      </table>
 186     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 187       <title>interpretation_rhs</title>
 188       <tgroup cols="4">
 189       <tbody>
 190        <row>
 191         <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
 192         <entry>::=</entry>
 193         <entry>&uri;</entry>
 194         <entry>A constant, specified by its URI</entry>
 195        </row>
 196        <row>
 197         <entry></entry>
 198         <entry>|</entry>
 199         <entry>&id;</entry>
 200         <entry>A constant, specified by its name, or a bound variable. If
 201                the constant name is ambiguous, the one corresponding to the
 202                last implicitly or explicitly specified alias is used.</entry>
 203        </row>
 204        <row>
 205         <entry></entry>
 206         <entry>|</entry>
 207         <entry><emphasis role="bold">_</emphasis></entry>
 208         <entry>An implicit parameter</entry>
 209        </row>
 210        <row>
 211         <entry></entry>
 212         <entry>|</entry>
 213         <entry><emphasis role="bold">(</emphasis>
 214                &interpretation_rhs;
 215                [&interpretation_rhs;]…
 216                <emphasis role="bold">)</emphasis></entry>
 217         <entry>An application</entry>
 218        </row>
 219       </tbody>
 220       </tgroup>
 221      </table>
 222
 223         </listitem>
 224       </varlistentry>
 225     </variablelist>
 226    </para>
 227  </sect1>
 228 </chapter>