DataAna.hs revision 1738d16957389457347bee85075d3d33d002158f
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : hets@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
967e5f3c25249c779575864692935627004d3f9eChristian MaederPortability : non-portable (MonadState)
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederanalyse alternatives of data types
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-}
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule HasCASL.DataAna where
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Data.Maybe
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Data.List as List
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maederimport Common.Id
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maederimport Common.Result
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport Common.AS_Annotation
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport HasCASL.As
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport HasCASL.Le
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport HasCASL.TypeAna
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport HasCASL.AsUtils
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HasCASL.Builtin
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport HasCASL.Unify
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaedermkSelId :: String -> Int -> Int -> Id
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermkSelId str n m = mkId [mkSimpleId (str ++ "_" ++ show n ++ "_" ++ show m)]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermkSelVar :: Int -> Int -> Type -> VarDecl
967e5f3c25249c779575864692935627004d3f9eChristian MaedermkSelVar n m ty = VarDecl (mkSelId "x" n m) ty Other []
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedergenTuple :: Int -> Int -> [Selector] -> [VarDecl]
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedergenTuple _ _ [] = []
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedergenTuple n m (Select _ ty _ : sels) =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder mkSelVar n m ty : genTuple n (m + 1) sels
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedergenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedergenSelVars _ [] = []
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedergenSelVars n (ts:sels) =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder genTuple n 1 ts : genSelVars (n + 1) sels
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedermakeSelTupleEqs :: Type -> [TypeArg] -> Term -> Int -> Int -> [Selector]
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder -> [Named Term]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedermakeSelTupleEqs dt args ct n m (Select mi ty p : sels) =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder (case mi of
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder Nothing -> []
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder Just i -> let sc = TypeScheme args ([] :=> getSelType dt p ty) []
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder vt = QualVar $ mkSelVar n m ty
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder eq = mkEqTerm eqId [] (mkApplTerm (mkOpTerm i sc) [ct]) vt
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder in [NamedSen ("ga_select_" ++ show i) eq])
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ++ makeSelTupleEqs dt args ct n (m + 1) sels
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedermakeSelTupleEqs _ _ _ _ _ [] = []
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedermakeSelEqs :: Type -> [TypeArg] -> Term -> Int -> [[Selector]]
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder -> [Named Term]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermakeSelEqs dt args ct n (sel:sels) =
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder makeSelTupleEqs dt args ct n 1 sel
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ++ makeSelEqs dt args ct (n + 1) sels
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedermakeSelEqs _ _ _ _ _ = []
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermakeAltSelEqs :: Type -> [TypeArg] -> AltDefn -> [Named Term]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermakeAltSelEqs dt args (Construct mc ts p sels) =
d48085f765fca838c1d972d2123601997174583dChristian Maeder case mc of
d48085f765fca838c1d972d2123601997174583dChristian Maeder Nothing -> []
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Just c -> let sc = TypeScheme args ([] :=> getConstrType dt p ts) []
d48085f765fca838c1d972d2123601997174583dChristian Maeder vars = genSelVars 1 sels
d48085f765fca838c1d972d2123601997174583dChristian Maeder as = map ( \ vs -> mkTupleTerm (map QualVar vs) []) vars
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder ct = mkApplTerm (mkOpTerm c sc) as
d48085f765fca838c1d972d2123601997174583dChristian Maeder in map (mapNamed (mkForall (map GenTypeVarDecl args
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder ++ map GenVarDecl (concat vars))))
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder $ makeSelEqs dt args ct 1 sels
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedermakeDataSelEqs :: DataEntry -> [Named Sentence]
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedermakeDataSelEqs (DataEntry _ i _ args alts) =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder map (mapNamed Formula) $
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder concatMap (makeAltSelEqs (typeIdToType i args star) args) alts
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederanaAlts :: [(Id, Type)] -> Type -> [Alternative] -> TypeMap -> Result [AltDefn]
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederanaAlts tys dt alts tm =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder do l <- mapM (anaAlt tys dt tm) alts
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder Result (checkUniqueness $ catMaybes $
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder map ( \ (Construct i _ _ _) -> i) l) $ Just ()
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder return l
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederanaAlt :: [(Id, Type)] -> Type -> TypeMap -> Alternative -> Result AltDefn
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederanaAlt _ _ tm (Subtype ts _) =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder do l <- mapM ( \ t -> anaType (Just star, t) tm) ts
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder return $ Construct Nothing (map snd l) Partial []
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederanaAlt tys dt tm (Constructor i cs p _) =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder do newCs <- mapM (anaComps tys dt tm) cs
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder let sels = map snd newCs
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result (checkUniqueness $ catMaybes $
967e5f3c25249c779575864692935627004d3f9eChristian Maeder map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return $ Construct (Just i) (map fst newCs) p sels
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederanaComps :: [(Id, Type)] -> Type -> TypeMap -> [Component]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder -> Result (Type, [Selector])
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederanaComps tys rt tm cs =
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder do newCs <- mapM (anaComp tys rt tm) cs
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder return (mkProductType (map fst newCs) [], map snd newCs)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaederanaComp :: [(Id, Type)] -> Type -> TypeMap -> Component
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder -> Result (Type, Selector)
99f1a09ee1847410faf46527f5465bd2070800c2Christian MaederanaComp tys rt tm (Selector s p t _ _) =
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder do ct <- anaCompType tys rt t tm
81d182b21020b815887e9057959228546cf61b6bChristian Maeder return (ct, Select (Just s) ct p)
242397ba0f1cc490e892130bf0df239deeecf5daChristian MaederanaComp tys rt tm (NoSelector t) =
242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder do ct <- anaCompType tys rt t tm
242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder return (ct, Select Nothing ct Partial)
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedergetSelType :: Type -> Partiality -> Type -> Type
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedergetSelType dt p rt = (case p of
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder Partial -> addPartiality [dt]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder Total -> id) $ FunType dt FunArr rt []
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaederanaCompType :: [(Id, Type)] -> Type -> Type -> TypeMap -> Result Type
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederanaCompType tys dt t tm = do
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski (_, ct) <- anaType (Just star, t) tm
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder let ds = unboundTypevars (varsOf dt) ct
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if null ds then return () else Result ds Nothing
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder mapM (checkMonomorphRecursion ct tm) tys
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder return ct
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskicheckMonomorphRecursion :: Type -> TypeMap -> (Id, Type) -> Result ()
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedercheckMonomorphRecursion t tm (i, rt) =
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder if occursIn tm i t then
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder if equalSubs tm t rt then return ()
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder else Result [Diag Error ("illegal polymorphic recursion"
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder ++ expected rt t) $ getMyPos t] Nothing
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder else return ()
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski