SPEC ::= BASIC-SPEC
| translation SPEC RENAMING
| reduction SPEC RESTRICTION
| union SPEC+
| extension SPEC+
| free-spec SPEC
| local-spec SPEC SPEC
| closed-spec SPEC
| spec-inst SPEC-NAME FIT-ARG*
RENAMING ::= renaming SYMB-MAP-ITEMS+
RESTRICTION ::= hide SYMB-ITEMS+
| reveal SYMB-MAP-ITEMS+
SPEC-DEFN ::= spec-defn SPEC-NAME GENERICITY SPEC
GENERICITY ::= genericity PARAMS IMPORTS
PARAMS ::= params SPEC*
IMPORTS ::= imports SPEC*
FIT-ARG ::= fit-spec SPEC SYMB-MAP-ITEMS*
| fit-view VIEW-NAME FIT-ARG*
VIEW-DEFN ::= view-defn VIEW-NAME GENERICITY VIEW-TYPE
SYMB-MAP-ITEMS*
VIEW-TYPE ::= view-type SPEC SPEC
SYMB-ITEMS ::= symb-items SYMB-KIND SYMB+
SYMB-MAP-ITEMS ::= symb-map-items SYMB-KIND SYMB-OR-MAP+
SYMB-KIND ::= implicit | sorts | ops | preds
! SYMB ::= ID | qual-id ID TYPE
! TYPE ::= OP-TYPE | PRED-TYPE | SORT
SYMB-MAP ::= symb-map SYMB SYMB
SYMB-OR-MAP ::= SYMB | SYMB-MAP
SPEC-NAME ::= SIMPLE-ID
VIEW-NAME ::= SIMPLE-ID
TOKEN-ID ::= ... | COMP-TOKEN-ID
MIXFIX-ID ::= ... | COMP-MIXFIX-ID
COMP-TOKEN-ID ::= comp-token-id TOKEN ID+
COMP-MIXFIX-ID ::= comp-mixfix-id TOKEN-PLACES ID+
