Symbolic notations

[Jazzpirate]

\symdecl[name=foo,type=tp]{bar} introduces a new symbol with name foo and macro \bar. If no name is given, the name is bar. The (optional) type is an arbitrary symbolic expression.

\notation... introduces a new notation for a symbol (more details below). \symdef[...]{bar}... combines \symdecl and \notation.

Notation schema

\notation[prec=p;p1x...xpn,args=args, vt=name]{foo}[n]{not}...

• n is the (optional) arity, subsumed by:
• args is a list of is,as and bs. If given, the length of * args* is the arity. If no args is given, the arity is n and all arguments are normal (i). If no n is given, then n=0.
  • i represents a normal argument
  • a represents an associative argument list
  • b represents a bound variable argument
• p is the operator precedence, the pi are the individual argument precedences. Default: pi=p, p=0, except if n=0, in which case p=\infprec (see bracketing below).
• foo is the name or macroname or URI of the symbol that gets the new notation.
• not is the actual notation, with the usual #i representing the ith argument.
• \notation takes an additional argument for each associative argument list, that provides a notation for the concatenation of two list elements (i.e. a binary macro).
• vt is one of (variant,lang,arity), name is a string identifying the notation variant. A notation for \foo with variant=bar is used via \foo[variant=bar] or \foo[bar]. Variants in the three dimensions (variant,lang,arity) can be composed (if a notation for the composition exist), e.g. \foo[bar,lang=de]. variant is generic, lang is used for language-specifc variants, arity is for variants of operators where commond "default" arguments are often suppressed -- e.g. least common multiple lcm(n,m) is called kleinstes gemeinsames Vielfaches in german, and correspondingly represented as kgV(n,m).

Question: how to handle binders and bounc variable arguments (separate issue: #8)

Example:

\notation{plus}[2]{#1 + #2}: \plus{a}{b} yields a+b

\notation[args=a]{plus}{#1}{#1 + #2}: \plus{a,b,c,d} yields a+b+c+d

\notation[args=ai]{sumlethan}{#1 < #2}{#1+#2}: \sumlethan{a,b,c}{A} yields a+b+c<A

Automatic bracketing

Automatic bracketing works by comparing a downwards precedence p_d with an upwards precedence p_u. The initial downward precedence is p_d:=-\infprec.
A semantic macro \foo{a1}...{an} sets the current downward precedence for each argument ai to its argument precedence p_d:=pi in the ith position. When expanding a semantic macro \bar, the operator precedence p of \bar is taken as upwards precedence p_u=p. Compare p_d and p_u. If p_u≤p_d, parentheses are wrapped around \bar, otherwise not.

Example:

\notation[prec=500]{plus}[2]{#1 + #2}
\notation[prec=600]{times}[2]{#1 * #2}
In both cases, argument precedences are operator precedences.

Consider \times{a}{\plus{b}{c}}. Then \times compares its precedence 600 with the (initial) downwards precedence -\infprec, where \infprec:=1000000. No parentheses are inserted. \times then sets the downwards precedence to 600 and expands its arguments.
\plus compares its precedende 500 with the downwards precedence 600 and inserts parentheses.
Result: a*(b+c)
Conversely: \plus{a}{\times{b,c}}. Here, \plus sets the downwards precedence to 500. \times compares its operator precedence 600 and does not insert parenthesis. Hence: a+b*c.

The default precedence \infprec for 0-ary semantic macros means no parentheses are ever automatically wrapped around constant symbols.

Question: do we need argument precedences in MMT?

Customization

The algorithm uses \notation@lparen and \notation@rparen as opening and closing brackets. By default, \notation@lparen:=( and \notation@rparen=). In displaymode, \left\notation@lparen and \right\notation@rparen are used.

\dobrackets{...} wraps brackets around its arguments and is used by the bracketing algorithm, hence allows for forcing brackets. \withbrackets{a}{b}{t} sets \notation@lparen:=a and \notation@rparen:=b in t <- allows customizing which brackets to use.

Question: Multiple notations in MMT, see #11

[Jazzpirate]

I'm becoming increasingly convinced that a symbol declaration should carry a fixed arity, rather than any notation having an arbitrary arity. Firstly, because otherwise things get awkward on the OMDoc/MMT-side, secondly, because otherwise #1 gets awkward.