module Casl-BasicItems

%% written/changed by Bjarke Wedemeijer (January 1998)

%% adapted by Mark van den Brand (Juni 1999)

%% adapted by Mark van den Brand (November 2000)

%% adapted by Christian Maeder (January 2002)

%% adapted by Christian Maeder (February 2004)

imports Casl-Lexical

exports

sorts

Basic-Spec Sort-S Op-S Pred-S Op-Type Pred-Type

lexical syntax

"."|[\183] -> Dot

context-free syntax

%% Basic-Items section

"{" "}" -> Basic-Spec

Ann Basic-Item+ -> Basic-Spec

Sig-Items -> Basic-Item

"free" Data-Item -> Basic-Item

"generated" Data-Item -> Basic-Item

"generated" "{" Sig-Items+ "}" Opt-Semi -> Basic-Item

Var-S {Var-Decl ";"}+ Opt-Semi -> Basic-Item

"forall" {Var-Decl ";"}+ Ann Dot-Item -> Basic-Item

Dot Ann Formula Opt-Semi -> Basic-Item

Dot Ann {Formula (Ann Dot)}+ Opt-Semi -> Dot-Item

%% old style

Axiom-S Ann {Formula (";" Ann)}+ Opt-Semi -> Basic-Item

%% Sig-Items

Sort-S Ann {Sort-Item (";" Ann)}+ Opt-Semi -> Sig-Items

Op-S Ann {Op-Item (";" Ann)}+ Opt-Semi -> Sig-Items

Pred-S Ann {Pred-Item (";" Ann)}+ Opt-Semi -> Sig-Items

Data-Item -> Sig-Items

%% Data-Item (abbreviation)

Datatype-S Ann {Datatype-Decl (";" Ann)}+ Opt-Semi -> Data-Item

%% Sort-Item

{Sort ","}+ -> Sort-Item

{Sort ","}+ "<" Sort -> Sort-Item

Sort "=" "{" Var ":" Sort Dot Formula "}" -> Sort-Item

Sort "=" {Sort "="}+ -> Sort-Item

%% Op-Item

{Op-Name ","}+ ":" Op-Type -> Op-Item

{Op-Name ","}+ ":" Op-Type "," {Op-Attr ","}+ -> Op-Item

Op-Name Op-Head "=" Term -> Op-Item

%% Op-Type

Some-Sorts "->" Sort -> Op-Type

Sort -> Op-Type

Some-Sorts "->?" Sort -> Op-Type

"?" Sort -> Op-Type

%% Sorts

{Sort "*"|[\215]}+ -> Some-Sorts

%% Op-Attr

"assoc" -> Op-Attr

"comm" -> Op-Attr

"idem" -> Op-Attr

"unit" Term -> Op-Attr

%% Op-Head

"(" {Arg-Decl ";"}+ ")" ":" Sort -> Op-Head

":" Sort -> Op-Head

"(" {Arg-Decl ";"}+ ")" ":" "?" Sort -> Op-Head

":" "?" Sort -> Op-Head

%% Arg-Decl

{Var ","}+ ":" Sort -> Arg-Decl

%% Pred-Item

{Pred-Name ","}+ ":" Pred-Type -> Pred-Item

Pred-Name Pred-Head "<=>" Formula -> Pred-Item

Pred-Name "<=>" Formula -> Pred-Item

%% Pred-Type

Some-Sorts -> Pred-Type

"(" ")" -> Pred-Type

%% Pred-Head

"(" {Arg-Decl ";"}+ ")" -> Pred-Head

%% Datatype-Decl

Sort "::=" Ann {Alternative ("|" Ann)}+ -> Datatype-Decl

%% Alternative

Op-Name"(" {Component ";"}+ ")" -> Alternative

Op-Name"(" {Component ";"}+ ")" "?" -> Alternative

Op-Name -> Alternative

Sort-S {Sort ","}+ -> Alternative

%% Component

{Op-Name ","}+ ":" Sort -> Component

{Op-Name ","}+ ":" "?" Sort -> Component

Sort -> Component

%% Var-Decl

{Var ","}+ ":" Sort -> Var-Decl

%% Var-S

"var" -> Var-S

"vars" -> Var-S

%% Axiom-S

"axiom" -> Axiom-S

"axioms" -> Axiom-S

%% Sort-S

"sort" -> Sort-S

"sorts" -> Sort-S

%% Op-S

"op" -> Op-S

"ops" -> Op-S

%% Pred-S

"pred" -> Pred-S

"preds" -> Pred-S

%% Datatype-S

"type" -> Datatype-S

"types" -> Datatype-S

%% Opt-Semi

";"? Ann -> Opt-Semi

%% Formula

Quantifier {Var-Decl ";"}+ Dot Formula -> Formula-Quant

Formula-Quant -> Formula

Formula-2 "<=>" Formula-2 -> Formula-1

Formula-2 "<=>" Formula-Quant -> Formula-1

Formula-2 -> Formula-1

Formula-1 -> Formula

Formula-3 "=>" Formula-3 -> Formula-2a

Formula-3 "=>" Formula-2a -> Formula-2a

Formula-3 "=>" Formula-Quant -> Formula-1

Formula-3 "if" Formula-3 -> Formula-2b

Formula-2b "if" Formula-3 -> Formula-2b

Formula-2b "if" Formula-Quant -> Formula-1

Formula-3 "if" Formula-Quant -> Formula-1

Formula-2a -> Formula-2

Formula-2b -> Formula-2

Formula-3 -> Formula-2

Formula-4 "/\\" Formula-4 -> Formula-3a

Formula-3a "/\\" Formula-4 -> Formula-3a

Formula-3a "/\\" Formula-Quant -> Formula-1

Formula-3 "/\\" Formula-Quant -> Formula-1

Formula-4 "\\/" Formula-4 -> Formula-3b

Formula-3b "\\/" Formula-4 -> Formula-3b

Formula-3b "\\/" Formula-Quant -> Formula-1

Formula-4 "\\/" Formula-Quant -> Formula-1

Formula-4 -> Formula-3

Formula-3a -> Formula-3

Formula-3b -> Formula-3

"not"|[\172] Formula-4 -> Formula-4

"not"|[\172] Formula-Quant -> Formula-Quant

"(" Formula ")" -> Formula-5

Formula-5 -> Formula-4

Atom -> Formula-5

"true" -> Atom

"false" -> Atom

"def" Term -> Atom

Term "=e="|"=" Term -> Atom

Term "in" Sort -> Atom

Term -> Atom

%% Quantifier

"forall" -> Quantifier

"exists" -> Quantifier

"exists" "!" -> Quantifier

%% Terms

{Term ","}+ -> Terms

%% Term

MixFix+ -> Term

Term "when" Formula "else" Term -> Term {right}

%% MixFix

Token -> MixFix

Literal -> MixFix

Place -> MixFix

QualPredName -> MixFix

QualVarName -> MixFix

QualOpName -> MixFix

MixFix ":"|"as" Sort -> MixFix

"(" Terms ")" -> MixFix

"[" Terms? "]" -> MixFix

"{" Terms? "}" -> MixFix

%% QualPredName

"(" "pred" Pred-Name ":" Pred-Type ")" -> QualPredName

%% QualVarName

"(" "var" Var ":" Sort ")" -> QualVarName

%% QualOpName

"(" "op" Op-Name ":" Op-Type ")" -> QualOpName

%% Various small definitions

Sort-Id -> Sort

Id -> Op-Name

Id -> Pred-Name

Simple-Id -> Var

context-free priorities

MixFix+ -> Term >

Term "when" Formula "else" Term -> Term