]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/help/C/sec_usernotation.xml
definition of equivalence for local environments,
[helm.git] / 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>