As.hs revision 4c4a6faea90bdb95062434ca9b9e85f5c3b2d012
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
81d182b21020b815887e9057959228546cf61b6bChristian Maeder{- HetCATS/HasCASL/As.hs
81d182b21020b815887e9057959228546cf61b6bChristian Maeder $Id$
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder Authors: Christian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder Year: 2002
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder abstract syntax for HasCASL
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder more liberal than HetCATS/HasCASL/Concrete-Syntax.txt
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder annotations almost as in HetCATS/CASL/AS_Basic_CASL.hs v 1.8
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder-}
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maedermodule HasCASL.As where
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport Common.Id
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.AS_Annotation
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Lib.Set
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata BasicSpec = BasicSpec [Annoted BasicItem]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder deriving (Show, Eq)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata BasicItem = SigItems SigItems
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder | ProgItems [Annoted ProgEq] [Pos]
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder -- pos "program", dots
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder | ClassItems Instance [Annoted ClassItem] [Pos]
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder -- pos "class", ";"s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | GenVarItems [GenVarDecl] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "var", ";"s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | FreeDatatype [Annoted DatatypeDecl] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "free", "type", ";"s
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder | GenItems [Annoted SigItems] [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos "generated" "{", ";"s, "}"
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- or "generated" "type" ";"s
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder | AxiomItems [GenVarDecl] [Annoted Formula] [Pos]
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- pos "forall" (if GenVarDecl not empty), dots
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder deriving (Show, Eq)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederdata SigItems = TypeItems Instance [Annoted TypeItem] [Pos] -- including sort
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -- pos "type", ";"s
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder | OpItems [Annoted OpItem] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "op", ";"s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | PredItems [Annoted PredItem] [Pos]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -- pos "pred", ";"s
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder deriving (Show, Eq)
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder-- "instance" indicator
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Instance = Instance | Plain deriving (Show, Eq)
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maederdata ClassItem = ClassItem ClassDecl [Annoted BasicItem] [Pos]
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -- pos "{", ";"s "}"
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata ClassDecl = ClassDecl [ClassId] Kind [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos ","s
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder | SubclassDecl [ClassId] Kind Class [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos ","s, "<"
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder | ClassDefn ClassId Kind Class [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos "="
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder | DownsetDefn ClassId Token Type [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos " =" "{", dot, "<", typeVar, "}"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata TypeItem = TypeDecl [TypePattern] Kind [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos ","s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | SubtypeDecl [TypePattern] Type [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos ","s, "<"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | IsoDecl [TypePattern] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "="s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | SubtypeDefn TypePattern Var Type (Annoted Formula) [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "=", "{", ":", dot, "}"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | AliasType TypePattern (Maybe Kind) TypeScheme [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos ":="
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | Datatype DatatypeDecl
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata TypePattern = TypePattern TypeId [TypeArg] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "("s, ")"s
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | TypePatternToken Token
998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian Maeder | MixfixTypePattern [TypePattern]
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder | BracketTypePattern BracketKind [TypePattern] [Pos]
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder -- pos brackets (no parenthesis)
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder | TypePatternArg TypeArg [Pos]
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder -- pos "(", ")"
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Type = TypeName TypeId Kind Int -- analysed (Int for internal use)
bbcc77a6eb9554dd3092cabafae1e5ca74a054eeChristian Maeder | TypeAppl Type Type
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | TypeToken Token
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | BracketType BracketKind [Type] [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos "," (between type arguments)
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | KindedType Type Kind [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos ":"
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | MixfixType [Type]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | LazyType Type [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos "?"
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | ProductType [Type] [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos crosses
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | FunType Type Arrow Type [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos arrow
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Arrow = FunArr| PFunArr | ContFunArr | PContFunArr
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder deriving (Show, Eq, Ord)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederdata Pred = IsIn ClassId [Type]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Qual t = [Pred] :=> t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder-- no curried notation for bound variables
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederdata TypeScheme = TypeScheme [TypeArg] (Qual Type) [Pos]
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -- pos "forall", ";"s, dot (singleton list)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -- pos "\" "("s, ")"s, dot for type aliases
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder deriving (Show, Eq)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedersimpleTypeScheme :: Type -> TypeScheme
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedersimpleTypeScheme t = TypeScheme [] ([] :=> t) []
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederdata Partiality = Partial | Total deriving (Show, Eq)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederdata OpItem = OpDecl [OpId] TypeScheme [OpAttr] [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos ","s, ":", ","s, "assoc", "comm", "idem", "unit"
2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder | OpDefn OpId [Pattern] TypeScheme Partiality Term [Pos]
2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder -- pos "("s, ")"s, ":" or ":?", "="
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder deriving (Show, Eq)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederdata PredItem = PredDecl [OpId] TypeScheme [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos ","s, ":", ","s
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder | PredDefn OpId [Pattern] Formula [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos "("s, ")"s, "<=>"
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder deriving (Show, Eq)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederdata BinOpAttr = Assoc | Comm | Idem deriving (Show, Eq, Ord)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederdata OpAttr = BinOpAttr BinOpAttr [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder | UnitOpAttr Term [Pos] deriving (Show, Eq)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederdata DatatypeDecl = DatatypeDecl
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder TypePattern
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder Kind
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder [Annoted Alternative]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (Maybe Class)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder [Pos]
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder -- pos "::=", "|"s, "deriving"
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder deriving (Show, Eq)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederdata Alternative = Constructor UninstOpId [Components] Partiality [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos: "?"
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder | Subtype [Type] [Pos]
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder -- pos: "type", ","s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
61091743da1a9ed6dfd5e077fdcc972553358962Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Components = Selector UninstOpId Partiality Type SeparatorKind Pos
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder -- pos ",", ":" or ":?"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | NoSelector Type
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder | NestedComponents [Components] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos : "(", ";"s, ")"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Quantifier = Universal | Existential | Unique
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maederdata TypeQual = OfType | AsType | InType deriving (Show, Eq)
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maederdata BracketKind = Parens | Squares | Braces deriving (Show, Eq)
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maederdata LogOp = NotOp | AndOp | OrOp | ImplOp | EquivOp deriving (Show, Eq)
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maederdata EqOp = EqualOp | ExEqualOp deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- proper formulae only exist after static analysis
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederdata Formula = TermFormula Term
405b95208385572f491e1e0207d8d14e31022fa6Christian Maeder | ConnectFormula LogOp [Formula] [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos not, "/\", "\/", impl, "<=>"
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder | EqFormula EqOp Term Term [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "=", "=e="
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | DefFormula Term [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "def"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | QuantifiedFormula Quantifier [VarDecl] Formula [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos quantifier, ";"s, dot
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | PolyFormula [TypeArg] Formula [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "forall", ";"s, dot
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Show, Eq)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- parse quantified formulae as terms first
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- eases also parsing of formulae in parenthesis
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maederdata Term = CondTerm Term Formula Term [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos "when", "else" (or if-then-else)
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | QualVar Var Type [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos "(", "var", ":", ")"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | QualOp InstOpId TypeScheme [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos "(", "op", ":", ")"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | ApplTerm Term Term [Pos] -- analysed
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos?
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder | TupleTerm [Term] [Pos]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -- pos "(", ","s, ")"
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder | TypedTerm Term TypeQual Type [Pos]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos ":", "as" or "in"
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | QuantifiedTerm Quantifier [GenVarDecl] Term [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- pos quantifier, ";"s, dot
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- only "forall" may have a TypeVarDecl
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | LambdaTerm [Pattern] Partiality Term [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- pos "\", dot (plus "!")
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | CaseTerm Term [ProgEq] [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- pos "case", "of", "|"s
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | LetTerm [ProgEq] Term [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- pos "where", ";"s
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | TermToken Token
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | MixfixTerm [Term]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | BracketTerm BracketKind [Term] [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- pos brackets, ","s
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder deriving (Show, Eq)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederdata Pattern = PatternVars [VarDecl] [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- pos ";"s
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder | PatternConstr InstOpId TypeScheme [Pattern] [Pos]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- 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 TypeArg = TypeArg TypeId Kind SeparatorKind [Pos]
-- pos "," or ":" ("+" or "-" pos is moved to ExtClass)
deriving (Show, Eq)
data GenVarDecl = GenVarDecl VarDecl
| GenTypeVarDecl TypeArg
deriving (Show, Eq)
-- ----------------------------------------------------------------------------
-- class
-- ----------------------------------------------------------------------------
data Variance = CoVar | ContraVar | InVar deriving (Show, Eq, Ord)
data Kind = ExtClass Class Variance [Pos]
-- pos "+" or "-"
| KindAppl Kind Kind [Pos]
-- pos "->"
deriving (Show)
data Class = Downset Type -- not parsed directly
| Intersection { iclass :: Set ClassId, classPos :: [Pos] }
-- pos "(", ","s, ")"
deriving (Show)
universe :: Class
universe = Intersection empty []
star :: Kind
star = ExtClass universe InVar []
-- ----------------------------------------------------------------------------
-- op names
-- ----------------------------------------------------------------------------
data OpId = OpId UninstOpId [TypeArg] [Pos] deriving (Show, Eq)
-- pos "[", ";"s, "]"
data InstOpId = InstOpId UninstOpId [Type] [Pos] 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)
-- ----------------------------------------------------------------------------
-- equality instances while ignoring positions
-- ----------------------------------------------------------------------------
instance Eq Class where
Intersection i1 _ == Intersection i2 _ = i1 == i2
Downset t1 == Downset t2 = t1 == t2
_ == _ = False
instance Eq Kind where
ExtClass c1 v1 _ == ExtClass c2 v2 _ = (c1, v1) == (c2, v2)
KindAppl p1 c1 _ == KindAppl p2 c2 _ = (p1, c1) == (p2, c2)
_ == _ = False
instance Eq Type where
TypeName i1 k1 v1 == TypeName i2 k2 v2 = (i1, k1, v1) == (i2, k2, v2)
TypeAppl f1 a1 == TypeAppl f2 a2 = (f1, a1) == (f2, a2)
TypeToken t1 == TypeToken t2 = t1 == t2
BracketType b1 l1 _ == BracketType b2 l2 _ = (b1, l1) == (b2, l2)
KindedType t1 k1 _ == KindedType t2 k2 _ = (t1, k1) == (t2, k2)
MixfixType l1 == MixfixType l2 = l1 == l2
LazyType t1 _ == LazyType t2 _ = t1 == t2
ProductType l1 _ == ProductType l2 _ = l1 == l2
FunType f1 a1 g1 _ == FunType f2 a2 g2 _ = (f1, a1, g1) == (f2, a2, g2)
_ == _ = False