BASIC-SPEC       ::= basic-spec BASIC-ITEMS*

BASIC-ITEMS      ::= CLASS-ITEMS | SIG-ITEMS 
                   | GENERATED-ITEMS | FREE-DATATYPES 
                   | GENERIC-VARS | LOCAL-VAR-AXIOMS | AXIOM-ITEMS
                   | INTERNAL-ITEMS | PROG-ITEMS

INTERNAL-ITEMS   ::= internal BASIC-ITEMS+
PROG-ITEMS       ::= prog-items PATTERN-EQ+

CLASS-ITEMS          ::= SIMPLE-CLASS-ITEMS | INSTANCE-CLASS-ITEMS
SIMPLE-CLASS-ITEMS   ::= class-items CLASS-ITEM+
INSTANCE-CLASS-ITEMS ::= instance-class-items CLASS-ITEM+

CLASS-ITEM       ::= class-item CLASS-DECL BASIC-ITEMS*

CLASS-DECL       ::= SIMPLE-CLASS-DECL | SUBCLASS-DECL
SIMPLE-CLASS-DECL::= class-decl CLASS-NAME+                      
SUBCLASS-DECL    ::= subclass-decl CLASS-NAME+ KIND

KIND             ::= TYPE-UNIVERSE | CLASS-KIND | INTERSECTION-KIND
                   | DOWNSET-KIND | FUN-KIND
TYPE-UNIVERSE    ::= type-universe
CLASS-KIND       ::= class-name CLASS-NAME
INTERSECTION-KIND::= intersection KIND+
DOWNSET-KIND     ::= downset TYPE
FUN-KIND         ::= fun-kind EXT-KIND KIND
EXT-KIND         ::= ext-kind KIND VARIANCE
VARIANCE         ::= covariant | contravariant | invariant

SIG-ITEMS        ::= TYPE-ITEMS | OP-ITEMS | FUN-ITEMS | PRED-ITEMS

TYPE-ITEMS          ::= SIMPLE-TYPE-ITEMS | INSTANCE-TYPE-ITEMS
SIMPLE-TYPE-ITEMS   ::= type-items TYPE-ITEM+
INSTANCE-TYPE-ITEMS ::= instance-type-items TYPE-ITEM+

TYPE-ITEM        ::= TYPE-DECL | SYNONYM-TYPE | DATATYPE-DECL
                   | SUBTYPE-DECL | ISO-DECL | SUBTYPE-DEFN
TYPE-DECL        ::= type-decl TYPE-NAME+ KIND
SYNONYM-TYPE     ::= synonym-type TYPE-NAME TYPE-ARG* TYPE
SUBTYPE-DECL     ::= subtype-decl TYPE-NAME+ TYPE
ISO-DECL         ::= iso-decl TYPENAME+
SUBTYPE-DEFN     ::= subtype-defn TYPE-NAME TYPE-ARG* VAR TYPE FORMULA

TYPE-ARG         ::= type-arg TYPEVAR EXT-KIND

OP-ITEMS         ::= op-items OP-ITEM+
FUN-ITEMS        ::= fun-items OP-ITEM+
OP-ITEM          ::= OP-DECL | OP-DEFN
OP-DECL          ::= op-decl OP-NAME+ TYPESCHEME OP-ATTR*

TYPESCHEME       ::= typescheme TYPE-ARG* TYPE

OP-ATTR          ::= BINARY-OP-ATTR | UNIT-OP-ATTR
BINARY-OP-ATTR   ::= assoc-op-attr | comm-op-attr | idem-op-attr
UNIT-OP-ATTR     ::= unit-op-attr TERM

OP-DEFN          ::= op-defn OP-NAME TYPE-ARG* OP-HEAD TERM
OP-HEAD          ::= TOTAL-OP-HEAD | PARTIAL-OP-HEAD
TOTAL-OP-HEAD    ::= total-op-head   TUPLE-ARG* TYPE
PARTIAL-OP-HEAD  ::= partial-op-head TUPLE-ARG* TYPE
TUPLE-ARG        ::= tuple-arg VAR-DECL*
VAR-DECL         ::= var-decl VAR TYPE

PRED-ITEMS       ::= pred-items PRED-ITEM+
PRED-ITEM        ::= PRED-DECL | PRED-DEFN
PRED-DECL        ::= pred-decl OP-NAME+ TYPESCHEME
PRED-DEFN        ::= pred-defn OP-NAME TYPE-ARG* TUPLE-ARG FORMULA

GENERATED-ITEMS  ::= generated SIG-ITEMS+
FREE-DATATYPE    ::= free-datatype DATATYPE-DECL+
GENERIC-VARS     ::= var-items GEN-VAR-DECL+
LOCAL-VAR-AXIOMS ::= local-var-axioms GEN-VAR-DECL+ FORMULA+
AXIOM-ITEMS      ::= axiom-items FORMULA+

GEN-VAR-DECL     ::= VAR-DECL | TYPE-ARG

DATATYPE-DECL    ::= datatype-decl TYPE-NAME TYPE-ARG* ALTERNATIVE+ 
                                                       CLASS-NAME*

ALTERNATIVE      ::= TOTAL-CONSTRUCT | PARTIAL-CONSTRUCT | SUBTYPES
TOTAL-CONSTRUCT  ::= total-construct   OP-NAME TUPLE-COMPONENT*
PARTIAL-CONSTRUCT::= partial-construct OP-NAME TUPLE-COMPONENT+
TUPLE-COMPONENT  ::= tuple-component COMPONENTS+
COMPONENTS       ::= TOTAL-SELECT | PARTIAL-SELECT | TYPE
TOTAL-SELECT     ::= total-select   OP-NAME+ TYPE
PARTIAL-SELECT   ::= partial-select OP-NAME+ TYPE
SUBTYPES         ::= subtypes TYPE+

TYPE             ::= TYPE-NAME | TYPE-APPL
                   | PRODUCT-TYPE | LAZY-TYPE | KINDED-TYPE | FUN-TYPE 
TYPE-APPL        ::= type-appl TYPE TYPE
PRODUCT-TYPE     ::= product-type TYPE+ 
LAZY-TYPE        ::= lazy-type TYPE
KINDED-TYPE      ::= kinded-type TYPE KIND
FUN-TYPE         ::= fun-type TYPE ARROW TYPE
ARROW            ::= partial-fun | total-fun 
                   | cont-partial-fun | cont-total-fun
 
FORMULA          ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION 
                   | IMPLICATION | EQUIVALENCE 
                   | NEGATION | ATOM
QUANTIFICATION   ::= quantification QUANTIFIER GEN-VAR-DECL+ FORMULA
QUANTIFIER       ::= universal | existential | unique-existential
CONJUNCTION      ::= conjunction FORMULA+
DISJUNCTION      ::= disjunction FORMULA+
IMPLICATION      ::= implication FORMULA FORMULA
EQUIVALENCE      ::= equivalence FORMULA FORMULA
NEGATION         ::= negation FORMULA

ATOM             ::= TRUTH | DEFINEDNESS 
                   | EXISTL-EQUATION | STRONG-EQUATION 
                   | MEMBERSHIP | PREDICATION
TRUTH            ::= true-atom | false-atom
DEFINEDNESS      ::= definedness TERM
EXISTL-EQUATION  ::= existl-equation TERM TERM
STRONG-EQUATION  ::= strong-equation TERM TERM
MEMBERSHIP       ::= membership TERM TYPE
PREDICATION      ::= predication TERM

TERM             ::= QUAL-VAR | INST-QUAL-NAME
                   | TERM-APPL | TUPLE-TERM
                   | TYPED-TERM 
                   | CONDITIONAL
                   | TOTAL-LAMBDA | PARTIAL-LAMBDA 
                   | LET-TERM | CASE-TERM 
                   | CAST
QUAL-VAR         ::= qual-var VAR TYPE 
INST-QUAL-NAME   ::= inst-qual-name OP-NAME TYPE* TYPESCHEME
TERM-APPL        ::= term-appl TERM TERM
TUPLE-TERM       ::= tuple-term TERM*
TYPED-TERM       ::= typed-term TERM TYPE
CONDITIONAL      ::= conditional TERM TERM TERM
PARTIAL-LAMBDA   ::= partial-lambda PATTERN* TERM
TOTAL-LAMBDA     ::= total-lambda   PATTERN* TERM
LET-TERM         ::= let-term PATTERN-EQ+ TERM
CASE-TERM        ::= case-term TERM CASE+
CAST             ::= cast TERM TYPE

PATTERN          ::= QUAL-VAR | INST-QUAL-NAME | PATTERN-APPL
                   | TUPLE-PATTERN | TYPED-PATTERN | AS-PATTERN
PATTERN-APPL     ::= pattern-appl PATTERN PATTERN
TUPLE-PATTERN    ::= tuple-pattern PATTERN*
TYPED-PATTERN    ::= typed-pattern PATTERN TYPE
AS-PATTERN       ::= as-pattern VAR PATTERN 

PATTERN-EQ       ::= pattern-eq PATTERN TERM
CASE             ::= case PATTERN TERM 

CLASS-NAME       ::= ID
TYPE-NAME        ::= ID
OP-NAME          ::= ID
VAR              ::= ID
TYPEVAR          ::= SIMPLE-ID