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

BASIC-ITEMS ::= SIG-ITEMS

| class/classes CLASS-ITEM ; ... ; CLASS-ITEM ;/

| class instance/instances CLASS-ITEM ; ... ; CLASS-ITEM ;/

| free type/types DATATYPE-DECL ; ... ; DATATYPE-DECL ;/

| generated type/types DATATYPE-DECL ; ... ; DATATYPE-DECL ;/

| generated { SIG-ITEMS ... SIG-ITEMS } ;/

| program/programs PROG-EQ ; ... ; PROG-EQ ;/

| var/vars GEN-VAR-DECL ; ... ; GEN-VAR-DECL ;/

| forall GEN-VAR-DECL ; ... ; GEN-VAR-DECL

"." AXIOM "." ... "." AXIOM ;/

| "." AXIOM "." ... "." AXIOM ;/

%% for backwards compatibility with CASL v1.0

BASIC-ITEMS ::= axiom/axioms AXIOM ;...; AXIOM ;/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

SIG-ITEMS ::= sort/sorts SORT-ITEM ; ... ; SORT-ITEM

| type/types DATATYPE-DECL ; ... ; DATATYPE-DECL ;/

| type/types TYPE-ITEM ; ... ; TYPE-ITEM ;/

| type instance/instances TYPE-ITEM ; ... ; TYPE-ITEM ;/

| op/ops OP-ITEM ; ... ; OP-ITEM ;/

| pred/preds PRED-ITEM ; ... ; PRED-ITEM ;/ %% old style

SORT-ITEM ::= TYPE-PATTERN , ... , TYPE-PATTERN

| TYPE-PATTERN , ... , TYPE-PATTERN < TYPE

| TYPE-PATTERN = ... = TYPE-PATTERN

| TYPE-PATTERN = { VAR : TYPE "." FORMULA }

TYPE-ITEM ::= SORT-ITEM

| TYPE-PATTERN , ... , TYPE-PATTERN : KIND

| TYPE-PATTERN := PSEUDOTYPE

TYPE-PATTERN ::= TYPE-NAME

| TYPE-NAME (TYPE-ARGS) ... (TYPE-ARGS)

| PRIM-TYPE-PATTERN ... PRIM-TYPE-PATTERN

PRIM-TYPE-PATTERN ::= [ ID , ... , ID ] %% compound list

| NO-BRACKET-TOKEN %% TYPE-NAME or TYPE-VAR

| { PRIM-TYPE-PATTERN ... PRIM-TYPE-PATTERN } | { }

| [ PRIM-TYPE-PATTERN ... PRIM-TYPE-PATTERN ] | [ ]

| TYPE-EXT-VAR

| TYPE-PATTERN-ARG

| (TYPE-PATTERN-ARG)

| (TYPE-ARGS) %% remaining arguments

TYPE-PATTERN-ARG ::= TYPE-EXT-VAR : CLASS

| TYPE-VAR : EXT-CLASS

| TYPE-VAR < TYPE

TYPE-VARS ::= TYPE-VAR , ... , TYPE-VAR

TYPE-EXT-VAR ::= TYPE-VAR | TYPE-VAR + | TYPE-VAR -

TYPE-EXT-VARS ::= TYPE-EXT-VAR , ... , TYPE-EXT-VAR

TYPE-ARG ::= TYPE-EXT-VARS %% globally declared or universe

| TYPE-VARS : EXT-CLASS

| TYPE-EXT-VARS : CLASS

| TYPE-EXT-VARS < TYPE

TYPE-ARGS :: TYPE-ARG ; ... ; TYPE-ARG

PSEUDOTYPE ::= TYPE

| \ TYPE-ARGS "." PSEUDOTYPE

| \ (TYPE-ARGS) ... (TYPE-ARGS) "." PSEUDOTYPE

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

CLASS-ITEM ::= CLASS-DECL

| CLASS-DECL {BASIC-ITEMS ... BASIC-ITEMS}

%% without "class" and without "type instance" inside

CLASS-DECL ::= CLASS-NAME , ... , CLASS-NAME

| CLASS-NAME , ... , CLASS-NAME < CLASS

| CLASS-NAME = CLASS

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

UNINST-OP-NAME :: = ID

OP-NAME ::= UNINST-OP-NAME

| UNINST-OP-NAME TYPE-INST-LIST ... TYPE-INST-LIST

TYPE-INST-LIST ::= [ TYPE-INST-DECL; ... ; TYPE-INST-DECL ]

TYPE-INST-DECL ::= TYPE-VAR , ... , TYPE-VAR %% global type vars

| TYPE-VAR-DECL

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

OP-ITEM ::= OP-NAME , ... , OP-NAME : TYPE-SCHEME

| OP-NAME , ... , OP-NAME : TYPE-SCHEME, OP-ATTR ,..., OP-ATTR

| OP-NAME : TYPE-SCHEME = TERM %% real constant (no shortcut)

| OP-NAME OP-ARGS : TYPE = TERM %% These forms are

| OP-NAME OP-ARGS :? TYPE = TERM %% discouraged

| OP-NAME :? TYPE = TERM %% shortcut for OP-NAME: () ->? TYPE

OP-ATTR ::= BIN-ATTR | unit TERM

BIN-ATTR ::= assoc | comm | idem

PRED-ITEM ::= OP-NAME, ..., OP-NAME: TYPE-SCHEME %% a product!

| OP-NAME ARG-DECLS <=> TERM %% This form is

%% not encouraged.

| OP-NAME <=> TERM %% Nor is this one.

%% The TYPE within a TYPE-SCHEME of a PRED-ITEM is expanded to TYPE ->? ()

%% not that (t1 -> t2) ->? () differs from t1 -> t2 ->? ()

%% therefore arguments of a predicate are products

%% curried ARG-DECLs must be put in parenthesis

%% because a TYPE consumes the following input

OP-ARGS ::= ARG-DECLS ... ARG-DECLS

ARG-DECLS ::= ( PATTERN ; ... ; PATTERN ) | ()

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% unknown IDs will become new variables

PATTERN ::= VAR , ... , VAR % globally declared

| VAR-DECL

| MIXFIX-PATTERN , ... , MIXFIX-PATTERN

MIXFIX-PATTERN ::= AS-PATTERN ... AS-PATTERN

| AS-PATTERN ... AS-PATTERN : TYPE

AS-PATTERN ::= INST-PATTERN

| VAR @ INST-PATTERN

| VAR : TYPE @ INST-PATTERN

INST-PATTERN ::= SIMPLE-PATTERN

| SIMPLE-PATTERN [TYPE, ... , TYPE]

| ( PATTERN ; ... ; PATTERN )

| ( )

SIMPLE-PATTERN ::= "__"

| NO-BRACKET-TOKEN %% VAR or part of ID

| [ PATTERN ; ... ; PATTERN ] | [ ] %% mixfix/compound

| { PATTERN ; ... ; PATTERN } | { } %% mixfix

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

PROG-EQ ::= MIXFIX-PATTERN = TERM %% TERM without formulae

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

DATATYPE-DECL ::= SIMPLE-DATATYPE-DECL | DERIVING-DATATYPE-DECL

SIMPLE-DATATYPE-DECL

::= TYPE-PATTERN "::=" ALTERNATIVE "|" ... "|" ALTERNATIVE

| TYPE-PATTERN : KIND "::="

ALTERNATIVE "|" ... "|" ALTERNATIVE

DERIVING-DATATYPE-DECL

::= SIMPLE-DATATYPE-DECL deriving CLASS

%% take instance-notation from TYPE-PATTERN

ALTERNATIVE ::= UNINST-OP-NAME COMPONENTS ... COMPONENTS

| UNINST-OP-NAME COMPONENTS ... COMPONENTS ?

| UNINST-OP-NAME

| sort/sorts/type/types TYPE , ... , TYPE

%% support for nested products

COMPONENTS ::= ( COMPONENT ; ... ; COMPONENT )

COMPONENT ::= UNINST-OP-NAME , ... , UNINST-OP-NAME : TYPE

| UNINST-OP-NAME , ... , UNINST-OP-NAME :? TYPE

| TYPE

| ( COMPONENT ; ... ; COMPONENT )

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

VAR-DECL ::= VAR ,..., VAR : TYPE

TYPE-VAR-DECL ::= TYPE-VAR , ... , TYPE-VAR: CLASS-NAME

| TYPE-VAR , ... , TYPE-VAR: type

| TYPE-VAR , ... , TYPE-VAR < TYPE

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

KIND ::= CLASS

| PROD-CLASS -> ... -> PROD-CLASS -> CLASS

PROD-CLASS ::= EXT-CLASS * ... * EXT-CLASS

EXT-CLASS ::= CLASS | CLASS + | CLASS -

%% intersection class must be put in parenthesis

CLASS ::= SIMPLE-CLASS | (CLASS , ... , CLASS)

SIMPLE-CLASS ::= type | CLASS-NAME

| { SIMPLE-ID . SIMPLE-ID < TYPE }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

TYPE-SCHEME ::= TYPE

| forall TYPE-VAR-DECL ; ... ; TYPE-VAR-DECL . TYPE-SCHEME

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

PRIM-TYPE ::= NO-BRACKET-TOKEN %% TYPE-VAR or TYPE-NAME

| [ ID , ... , ID ] %% compound list

| { TYPE } | { }

| [ TYPE ] | [ ]

| ( TYPE )

| ( ) %% unit

MIXFIX-TYPE ::= PRIM-TYPE ... PRIM-TYPE

| PRIM-TYPE ... PRIM-TYPE : KIND

PRODUCT-TYPE ::= MIXFIX-TYPE * ... * MIXFIX-TYPE

%% product-types (possibly) separated by arrows

TYPE ::= PRODUCT-TYPE ARROW ... ARROW PRODUCT-TYPE

%% ARROW must be treated like a terminal in the above rule

ARROW ::= ->? | -> | -->? | -->

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

FORMULA ::= TERM %% of type logical or ?unit

%% EQUAL-OP ::= "=" | =e= (only for backward compatibility)

%% BIN-CONNECT ::= /\ | \/ | => | if | <=>

%% also Prelude: not, true, false, def, __when__else__

TERM ::= MIXFIX-TERM

| MIXFIX-TERM TYPE-OP TYPE

| MIXFIX-TERM QUANT-TERM

| QUANT-TERM

| MIXFIX-TERM CASE-TERM

| CASE-TERM

| MIXFIX-TERM LET-TERM

| LET-TERM

MIXFIX-TERM ::= INST-TERM ... INST-TERM

TYPE-OP ::= ":" | as | in

LET-TERM ::= let PROG-EQ ; ... ; PROG-EQ in TERM

%% ";" is already used as item-separator

CASE-TERM ::= case TERM of PATTERN -> TERM "|" ... "|" PATTERN -> TERM

QUANT-TERM ::= QUANTIFIER VAR-DECL ;...; VAR-DECL "." TERM

| forall TYPE-VAR-DECL ;...; TYPE-VAR-DECL "." TERM

| \ LAMBDA-DOT TERM % for unit

| \ VAR-DECL LAMBDA-DOT TERM

| \ (PATTERN) ... (PATTERN) LAMBDA-DOT TERM

%% case/lambda-Terms must be without formula ingredients

LAMBDA-DOT ::= "." | ".!"

QUANTIFIER ::= forall | exists | exists!

INST-TERM ::= SIMPLE-TERM

| SIMPLE-TERM [TYPE, ... , TYPE]

| LITERAL

| QUAL-PRED-NAME | QUAL-VAR-NAME | QUAL-OP-NAME

| ( TERM , ... , TERM ) | ( )

SIMPLE-TERM ::= "__"

| NO-BRACKET-TOKEN %% plus formula keywords

| [ TERM , ... , TERM ] | [ ] %% mixfix/compound

| { TERM , ... , TERM } | { } %% mixfix

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

QUAL-VAR-NAME ::= ( var VAR : TYPE )

INST-OP-NAME ::= ID [TYPE, ... , TYPE] ... [TYPE, ... , TYPE]

QUAL-PRED-NAME ::= ( pred UNINST-OP-NAME : TYPE-SCHEME )

| ( pred INST-OP-NAME : TYPE)

QUAL-OP-NAME ::= ( op UNINST-OP-NAME : TYPE-SCHEME )

| ( op INST-OP-NAME : TYPE)

TYPE-NAME ::= ID %% MIXFIX-COMPOUND-ID

%% exluded are arrows, "*", "<", ">" and ":=" (and ":", ":?", "=", "::=")

CLASS-NAME ::= SIMPLE-ID

%% disjoint with TYPE-VAR and TYPE-NAME ingredients

VAR ::= ID %% mixfix but not compound

TYPE-VAR ::= SIMPLE-ID