Open ComFreek opened 4 years ago
Thanks for this write-up. I updated the documentation slightly to account for it. For now I have marked flexary notations as experimental.
Still need to document the L, %L, and V, %i, %n cases.
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.)
NotationComponents.scala
.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 positionsAssociativity 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.Associativity with to-be-escaped-delimiters:
integerMod: nat -> nat -> nat # 1 %D% 2
for%
to be left-associative and for10 % 3
to parse correctly.integerMod: nat -> nat -> nat # 1 %R% 2
for%
to be right-associative and for10 % 3
to parse correctly.Flexary notations: these make a constant receive flexary many arguments.
my_union # 1UNION…
allows writinga UNION b UNION c
that is parsed asOMA(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 between1
,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…
, wheren
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 write12 / 4
and MMT tries to infer the implicit argument (a proof that4 != 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)" asOMA(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 termOMA(?LFApply, List(f, x))
, whereLFApply
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
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