hets/HasCASL/Le.hs

	Le.hs revision df638d53c2d5fe5e80b943a58609c8936848ed82
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- HetCATS/HasCASL/Le.hs
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder   $Id$
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder   Authors: Christian Maeder
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu   Year:    2002/2003
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder   abstract syntax after/during static analysis
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-}
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedermodule HasCASL.Le where
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport HasCASL.As
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Lib.Map as Map
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Lib.Set as Set
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Result
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.GlobalAnnotations
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederimport Common.Named
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-- classInfo
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata ClassInfo = ClassInfo { superClasses :: Set ClassId
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                           , classKind :: Kind
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder               , classDefn :: Maybe Class
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder               } deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedernewClassInfo :: ClassInfo
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian MaedernewClassInfo = ClassInfo Set.empty star Nothing
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedertype ClassMap = Map ClassId ClassInfo
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-- typeInfo
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata GenKind = Free | Generated | Loose deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata AltDefn = Construct UninstOpId [Type] Partiality [Selector]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder               -- argument types
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder           deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata Selector = Select UninstOpId Type Partiality -- only result type
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder        deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata TypeDefn = NoTypeDefn
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder              | Supertype Vars Type Formula
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder          | DatatypeDefn GenKind [TypeArg] [AltDefn]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder          | AliasTypeDefn TypeScheme
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder          | TypeVarDefn deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata TypeInfo = TypeInfo { typeKind :: Kind
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             , otherTypeKinds :: [Kind]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             , superTypes :: [Type]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             , typeDefn :: TypeDefn
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             } deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedertype TypeMap = Map TypeId TypeInfo
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-- assumptions
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder-----------------------------------------------------------------------------
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata OpInfo = OpInfo { opType :: TypeScheme
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             , opAttrs :: [OpAttr]
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             , opDefn :: OpDefn
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder             } deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maederdata OpDefn = NoOpDefn
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder        | ConstructData TypeId     -- target type
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder        | SelectData [UninstOpId] TypeId   -- constructors of source type
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder        | Definition Term
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder        | VarDefn deriving (Show, Eq)
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maeder
c3ebe5e0a6545997d56e4156de02d00518c71c0cChristian Maedertype Assumps = Map UninstOpId [OpInfo]
de4e22f27c1e1c6e0efbc72ffe1670f74181e49eChristian Maeder
-----------------------------------------------------------------------------
-- local env
-----------------------------------------------------------------------------

data Env = Env { classMap :: ClassMap
               , typeMap :: TypeMap
           , assumps :: Assumps
           , sentences :: [Named Formula]
               , globalAnnos :: GlobalAnnos
           , envDiags :: [Diagnosis]
           , counter :: Int
           } deriving Show

instance Eq Env where
    Env c1 t1 a1 s1 _ _ _ == Env c2 t2 a2 s2 _ _ _ =
    (c1, t1, a1, s1) == (c2, t2, a2, s2)

initialEnv :: Env
initialEnv = Env Map.empty Map.empty Map.empty [] emptyGlobalAnnos [] 1