22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder{- |

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederModule : $Header$

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederDescription : the abstract syntax for analysis and final signature instance

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederLicense : GPLv2 or higher

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroederMaintainer : Christian.Maeder@dfki.de

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederStability : experimental

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederPortability : portable

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederabstract syntax during static analysis

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-}

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroedermodule HasCASL.Le where

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport HasCASL.As

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport HasCASL.FoldType

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederimport HasCASL.AsUtils

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport qualified Data.Map as Map

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Data.Set as Set

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Common.Lib.State as State

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport Common.Result

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Id

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.AS_Annotation (Named)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.GlobalAnnotations

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport Common.Prec

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder-- * class info

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | store the raw kind and all superclasses of a class identifier

61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroederdata ClassInfo = ClassInfo

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder { rawKind :: RawKind

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , classKinds :: Set.Set Kind

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder } deriving (Show, Eq, Ord)

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | mapping class identifiers to their definition

61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroedertype ClassMap = Map.Map Id ClassInfo

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- * type info

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | data type generatedness indicator

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | an analysed alternative with a list of (product) types

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederdata AltDefn =

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder Construct (Maybe Id) [Type] Partiality [[Selector]]

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder -- only argument types

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder deriving (Show, Eq, Ord)

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | an analysed component

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Selector =

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder Select (Maybe Id) Type Partiality deriving (Show, Eq, Ord)

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder -- only result type

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroeder-- | a mapping of type (and disjoint class) identifiers

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroedertype IdMap = Map.Map Id Id

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder{- | data entries are produced from possibly mutual recursive data types. The

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertop-level identifiers of these types are never renamed but there renaming is

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederstored in the identifier map. This identifier map must never be empty (even

42b0311155dd27a5f8ba917b280c9f7989b73ec9Jonathan von Schroederwithout renamings) because (the domain of) this map is used to store the

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederother (recursively dependent) top-level identifiers. -}

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroederdata DataEntry =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder DataEntry IdMap Id GenKind [TypeArg] RawKind (Set.Set AltDefn)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Show, Eq, Ord)

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | possible definitions for type identifiers

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroederdata TypeDefn =

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroeder NoTypeDefn

10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder | PreDatatype -- auxiliary entry for DatatypeDefn

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder | DatatypeDefn DataEntry

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | AliasTypeDefn Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Show, Eq)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | for type identifiers also store the raw kind, instances and supertypes

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata TypeInfo = TypeInfo

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { typeKind :: RawKind

6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder , otherTypeKinds :: Set.Set Kind

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder , superTypes :: Set.Set Id -- only declared or direct supertypes?

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , typeDefn :: TypeDefn

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder } deriving Show

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Eq TypeInfo where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a == b = compare a b == EQ

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Ord TypeInfo where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder compare t1 t2 = compare

6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (typeKind t1, otherTypeKinds t1, superTypes t1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (typeKind t2, otherTypeKinds t2, superTypes t2)

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder-- | mapping type identifiers to their definition

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype TypeMap = Map.Map Id TypeInfo

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | the minimal information for a sort

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederstarTypeInfo :: TypeInfo

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederstarTypeInfo = TypeInfo rStar (Set.singleton universe) Set.empty NoTypeDefn

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder-- | rename the type according to identifier map (for comorphisms)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapType :: IdMap -> Type -> Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapType m = if Map.null m then id else

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder foldType mapTypeRec

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder { foldTypeName = \ t i k n -> if n /= 0 then t else

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder case Map.lookup i m of

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder Just j -> TypeName j k 0

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> t }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder-- * sentences

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | data types are also special sentences because of their properties

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroederdata Sentence =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Formula Term

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder | DatatypeSen [DataEntry]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | ProgEqSen Id TypeScheme ProgEq

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Show, Eq, Ord)

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance GetRange Sentence where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getRange s = case s of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Formula t -> getRange t

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder _ -> nullRange

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder-- * variables

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder-- | type variable are kept separately

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroederdata TypeVarDefn = TypeVarDefn Variance VarKind RawKind Int deriving Show

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | mapping type variables to their definition

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype LocalTypeVars = Map.Map Id TypeVarDefn

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder

d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder-- | the type of a local variable

d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroederdata VarDefn = VarDefn Type deriving Show

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder-- * assumptions

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | name and scheme of a constructor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata ConstrInfo = ConstrInfo

d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder { constrId :: Id

d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder , constrType :: TypeScheme

d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder } deriving (Show, Eq, Ord)

e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder

e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder-- | possible definitions of functions

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata OpDefn =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder NoOpDefn OpBrand

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | ConstructData Id -- ^ target type

10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder | SelectData (Set.Set ConstrInfo) Id -- ^ constructors of source type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | Definition OpBrand Term

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Show, Eq)

10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | scheme, attributes and definition for function identifiers

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata OpInfo = OpInfo

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder { opType :: TypeScheme

61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder , opAttrs :: Set.Set OpAttr

4cd542a7f4e378ab5a36b49da804b258442b13f9Jonathan von Schroeder , opDefn :: OpDefn

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder } deriving Show

4cd542a7f4e378ab5a36b49da804b258442b13f9Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Eq OpInfo where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder o1 == o2 = compare o1 o2 == EQ

10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Ord OpInfo where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder compare o1 o2 = compare (opType o1) $ opType o2

4cd542a7f4e378ab5a36b49da804b258442b13f9Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | test for constructor

4cd542a7f4e378ab5a36b49da804b258442b13f9Jonathan von SchroederisConstructor :: OpInfo -> Bool

61d26ef772466529400bc460e7c69f67c1173b56Jonathan von SchroederisConstructor o = case opDefn o of

6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder ConstructData _ -> True

6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder _ -> False

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | mapping operation identifiers to their definition

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype Assumps = Map.Map Id (Set.Set OpInfo)

6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder

6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder-- * the local environment and final signature

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder-- | the signature is established by the classes, types and assumptions

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroederdata Env = Env

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder { classMap :: ClassMap

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , typeMap :: TypeMap

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , localTypeVars :: LocalTypeVars

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , assumps :: Assumps

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , binders :: Map.Map Id Id -- binder with associated op-id

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , localVars :: Map.Map Id VarDefn

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , sentences :: [Named Sentence]

383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder , declSymbs :: Set.Set Symbol

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder , envDiags :: [Diagnosis]

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder , preIds :: (PrecMap, Set.Set Id)

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder , globAnnos :: GlobalAnnos

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , counter :: Int

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder } deriving Show

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Eq Env where

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroeder a == b = compare a b == EQ

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroederinstance Ord Env where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder compare e1 e2 = compare

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (classMap e1, typeMap e1, assumps e1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (classMap e2, typeMap e2, assumps e2)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder-- | the empty environment (fresh variables start with 1)

f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von SchroederinitialEnv :: Env

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinitialEnv = Env

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder { classMap = Map.empty

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder , typeMap = Map.empty

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder , localTypeVars = Map.empty

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder , assumps = Map.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , binders = Map.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , localVars = Map.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , sentences = []

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , declSymbs = Set.empty

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder , envDiags = []

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroeder , preIds = (emptyPrecMap, Set.empty)

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder , globAnnos = emptyGlobalAnnos

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , counter = 1 }

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- utils for singleton sets that could also be part of "Data.Set". These

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroederfunctions rely on 'Data.Set.size' being computable in constant time and

80fa8cedf41af85cd602945b6a267242f44a7b81Jonathan von Schroederwould need to be rewritten for set implementations with a size

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederfunction that is only linear. -}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederdata Constrain = Kinding Type Kind

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder | Subtyping Type Type

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder deriving (Eq, Ord, Show)

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- * accessing the environment

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | add diagnostic messages

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddDiags :: [Diagnosis] -> State.State Env ()

5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederaddDiags ds = do

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder e <- State.get

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder State.put $ e {envDiags = reverse ds ++ envDiags e}

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | add sentences

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederappendSentences :: [Named Sentence] -> State.State Env ()

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von SchroederappendSentences fs = do

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder e <- State.get

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder State.put $ e {sentences = reverse fs ++ sentences e}

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder

ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | store a class map

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederputClassMap :: ClassMap -> State.State Env ()

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederputClassMap ce = do

59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder e <- State.get

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder State.put e { classMap = ce }

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder-- | store local assumptions

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederputLocalVars :: Map.Map Id VarDefn -> State.State Env ()

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederputLocalVars vs = do

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder e <- State.get

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder State.put e { localVars = vs }

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder-- | converting a result to a state computation

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfromResult :: (Env -> Result a) -> State.State Env (Maybe a)

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederfromResult f = do

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder e <- State.get

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let Result ds mr = f e

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder addDiags ds

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder return mr

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder-- | add the symbol to the state

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddSymbol :: Symbol -> State.State Env ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddSymbol sy = do

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder e <- State.get

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder State.put e { declSymbs = Set.insert sy $ declSymbs e }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | store local type variables

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederputLocalTypeVars :: LocalTypeVars -> State.State Env ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederputLocalTypeVars tvs = do

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder e <- State.get

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder State.put e { localTypeVars = tvs }

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder-- | store a complete type map

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederputTypeMap :: TypeMap -> State.State Env ()

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederputTypeMap tm = do

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder e <- State.get

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder State.put e { typeMap = tm }

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder-- | store assumptions

617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederputAssumps :: Assumps -> State.State Env ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederputAssumps ops = do

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder e <- State.get

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder State.put e { assumps = ops }

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder-- | store assumptions

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von SchroederputBinders :: Map.Map Id Id -> State.State Env ()

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von SchroederputBinders bs = do

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder e <- State.get

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder State.put e { binders = bs }

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

952051448ecc60de5f22f778ee60c16c781ab114Jonathan von Schroeder-- | get the variable

952051448ecc60de5f22f778ee60c16c781ab114Jonathan von SchroedergetVar :: VarDecl -> Id

952051448ecc60de5f22f778ee60c16c781ab114Jonathan von SchroedergetVar(VarDecl v _ _ _) = v

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder-- | check uniqueness of variables

952051448ecc60de5f22f778ee60c16c781ab114Jonathan von SchroedercheckUniqueVars :: [VarDecl] -> State.State Env ()

d0e186c57fb178eed89f4f0b6494f391ec7424d8Jonathan von SchroedercheckUniqueVars = addDiags . checkUniqueness . map getVar

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder

d0e186c57fb178eed89f4f0b6494f391ec7424d8Jonathan von Schroeder-- * morphisms

d0e186c57fb178eed89f4f0b6494f391ec7424d8Jonathan von Schroeder

d0e186c57fb178eed89f4f0b6494f391ec7424d8Jonathan von Schroeder-- mapping qualified operation identifiers (aka renamings)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

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

data Morphism = Morphism

{ msource :: Env

, mtarget :: Env

, typeIdMap :: IdMap

, classIdMap :: IdMap

, funMap :: FunMap

} deriving (Show, Eq, Ord)

-- | construct morphism for subsignatures

mkMorphism :: Env -> Env -> Morphism

mkMorphism e1 e2 = Morphism

{ msource = e1

, mtarget = e2

, typeIdMap = Map.empty

, classIdMap = Map.empty

, funMap = Map.empty }

isInclMor :: Morphism -> Bool

isInclMor m =

Map.null (typeIdMap m) && Map.null (classIdMap m) && Map.null (funMap m)

-- * symbol stuff

-- | the type or kind of an identifier

data SymbolType a =

OpAsItemType TypeScheme

| TypeAsItemType (AnyKind a)

| ClassAsItemType (AnyKind a)

deriving (Show, Eq, Ord)

-- | symbols with their type and env (to look up type aliases)

data Symbol =

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

deriving Show

instance Eq Symbol where

s1 == s2 = compare s1 s2 == EQ

instance Ord Symbol where

compare s1 s2 = compare (symName s1, symType s1) (symName s2, symType s2)

-- | mapping symbols to symbols

type SymbolMap = Map.Map Symbol Symbol

-- | a set of symbols

type SymbolSet = Set.Set Symbol

-- | create a type symbol

idToTypeSymbol :: Env -> Id -> RawKind -> Symbol

idToTypeSymbol e idt k = Symbol idt (TypeAsItemType $ nonVarRawKind k) e

-- | create a class symbol

idToClassSymbol :: Env -> Id -> RawKind -> Symbol

idToClassSymbol e idt k = Symbol idt (ClassAsItemType $ nonVarRawKind k) e

-- | create an operation symbol

idToOpSymbol :: Env -> Id -> TypeScheme -> Symbol

idToOpSymbol e idt typ = Symbol idt (OpAsItemType typ) e

-- | raw symbols where the type of a qualified raw symbol is not yet analysed

data RawSymbol =

AnID Id

| AKindedId SymbKind Id

| AQualId Id (SymbolType Id)

| ASymbol Symbol

deriving (Show, Eq, Ord)

-- | mapping raw symbols to raw symbols

type RawSymbolMap = Map.Map RawSymbol RawSymbol

-- | create a raw symbol from an identifier

idToRaw :: Id -> RawSymbol

idToRaw = AnID

-- | extract the top identifer from a raw symbol

rawSymName :: RawSymbol -> Id

rawSymName r = case r of

AnID i -> i

AKindedId _ i -> i

AQualId i _ -> i

ASymbol s -> symName s

-- | convert a symbol type to a symbol kind

symbTypeToKind :: SymbolType a -> SymbKind

symbTypeToKind s = case s of

OpAsItemType _ -> SyKop

TypeAsItemType _ -> SyKtype

ClassAsItemType _ -> SyKclass

-- | wrap a symbol as raw symbol (is 'ASymbol')

symbolToRaw :: Symbol -> RawSymbol

symbolToRaw = ASymbol

-- | create a raw symbol from a symbol kind and an identifier

symbKindToRaw :: SymbKind -> Id -> RawSymbol

symbKindToRaw sk = case sk of

Implicit -> AnID

_ -> AKindedId $ case sk of

SyKpred -> SyKop

SyKfun -> SyKop

SyKsort -> SyKtype

_ -> sk

getCompoundLists :: Env -> Set.Set [Id]

getCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union

(Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e

where getCompound (Id _ cs _) = cs