X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_usernotation.xml;h=efb9e564bb187d87d895b705cb3959496f4310ca;hb=cb424002ff13c0f0b52b54ab0477b133333878ae;hp=f4b3cc4112380d01948a31c6d24b110324ade597;hpb=275a432d33c455d75725d5991e82b62e7d01f68d;p=helm.git diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml index f4b3cc411..efb9e564b 100644 --- a/helm/software/matita/help/C/sec_usernotation.xml +++ b/helm/software/matita/help/C/sec_usernotation.xml @@ -2,12 +2,453 @@ Extending the syntax - Introduction: TODO + Introduction: &TODO; notation notation + notation usage "presentation" associativity with precedence p for content - notation: &TODO; + + + Synopsis: + + notation + [&usage;] "¬ation_lhs;" [&associativity;] with precedence &nat; + for + ¬ation_rhs; + + + + + Action: + + Declares a mapping between the presentation + AST presentation and the content AST + content. The declared presentation AST fragment + presentation is at precedence level + p. The precedence level is used to determine where + parentheses must be inserted. In particular, the content AST fragment + content 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. + If presentation describes a binary + infix operator and if no precedence level is explicitly given for the + operator arguments, an associativity declaration + can be given to automatically choose the right level for the operands. + Otherwise, no associativity can be given. + If direction is + omitted, the mapping is bi-directional and is used both during + parsing and pretty-printing of terms. If direction + is >, the mapping is used only during parsing; + if it is <, 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. + + + + Notation arguments: + + + + usage + + + + &usage; + ::= + < + Only for pretty-printing + + + + | + > + Only for parsing + + + +
+ + + associativity + + + + &associativity; + ::= + left associative + Left associative + + + + | + right associative + Right associative + + + + | + non associative + Non associative (default) + + + +
+ + + notation_rhs + + + + ¬ation_rhs; + ::= + &unparsed_ast; + &TODO; + + + + | + &unparsed_meta; + &TODO; + + + +
+ + + unparsed_ast + + + + &unparsed_ast; + ::= + @{&enriched_term;} + A content level AST (a term which is parsed, but not disambiguated). + + + + | + @&id; + @id is just an abbreviation for @{id} + + + + | + @&csymbol; + @'symbol is just an abbreviation for @{'symbol} + + + +
+ + + enriched_term + + + + &enriched_term; + ::= + 〈〈A term that may contain occurrences of &unparsed_meta;, even as variable names in binders, and occurrences of &csymbol;〉〉 + &TODO; + + + +
+ + + unparsed_meta + + + + &unparsed_meta; + ::= + ${&level2_meta;} + &TODO; + + + + | + $&id; + $id is just an abbreviation for ${id} + + + + | + $_ + $_ is just an abbreviation for ${_} + + + +
+ + + level2_meta + + + + &level2_meta; + ::= + &unparsed_ast; + &TODO; + + + + | + term &nat; &id; + &TODO; + + + + | + number &id; + &TODO; + + + + | + ident &id; + &TODO; + + + + | + fresh &id; + &TODO; + + + + | + anonymous + &TODO; + + + + | + &id; + &TODO; + + + + | + fold [left|right] &level2_meta; rec &id; &level2_meta; + &TODO; + + + + | + default &level2_meta; &level2_meta; + &TODO; + + + + | + if &level2_meta; then &level2_meta; else &level2_meta; + &TODO; + + + + | + fail + &TODO; + + + +
+ + + notation_lhs + + + + ¬ation_lhs; + ::= + &layout; [&layout;]… + + + +
+ + + layout + + + + &layout; + ::= + &layout; \sub &layout; + Subscript + + + + | + &layout; \sup &layout; + Superscript + + + + | + &layout; \below &layout; + + + + + | + &layout; \above &layout; + + + + + | + &layout; \over &layout; + + + + + | + &layout; \atop &layout; + + + + + | + \frac &layout; &layout; + Fraction + + + + | + \sqrt &layout; + Square root + + + + | + \root &layout; \of &layout; + Generalized root + + + + | + hbox ( &layout; [&layout;]… ) + Horizontal box + + + + | + vbox ( &layout; [&layout;]… ) + Vertical box + + + + | + hvbox ( &layout; [&layout;]… ) + Horizontal and vertical box + + + + | + hovbox ( &layout; [&layout;]… ) + Horizontal or vertical box + + + + | + break + Breakable space + + + + | + ( &layout; [&layout;]… ) + Group + + + + | + &id; + Placeholder for a term with no explicit precedence + + + + | + term &nat; &id; + Placeholder for a term with explicit expected precedence + + + + | + number &id; + Placeholder for a natural number + + + + | + ident &id; + Placeholder for an identifier + + + + | + &literal; + Literal + + + + | + opt &layout; + Optional layout (it can be omitted for parsing) + + + + | + list0 &layout; + [sep &literal;] + List of layouts separated by sep (default: + any blank) + + + + | + list1 &layout; + [sep &literal;] + Non empty list of layouts separated by sep + (default: any blank) + + + +
+ + + literal + + + + &literal; + ::= + &symbol; + Unicode symbol + + + + | + &nat; + Natural number (a constant) + + + + | + '&id;' + New keyword for the lexer + + + +
+ + + + @@ -22,7 +463,7 @@ interpretation &qstring; &csymbol; [&interpretation_argument;]… - = + = &interpretation_rhs;