Abstract-Syntax.txt revision 7dd4c81b6f5e1948fcbb23e5b02bfc32cbfc69b9
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederBASIC-SPEC ::= basic-spec BASIC-ITEMS*
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederBASIC-ITEMS ::= SIG-ITEMS | CLASS-ITEMS | INSTANCE-ITEMS
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski | FREE-DATATYPE | SORT-GEN
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder | VAR-ITEMS | LOCAL-VAR-AXIOMS | AXIOM-ITEMS
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederSIG-ITEMS ::= SORT-ITEMS | TYPE-ITEMS | OP-ITEMS | PRED-ITEMS
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder | DATATYPE-ITEMS
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederSORT-ITEMS ::= sort-items SORT-ITEM+ %% Only for reverse compatibility
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederSORT-ITEM ::= SORT-DECL
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederSORT-DECL ::= sort-decl TYPE-NAME+ CLASS*
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederTYPE-ITEMS ::= type-constr-items TYPE-ITEM+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederTYPE-ITEM ::= TYPE-DECL | TYPE-ALIAS-DEFN
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederTYPE-DECL ::= TYPE-VAL-DECL | TYPE-FUN-DECL
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederTYPE-VAL-DECL ::= type-val-const-decl TYPE-NAME+ KIND
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederTYPE-FUN-DECL ::= type-constr-fun-decl TYPE-PATTERN+ CLASS+
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederTYPE-PATTERN ::= type-constr-pattern TYPE-NAME TYPE-ARG*
04dada28736b4a237745e92063d8bdd49a362debChristian MaederTYPE-ARG ::= TYPE-VARS | TYPE-ARG-DECL
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederTYPE-VARS ::= type-vars TYPE-VAR+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederTYPE-ARG-DECL ::= type-arg-decl TYPE-VAR+ EXT-CLASS
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian MaederTYPE-ALIAS-DEFN ::= TYPE-ALIAS-VAL-DEFN | TYPE-ALIAS-FUN-DEFN
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederTYPE-ALIAS-VAL-DEFN ::= type-alias-val-defn TYPE-NAME PSEUDOTYPE
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPSEUDOTYPE ::= TYPE | LAMBDA-TYPE
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederLAMBDA-TYPE ::= lambda-type TYPE-VAR-DECL+ TYPE
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederTYPE-ALIAS-FUN-DEFN ::= type-alias-fun-defn TYPE-PATTERN TYPE
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian MaederCLASS-ITEMS ::= class-items CLASS-ITEM+
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederCLASS-ITEM ::= CLASS-DECL | SUBCLASS-DECL
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederCLASS-DECL ::= class-decl CLASS-NAME+
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaederSUBCLASS-DECL ::= subclass-decl CLASS-NAME+ CLASS-NAME
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian MaederOP-ITEMS ::= op-items OP-ITEM+
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederOP-ITEM ::= OP-DECL | OP-DEFN
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaederOP-DECL ::= op-decl OP-NAME+ TYPE-SCHEME OP-ATTR*
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski %% OP-TYPE, TOTAL-OP-TYPE, PARTIAL-OP-TYPE, SORT-LIST: obsolete
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederOP-ATTR ::= BINARY-OP-ATTR | UNIT-OP-ATTR
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaederBINARY-OP-ATTR ::= assoc-op-attr | comm-op-attr | idem-op-attr
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederUNIT-OP-ATTR ::= unit-op-attr TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederOP-DEFN ::= OP-FUN-DEFN | OP-VAL-DEFN | OP-REC-VAL-DEFN
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederOP-FUN-DEFN ::= op-fun-defn OP-NAME OP-HEAD TERM
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder %% not encouraged
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder %% equivalent to quantified external formula,
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder %% loose definition due to intensionality
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederOP-HEAD ::= TOTAL-OR-NO-HEAD | PARTIAL-OP-HEAD
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTOTAL-OP-HEAD ::= total-op-head ARG-DECL+ TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPARTIAL-OP-HEAD ::= partial-op-head ARG-DECL+ TYPE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederARG-DECL ::= arg-decl VAR+ TYPE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederOP-VAL-DEFN ::= op-val-defn OP-NAME TYPE TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederOP-REC-VAL-DEFN ::= op-rec-val-defn OP-NAME TYPE TERM
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederPRED-ITEMS ::= pred-items PRED-ITEM+ %% only for compatibility
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPRED-ITEM ::= PRED-DECL | PRED-DEFN
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPRED-DECL ::= pred-decl OP-NAME+ TYPE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederPRED-TYPE: obsolete
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederPRED-DEFN ::= PRED-FUN-DEFN | PRED-VAL-DEFN | PRED-REC-VAL-DEFN
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederPRED-FUN-DEFN ::= pred-fun-defn OP-NAME PRED-HEAD FORMULA
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederPRED-HEAD ::= pred-head ARG-DECL+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederPRED-VAL-DEFN ::= pred-val-defn OP-NAME TYPE TERM
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederPRED-REC-VAL-DEFN::= pred-rec-val-defn OP-NAME TYPE TERM
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederDATATYPE-ITEMS ::= datatype-items DATATYPE-DECL+
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederDATATYPE-DECL ::= SIMPLE-DATATYPE-DECL | DERIVING-DATATYPE-DECL
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederSIMPLE-DATATYPE-DECL
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder ::= simple-datatype-decl TYPE-PATTERN ALTERNATIVE+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederDERIVING-DATATYPE-DECL
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ::= deriving-datatype-decl SIMPLE-DATATYPE-DECL CLASS+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederALTERNATIVE ::= TOTAL-CONSTRUCT | PARTIAL-CONSTRUCT
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTOTAL-CONSTRUCT ::= total-construct OP-NAME COMPONENTS*
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederPARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederCOMPONENTS ::= TOTAL-SELECT | PARTIAL-SELECT | TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTOTAL-SELECT ::= total-select OP-NAME+ TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPARTIAL-SELECT ::= partial-select OP-NAME+ TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederFREE-DATATYPE ::= free-datatype DATATYPE-ITEMS
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederSORT-GEN ::= sort-gen SIG-ITEMS+
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederVAR-ITEMS ::= var-items GEN-VAR-DECL+
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederGEN-VAR-DECL ::= VAR-DECL | TYPE-VAR-DECL
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederVAR-DECL ::= var-decl VAR+ TYPE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederTYPE-VAR-DECL ::= type-var-decl TYPE-VAR+ CLASS+
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaederLOCAL-VAR-AXIOMS ::= local-var-axioms VAR-DECL+ AXIOM+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederAXIOM-ITEMS ::= axiom-items AXIOM+
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederKIND ::= kind EXT-CLASS* CLASS %% Argumente, Resultat
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederEXT-CLASS ::= CLASS+ | VARIANCE | CLASSES-WITH-VARIANCE
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederCLASSES-WITH-VARIANCE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ::= class-with-variance CLASS+ VARIANCE
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederVARIANCE ::= covariant | contravariant | invariant
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder%% Idee: Varianz von Konstruktoren kann spezifiziert werden,
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder%% wird bei Datentypen ausserdem inferiert (?). Irrtuemer geben
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder%% dann eben Inkonsistenzen.
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederCLASS ::= UNIVERSE | DOWNSET | CLASS-NAME
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederUNIVERSE ::= type
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederDOWNSET ::= downset TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederTYPE-SCHEME ::= TYPE | POLYMORPHIC-TYPE
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederPOLYMORPHIC-TYPE ::= polymorphic-type TYPE-VAR-DECL+ TYPE
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTYPE ::= TYPE-VAR | PROD-TYPE | TOTAL-FUN-TYPE
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder | PARTIAL-FUN-TYPE | TOTAL-CONT-TYPE
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski | PARTIAL-CONT-TYPE | PRED-TYPE | UNIT-TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | TYPE-APPL
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederPROD-TYPE ::= prod-type TYPE+
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTOTAL-FUN-TYPE ::= total-funp-type TYPE TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPARTIAL-FUN-TYPE ::= partial-fun-type TYPE TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTOTAL-CONT-TYPE ::= total-cont-type TYPE TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPARTIAL-CONT-TYPE::= partial-cont-type TYPE TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPRED-TYPE ::= pred-type TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederUNIT-TYPE ::= unit-type
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTYPE-APPL ::= type-constr-application TYPE-NAME TYPE*
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederAXIOM ::= EXT-FORMULA | TYPE-QUANTIFICATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTYPE-QUANTIFICATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder ::= type-quantification TYPE-VAR-DECL+ EXT-FORMULA
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederEXT-FORMULA ::= FORMULA | REC-EQUATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederFORMULA ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | IMPLICATION | EQUIVALENCE | NEGATION | ATOM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederQUANTIFICATION ::= quantification QUANTIFIER VAR-DECL+ FORMULA
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederQUANTIFIER ::= universal | existential | unique-existential
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederCONJUNCTION ::= conjunction FORMULA+
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederDISJUNCTION ::= disjunction FORMULA+
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederIMPLICATION ::= implication FORMULA FORMULA
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederEQUIVALENCE ::= equivalence FORMULA FORMULA
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederNEGATION ::= negation FORMULA
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederREC-EQUATION ::= rec-equation OP-NAME TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederATOM ::= TRUTH | EXISTL-EQUATION | STRONG-EQUATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | INTERNAL-FORMULA %% !!!
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTRUTH ::= true-atom | false-atom
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPREDICATION, PRED-SYMB, QUAL-PRED-NAME: obsolete
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederEXISTL-EQUATION ::= existl-equation TERM TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederSTRONG-EQUATION ::= strong-equation TERM TERM
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederINT-FORMULA ::= TERM %% Of type unit --> static analysis
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTERMS: obsolete
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTERM ::= VAR | QUAL-VAR | APPLICATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | TYPED-TERM | CONDITIONAL | TOTAL-LAMBDA-TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | PARTIAL-LAMBDA-TERM | PRED-LAMBDA-TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder | POLY-LAMBDA-TERM | PROJECTION1-TERM
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder | ... | PROJECTIONN-TERM | UNIT-TERM | TUPLE-TERM
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder | CONSTANT-TERM | CASE-TERM | RES-TERM
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder | FIX-TERM | LOGIC-TERM
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder%% Checking that abstractions don't contain conditionals is left to the
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder%% static analysis!
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederQUAL-VAR ::= qual-var VAR TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederAPPLICATION ::= application TERM TERM
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederOP-SYMB ::= OP-NAME | QUAL-OP-NAME
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederQUAL-OP-NAME ::= qual-op-name OP-NAME OP-TYPE
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederTYPED-TERM ::= typed-term TERM TYPE
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederCONDITIONAL ::= conditional FORMULA TERM TERM
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederDEFINEDNESS ::= definedness TERM
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederTOTAL-LAMBDA-TERM::= total-lambda-term VAR-DECL+ TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPARTIAL-LAMBDA-TERM
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder ::= partial-lambda-term VAR-DECL+ TERM
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederPRED-LAMBDA-TERM ::= pred-lambda-term VAR-DECL+ INT-FORMULA
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederPROJECTION1-TERM ::= projection1-term TERM
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder...
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederPROJECTIONN-TERM ::= projectionn-term TERM
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederUNIT-TERM ::= unit-term
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederTUPLE-TERM ::= tuple-term TERM TERM+
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederCONSTANT-TERM ::= constant-term OP-NAME TYPE*
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederCASE-TERM ::= case-term TERM CASE+
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederCASE ::= case OP-NAME TOTAL-OP-HEAD TERM
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederRES-TERM ::= res-term TERM TERM
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaederFIX-TERM ::= fix-term TERM
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederLOGIC-TERM ::= INT-TRUTH
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder | INT-NEGATION
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder | INT-CONJUNCTION
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | INT-DISJUNCTION
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | INT-IMPLICATION
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder | INT-EQUIVALENCE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder | INT-QUANTIFICATION
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederINT-TRUTH ::= SIMPLE-INT-TRUTH | TYPED-INT-TRUTH
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederTYPED-INT-TRUTH ::= typed-int-truth SIMPLE-INT-TRUTH TYPE
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederSIMPLE-INT-TRUTH ::= tt | ff
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederINT-NEGATION ::= int-negation INT-FORMULA
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederINT-CONJUNCTION ::= int-conjunction INT-FORMULA INT-FORMULA+
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederINT-DISJUNCTION ::= int-disjunction INT-FORMULA INT-FORMULA+
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederINT-IMPLICATION ::= int-implication INT-FORMULA INT-FORMULA
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederINT-EQUIVALENCE ::= int-equivalence INT-FORMULA INT-FORMULA
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederINT-QUANTIFICATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder ::= SIMPLE-INT-QUANTIFICATION
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder | TYPED-INT-QUANTIFICATION
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederTYPED-INT-QUANTIFICATION
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder ::= typed-int-quantification SIMPLE-INT-QUANTIFICATION TYPE
15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaederSIMPLE-INT-QUANTIFICATION
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder ::= simple-int-quantification INT-QUANTIFIER TERM
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiINT-QUANTIFIER ::= int-all | int-exists | int-exists-uniquely
SORT: obsolete
CLASS-NAME ::= TOKEN-ID
TYPE-NAME ::= ID
OP-NAME ::= ID
PRED-NAME: obsolete
VAR ::= SIMPLE-ID
TYPE-VAR ::= SIMPLE-ID
SIMPLE-ID ::= WORDS
ID ::= TOKEN-ID | MIXFIX-ID
TOKEN-ID ::= TOKEN
TOKEN ::= WORDS | DOT-WORDS | SIGNS | DIGIT | QUOTED-CHAR
MIXFIX-ID ::= TOKEN-PLACES
TOKEN-PLACES ::= token-places TOKEN-OR-PLACE+
TOKEN-OR-PLACE ::= TOKEN | PLACE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% With subsorting %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
SORT-ITEM ::= ... | SUBSORT-DECL | ISO-DECL | SUBSORT-DEFN
%% again: only for compatibility
SUBSORT-DECL ::= subsort-decl TYPE-NAME+ TYPE
ISO-DECL ::= iso-decl TYPE-NAME+
SUBSORT-DEFN ::= subsort-defn TYPE-NAME+ VAR
TYPE FORMULA
TYPE-ITEM ::= ...
| SUBTYPE-DECL | TYPE-ISO-DECL | SUBTYPE-DEFN
SUBTYPE-DECL ::= SUBTYPE-VAL-DECL | SUBTYPE-FUN-DECL
SUBTYPE-VAL-DECL ::= subtype-val-decl TYPE-NAME PSEUDOTYPE
SUBTYPE-FUN-DECL ::= subtype-fun-decl TYPE-PATTERN+ TYPE
TYPE-ISO-DECL ::= TYPE-ISO-VAL-DECL | TYPE-ISO-FUN-DECL
TYPE-ISO-VAL-DECL::= type-iso-val-decl TYPE-NAME+
TYPE-ISO-FUN-DECL::= type-iso-fun-decl TYPE-PATTERN+
SUBTYPE-DEFN ::= subtype-defn TYPE-PATTERN VAR TYPE FORMULA
%% alias < type must be caught by the static semantics !
ALTERNATIVE ::= ... | SUBTYPE
SUBTYPE ::= subtype TYPE
TERM ::= ... | MEMBERSHIP
MEMBERSHIP ::= membership TERM TYPE
TERM ::= ... | CAST
CAST ::= cast TERM TYPE
Concrete Syntax
===============
BASIC-SPEC ::= BASIC-ITEMS...BASIC-ITEMS | { }
BASIC-ITEMS ::= SIG-ITEMS
| class/classes CLASS-DECL ;...; CLASS-DECL ;/
| instance/instances INSTANCE-DECL ;...; INSTANCE-DECL ;/
| free type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
| generated type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
| generated { SIG-ITEMS...SIG-ITEMS } ;/
| var/vars GEN-VAR-DECL ;...; GEN-VAR-DECL ;/
| forall GEN-VAR-DECL ;...; GEN-VAR-DECL
"." AXIOM "."..."." AXIOM ;/
| "." AXIOM "."..."." AXIOM ;/
The following alternative concrete syntax productions:
BASIC-ITEMS ::= var/vars GEN-VAR-DECL ;...; GEN-VAR-DECL
"." AXIOM "."..."." AXIOM ;/
| axiom/axioms AXIOM ;...; AXIOM ;/
are included for backwards compatibility with CASL v1.0, but may be
removed in some future version.
SIG-ITEMS ::= sort/sorts SORT-ITEM ;...; SORT-ITEM ;/
| type/types TYPE-ITEM;...; TYPE-ITEM ;/
| op/ops OP-ITEM ;...; OP-ITEM ;/
| pred/preds PRED-ITEM ;...; PRED-ITEM ;/
| type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
SORT-ITEM ::= TYPE-NAME ,..., TYPE-NAME
| TYPE-NAME ,..., TYPE-NAME < TYPE-NAME
| TYPE-NAME = { VAR : TYPE "." FORMULA }
| TYPE-NAME =...= TYPE-NAME
TYPE-ITEM ::= TYPE-NAME ,..., TYPE-NAME: KIND
| TYPE-PATTERN ,..., TYPE-PATTERN:
CLASS ,..., CLASS
| TYPE-NAME = PSEUDOTYPE
| TYPE-PATTERN = TYPE
TYPE-PATTERN
::= TYPE-NAME
| TYPE-NAME(TYPE-VAR-OR-DECL ;...; TYPE-VAR-OR-DECL)
| TYPE-NAME TYPE-VAR-OR-DECL ... TYPE-VAR-OR-DECL
TYPE-VAR-OR-DECL::= TYPE-VAR | TYPE-VAR: EXT-CLASS
PSEUDOTYPE ::= TYPE
| \ TYPE-VAR-DECL ;...; TYPE-VAR-DECL "." TYPE
CLASS-ITEMS ::= class/classes CLASS-ITEM; ...; CLASS-ITEM
CLASS-ITEM ::= CLASS-NAME
| CLASS-NAME ,..., CLASS-NAME < CLASS-NAME
INSTANCE-ITEMS ::= instance/instances INSTANCE-ITEM ;...; INSTANCE-ITEM
INSTANCE-ITEM ::= INSTANCE-DECL | INSTANCE-DEFN
INSTANCE-DECL ::= CLASS-NAME < CLASS-NAME
| TYPE-VAR: CLASS-NAME < CLASS-NAME
| TYPE: KIND
| TYPE(CLASS, ...,CLASS): CLASS
| TYPE-PATTERN: CLASS
INSTANCE-DEFN ::= INSTANCE-DECL { BASIC-SPEC }
OP-ITEM ::= OP-NAME, ..., OP-NAME: TYPE-SCHEME
| OP-NAME, ..., OP-NAME: TYPE-SCHEME, OP-ATTR ,..., OP-ATTR
| OP-NAME: TYPE = TERM
| OP-NAME: TYPE =rec TERM
| OP-NAME OP-ARGS : TYPE = TERM %% This form is
| OP-NAME OP-ARGS :? TYPE = TERM %% not encouraged
%% OP-ARGS instead of OP-HEAD and PRED-HEAD
%% OP-TYPE: obsolete
%% SOME-SORTS: obsolete
OP-ATTR ::= assoc | comm | idem | unit TERM
PRED-ITEM ::= OP-NAME, ..., OP-NAME: TYPE
| OP-NAME OP-ARGS <=> FORMULA %% This form is
%% not encouraged.
| OP-NAME <=> FORMULA %% Nor is this one.
| OP-NAME: TYPE = TERM %% \-Term -? unit
| OP-NAME: TYPE =rec TERM %% \-Term ->? unit
%% PRED-TYPE: obsolete
OP-ARGS ::= ARG-DECLS ... ARG-DECLS
ARG-DECLS ::= ( ARG-DECL ;...; ARG-DECL )
ARG-DECL ::= VAR ,..., VAR : TYPE
%% curried ARG-DECLs must be but in parenthesis
%% because a TYPE would "eat" a following VAR
DATATYPE-DECL ::= SIMPLE-DATATYPE-DECL | DERIVING-DATATYPE-DECL
SIMPLE-DATATYPE-DECL
::= TYPE-PATTERN "::="
ALTERNATIVE "|"..."|" ALTERNATIVE
DERIVING-DATATYPE-DECL
::= SIMPLE-DATATYPE-DECL deriving CLASS ,..., CLASS
ALTERNATIVE ::= OP-NAME COMPONENTS ... COMPONENTS
| OP-NAME COMPONENTS ... COMPONENTS ?
| OP-NAME
| sort/sorts TYPE-NAME ,..., TYPE-NAME
| type/types TYPE ,..., TYPE
%% compare with OP-ARGS
COMPONENTS ::= ( COMPONENT ;...; COMPONENT )
COMPONENT ::= OP-NAME ,..., OP-NAME : TYPE
| OP-NAME ,..., OP-NAME : ? TYPE
| TYPE
VAR-DECL ::= VAR ,..., VAR : TYPE
TYPE-VAR-DECL ::= TYPE-VAR, ..., TYPE-VAR: CLASS ,..., CLASS
KIND ::= EXT-CLASS * ... * EXT-CLASS -> CLASS,...,CLASS
EXT-CLASS ::= CLASS ,..., CLASS | + | -
| CLASS ,..., CLASS +
| CLASS ,..., CLASS -
%% VARIANCE ::= covariant | contravariant | invariant
CLASS ::= type | {TYPE} | CLASS-NAME
TYPE-SCHEME ::= TYPE | forall TYPE-VAR-DECL;...;TYPE-VAR-DECL. TYPE
PRIM-TYPE ::= NO-BRACKET-TOKEN %% TYPE-VAR or TYPE-NAME
| (TYPE)
| () %% unit
MIXFIX-TYPE ::= PRIM-TYPE ... PRIM-TYPE
PRODUCT-TYPE ::= MIXFIX-TYPE * ... * MIXFIX-TYPE
TYPE ::= PRODUCT-TYPE ARR ... ARR PRODUCT-TYPE
ARR ::= ->? | -> | -->? | -->
AXIOM ::= EXT-FORMULA | TYPE-QUANTIFICATION
TYPE-QUANTIFICATION
::= forall TYPE-VAR-DECL ;...; TYPE-VAR-DECL "." EXT-FORMULA
EXT-FORMULA ::= FORMULA | OP-NAME =rec TERM
FORMULA ::= QUANTIFIER VAR-DECL ;...; VAR-DECL "." FORMULA
| FORMULA /\ FORMULA /\.../\ FORMULA
| FORMULA \/ FORMULA \/...\/ FORMULA
| FORMULA => FORMULA
| FORMULA if FORMULA
| FORMULA <=> FORMULA
| not FORMULA
| true | false
| TERM =e= TERM
| TERM = TERM
| ( FORMULA )
| MIXFIX...MIXFIX
| TERM
QUANTIFIER ::= forall | exists | exists!
TERMS: obsolete
TERM ::= MIXFIX...MIXFIX
MIXFIX ::= NO-BRACKET-TOKEN | LITERAL | PLACE
| QUAL-PRED-NAME | QUAL-VAR-NAME | QUAL-OP-NAME
| OP-NAME
| OP-NAME(TYPE, ..., TYPE)
| OP-NAME TYPE ... TYPE
| TERM : TYPE
| TERM as TYPE
| TERM when FORMULA else TERM
| TERM ... TERM
| ( TERM ,..., TERM )
| [ TERM ,..., TERM ] | [ ]
| { TERM ,..., TERM } | { }
| pr1(TERM) | ... | prn(TERM)
| ()
| \ VAR-DECL "." ! TERM
| \ VAR-DECL "." TERM
| case TERM of TERM -> TERM; ... TERM -> TERM ;/
| TERM res TERM
| tt | tt TYPE | tt(TYPE)
| ff | ff TYPE | ff(TYPE)
| neg TERM
| TERM and ... and TERM
| TERM or ... or TERM
| TERM impl TERM
| TERM equiv TERM
| INT-QUANTIFIER TERM | INT-QUANTIFIER TYPE TERM
| INT-QUANTIFIER(TYPE) TERM
INT-QUANTIFIER ::= all | ex | ex!
QUAL-VAR-NAME ::= ( var VAR : TYPE )
QUAL-PRED-NAME ::= ( pred OP-NAME : TYPE )
QUAL-OP-NAME ::= ( op OP-NAME : TYPE )
TYPE-NAME::= ID
OP-NAME ::= ID
PRED-NAME: obsolete
CLASS-NAME ::= TOKEN-ID
VAR ::= SIMPLE-ID
TYPE-VAR ::= SIMPLE-ID
SIMPLE-ID ::= WORDS
ID ::= TOKEN-ID | MIXFIX-ID
TOKEN-ID ::= TOKEN
MIXFIX-ID ::= TOKEN-ID PLACE-TOKEN-ID ... PLACE-TOKEN-ID
| PLACE-TOKEN-ID ... PLACE-TOKEN-ID
PLACE-TOKEN-ID ::= PLACE TOKEN-ID
| PLACE
PLACE ::= __
TOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
| SIGNS
NO-BRACKET-TOKEN::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
| NO-BRACKET-SIGNS
SIGNS ::= NO-BRACKET-SIGNS | BRACKET-SIGNS
| NO-BRACKET-SIGNS BRACKET-SIGNS
BRACKET-SIGNS ::= BRACKET SIGNS
| BRACKET
BRACKET ::= [ | ] | { | }
LITERAL ::= DIGITS | FRACTION | FLOATING | STRING