2 <!-- ============ User Notation ====================== -->
3 <chapter id="sec_usernotation">
4 <title>Extending the syntax</title>
7 <title>notation</title>
8 <titleabbrev>notation</titleabbrev>
9 <para><userinput>notation usage "presentation" associativity with precedence p for content</userinput></para>
12 <varlistentry role="tactic.synopsis">
13 <term>Synopsis:</term>
15 <para><emphasis role="bold">notation</emphasis>
16 [&usage;] <emphasis role="bold">"</emphasis>¬ation_lhs;<emphasis role="bold">"</emphasis> [&associativity;] <emphasis role="bold">with</emphasis> <emphasis role="bold">precedence</emphasis> &nat;
17 <emphasis role="bold">for</emphasis>
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
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>></command>, the mapping is used only during parsing;
45 if it is <command><</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>
51 <term>Notation arguments:</term>
54 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
59 <entry id="grammar.usage">&usage;</entry>
61 <entry><emphasis role="bold"><</emphasis></entry>
62 <entry>Only for pretty-printing</entry>
67 <entry><emphasis role="bold">></emphasis></entry>
68 <entry>Only for parsing</entry>
74 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
75 <title>associativity</title>
79 <entry id="grammar.associativity">&associativity;</entry>
81 <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
82 <entry>Left associative</entry>
87 <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
88 <entry>Right associative</entry>
93 <entry><emphasis role="bold">non</emphasis> <emphasis role="bold">associative</emphasis></entry>
94 <entry>Non associative (default)</entry>
100 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
101 <title>notation_rhs</title>
105 <entry id="grammar.notation_rhs">¬ation_rhs;</entry>
107 <entry>&TODO;</entry>
108 <entry>&TODO;</entry>
114 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
115 <title>notation_lhs</title>
119 <entry id="grammar.notation_lhs">¬ation_lhs;</entry>
121 <entry>&TODO;</entry>
122 <entry>&TODO;</entry>
134 <title>interpretation</title>
135 <titleabbrev>interpretation</titleabbrev>
136 <para><userinput>interpretation "description" 'symbol p<subscript>1</subscript> … p<subscript>n</subscript> =
137 rhs</userinput></para>
138 <para id="interpretation">
140 <varlistentry role="tactic.synopsis">
141 <term>Synopsis:</term>
143 <para><emphasis role="bold">interpretation</emphasis>
144 &qstring; &csymbol; [&interpretation_argument;]…
145 <emphasis role="bold">=</emphasis>
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.
167 <term>Interpretation arguments:</term>
170 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
171 <title>interpretation_argument</title>
175 <entry id="grammar.interpretation_argument">&interpretation_argument;</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 "η", then the mapping performs
180 (multiple) η-expansions to grant that the semantic actual
181 parameter begins with at least n λ-abstractions.</entry>
186 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
187 <title>interpretation_rhs</title>
191 <entry id="grammar.interpretation_rhs">&interpretation_rhs;</entry>
194 <entry>A constant, specified by its URI</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>
207 <entry><emphasis role="bold">_</emphasis></entry>
208 <entry>An implicit parameter</entry>
213 <entry><emphasis role="bold">(</emphasis>
215 [&interpretation_rhs;]…
216 <emphasis role="bold">)</emphasis></entry>
217 <entry>An application</entry>