SPEC ::= BASIC-SPEC | TRANSLATION | REDUCTION
| UNION | EXTENSION | FREE-SPEC | LOCAL-SPEC
| CLOSED-SPEC | SPEC-INST
TRANSLATION ::= translation SPEC RENAMING
RENAMING ::= renaming SYMB-MAP-ITEMS+
REDUCTION ::= reduction SPEC RESTRICTION
RESTRICTION ::= HIDE | REVEAL
HIDE ::= hide SYMB-ITEMS+
REVEAL ::= reveal SYMB-MAP-ITEMS+
UNION ::= union SPEC+
EXTENSION ::= extension SPEC+
FREE-SPEC ::= free-spec SPEC
LOCAL-SPEC ::= local-spec SPEC SPEC
CLOSED-SPEC ::= closed-spec SPEC
SPEC-DEFN ::= spec-defn SPEC-NAME GENERICITY SPEC
GENERICITY ::= genericity PARAMS IMPORTS
PARAMS ::= params SPEC*
IMPORTS ::= imports SPEC*
SPEC-INST ::= spec-inst SPEC-NAME FIT-ARG*
FIT-ARG ::= FIT-SPEC | FIT-VIEW
FIT-SPEC ::= fit-spec SPEC SYMB-MAP-ITEMS*
FIT-VIEW ::= 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
! QUAL-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+
