8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : $Header$

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : maeder@tzi.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : experimental

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaPortability : portable

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakovaabstract syntax during static analysis

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-}

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodule HasCASL.Le where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.As

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport HasCASL.AsUtils

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Common.Lib.Map as Map

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Common.Lib.Set as Set

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Lib.State

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Result

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Id

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.AS_Annotation(Named)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- * class info

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova-- | store the raw kind and all superclasses of a class identifier

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata ClassInfo = ClassInfo { rawKind :: RawKind

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , classKinds :: [Kind]

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova } deriving (Show, Eq)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovatype ClassMap = Map.Map ClassId ClassInfo

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- * type info

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | data type generatedness indicator

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | an analysed alternative with a list of (product) types

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata AltDefn = Construct (Maybe UninstOpId) [Type] Partiality [[Selector]]

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova -- only argument types

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova deriving (Show, Eq, Ord)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | an analysed component

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata Selector = Select (Maybe UninstOpId) Type Partiality -- only result type

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova deriving (Show, Eq, Ord)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- | a mapping of type (and disjoint class) identifiers

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovatype IdMap = Map.Map TypeId TypeId

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | for data types the morphism needs to be kept as well

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovadata DataEntry = DataEntry IdMap TypeId GenKind [TypeArg] RawKind [AltDefn]

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova deriving (Show, Eq, Ord)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- | possible definitions for type identifiers

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata TypeDefn = NoTypeDefn

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova | PreDatatype -- auxiliary entry for DatatypeDefn

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova | DatatypeDefn DataEntry

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova | AliasTypeDefn TypeScheme

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova deriving (Show, Eq)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | for type identifiers also store the raw kind, instances and supertypes

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata TypeInfo = TypeInfo { typeKind :: RawKind

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova , otherTypeKinds :: [Kind]

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova , superTypes :: Set.Set TypeId

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova , typeDefn :: TypeDefn

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova } deriving (Show, Eq)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovatype TypeMap = Map.Map TypeId TypeInfo

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova-- | the minimal information for a sort

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovastarTypeInfo :: TypeInfo

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovastarTypeInfo = TypeInfo rStar [universe] Set.empty NoTypeDefn

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova-- | recursively substitute type names within a type

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovarename :: (TypeId -> RawKind -> Int -> Type) -> Type -> Type

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovarename m t = case t of

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova TypeName i k n -> m i k n

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova TypeAppl t1 t2 -> TypeAppl (rename m t1) (rename m t2)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova ExpandedType t1 t2 -> ExpandedType (rename m t1) (rename m t2)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova TypeToken _ -> t

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova BracketType b l ps ->

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova BracketType b (map (rename m) l) ps

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova KindedType tk k ps ->

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova KindedType (rename m tk) k ps

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova MixfixType l -> MixfixType $ map (rename m) l

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova-- | rename the type according to identifier map (for comorphisms)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovamapType :: IdMap -> Type -> Type

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovamapType m ty = if Map.null m then ty else

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova rename ( \ i k n ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let t = TypeName i k n in

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova if n == 0 then

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case Map.lookup i m of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just j -> TypeName j k 0

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova _ -> t

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else t) ty

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-- * sentences

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | data types are also special sentences because of their properties

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata Sentence = Formula Term

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova | DatatypeSen [DataEntry]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova | ProgEqSen UninstOpId TypeScheme ProgEq

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova deriving (Show, Eq, Ord)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- * variables

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | type variable are kept separately

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata TypeVarDefn = TypeVarDefn Variance VarKind RawKind Int deriving Show

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovatype LocalTypeVars = Map.Map TypeId TypeVarDefn

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | the type of a local variable

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata VarDefn = VarDefn Type deriving Show

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- * assumptions

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | name and scheme of a constructor

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata ConstrInfo = ConstrInfo { constrId :: UninstOpId

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , constrType :: TypeScheme

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova } deriving (Show, Eq)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | possible definitions of functions

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata OpDefn = NoOpDefn OpBrand

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova | ConstructData TypeId -- target type

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova | SelectData [ConstrInfo] TypeId -- constructors of source type

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova | Definition OpBrand Term

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova deriving (Show, Eq)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | scheme, attributes and definition for function identifiers

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata OpInfo = OpInfo { opType :: TypeScheme

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , opAttrs :: [OpAttr]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , opDefn :: OpDefn

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova } deriving (Show, Eq)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | test for constructor

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaisConstructor :: OpInfo -> Bool

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaisConstructor o = case opDefn o of

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ConstructData _ -> True

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova _ -> False

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | a list of infos for overloaded functions

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovadata OpInfos = OpInfos { opInfos :: [OpInfo] } deriving (Show, Eq)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovatype Assumps = Map.Map UninstOpId OpInfos

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- * the local environment and final signature

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | the precedence map

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovatype PrecMap = (Map.Map Id Int, Int, Int)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-- | the signature is established by the classes, types and assumptions

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovadata Env = Env { classMap :: ClassMap

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , typeMap :: TypeMap

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , localTypeVars :: LocalTypeVars

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , assumps :: Assumps

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , localVars :: Map.Map Id VarDefn

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , sentences :: [Named Sentence]

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , envDiags :: [Diagnosis]

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova , preIds :: (PrecMap, Set.Set Id)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , counter :: Int

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova } deriving Show

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-- | the empty environment (fresh variables start with 1)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovainitialEnv :: Env

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovainitialEnv = Env Map.empty Map.empty Map.empty Map.empty Map.empty [] []

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ((Map.empty, 0, 0), Set.empty) 1

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-- * accessing the environment

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova-- | add diagnostic messages

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaaddDiags :: [Diagnosis] -> State Env ()

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovaaddDiags ds =

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova do e <- get

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova put $ e {envDiags = reverse ds ++ envDiags e}

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | add sentences

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaappendSentences :: [Named Sentence] -> State Env ()

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaappendSentences fs =

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova do e <- get

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova put $ e {sentences = reverse fs ++ sentences e}

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-- | store a class map

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaputClassMap :: ClassMap -> State Env ()

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaputClassMap ce = do

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova e <- get

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova put e { classMap = ce }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | store local assumptions

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputLocalVars :: Map.Map Id VarDefn -> State Env ()

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputLocalVars vs = do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova e <- get

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova put e { localVars = vs }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | converting a result to a state computation

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovafromResult :: (Env -> Result a) -> State Env (Maybe a)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafromResult f = do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova e <- get

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova let Result ds mr = f e

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova addDiags ds

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return mr

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | store local type variables

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputLocalTypeVars :: LocalTypeVars -> State Env ()

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputLocalTypeVars tvs = do

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova e <- get

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova put e { localTypeVars = tvs }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | store a complete type map

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputTypeMap :: TypeMap -> State Env ()

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputTypeMap tm = do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova e <- get

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova put e { typeMap = tm }

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | store assumptions

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputAssumps :: Assumps -> State Env ()

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaputAssumps ops = do

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova e <- get

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova put e { assumps = ops }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | get the variable

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetVar :: VarDecl -> Id

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovagetVar(VarDecl v _ _ _) = v

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova-- | check uniqueness of variables

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovacheckUniqueVars :: [VarDecl] -> State Env ()

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovacheckUniqueVars = addDiags . checkUniqueness . map getVar

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova-- * morphisms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina Sojakovatype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova-- | keep types and class disjoint and use a single identifier map for both

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovadata Morphism = Morphism { msource :: Env

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , mtarget :: Env

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova , typeIdMap :: IdMap

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova , funMap :: FunMap }

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova deriving Show

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- | construct morphism for subsignatures

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovamkMorphism :: Env -> Env -> Morphism

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovamkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- * symbol stuff

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- | the type or kind of an identifier

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata SymbolType a = OpAsItemType TypeScheme

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova | TypeAsItemType (AnyKind a)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova | ClassAsItemType (AnyKind a)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova deriving (Show, Eq, Ord)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- symbols (may) need the env to look up type aliases

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakovadata Symbol = Symbol {symName :: Id, symType :: SymbolType (), symEnv :: Env}

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova deriving Show

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq Symbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova s1 == s2 = (symName s1, symType s1) == (symName s2, symType s2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Ord Symbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova s1 <= s2 = (symName s1, symType s1) <= (symName s2, symType s2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovatype SymbolMap = Map.Map Symbol Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovatype SymbolSet = Set.Set Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToTypeSymbol :: Env -> Id -> RawKind -> Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToTypeSymbol e idt k = Symbol idt (TypeAsItemType k) e

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToClassSymbol :: Env -> Id -> RawKind -> Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToClassSymbol e idt k = Symbol idt (ClassAsItemType k) e

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaidToOpSymbol :: Env -> Id -> TypeScheme -> Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToOpSymbol e idt typ = Symbol idt (OpAsItemType typ) e

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- note that the type of a qualified raw symbol is not analysed!

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata RawSymbol = AnID Id | AKindedId SymbKind Id

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova | AQualId Id (SymbolType ClassId)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova | ASymbol Symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova deriving (Show, Eq, Ord)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovatype RawSymbolMap = Map.Map RawSymbol RawSymbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToRaw :: Id -> RawSymbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaidToRaw x = AnID x

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarawSymName :: RawSymbol -> Id

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarawSymName (AnID i) = i

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarawSymName (AKindedId _ i) = i

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarawSymName (AQualId i _) = i

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovarawSymName (ASymbol s) = symName s

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbTypeToKind :: SymbolType a -> SymbKind

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbTypeToKind (OpAsItemType _) = SK_op

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbTypeToKind (TypeAsItemType _) = SK_type

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbTypeToKind (ClassAsItemType _) = SK_class

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbolToRaw :: Symbol -> RawSymbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbolToRaw sym = ASymbol sym

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbKindToRaw :: SymbKind -> Id -> RawSymbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbKindToRaw Implicit = AnID

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasymbKindToRaw sk = AKindedId $ case sk of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova SK_pred -> SK_op

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova SK_fun -> SK_op

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova SK_sort -> SK_type

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova _ -> sk

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova