matita/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">right</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>&unparsed_ast;</entry>
 108         <entry>&TODO;</entry>
 109        </row>
 110        <row>
 111         <entry></entry>
 112         <entry>|</entry>
 113         <entry>&unparsed_meta;</entry>
 114         <entry>&TODO;</entry>
 115        </row>
 116       </tbody>
 117       </tgroup>
 118      </table>
 119
 120     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 121       <title>unparsed_ast</title>
 122       <tgroup cols="4">
 123       <tbody>
 124        <row>
 125         <entry id="grammar.unparsed_ast">&unparsed_ast;</entry>
 126         <entry>::=</entry>
 127         <entry><emphasis role="bold">@{</emphasis>&enriched_term;<emphasis role="bold">}</emphasis></entry>
 128         <entry>A content level AST (a term which is parsed, but not disambiguated).</entry>
 129        </row>
 130        <row>
 131         <entry></entry>
 132         <entry>|</entry>
 133         <entry><emphasis role="bold">@</emphasis>&id;</entry>
 134         <entry><command>@id</command> is just an abbreviation for <command>@{id}</command></entry>
 135        </row>
 136        <row>
 137         <entry></entry>
 138         <entry>|</entry>
 139         <entry><emphasis role="bold">@</emphasis>&csymbol;</entry>
 140         <entry><command>@'symbol</command> is just an abbreviation for <command>@{'symbol}</command></entry>
 141        </row>
 142       </tbody>
 143       </tgroup>
 144      </table>
 145
 146     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 147       <title>enriched_term</title>
 148       <tgroup cols="4">
 149       <tbody>
 150        <row>
 151         <entry id="grammar.enriched_term">&enriched_term;</entry>
 152         <entry>::=</entry>
 153         <entry>〈〈A term that may contain occurrences of &unparsed_meta;, even as variable names in binders, and occurrences of &csymbol;〉〉</entry>
 154         <entry>&TODO;</entry>
 155        </row>
 156       </tbody>
 157       </tgroup>
 158      </table>
 159
 160     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 161       <title>unparsed_meta</title>
 162       <tgroup cols="4">
 163       <tbody>
 164        <row>
 165         <entry id="grammar.unparsed_meta">&unparsed_meta;</entry>
 166         <entry>::=</entry>
 167         <entry><emphasis role="bold">${</emphasis>&level2_meta;<emphasis role="bold">}</emphasis></entry>
 168         <entry>&TODO;</entry>
 169        </row>
 170        <row>
 171         <entry></entry>
 172         <entry>|</entry>
 173         <entry><emphasis role="bold">$</emphasis>&id;</entry>
 174         <entry><command>$id</command> is just an abbreviation for <command>${id}</command></entry>
 175        </row>
 176        <row>
 177         <entry></entry>
 178         <entry>|</entry>
 179         <entry><emphasis role="bold">$</emphasis><emphasis role="bold">_</emphasis></entry>
 180         <entry><command>$_</command> is just an abbreviation for <command>${_}</command></entry>
 181        </row>
 182       </tbody>
 183       </tgroup>
 184      </table>
 185
 186     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 187       <title>level2_meta</title>
 188       <tgroup cols="4">
 189       <tbody>
 190        <row>
 191         <entry id="grammar.level2_meta">&level2_meta;</entry>
 192         <entry>::=</entry>
 193         <entry>&unparsed_ast;</entry>
 194         <entry>&TODO;</entry>
 195        </row>
 196        <row>
 197         <entry></entry>
 198         <entry>|</entry>
 199         <entry><emphasis role="bold">term</emphasis> &nat; &id;</entry>
 200         <entry>&TODO;</entry>
 201        </row>
 202        <row>
 203         <entry></entry>
 204         <entry>|</entry>
 205         <entry><emphasis role="bold">number</emphasis> &id;</entry>
 206         <entry>&TODO;</entry>
 207        </row>
 208        <row>
 209         <entry></entry>
 210         <entry>|</entry>
 211         <entry><emphasis role="bold">ident</emphasis> &id;</entry>
 212         <entry>&TODO;</entry>
 213        </row>
 214        <row>
 215         <entry></entry>
 216         <entry>|</entry>
 217         <entry><emphasis role="bold">fresh</emphasis> &id;</entry>
 218         <entry>&TODO;</entry>
 219        </row>
 220        <row>
 221         <entry></entry>
 222         <entry>|</entry>
 223         <entry><emphasis role="bold">anonymous</emphasis></entry>
 224         <entry>&TODO;</entry>
 225        </row>
 226        <row>
 227         <entry></entry>
 228         <entry>|</entry>
 229         <entry>&id;</entry>
 230         <entry>&TODO;</entry>
 231        </row>
 232        <row>
 233         <entry></entry>
 234         <entry>|</entry>
 235         <entry><emphasis role="bold">fold</emphasis> [<emphasis role="bold">left</emphasis>|<emphasis role="bold">right</emphasis>] &level2_meta; <emphasis role="bold">rec</emphasis> &id; &level2_meta;</entry>
 236         <entry>&TODO;</entry>
 237        </row>
 238        <row>
 239         <entry></entry>
 240         <entry>|</entry>
 241         <entry><emphasis role="bold">default</emphasis> &level2_meta; &level2_meta;</entry>
 242         <entry>&TODO;</entry>
 243        </row>
 244        <row>
 245         <entry></entry>
 246         <entry>|</entry>
 247         <entry><emphasis role="bold">if</emphasis> &level2_meta; <emphasis role="bold">then</emphasis> &level2_meta; <emphasis role="bold">else</emphasis> &level2_meta;</entry>
 248         <entry>&TODO;</entry>
 249        </row>
 250        <row>
 251         <entry></entry>
 252         <entry>|</entry>
 253         <entry><emphasis role="bold">fail</emphasis></entry>
 254         <entry>&TODO;</entry>
 255        </row>
 256       </tbody>
 257       </tgroup>
 258      </table>
 259
 260     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 261       <title>notation_lhs</title>
 262       <tgroup cols="4">
 263       <tbody>
 264        <row>
 265         <entry id="grammar.notation_lhs">&notation_lhs;</entry>
 266         <entry>::=</entry>
 267         <entry>&layout; [&layout;]…</entry>
 268        </row>
 269       </tbody>
 270       </tgroup>
 271     </table>
 272
 273     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 274       <title>layout</title>
 275       <tgroup cols="4">
 276       <tbody>
 277        <row>
 278         <entry id="grammar.layout">&layout;</entry>
 279         <entry>::=</entry>
 280         <entry>&layout; <emphasis role="bold">\sub</emphasis> &layout;</entry>
 281         <entry>Subscript</entry>
 282        </row>
 283        <row>
 284         <entry></entry>
 285         <entry>|</entry>
 286         <entry>&layout; <emphasis role="bold">\sup</emphasis> &layout;</entry>
 287         <entry>Superscript</entry>
 288        </row>
 289        <row>
 290         <entry></entry>
 291         <entry>|</entry>
 292         <entry>&layout; <emphasis role="bold">\below</emphasis> &layout;</entry>
 293         <entry></entry>
 294        </row>
 295        <row>
 296         <entry></entry>
 297         <entry>|</entry>
 298         <entry>&layout; <emphasis role="bold">\above</emphasis> &layout;</entry>
 299         <entry></entry>
 300        </row>
 301        <row>
 302         <entry></entry>
 303         <entry>|</entry>
 304         <entry>&layout; <emphasis role="bold">\over</emphasis> &layout;</entry>
 305         <entry></entry>
 306        </row>
 307        <row>
 308         <entry></entry>
 309         <entry>|</entry>
 310         <entry>&layout; <emphasis role="bold">\atop</emphasis> &layout;</entry>
 311         <entry></entry>
 312        </row>
 313        <row>
 314         <entry></entry>
 315         <entry>|</entry>
 316         <entry>&layout; <emphasis role="bold">\frac</emphasis> &layout;</entry>
 317         <entry>Fraction</entry>
 318        </row>
 319        <row>
 320         <entry></entry>
 321         <entry>|</entry>
 322         <entry><emphasis role="bold">\infrule</emphasis> &layout; &layout; &layout;</entry>
 323         <entry>Inference rule (premises, conclusion, rule name)</entry>
 324        </row>
 325        <row>
 326         <entry></entry>
 327         <entry>|</entry>
 328         <entry><emphasis role="bold">\sqrt</emphasis> &layout;</entry>
 329         <entry>Square root</entry>
 330        </row>
 331        <row>
 332         <entry></entry>
 333         <entry>|</entry>
 334         <entry><emphasis role="bold">\root</emphasis> &layout; <emphasis role="bold">\of</emphasis> &layout;</entry>
 335         <entry>Generalized root</entry>
 336        </row>
 337        <row>
 338         <entry></entry>
 339         <entry>|</entry>
 340         <entry><emphasis role="bold">hbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
 341         <entry>Horizontal box</entry>
 342        </row>
 343        <row>
 344         <entry></entry>
 345         <entry>|</entry>
 346         <entry><emphasis role="bold">vbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
 347         <entry>Vertical box</entry>
 348        </row>
 349        <row>
 350         <entry></entry>
 351         <entry>|</entry>
 352         <entry><emphasis role="bold">hvbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
 353         <entry>Horizontal and vertical box</entry>
 354        </row>
 355        <row>
 356         <entry></entry>
 357         <entry>|</entry>
 358         <entry><emphasis role="bold">hovbox</emphasis> <emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
 359         <entry>Horizontal or vertical box</entry>
 360        </row>
 361        <row>
 362         <entry></entry>
 363         <entry>|</entry>
 364         <entry><emphasis role="bold">break</emphasis></entry>
 365         <entry>Breakable space</entry>
 366        </row>
 367        <row>
 368         <entry></entry>
 369         <entry>|</entry>
 370         <entry><emphasis role="bold">(</emphasis> &layout; [&layout;]… <emphasis role="bold">)</emphasis></entry>
 371         <entry>Group</entry>
 372        </row>
 373        <row>
 374         <entry></entry>
 375         <entry>|</entry>
 376         <entry>&id;</entry>
 377         <entry>Placeholder for a term with no explicit precedence</entry>
 378        </row>
 379        <row>
 380         <entry></entry>
 381         <entry>|</entry>
 382         <entry><emphasis role="bold">term</emphasis> &nat; &id;</entry>
 383         <entry>Placeholder for a term with explicit expected precedence</entry>
 384        </row>
 385        <row>
 386         <entry></entry>
 387         <entry>|</entry>
 388         <entry><emphasis role="bold">number</emphasis> &id;</entry>
 389         <entry>Placeholder for a natural number</entry>
 390        </row>
 391        <row>
 392         <entry></entry>
 393         <entry>|</entry>
 394         <entry><emphasis role="bold">ident</emphasis> &id;</entry>
 395         <entry>Placeholder for an identifier</entry>
 396        </row>
 397        <row>
 398         <entry></entry>
 399         <entry>|</entry>
 400         <entry>&literal;</entry>
 401         <entry>Literal</entry>
 402        </row>
 403        <row>
 404         <entry></entry>
 405         <entry>|</entry>
 406         <entry><emphasis role="bold">opt</emphasis> &layout;</entry>
 407         <entry>Optional layout (it can be omitted for parsing)</entry>
 408        </row>
 409        <row>
 410         <entry></entry>
 411         <entry>|</entry>
 412         <entry><emphasis role="bold">list0</emphasis> &layout;
 413                [<emphasis role="bold">sep</emphasis> &literal;]</entry>
 414         <entry>List of layouts separated by <command>sep</command> (default:
 415                any blank)</entry>
 416        </row>
 417
 418        <row>
 419         <entry></entry>
 420         <entry>|</entry>
 421         <entry><emphasis role="bold">list1</emphasis> &layout;
 422                [<emphasis role="bold">sep</emphasis> &literal;]</entry>
 423         <entry>Non empty list of layouts separated by <command>sep</command>
 424                (default: any blank)</entry>
 425        </row>
 426
 427        <row>
 428         <entry></entry>
 429         <entry>|</entry>
 430         <entry><emphasis role="bold">mstyle</emphasis> &id; value (&layout;)
 431         </entry>
 432         <entry>Style attributes like color #ff0000</entry>
 433        </row>
 434
 435        <row>
 436         <entry></entry>
 437         <entry>|</entry>
 438         <entry><emphasis role="bold">mpadded</emphasis> &id; value (&layout;)
 439         </entry>
 440         <entry>padding attributes like width -150%</entry>
 441        </row>
 442
 443        <row>
 444         <entry></entry>
 445         <entry>|</entry>
 446         <entry><emphasis role="bold">maction</emphasis> (&layout;)
 447                 [ (&layout;) … ]
 448         </entry>
 449         <entry>Alternative notations (output only)</entry>
 450        </row>
 451
 452
 453       </tbody>
 454       </tgroup>
 455     </table>
 456
 457     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 458       <title>literal</title>
 459       <tgroup cols="4">
 460       <tbody>
 461        <row>
 462         <entry id="grammar.literal">&literal;</entry>
 463         <entry>::=</entry>
 464         <entry>&symbol;</entry>
 465         <entry>Unicode symbol</entry>
 466        </row>
 467        <row>
 468         <entry></entry>
 469         <entry>|</entry>
 470         <entry>&nat;</entry>
 471         <entry>Natural number (a constant)</entry>
 472        </row>
 473        <row>
 474         <entry></entry>
 475         <entry>|</entry>
 476         <entry><emphasis role="bold">&apos;</emphasis>&id;<emphasis role="bold">&apos;</emphasis></entry>
 477         <entry>New keyword for the lexer</entry>
 478        </row>
 479       </tbody>
 480       </tgroup>
 481     </table>
 482
 483         </listitem>
 484       </varlistentry>
 485     </variablelist>
 486   </para>
 487  </sect1>
 488  <sect1>
 489    <title>interpretation</title>
 490    <titleabbrev>interpretation</titleabbrev>
 491    <para><userinput>interpretation &quot;description&quot; 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
 492          rhs</userinput></para>
 493    <para id="interpretation">
 494     <variablelist>
 495       <varlistentry role="tactic.synopsis">
 496         <term>Synopsis:</term>
 497         <listitem>
 498           <para><emphasis role="bold">interpretation</emphasis>
 499            &qstring; &csymbol; [&interpretation_argument;]…
 500            <emphasis role="bold">=</emphasis>
 501            &interpretation_rhs;
 502           </para>
 503         </listitem>
 504       </varlistentry>
 505       <varlistentry>
 506        <term>Action:</term>
 507        <listitem>
 508          <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>
 509           (the simultaneous substitution in <command>rhs</command> of the
 510           interpretation <command>{…}</command> of every content-level
 511           actual argument <command>t<subscript>i</subscript></command> for its
 512           corresponding formal parameter
 513           <command>p<subscript>i</subscript></command>). The
 514           <command>description</command> must be a textual description of the
 515           meaning associated to <command>'symbol</command> by this
 516           interpretation, and is used by the user interface of Matita to
 517           provide feedback on the interpretation of ambiguous terms.
 518          </para>
 519        </listitem>
 520       </varlistentry>
 521       <varlistentry>
 522         <term>Interpretation arguments:</term>
 523         <listitem>
 524
 525     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 526       <title>interpretation_argument</title>
 527       <tgroup cols="4">
 528       <tbody>
 529        <row>
 530         <entry id="grammar.interpretation_argument">&interpretation_argument;</entry>
 531         <entry>::=</entry>
 532         <entry>[<emphasis role="bold">η</emphasis><emphasis role="bold">.</emphasis>]… &id;</entry>
 533         <entry>A formal parameter. If the name of the formal parameter is
 534          prefixed by n symbols &quot;η&quot;, then the mapping performs
 535          (multiple) η-expansions to grant that the semantic actual
 536          parameter begins with at least n λ-abstractions.</entry>
 537        </row>
 538       </tbody>
 539       </tgroup>
 540      </table>
 541     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 542       <title>interpretation_rhs</title>
 543       <tgroup cols="4">
 544       <tbody>
 545        <row>
 546         <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
 547         <entry>::=</entry>
 548         <entry>&uri;</entry>
 549         <entry>A constant, specified by its URI</entry>
 550        </row>
 551        <row>
 552         <entry></entry>
 553         <entry>|</entry>
 554         <entry>&id;</entry>
 555         <entry>A constant, specified by its name, or a bound variable. If
 556                the constant name is ambiguous, the one corresponding to the
 557                last implicitly or explicitly specified alias is used.</entry>
 558        </row>
 559        <row>
 560         <entry></entry>
 561         <entry>|</entry>
 562         <entry><emphasis role="bold">?</emphasis></entry>
 563         <entry>An implicit parameter</entry>
 564        </row>
 565        <row>
 566         <entry></entry>
 567         <entry>|</entry>
 568         <entry><emphasis role="bold">(</emphasis>
 569                &interpretation_rhs;
 570                [&interpretation_rhs;]…
 571                <emphasis role="bold">)</emphasis></entry>
 572         <entry>An application</entry>
 573        </row>
 574       </tbody>
 575       </tgroup>
 576      </table>
 577
 578         </listitem>
 579       </varlistentry>
 580     </variablelist>
 581    </para>
 582  </sect1>
 583 </chapter>