Appendix A. Metaslang Grammar

The grammar description formalism.

wiffle ::= waffle [ waffle-tail ] | piffle { + piffle }*

piffle ::= 1 | M { piffle }*

Models.

spec ::= spec-form op ::= op-name

Symbols and Names.

symbol ::= name | literal | special-symbol 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-definition ::= unit-identifier = unit-term unit-term ::= spec-term | morphism-term | diagram-term | target-code-term | proof-term specware-file-contents ::= unit-term | infile-unit-definition { infile-unit-definition }* infile-unit-definition ::= fragment-identifier = unit-term

Unit Identifiers.

unit-identifier ::= swpath-based-path | relative-path swpath-based-path ::= / relative-path relative-path ::= { path-element / }* path-element [ # path-element ] 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 qualifiable-name ::= unqualified-name | qualified-name unqualified-name ::= name qualified-name ::= qualifier . name

Translations.

spec-translation ::= translate spec-term by name-map name-map ::= { [ name-map-item { , name-map-item }* ] } name-map-item ::= sort-name-map-item | op-name-map-item sort-name-map-item ::= [ sort ] qualifiable-name +-> qualifiable-name op-name-map-item ::= [ op ] annotable-qualifiable-name +-> annotable-qualifiable-name annotable-qualifiable-name ::= qualifiable-name [ : sort ]

Substitutions.

spec-substitution ::= spec-term [ morphism-term ]

Diagram Colimits.

diagram-colimit ::= colimit diagram-term

Obligators.

obligator ::= obligations unit-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 ::= name +-> spec-term diagram-edge ::= name : name -> name +-> morphism-term

Generate Terms.

target-code-term ::= generate target-language-name spec-term [ in string-literal ] target-language-name ::= 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 | sort-declaration | op-declaration | definition definition ::= sort-definition | op-definition | claim-definition equals ::= is | =

Import-declarations.

import-declaration ::= import spec-term

Sort-declarations.

sort-declaration ::= sort sort-name [ formal-sort-parameters ] formal-sort-parameters ::= local-sort-variable | ( local-sort-variable-list ) local-sort-variable ::= name local-sort-variable-list ::= local-sort-variable { , local-sort-variable }*

Sort-definitions.

sort-definition ::= sort sort-name [ formal-sort-parameters ] equals sort

Op-declarations.

op-declaration ::= op op-name [ fixity ] : sort-scheme fixity ::= associativity priority associativity ::= infixl | infixr priority ::= nat-literal sort-scheme ::= [ sort-variable-binder ] sort sort-variable-binder ::= fa ( local-sort-variable-list )

Op-definitions.

op-definition ::= def [ sort-variable-binder ] formal-expression [ : sort ] equals expression formal-expression ::= op-name | formal-application formal-application ::= formal-application-head formal-parameter formal-application-head ::= op-name | formal-application formal-parameter ::= closed-pattern

Claim-definitions.

claim-definition ::= claim-kind claim-name equals claim claim-kind ::= axiom | theorem | conjecture claim-name ::= name claim ::= [ sort-quantification ] expression sort-quantification ::= sort sort-variable-binder

Sorts.

sort ::= sort-sum | sort-arrow | slack-sort slack-sort ::= sort-product | tight-sort tight-sort ::= sort-instantiation | closed-sort closed-sort ::= sort-name | local-sort-variable | sort-record | sort-restriction | sort-comprehension | sort-quotient | ( sort )

Sort-sums.

sort-sum ::= sort-summand { sort-summand }* sort-summand ::= | constructor [ slack-sort ] constructor ::= name

Sort-arrows.

sort-arrow ::= arrow-source -> sort arrow-source ::= sort-sum | slack-sort

Sort-products.

sort-product ::= tight-sort * tight-sort { * tight-sort }*

Sort-instantiations.

sort-instantiation ::= sort-name actual-sort-parameters actual-sort-parameters ::= closed-sort | ( proper-sort-list ) proper-sort-list ::= sort , sort { , sort }*

Sort-names.

sort-name ::= qualifiable-name

Sort-records.

sort-record ::= { [ field-sorter-list ] } | ( ) field-sorter-list ::= field-sorter { , field-sorter }* field-sorter ::= field-name : sort field-name ::= name

Sort-restrictions.

sort-restriction ::= ( slack-sort | expression )

Sort-comprehensions.

sort-comprehension ::= { annotated-pattern | expression }

Sort-quotients.

sort-quotient ::= closed-sort / closed-expression

Expressions.

expression ::= lambda-form | case-expression | let-expression | if-expression | quantification | tight-expression tight-expression ::= application | annotated-expression | closed-expression closed-expression ::= op-name | local-variable | literal | field-selection | tuple-display | record-display | sequential-expression | list-display | structor | ( expression )

Lambda-forms.

lambda-form ::= fn match

Case-expressions.

case-expression ::= case expression of match

Let-expressions.

let-expression ::= let let-bindings in expression let-bindings ::= recless-let-binding | rec-let-binding-sequence recless-let-binding ::= pattern equals expression rec-let-binding-sequence ::= rec-let-binding { rec-let-binding }* rec-let-binding ::= def name formal-parameter-sequence [ : sort ] equals expression formal-parameter-sequence ::= formal-parameter { formal-parameter }*

If-expressions.

if-expression ::= if expression then expression else expression

Quantifications.

quantification ::= quantifier ( local-variable-list ) expression quantifier ::= fa | ex local-variable-list ::= annotable-variable { , annotable-variable }* annotable-variable ::= local-variable [ : sort ] local-variable ::= name

Applications.

application ::= prefix-application | infix-application prefix-application ::= application-head actual-parameter application-head ::= closed-expression | prefix-application actual-parameter ::= closed-expression infix-application ::= actual-parameter op-name actual-parameter

Annotated-expressions.

annotated-expression ::= tight-expression : sort

Op-names.

op-name ::= qualifiable-name

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.

sequential-expression ::= ( open-sequential-expression ) open-sequential-expression ::= void-expression ; sequential-tail void-expression ::= expression sequential-tail ::= expression | open-sequential-expression

List-displays.

list-display ::= [ list-display-body ] list-display-body ::= [ expression { , expression }* ]

Structors.

structor ::= projector | relaxator | restrictor | quotienter | chooser | embedder | embedding-test

projector ::= project field-selector

relaxator ::= relax closed-expression

restrictor ::= restrict closed-expression

quotienter ::= quotient closed-expression

chooser ::= choose closed-expression

embedder ::= [ embed ] constructor

embedding-test ::= embed? constructor

Matches.

match ::= [ | ] branch { | branch }* branch ::= pattern -> expression

Patterns.

pattern ::= annotated-pattern | tight-pattern tight-pattern ::= aliased-pattern | cons-pattern | embed-pattern | quotient-pattern | relax-pattern | closed-pattern closed-pattern ::= variable-pattern | wildcard-pattern | literal-pattern | list-pattern | tuple-pattern | record-pattern | ( pattern )

annotated-pattern ::= pattern : sort aliased-pattern ::= variable-pattern as tight-pattern cons-pattern ::= closed-pattern :: tight-pattern embed-pattern ::= constructor [ closed-pattern ] quotient-pattern ::= quotient closed-expression tight-pattern relax-pattern ::= relax closed-expression tight-pattern variable-pattern ::= local-variable wildcard-pattern ::= _ literal-pattern ::= literal list-pattern ::= [ list-pattern-body ] list-pattern-body ::= [ pattern { , pattern }* ] tuple-pattern ::= ( tuple-pattern-body ) tuple-pattern-body ::= [ pattern , pattern { , pattern }* ] record-pattern ::= { record-pattern-body } record-pattern-body ::= [ field-patterner { , field-patterner }* ] field-patterner ::= field-name [ equals pattern ]