X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_usernotation.xml;h=66952a8145e1bc0fb6d28ba11d4c8dc78c9267b1;hb=2d2add82882aa070af5d942ebf5b7fa43359e1fd;hp=92698f824e31b155c8e0d6644d6ac21c4ad311b8;hpb=c52baa34c7363fa58f81aea95bb0d72e10afdaf1;p=helm.git
diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index 92698f824..66952a814 100644
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -2,6 +2,554 @@
Extending the syntax
- &TODO;
-
+ Introduction: &TODO;
+
+ notation
+ notation
+ notation usage "presentation" associativity with precedence p for content
+
+
+
+ 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;
+
+
+
+
+ |
+ &layout; \frac &layout;
+ Fraction
+
+
+
+ |
+ \infrule &layout; &layout; &layout;
+ Inference rule (premises, conclusion, rule name)
+
+
+
+ |
+ \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
+
+
+
+
+
+
+
+
+
+
+
+ interpretation
+ interpretation
+ interpretation "description" 'symbol p1 ⦠pn =
+ rhs
+
+
+
+ Synopsis:
+
+ interpretation
+ &qstring; &csymbol; [&interpretation_argument;]â¦
+ =
+ &interpretation_rhs;
+
+
+
+
+ Action:
+
+ It declares a bi-directional mapping {â¦} between the content-level AST 'symbol t1 ⦠tn and the semantic term rhs[{t1}/p1;â¦;{tn}/pn]
+ (the simultaneous substitution in rhs of the
+ interpretation {â¦} of every content-level
+ actual argument ti for its
+ corresponding formal parameter
+ pi). The
+ description must be a textual description of the
+ meaning associated to 'symbol by this
+ interpretation, and is used by the user interface of Matita to
+ provide feedback on the interpretation of ambiguous terms.
+
+
+
+
+ Interpretation arguments:
+
+
+
+ interpretation_argument
+
+
+
+ &interpretation_argument;
+ ::=
+ [η.]⦠&id;
+ A formal parameter. If the name of the formal parameter is
+ prefixed by n symbols "η", then the mapping performs
+ (multiple) η-expansions to grant that the semantic actual
+ parameter begins with at least n λ-abstractions.
+
+
+
+
+
+ interpretation_rhs
+
+
+
+ &interpretation_rhs;
+ ::=
+ &uri;
+ A constant, specified by its URI
+
+
+
+ |
+ &id;
+ A constant, specified by its name, or a bound variable. If
+ the constant name is ambiguous, the one corresponding to the
+ last implicitly or explicitly specified alias is used.
+
+
+
+ |
+ _
+ An implicit parameter
+
+
+
+ |
+ (
+ &interpretation_rhs;
+ [&interpretation_rhs;]â¦
+ )
+ An application
+
+
+
+
+
+
+
+
+
+
+