1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
5ba323da9f037264b4a356085e844889aedeac23Christian MaederDescription : the abstract syntax for analysis and final signature instance
c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederabstract syntax during static analysis
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maederimport qualified Common.Lib.State as State
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified Data.Map as Map
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederimport qualified Data.Set as Set
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * class info
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | store the raw kind and all superclasses of a class identifier
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata ClassInfo = ClassInfo
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { rawKind :: RawKind
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , classKinds :: Set.Set Kind
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | mapping class identifiers to their definition
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maedertype ClassMap = Map.Map Id ClassInfo
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * type info
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | data type generatedness indicator
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord, Typeable, Data)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | an analysed alternative with a list of (product) types
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata AltDefn =
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Construct (Maybe Id) [Type] Partiality [[Selector]]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -- only argument types
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | an analysed component
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata Selector =
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Select (Maybe Id) Type Partiality deriving (Show, Eq, Ord, Typeable, Data)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -- only result type
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | a mapping of type (and disjoint class) identifiers
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maedertype IdMap = Map.Map Id Id
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder{- | data entries are produced from possibly mutual recursive data types. The
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maedertop-level identifiers of these types are never renamed but there renaming is
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederstored in the identifier map. This identifier map must never be empty (even
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederwithout renamings) because (the domain of) this map is used to store the
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maederother (recursively dependent) top-level identifiers. -}
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata DataEntry =
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder DataEntry IdMap Id GenKind [TypeArg] RawKind (Set.Set AltDefn)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | possible definitions for type identifiers
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata TypeDefn =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | PreDatatype -- auxiliary entry for DatatypeDefn
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | DatatypeDefn DataEntry
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder | AliasTypeDefn Type
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | for type identifiers also store the raw kind, instances and supertypes
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata TypeInfo = TypeInfo
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { typeKind :: RawKind
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder , otherTypeKinds :: Set.Set Kind
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , superTypes :: Set.Set Id -- only declared or direct supertypes?
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , typeDefn :: TypeDefn
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Typeable, Data)
5ba323da9f037264b4a356085e844889aedeac23Christian Maederinstance Eq TypeInfo where
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder a == b = compare a b == EQ
16e124196c6b204769042028c74f533509c9b5d3Christian Maederinstance Ord TypeInfo where
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder compare t1 t2 = compare
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (typeKind t1, otherTypeKinds t1, superTypes t1)
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (typeKind t2, otherTypeKinds t2, superTypes t2)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | mapping type identifiers to their definition
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maedertype TypeMap = Map.Map Id TypeInfo
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | the minimal information for a sort
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederstarTypeInfo :: TypeInfo
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederstarTypeInfo = TypeInfo rStar (Set.singleton universe) Set.empty NoTypeDefn
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | rename the type according to identifier map (for comorphisms)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedermapType :: IdMap -> Type -> Type
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian MaedermapType m = if Map.null m then id else
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder foldType mapTypeRec
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder { foldTypeName = \ t i k n -> if n /= 0 then t else
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder Just j -> TypeName j k 0
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder Nothing -> t }
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * sentences
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | data types are also special sentences because of their properties
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata Sentence =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | DatatypeSen [DataEntry]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder | ProgEqSen Id TypeScheme ProgEq
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maederinstance GetRange Sentence where
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder getRange s = case s of
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder Formula t -> getRange t
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder _ -> nullRange
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * variables
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | type variable are kept separately
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata TypeVarDefn = TypeVarDefn Variance VarKind RawKind Int
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable, Data)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | mapping type variables to their definition
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maedertype LocalTypeVars = Map.Map Id TypeVarDefn
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | the type of a local variable
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata VarDefn = VarDefn Type deriving (Show, Typeable, Data)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * assumptions
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | name and scheme of a constructor
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata ConstrInfo = ConstrInfo
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder { constrId :: Id
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , constrType :: TypeScheme
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | possible definitions of functions
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder NoOpDefn OpBrand
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder | ConstructData Id -- ^ target type
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder | SelectData (Set.Set ConstrInfo) Id -- ^ constructors of source type
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Definition OpBrand Term
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | scheme, attributes and definition for function identifiers
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata OpInfo = OpInfo
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { opType :: TypeScheme
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder , opAttrs :: Set.Set OpAttr
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , opDefn :: OpDefn
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Typeable, Data)
ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Eq OpInfo where
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder o1 == o2 = compare o1 o2 == EQ
ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Ord OpInfo where
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder compare = comparing opType
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | test for constructor
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisConstructor :: OpInfo -> Bool
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisConstructor o = case opDefn o of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ConstructData _ -> True
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | mapping operation identifiers to their definition
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- * the local environment and final signature
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | the signature is established by the classes, types and assumptions
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata Env = Env
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { classMap :: ClassMap
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , typeMap :: TypeMap
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , localTypeVars :: LocalTypeVars
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , assumps :: Assumps
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder , binders :: Map.Map Id Id -- binder with associated op-id
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , localVars :: Map.Map Id VarDefn
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , sentences :: [Named Sentence]
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder , declSymbs :: Set.Set Symbol
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , envDiags :: [Diagnosis]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , preIds :: (PrecMap, Set.Set Id)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , globAnnos :: GlobalAnnos
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , counter :: Int
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Typeable, Data)
ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Eq Env where
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder a == b = compare a b == EQ
16e124196c6b204769042028c74f533509c9b5d3Christian Maederinstance Ord Env where
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder compare e1 e2 = compare
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (classMap e1, typeMap e1, assumps e1)
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (classMap e2, typeMap e2, assumps e2)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | the empty environment (fresh variables start with 1)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederinitialEnv :: Env
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederinitialEnv = Env
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , localTypeVars = Map.empty
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , sentences = []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , envDiags = []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , preIds = (emptyPrecMap, Set.empty)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , globAnnos = emptyGlobalAnnos
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , counter = 1 }
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder{- utils for singleton sets that could also be part of "Data.Set". These
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maederfunctions rely on 'Data.Set.size' being computable in constant time and
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maederwould need to be rewritten for set implementations with a size
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maederfunction that is only linear. -}
ad187062b0009820118c1b773a232e29b879a2faChristian Maederdata Constrain = Kinding Type Kind
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder | Subtyping Type Type
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- * accessing the environment
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | add diagnostic messages
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederaddDiags :: [Diagnosis] -> State.State Env ()
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederaddDiags ds = do
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder State.put $ e {envDiags = reverse ds ++ envDiags e}
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | add sentences
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederappendSentences :: [Named Sentence] -> State.State Env ()
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederappendSentences fs = do
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder State.put $ e {sentences = reverse fs ++ sentences e}
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | store a class map
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederputClassMap :: ClassMap -> State.State Env ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederputClassMap ce = do
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder State.put e { classMap = ce }
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | store local assumptions
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederputLocalVars :: Map.Map Id VarDefn -> State.State Env ()
de2f13b8310de00ca228385b1530660e036054c2Christian MaederputLocalVars vs = do
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder State.put e { localVars = vs }
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | converting a result to a state computation
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederfromResult :: (Env -> Result a) -> State.State Env (Maybe a)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederfromResult f = do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let Result ds mr = f e
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder-- | add the symbol to the state
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaederaddSymbol :: Symbol -> State.State Env ()
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaederaddSymbol sy = do
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder State.put e { declSymbs = Set.insert sy $ declSymbs e }
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | store local type variables
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederputLocalTypeVars :: LocalTypeVars -> State.State Env ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederputLocalTypeVars tvs = do
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder State.put e { localTypeVars = tvs }
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | store a complete type map
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederputTypeMap :: TypeMap -> State.State Env ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederputTypeMap tm = do
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder State.put e { typeMap = tm }
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | store assumptions
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederputAssumps :: Assumps -> State.State Env ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederputAssumps ops = do
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder State.put e { assumps = ops }
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- | store assumptions
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederputBinders :: Map.Map Id Id -> State.State Env ()
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederputBinders bs = do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder State.put e { binders = bs }
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | get the variable
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedergetVar :: VarDecl -> Id
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaedergetVar (VarDecl v _ _ _) = v
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | check uniqueness of variables
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedercheckUniqueVars :: [VarDecl] -> State.State Env ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedercheckUniqueVars = addDiags . checkUniqueness . map getVar
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- * morphisms
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- mapping qualified operation identifiers (aka renamings)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedertype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- | keep types and class disjoint and use a single identifier map for both
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata Morphism = Morphism
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { msource :: Env
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , mtarget :: Env
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , typeIdMap :: IdMap
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu , classIdMap :: IdMap
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , funMap :: FunMap
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | construct morphism for subsignatures
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermkMorphism :: Env -> Env -> Morphism
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedermkMorphism e1 e2 = Morphism
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { msource = e1
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , mtarget = e2
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu , classIdMap = Map.empty
2faad0c99d17a6ef53a464864caccbb20cf48409Christian MaederisInclMor :: Morphism -> Bool
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder Map.null (typeIdMap m) && Map.null (classIdMap m) && Map.null (funMap m)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * symbol stuff
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | the type or kind of an identifier
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maederdata SymbolType =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OpAsItemType TypeScheme
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder | TypeAsItemType RawKind
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder | ClassAsItemType RawKind
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder | SuperClassSymbol Kind
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder | TypeKindInstance Kind
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder | SuperTypeSymbol Id
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder | TypeAliasSymbol Type
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder | PredAsItemType TypeScheme
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder-- | symbols with their type
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder Symbol { symName :: Id, symType :: SymbolType }
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable, Data)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Eq Symbol where
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder s1 == s2 = compare s1 s2 == EQ
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Ord Symbol where
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder compare s1 s2 = compare (symName s1, symType s1) (symName s2, symType s2)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | mapping symbols to symbols
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maedertype SymbolMap = Map.Map Symbol Symbol
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | a set of symbols
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maedertype SymbolSet = Set.Set Symbol
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | create a type symbol
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaederidToTypeSymbol :: Id -> RawKind -> Symbol
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaederidToTypeSymbol idt k = Symbol idt (TypeAsItemType $ nonVarRawKind k)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | create a class symbol
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaederidToClassSymbol :: Id -> RawKind -> Symbol
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaederidToClassSymbol idt k = Symbol idt (ClassAsItemType $ nonVarRawKind k)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | create an operation symbol
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaederidToOpSymbol :: Id -> TypeScheme -> Symbol
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder{- | raw symbols where the type of a qualified raw symbol can be a type scheme
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maederand also be a kind if the symbol kind is unknown. -}
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata RawSymbol =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | AKindedId SymbKind Id
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | ASymbol Symbol
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | mapping raw symbols to raw symbols
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedertype RawSymbolMap = Map.Map RawSymbol RawSymbol
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | create a raw symbol from an identifier
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederidToRaw :: Id -> RawSymbol
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederidToRaw = AnID
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | extract the top identifer from a raw symbol
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederrawSymName :: RawSymbol -> Id
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederrawSymName r = case r of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder AKindedId _ i -> i
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ASymbol s -> symName s
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | convert a symbol type to a symbol kind
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaedersymbTypeToKind :: SymbolType -> SymbKind
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedersymbTypeToKind s = case s of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder OpAsItemType _ -> SyKop
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder TypeAsItemType _ -> SyKtype
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder SuperTypeSymbol _ -> SyKtype
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder TypeKindInstance _ -> SyKtype
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder TypeAliasSymbol _ -> SyKtype
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder ClassAsItemType _ -> SyKclass
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder SuperClassSymbol _ -> SyKclass
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder PredAsItemType _ -> SyKpred
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | wrap a symbol as raw symbol (is 'ASymbol')
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersymbolToRaw :: Symbol -> RawSymbol
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedersymbolToRaw = ASymbol
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | create a raw symbol from a symbol kind and an identifier
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersymbKindToRaw :: SymbKind -> Id -> RawSymbol
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedersymbKindToRaw sk = case sk of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Implicit -> AnID
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder _ -> AKindedId $ case sk of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder SyKpred -> SyKop
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder SyKfun -> SyKop
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder SyKsort -> SyKtype
b38e57295a9ba3a4de9719171dcff2d9f3b554cdChristian MaedergetCompoundLists :: Env -> Set.Set [Id]
b38e57295a9ba3a4de9719171dcff2d9f3b554cdChristian MaedergetCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union
b38e57295a9ba3a4de9719171dcff2d9f3b554cdChristian Maeder (Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e
b38e57295a9ba3a4de9719171dcff2d9f3b554cdChristian Maeder where getCompound (Id _ cs _) = cs