SPEC ::= BASIC-SPEC
| SPEC RENAMING
| SPEC RESTRICTION
| SPEC and SPEC and...and SPEC
| SPEC then SPEC then...then SPEC
| free GROUPED-SPEC
| local SPEC within SPEC
| closed GROUPED-SPEC
| GROUPED-SPEC
GROUPED-SPEC ::= { SPEC }
| SPEC-NAME
| SPEC-NAME [ FIT-ARG ]...[ FIT-ARG ]
RENAMING ::= with SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS
RESTRICTION ::= hide SYMB-ITEMS ,..., SYMB-ITEMS
| reveal SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS
SPEC-DEFN ::= spec SPEC-NAME = SPEC end/
| spec SPEC-NAME SOME-GENERICS = SPEC end/
SOME-GENERICS ::= SOME-PARAMS | SOME-PARAMS SOME-IMPORTS
SOME-PARAMS ::= [ SPEC ]...[ SPEC ]
SOME-IMPORTS ::= given SPEC-NAME ,..., SPEC-NAME
FIT-ARG ::= SPEC fit SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS
| SPEC
| view VIEW-NAME
| view VIEW-NAME [ FIT-ARG ]...[ FIT-ARG ]
VIEW-DEFN ::= view VIEW-NAME : VIEW-TYPE end/
| view VIEW-NAME : VIEW-TYPE =
SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS end/
| view VIEW-NAME SOME-GENERICS : VIEW-TYPE end/
| view VIEW-NAME SOME-GENERICS : VIEW-TYPE =
SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS end/
VIEW-TYPE ::= SPEC -> SPEC
SYMB-ITEMS ::= SYMB
| SOME-SYMB-KIND SYMB ,..., SYMB
SYMB-MAP-ITEMS ::= SYMB-OR-MAP
| SOME-SYMB-KIND SYMB-OR-MAP ,..., SYMB-OR-MAP
SOME-SYMB-KIND ::= sort/sorts | op/ops | pred/preds
SYMB ::= ID | QUAL-PRED-NAME | QUAL-OP-NAME
SYMB-MAP ::= SYMB "|->" SYMB
SYMB-OR-MAP ::= SYMB | SYMB-MAP
SPEC-NAME ::= SIMPLE-ID
VIEW-NAME ::= SIMPLE-ID
TOKEN-ID ::= ... | TOKEN [ ID ,..., ID ]
MIXFIX-ID ::= ... | TOKEN-PLACES [ ID ,..., ID ]
