Chapter 5. Extending the syntax

Table of Contents

Introduction: TODO


notation usage "presentation" associativity with precedence p for content


notation [usage] "notation_lhs" [associativity] with precedence nat for notation_rhs


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:

Table 5.1. usage

usage::=<Only for pretty-printing
 |>Only for parsing

Table 5.2. associativity

associativity::=left associativeLeft associative
 |right associativeRight associative
 |non associativeNon associative (default)

Table 5.3. notation_rhs

Table 5.4. 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}

Table 5.5. enriched_term

enriched_term::=〈〈A term that may contain occurrences of unparsed_meta, even as variable names in binders, and occurrences of csymbol〉〉TODO

Table 5.6. unparsed_meta

 |$id$id is just an abbreviation for ${id}
 |$_$_ is just an abbreviation for ${_}

Table 5.7. level2_meta

 |term nat idTODO
 |number idTODO
 |ident idTODO
 |fresh idTODO
 |fold [left|right] level2_meta rec id level2_metaTODO
 |default level2_meta level2_metaTODO
 |if level2_meta then level2_meta else level2_metaTODO

Table 5.8. notation_lhs

Table 5.9. layout

layout::=layout \sub layoutSubscript
 |layout \sup layoutSuperscript
 |layout \below layout 
 |layout \above layout 
 |layout \over layout 
 |layout \atop layout 
 |layout \frac layoutFraction
 |\infrule layout layout layoutInference rule (premises, conclusion, rule name)
 |\sqrt layoutSquare root
 |\root layout \of layoutGeneralized 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
 |breakBreakable space
 |( layout [layout]… )Group
 |idPlaceholder for a term with no explicit precedence
 |term nat idPlaceholder for a term with explicit expected precedence
 |number idPlaceholder for a natural number
 |ident idPlaceholder for an identifier
 |opt layoutOptional 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)
 |mstyle id value (layout) Style attributes like color #ff0000
 |mpadded id value (layout) padding attributes like width -150%
 |maction (layout) [ (layout) … ] Alternative notations (output only)

Table 5.10. literal

literal::=symbolUnicode symbol
 |natNatural number (a constant)
 |'id'New keyword for the lexer