Document notations more thoroughly

[ComFreek]

• Compile a list of all possible notation formats. Here is a starter written up by me with help from @Jazzpirate and reverse engineering of MMT's NotationComponents.scala.
• Document when OMAs and ApplySpines get produced

Forms of Notations and How to Specify Notations

MMT distinguishes multiple forms of notations; every constant can have none, some, or all of them: parsing notation, presentation notation, (a third I forgot)

For a constant, a parsing notation is specified using a constant component # <notation syntax here> that starts with a hash symbol. A non-exhaustive list of syntax examples is:

• c # <notation syntax here> (untyped constant)
• c : <type here> ❘ # <notation syntax here> (typed constant)
• c : <type here> ❘ = <def here> ❘ # <notation syntax here>

For a constant, a presentation notation is specified using two hash symbols ## <presentation notation syntax here>. Unless otherwise noted, the presentation notation syntax follows the same syntax as normal notation syntax.

Syntax of Notations

Special characters within notation components: %, digits 0-9, V, … (these four categories as reverse-engineered from here), jOD, jDD, jMD. The first two can be escaped via %D and %R, see second bullet point below.

• Infix operators: plus # 1 + 2, where 1, 2 are the 1-based parameter positions

• Associativity of infix operators: by default every delimiters is left-associtiatve, so e.g. plus # 1 + 2 makes + left-associtative. You can override this with %R: plus # 1 %R+ 2 makes + right-associative.

  • Note that associativity is a property of delimiters. Is there an example of a notation with multiple delimiters and associativities?

  • Associativity with to-be-escaped-delimiters:

    • left associative: integerMod: nat -> nat -> nat # 1 %D% 2 for % to be left-associative and for 10 % 3 to parse correctly.
    • right-associative: integerMod: nat -> nat -> nat # 1 %R% 2 for % to be right-associative and for 10 % 3 to parse correctly.

• Flexary notations: these make a constant receive flexary many arguments.

  • my_union # 1UNION… allows writing a UNION b UNION c that is parsed as OMA(my_union, List(a, b, c))

    • There is no LFApply here since pure LF doesn't support flexary function types! Hence, for the parsed term to typecheck, my_union must be special-handled, see LFS, but "that is brittle" (according to @Jazzpirate)

    • Be sure to get the surface syntax right! Use a Unicode ellipsis …, do not insert any space between 1, UNION, and …!

    • Read as "First argument is a sequence separated by 'UNION'".

  • my_union # UNION 1 …

    • Read as "First comes 'UNION', then first argument is a sequence separated by the whitspace character (' ')". Possibly one needs to use '%s' instead of ' ' to mark an explicit whitespace. Pay attention with precedence since the LF apply also uses a whitespace.

  • General syntax: ns…, where n is the 1-based index of a parameter, s is a separator consisting of 1 to multiple characters, and … is the Unicode ellipsis.

    That says: "The n-th argument is to be parsed as a sequence separated by s"

• How do I define implicit parameters?

  • If you want the n-th parameter to be implicit, then write %In (e.g. %I1 for the first argument to be implicit).

  • If a non-implicit parameter comes after an implicit one, then you don't need to write implicitness of the implicit parameter in the notation.

    Example: list_append: {X: type} X -> List X -> List X # cons 2 3. Since we left off the first parameter, the first parameter is marked as implicit.

  • Usually, one needs to explicitly mark implicitness if the last parameter is implicit (i.e. the previous point doesn't apply.)

    Example: division: {y: R} R -> y -> (|- y != 0) -> R # 2 / 1 %I3. That allows us to write 12 / 4 and MMT tries to infer the implicit argument (a proof that 4 != 0) on its own.

    Somebody should look over the last example. Does that actually work that way?

OMA vs ApplySpine

MMT uses OMDoc as the grammar for terms, mostly. In OMDoc the OMA production serves to encode function applications. E.g. in pure OMDoc, you could encode "the function f applied to variable x (in scope)" as OMA(OMS(...path to f), OMV("x")) (if "x" is a variable in scope).

Within a theory which has (transitively) LF as a meta theory, almost all function applications such as f x get turned into the OMDoc term OMA(?LFApply, List(f, x)), where LFApply is an untyped constant written down in MMT/urtheories.

(beware: if LF is only "included", i.e. via regular inclue, notations aren't touched.)

theory T	theory S	definiens component of d
{c # not, x, y}	include ?T, d = not x y	OMA(?c, List(?x, ?y))
{c # not, x, y}	include ?T, include ?LF, d = not x y	OMA(?LFApply, List(?c, ?x, ?y))
{c # not 1 2, x, y}	include ?T, d = not x y	OMA(?c, List(?x, ?y))
{c # not 1, x, y}	include ?T, include ?LF, d = not x y	OMA(?LFApply, List(OMA(?c, ?x), ?y))
{c # not 1 2, x, y}	include ?T, include ?LF, d = not x y	OMA(?c, List(?x, ?y))

in non-LF contexts it doesn't make a difference whether argument marked had been provided or no

[rappatoni]

Thanks for this write-up. I updated the documentation slightly to account for it. For now I have marked flexary notations as experimental.

[rappatoni]

Still need to document the L, %L, and V, %i, %n cases.

[ComFreek]

I think an overview table with columns "modifier", "short desc." and "example" (e.g. with entry %R | right associativity | 1 %R=> 2) would be nice in the documentation.
Furthermore, we could maintain a longer prose text with more examples (as is the case now).

(Not saying you in particular should do this; just something next time someone picks up documentation.)