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 ::= word-symbol | non-word-symbol word-symbol ::= word-start-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-symbol ::= 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 ::= word-symbol |
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 ::= word-symbol 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 type-name-map-item ::= [ type ] name +-> name op-name-map-item ::= [ op ] annotable-name +-> annotable-name annotable-name ::= name [ : type-descriptor ] |
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 | definition definition ::= type-definition | op-definition | claim-definition equals ::= is | = |
Import-declarations.
import-declaration ::= import spec-term |
Type-declarations.
Type-definitions.
type-definition ::= type type-name [ formal-type-parameters ] equals type-descriptor |
Op-declarations.
op-declaration ::= op op-name [ fixity ] : type-scheme fixity ::= associativity priority associativity ::= infixl | infixr priority ::= nat-literal type-scheme ::= [ type-variable-binder ] type-descriptor type-variable-binder ::= `[ local-type-variable-list `] |
Op-definitions.
Claim-definitions.
claim-definition ::= claim-kind claim-name is claim 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-descriptor 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 | annotated-expression | tight-expression tight-expression ::= application | restrict-expression | closed-expression closed-expression ::= op-name | local-variable | literal | field-selection | tuple-display | record-display | sequential-expression | list-display | 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.
Annotated-expressions.
annotated-expression ::= tight-expression : type-descriptor |
Applications.
Restrict-expressions.
restrict-expression ::= restrict closed-expression closed-expression |
Literals.
literal ::= boolean-literal | nat-literal | char-literal | string-literal |
Boolean-literals.
boolean-literal ::= true | false |
Nat-literals.
nat-literal ::= decimal-digit { decimal-digit }* |
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 hexadecimal-digit ::= decimal-digit | a | b | c | d | e | f | A | B | C | D | E | F |
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 }* ] |
Structors.
structor ::= projector | relaxator | quotienter | chooser | embedder | embedding-test |
projector ::= project field-selector |
relaxator ::= relax closed-expression |
quotienter ::= quotient closed-expression |
chooser ::= choose closed-expression |
embedder ::= [ embed ] constructor |
embedding-test ::= embed? constructor |
Patterns.