1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- HetCATS/HasCASL/As.hs

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder $Id$

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Authors: Christian Maeder

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Year: 2002

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder abstract syntax for HasCASL

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder more liberal than HetCATS/HasCASL/Concrete-Syntax.txt

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder annotations almost as in HetCATS/CASL/AS_Basic_CASL.hs v 1.8

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder-}

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule As where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Id

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport AS_Annotation

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederdata BasicSpec = BasicSpec [Annoted BasicItem]

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederdata BasicItem = SigItems SigItems

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder | ProgItems [Annoted ProgEq] [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "program", dots

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | ClassItems Instance [Annoted ClassItem] [Pos]

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu -- pos "class", ";"s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | GenVarItems [GenVarDecl] [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "var", ";"s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | FreeDatatype [Annoted DatatypeDecl] [Pos]

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder -- pos "free", "type", ";"s

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz | GenItems [Annoted SigItems] [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "generated" "{", ";"s, "}"

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -- or "generated" "type" ";"s

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder | AxiomItems [GenVarDecl] [Annoted Formula] [Pos]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -- pos "forall" (if GenVarDecl not empty), dots

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder deriving (Show, Eq)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescudata SigItems = TypeItems Instance [Annoted TypeItem] [Pos] -- including sort

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -- pos "type", ";"s

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder | OpItems [Annoted OpItem] [Pos]

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder -- pos "op", ";"s

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder | PredItems [Annoted PredItem] [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "pred", ";"s

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- "instance" indicator

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederdata Instance = Instance | Plain deriving (Show, Eq)

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata ClassItem = ClassItem ClassDecl [Annoted BasicItem] [Pos]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -- pos "{", ";"s "}"

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder deriving (Show, Eq)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maederdata ClassDecl = ClassDecl [ClassId] [Pos]

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz -- pos ","s

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | SubclassDecl [ClassId] Class [Pos]

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder -- pos ","s, "<"

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder | ClassDefn ClassId Class [Pos]

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder -- pos "="

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder | DownsetDefn ClassId Token Type [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos " =" "{", dot, "<", typeVar, "}"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederdata TypeItem = TypeDecl [TypePattern] Kind [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos ","s

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | SubtypeDecl [TypePattern] Type [Pos]

431eff6083370269f3a37767bcde001f389ac927mcodescu -- pos ","s, "<"

431eff6083370269f3a37767bcde001f389ac927mcodescu | IsoDecl [TypePattern] [Pos]

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder -- pos "="s

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder | SubtypeDefn TypePattern Var Type (Annoted Formula) [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "=", "{", ":", dot, "}"

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu | AliasType TypePattern Kind PseudoType [Pos]

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu -- pos ":="

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu | Datatype DatatypeDecl

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu deriving (Show, Eq)

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescudata TypePattern = TypePattern TypeId [TypeArg] [Pos]

431eff6083370269f3a37767bcde001f389ac927mcodescu -- pos "("s, ")"s

431eff6083370269f3a37767bcde001f389ac927mcodescu | TypePatternToken Token

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu | MixfixTypePattern [TypePattern]

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu | BracketTypePattern BracketKind [TypePattern] [Pos]

42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu -- pos brackets

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | TypePatternArgs [TypeArg]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederdata PseudoType = SimplePseudoType Type

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | PseudoType [TypeArgs] PseudoType [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "\" "("s, ")"s, dot

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata Type = TypeName TypeId Int -- analysed

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- Int > 0 means generalized

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder | TypeAppl Type Type

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | TypeToken Token

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | BracketType BracketKind [Type] [Pos]

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -- pos "," (between type arguments)

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | KindedType Type Kind Pos

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder -- pos ":"

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder | MixfixType [Type]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | LazyType Type Pos

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "?"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | ProductType [Type] [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos crosses

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder | FunType Type Arrow Type [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos arrow

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata Arrow = FunArr| PFunArr | ContFunArr | PContFunArr

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederdata Pred = IsIn ClassId [Type]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata Qual t = [Pred] :=> t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- no curried notation for bound variables

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederdata TypeScheme = SimpleTypeScheme Type

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | TypeScheme [TypeArg] (Qual Type) [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos "forall", ";"s, dot

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata Partiality = Partial | Total deriving (Show, Eq)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederdata OpItem = OpDecl [OpId] TypeScheme [OpAttr] [Pos]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos ","s, ":", ","s, "assoc", "comm", "idem", "unit"

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder | OpDefn OpId [Pattern] TypeScheme Partiality Term [Pos]

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder -- pos "("s, ")"s, ":" or ":?", "="

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder deriving (Show, Eq)

935613eb8e67d724f1c4a4d4a37be3324ef6708dChristian Maeder

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maederdata PredItem = PredDecl [OpId] TypeScheme [Pos]

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder -- pos ","s, ":", ","s

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | PredDefn OpId [Pattern] Formula [Pos]

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -- pos "("s, ")"s, "<=>"

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder deriving (Show, Eq)

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maederdata BinOpAttr = Assoc | Comm | Idem deriving (Show, Eq)

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maederdata OpAttr = BinOpAttr BinOpAttr Pos | UnitOpAttr Term Pos deriving (Show, Eq)

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maederdata DatatypeDecl = DatatypeDecl

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder TypePattern

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Kind

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder [Annoted Alternative]

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder (Maybe Class)

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder [Pos]

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder -- pos "::=", "|"s, "deriving"

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder deriving (Show, Eq)

392b67dbb9414475750ac2a977348de77354c600Christian Maeder

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maederdata Alternative = Constructor UninstOpId [Components] Partiality [Pos]

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder -- pos: "?"

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder | Subtype [Type] [Pos]

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder -- pos: "type", ","s

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder deriving (Show, Eq)

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maederdata Components = Selector UninstOpId Partiality Type SeparatorKind Pos

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -- pos ",", ":" or ":?"

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | NoSelector Type

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | NestedComponents [Components] [Pos]

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder -- pos : "(", ";"s, ")"

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder deriving (Show, Eq)

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederdata Quantifier = Universal | Existential | Unique

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder deriving (Show, Eq)

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maederdata TypeQual = OfType | AsType | InType deriving (Show, Eq)

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maederdata BracketKind = Parens | Squares | Braces deriving (Show, Eq)

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder

data LogOp = NotOp | AndOp | OrOp | ImplOp | EquivOp deriving (Show, Eq)

data EqOp = EqualOp | ExEqualOp deriving (Show, Eq)

-- proper formulae only exist after static analysis

data Formula = TermFormula Term

| ConnectFormula LogOp [Formula] [Pos]

-- pos not, "/\", "\/", impl, "<=>"

| EqFormula EqOp Term Term [Pos]

-- pos "=", "=e="

| DefFormula Term [Pos]

-- pos "def"

| QuantifiedFormula Quantifier [VarDecl] Formula [Pos]

-- pos quantifier, ";"s, dot

| PolyFormula [TypeArg] Formula [Pos]

-- pos "forall", ";"s, dot

deriving (Show, Eq)

-- parse quantified formulae as terms first

-- eases also parsing of formulae in parenthesis

data Term = CondTerm Term Formula Term [Pos]

-- pos "when", "else"

| QualVar Var Type [Pos]

-- pos "(", "var", ":", ")"

| QualOp InstOpId TypeScheme [Pos]

-- pos "(", "op", ":", ")"

| ApplTerm Term Term [Pos] -- analysed

-- pos?

| TupleTerm [Term] [Pos]

-- pos "(", ","s, ")"

| TypedTerm Term TypeQual Type Pos

-- pos ":", "as" or "in"

| QuantifiedTerm Quantifier [GenVarDecl] Term [Pos]

-- pos quantifier, ";"s, dot

-- only "forall" may have a TypeVarDecl

| LambdaTerm [Pattern] Partiality Term [Pos]

-- pos "\", dot (plus "!")

| CaseTerm Term [ProgEq] [Pos]

-- pos "case", "of", "|"s

| LetTerm [ProgEq] Term [Pos]

-- pos "where", ";"s

| TermToken Token

| MixfixTerm [Term]

| BracketTerm BracketKind [Term] [Pos]

-- pos brackets, ","s

deriving (Show, Eq)

data Pattern = PatternVars [VarDecl] [Pos]

-- pos ";"s

| PatternConstr InstOpId TypeScheme [Pattern] [Pos]

-- constructor or toplevel operation applied to arguments

-- pos "("s, ")"s

| PatternToken Token

| BracketPattern BracketKind [Pattern] [Pos]

-- pos brackets, ";"s, ","s

| TuplePattern [Pattern] [Pos]

-- pos ","s

| MixfixPattern [Pattern] -- or HO-Pattern

| TypedPattern Pattern Type [Pos]

-- pos ":"

| AsPattern Pattern Pattern [Pos]

-- pos "@"

deriving (Show, Eq)

data ProgEq = ProgEq Pattern Term Pos deriving (Show, Eq)

-- pos "=" (or "->" following case-of)

-- ----------------------------------------------------------------------------

-- (type) var decls

-- ----------------------------------------------------------------------------

data SeparatorKind = Comma | Other deriving (Show, Eq)

data VarDecl = VarDecl Var Type SeparatorKind Pos deriving (Show, Eq)

-- pos "," or ":"

data TypeVarDecls = TypeVarDecls [TypeArg] [Pos] deriving (Show, Eq)

-- pos "[", ";"s, "]"

data TypeArg = TypeArg TypeId Kind SeparatorKind Pos

-- pos "," or ":" ("+" or "-" pos is moved to ExtClass)

deriving (Show, Eq)

data TypeArgs = TypeArgs [TypeArg] [Pos] deriving (Show, Eq)

-- pos ";"s

data GenVarDecl = GenVarDecl VarDecl

| GenTypeVarDecl TypeArg

deriving (Show, Eq)

-- ----------------------------------------------------------------------------

-- class

-- ----------------------------------------------------------------------------

data Variance = CoVar | ContraVar | InVar deriving (Show, Eq)

data Kind = PlainClass Class

| ExtClass Kind Variance Pos

-- pos "+" or "-"

| ProdClass [Kind] [Pos]

-- pos crosses

| KindAppl Kind Kind Pos

-- pos "->"

deriving (Show, Eq)

data Class = Downset Type -- not parsed directly

| Intersection { iclass :: [ClassId], classPos :: [Pos] }

-- pos "(", ","s, ")"

deriving (Show, Eq)

universe :: Class

universe = Intersection [] []

nullKind :: Kind

nullKind = PlainClass universe

-- ----------------------------------------------------------------------------

-- op names

-- ----------------------------------------------------------------------------

data OpId = OpId UninstOpId [TypeVarDecls] deriving (Show, Eq)

data Types = Types [Type] [Pos] deriving (Show, Eq) -- [TYPE, ..., TYPE]

data InstOpId = InstOpId UninstOpId [Types] deriving (Show, Eq)

-- ----------------------------------------------------------------------------

-- ids

-- ----------------------------------------------------------------------------

type TypeId = Id

type UninstOpId = Id

type Var = Id

type ClassId = Id -- TOKEN-ID (one token with compound list, like CASL sorts)