BASIC-SPEC      ::= BASIC-ITEMS...BASIC-ITEMS | { }

BASIC-ITEMS     ::= class/classes CLASS-ITEM ;...; CLASS-ITEM ;/
                  | class instance/instances CLASS-ITEM ;...; CLASS-ITEM ;/
                  | SIG-ITEMS
                  | free type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
                  | generated type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
                  | generated { SIG-ITEMS...SIG-ITEMS } ;/
                  | internal { BASIC-ITEMS...BASIC-ITEMS } ;/
                  | var/vars GEN-VAR-DECL ;...; GEN-VAR-DECL ;/
                  | forall GEN-VAR-DECL ;...; GEN-VAR-DECL
                             "." FORMULA "."..."." FORMULA ;/ 
                  | "." FORMULA "."..."." FORMULA ;/ 
                  | program/programs PATTERN-EQ ;...; PATTERN-EQ ;/
                  | axiom/axioms FORMULA ;...; FORMULA ;/  

%% for backwards compatibility with CASL v1.0: axiom

CLASS-ITEM      ::= CLASS-DECL 
                  | CLASS-DECL { BASIC-ITEMS...BASIC-ITEMS }

CLASS-DECL      ::= CLASS-NAME ,..., CLASS-NAME
                  | CLASS-NAME ,..., CLASS-NAME : KIND
                  | CLASS-NAME ,..., CLASS-NAME < KIND

KIND            ::= Type
                  | CLASS-NAME
                  | ( KIND ,..., KIND ) 
                  | { VAR "." VAR < TYPE }
                  | EXT-KIND -> KIND 

EXT-KIND        ::= KIND | KIND + | KIND -

SIG-ITEMS       ::= sort/sorts SORT-ITEM ;...; SORT-ITEM
                  | type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
                  | type/types TYPE-ITEM ;...; TYPE-ITEM ;/
                  | type/types instance/instances TYPE-ITEM ;...; TYPE-ITEM ;/
                  | op/ops OP-ITEM ;...; OP-ITEM ;/
                  | fun/funs OP-ITEM ;...; OP-ITEM ;/ 
                  | pred/preds PRED-ITEM ;...; PRED-ITEM ;/ 

SORT-ITEM       ::= TYPE-PATTERN ,..., TYPE-PATTERN
                  | TYPE-PATTERN ,..., TYPE-PATTERN : KIND
                  | TYPE-PATTERN ,..., TYPE-PATTERN < TYPE 
                  | TYPE-PATTERN =...= TYPE-PATTERN
                  | TYPE-PATTERN = { VARS : TYPE "." FORMULA }

%% several vars to pattern match a tuple (different from summary)
VARS            ::= VAR 
                  | (VARS, ..., VARS)

TYPE-ITEM       ::= SORT-ITEM
                  | TYPE-PATTERN := SYNONYM-TYPE

SYNONYM-TYPE    ::= TYPE 
                  | \ TYPE-ARGS "." SYNONYM-TYPE

TYPE-PATTERN    ::= TYPE-NAME                   %% mixid with places
                  | TYPE-NAME TYPE-ARGS         %% simple prefix id
		  | TYPE-ARG TYPE-NAME TYPE-ARG %% simple sinfix symbol  
		  | [ TYPE-ARG ]                %% outfix typename [__]
		  | { TYPE-ARG }                %% outfix typename {__}

TYPE-ARGS       ::= TYPE-ARG...TYPE-ARG
TYPE-ARG        ::= EXT-TYPE-VAR
                  | EXT-TYPE-VAR : EXT-KIND
                  | EXT-TYPE-VAR < TYPE
                  | ( TYPE-ARG )    
EXT-TYPE-VAR    ::= TYPE-VAR | TYPE-VAR + | TYPE-VAR -

DATATYPE-DECL   ::= TYPE-PATTERN "::=" ALTERNATIVES
                  | TYPE-PATTERN "::=" ALTERNATIVES deriving CLASSES

CLASSES         ::= CLASS-NAME ,..., CLASS-NAME

ALTERNATIVES    ::= ALTERNATIVE "|"..."|" ALTERNATIVE

ALTERNATIVE     ::= OP-NAME TUPLE-COMPONENT...TUPLE-COMPONENT
                  | OP-NAME TUPLE-COMPONENT...TUPLE-COMPONENT ?
                  | OP-NAME
                  | sort/sorts TYPE-NAME ,..., TYPE-NAME
                  | type/types TYPE ,..., TYPE

TUPLE-COMPONENT ::= ( COMPONENT ;...; COMPONENT ) 
		  | SIMPLE-ID   %% for a simple curried type argument 

COMPONENT       ::= OP-NAME ,..., OP-NAME : TYPE
                  | OP-NAME ,..., OP-NAME :? TYPE
                  | TYPE

OP-ITEM         ::= OP-NAME ,..., OP-NAME : TYPESCHEME
                  | OP-NAME ,..., OP-NAME : TYPESCHEME, OP-ATTRS
                  | OP-NAME : TYPESCHEME = TERM
                  | OP-NAME [ TYPE-VAR-DECLS ] OP-HEAD = TERM
                  | OP-NAME OP-HEAD = TERM

OP-HEAD         ::= TUPLE-ARGS : TYPE
                  | TUPLE-ARGS :? TYPE 
                  | :? TYPE

TUPLE-ARGS      ::= TUPLE-ARG...TUPLE-ARG
TUPLE-ARG       ::= ( VAR-DECL ;...; VAR-DECL ) 
VAR_DECL        ::= VAR ,..., VAR : TYPE

OP-ATTRS        ::= OP-ATTR ,..., OP-ATTR
OP-ATTR         ::= BIN-ATTR | unit TERM
BIN-ATTR        ::= assoc | comm | idem 

PRED-ITEM       ::= OP-NAME, ..., OP-NAME: TYPESCHEME
                  | OP-NAME [ TYPE-VAR-DECLS ] TUPLE-ARG <=> FORMULA 
                  | OP-NAME TUPLE-ARG <=> FORMULA 
                  | OP-NAME <=> FORMULA 

TYPESCHEME      ::= TYPE 
                  | forall TYPE-VAR-DECLS . TYPESCHEME

TYPE-VAR-DECLS  ::= TYPE-VARS ;...; TYPE-VARS

TYPE-VARS       ::= EXT-TYPE-VAR ,...,  EXT-TYPE-VAR
                  | EXT-TYPE-VAR ,...,  EXT-TYPE-VAR : EXT-KIND
                  | EXT-TYPE-VAR ,...,  EXT-TYPE-VAR < TYPE

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

TYPE            ::= TYPE ARROW TYPE
                  | TYPE *...* TYPE
                  | ( TYPE )
                  | Pred TYPE           %% predefined Alias
                  | ? TYPE
                  | Unit                %% predefined (empty product)
                  | Logical             %% predefined Alias
                  | TYPE : KIND
                  | TYPE TYPE
ARROW           ::= ->? | -> | -->? | -->

FORMULA         ::= QUANTIFIER GEN-VAR-DECL ;...; GEN-VAR-DECL 
                               "." FORMULA
                  | FORMULA /\.../\ FORMULA
                  | FORMULA \/...\/ FORMULA
                  | FORMULA => FORMULA
                  | FORMULA if FORMULA
                  | FORMULA <=> FORMULA
                  | not FORMULA
                  | true | false
                  | def TERM 
                  | TERM in TYPE
                  | TERM = TERM
                  | TERM =e= TERM
                  | TERM

TERM            ::= QUAL-VAR
                  | INST-QUAL-NAME
                  | TERM TERM
                  | (TERM ,..., TERM) | ( )
                  | TERM : TYPE
                  | TERM when FORMULA else TERM
                  | \ LAMBDA-DOT TERM  
                  | \ PATTERN...PATTERN LAMBDA-DOT TERM
                  | let PATTERN-EQ ;...; PATTERN-EQ in TERM
                  | TERM where PATTERN-EQ ;...; PATTERN-EQ ;/
                  | case TERM of CASE "|"..."|" CASE
                  | if TERM then TERM else TERM
                  | TERM as TYPE
                  | LITERAL
                  | MIXFIX

LAMBDA-DOT      ::= "." | .!
QUANTIFIER      ::= forall | exists | exists!

PATTERN-EQ      ::= PATTERN = TERM
CASE            ::= PATTERN -> TERM 

PATTERN         ::= QUAL-VAR
                  | INST-QUAL-NAME
                  | PATTERN PATTERN
                  | (PATTERN ,..., PATTERN) | () 
                  | PATTERN : TYPE
                  | VAR @ PATTERN
                  | MIXFIX

MIXFIX          ::= PLACE
                  | NO-BRACKET-TOKEN            
                  | [ MIXFIX ,..., MIXFIX ]  | [ ] 
                  | { MIXFIX ,..., MIXFIX }  | { } 
                  | ( MIXFIX ,..., MIXFIX )  | ( )
                  | MIXFIX...MIXFIX 

QUAL-VAR        ::= (var VAR : TYPE)
INST-QUAL-NAME  ::= (op INST-OP-NAME : TYPESCHEME)
                  | (fun INST-OP-NAME : TYPESCHEME)
                  | (pred INST-OP-NAME : TYPESCHEME)
      
INST-OP-NAME    ::= OP-NAME
                  | OP-NAME [TYPE ,..., TYPE]

OP-NAME         ::= ID   %% "|" excluded for constructors only
TYPE-NAME       ::= ID   %% "?", "<", "=", "|" excluded
CLASS-NAME      ::= ID   %% simple but possibly compound
VAR             ::= ID   %% "<" excluded for GEN-VAR-DECL
TYPEVAR         ::= SIMPLE-ID