This appendix lists the grammar rules of the Metaslang specification language. These rules are identical to those of the Chapter on Metaslang. They are brought together here, without additional text, for easy reference.
The Grammar Description Formalism.
wiffle ::= waffle [ waffle-tail ] | piffle { + piffle }* |
piffle ::= 1 | M { piffle }* |
Symbols and Names.
symbol ::= simple-name | literal | special-symbol simple-name ::= first-syllable { _ next-syllable }* first-syllable ::= first-word-syllable | non-word-syllable next-syllable ::= next-word-syllable | non-word-syllable first-word-syllable ::= word-start-mark { word-continue-mark }* next-word-syllable ::= word-continue-mark { word-continue-mark }* word-start-mark ::= letter word-continue-mark ::= letter | decimal-digit | ' | ? letter ::= A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | a | b | c | d | e | f | g | h | i | j | k | l | m | n | o | p | q | r | s | t | u | v | w | x | y | z decimal-digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 non-word-syllable ::= non-word-mark { non-word-mark }* non-word-mark ::= ` | ~ | ! | @ | $ | ^ | & | * | - | = | + | \ | | | : | < | > | / | ' | ? special-symbol ::= _ | ( | ) | [ | ] | { | } | ; | , | . |
Comments.
comment ::= line-end-comment | block-comment line-end-comment ::= % line-end-comment-body line-end-comment-body ::= any-text-up-to-end-of-line block-comment ::= (* block-comment-body *) block-comment-body ::= any-text-including-newlines-and-nested-block-comments |
Units.
Unit Identifiers.
unit-identifier ::= swpath-based-path | relative-path swpath-based-path ::= / relative-path relative-path ::= { path-element / }* path-element [ # fragment-identifier ] path-element ::= path-mark { path-mark }* path-mark ::= letter | decimal-digit | ! | $ | & | ' | + | - | = | @ | ^ | ` | ~ | . |
Specs.
spec-term ::= unit-identifier | spec-form | spec-qualification | spec-translation | spec-substitution | diagram-colimit | obligator |
Spec Forms.
spec-form ::= spec { declaration }* endspec |
Qualifications.
spec-qualification ::= qualifier qualifying spec-term qualifier ::= simple-name name ::= simple-name | qualified-name qualified-name ::= qualifier . simple-name |
Translations.
spec-translation ::= translate spec-term by name-map name-map ::= { [ name-map-item { , name-map-item }* ] } name-map-item ::= type-name-map-item | op-name-map-item | wildcard-map-item type-name-map-item ::= [ type ] name +-> name op-name-map-item ::= [ op ] annotable-name +-> annotable-name annotable-name ::= name [ type-annotation ] type-annotation ::= : type-descriptor wildcard-map-item ::= wildcard +-> wildcard wildcard ::= simple-wildcard | qualified-wildcard simple-wildcard ::= _ qualified-wildcard ::= qualifier . simple-wildcard |
Substitutions.
spec-substitution ::= spec-term [ morphism-term ] |
Diagram Colimits.
diagram-colimit ::= colimit diagram-term |
Morphisms.
morphism-term ::= unit-identifier | spec-morphism spec-morphism ::= morphism spec-term -> spec-term name-map |
Diagrams.
diagram-term ::= unit-identifier | diagram-form diagram-form ::= diagram { diagram-element { , diagram-element }* } diagram-element ::= diagram-node | diagram-edge diagram-node ::= simple-name +-> spec-term diagram-edge ::= simple-name : simple-name -> simple-name +-> morphism-term |
Target Code Terms.
target-code-term ::= generate target-language-name spec-term [ generate-option ] generate-option ::= in string-literal | with unit-identifier target-language-name ::= c | java | lisp |
Proof Terms.
proof-term ::= prove claim-name in spec-term [ with prover-name ] [ using claim-list ] [ options prover-options ] prover-name ::= snark claim-list ::= claim-name { , claim-name }* prover-options ::= string-literal |
Declarations.
declaration ::= import-declaration | type-declaration | op-declaration | claim-declaration | definition definition ::= type-definition | op-definition equals ::= is | = |
Import-declarations.
import-declaration ::= import spec-term { , spec-term }* |
Type-declarations.
Type-definitions.
type-definition ::= type-abbreviation | new-type-definition type-abbreviation ::= def [ type ] type-name [ formal-type-parameters ] equals type-descriptor new-type-definition ::= def [ type ] type-name [ formal-type-parameters ] equals new-type-descriptor |
Op-declarations.
Op-definitions.
op-definition ::= def [ op ] [ type-variable-binder ] formal-expression [ type-annotation ] equals expression | def [ op ] formal-expression polytype-annotation equals expression |
Claim-declarations.
claim-declaration ::= claim-kind claim-name is claim [ proof-script ] claim-kind ::= axiom | theorem | conjecture claim-name ::= name claim ::= [ type-variable-binder ] expression |
Type-descriptors.
Type-sums.
type-sum ::= type-summand { type-summand }* type-summand ::= | constructor [ slack-type-descriptor ] constructor ::= simple-name |
Type-arrows.
type-arrow ::= arrow-source -> type-descriptor arrow-source ::= type-sum | slack-type-descriptor |
Type-products.
type-product ::= tight-type-descriptor * tight-type-descriptor { * tight-type-descriptor }* |
Type-instantiations.
Type-records.
type-record ::= { [ field-typer-list ] } | ( ) field-typer-list ::= field-typer { , field-typer }* field-typer ::= field-name type-annotation field-name ::= simple-name |
Type-restrictions.
type-restriction ::= ( slack-type-descriptor | expression ) |
Type-comprehensions.
type-comprehension ::= { annotated-pattern | expression } |
Type-quotients.
type-quotient ::= closed-type-descriptor / closed-expression |
Expressions.
expression ::= lambda-form | case-expression | let-expression | if-expression | quantification | unique-solution | annotated-expression | tight-expression tight-expression ::= application | closed-expression closed-expression ::= op-name | local-variable | literal | field-selection | tuple-display | record-display | sequential-expression | list-display | monadic-expression | structor | ( expression ) | ( inbuilt-op ) inbuilt-op ::= inbuilt-prefix-op | inbuilt-infix-op inbuilt-prefix-op ::= ~ inbuilt-infix-op ::= <=> | => | || | && | = | ~= | << |
Lambda-forms.
lambda-form ::= fn match |
Case-expressions.
case-expression ::= case expression of match |
Let-expressions.
If-expressions.
if-expression ::= if expression then expression else expression |
Quantifications.
Unique-solutions.
unique-solution ::= the ( local-variable-list ) expression |
Annotated-expressions.
annotated-expression ::= tight-expression type-annotation |
Applications.
Literals.
literal ::= boolean-literal | nat-literal | char-literal | string-literal |
Boolean-literals.
boolean-literal ::= true | false |
Nat-literals.
nat-literal ::= decimal-digit { decimal-digit }* | 0 X hexadecimal-digit { hexadecimal-digit }* | 0 x hexadecimal-digit { hexadecimal-digit }* | 0 O octal-digit { octal-digit }* | 0 o octal-digit { octal-digit }* | 0 B binary-digit { binary-digit }* | 0 b binary-digit { binary-digit }* hexadecimal-digit ::= decimal-digit | a | b | c | d | e | f | A | B | C | D | E | F octal-digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 binary-digit ::= 0 | 1 |
Char-literals.
char-literal ::= #char-literal-glyph char-literal-glyph ::= char-glyph | " char-glyph ::= letter | decimal-digit | other-char-glyph other-char-glyph ::= ! | : | @ | # | $ | % | ^ | & | * | ( | ) | _ | - | + | = | | | ~ | ` | . | , | < | > | ? | / | ; | ' | [ | ] | { | } | \\ | \" | \a | \b | \t | \n | \v | \f | \r | \s | \x hexadecimal-digit hexadecimal-digit |
String-literals.
string-literal ::= " string-body " string-body ::= { string-literal-glyph }* string-literal-glyph ::= char-glyph | significant-whitespace significant-whitespace ::= space | tab | newline |
Field-selections.
field-selection ::= closed-expression . field-selector field-selector ::= nat-literal | field-name |
Tuple-displays.
tuple-display ::= ( tuple-display-body ) tuple-display-body ::= [ expression , expression { , expression }* ] |
Record-displays.
record-display ::= { record-display-body } record-display-body ::= [ field-filler { , field-filler }* ] field-filler ::= field-name equals expression |
Sequential-expressions.
List-displays.
list-display ::= [ list-display-body ] list-display-body ::= [ expression { , expression }* ] |
Monadic-expressions.
Structors.
structor ::= projector | quotienter | chooser | embedder | embedding-test |
projector ::= project field-selector |
quotienter ::= quotient [ type-name ] |
chooser ::= choose [ type-name ] |
embedder ::= [ embed ] constructor |
embedding-test ::= embed? constructor |
Matches.
match ::= [ | ] branch { | branch }* branch ::= pattern [ guard ] -> expression guard ::= | expression |
Patterns.