DataAna.hs revision 0ea85310d2beb8aa03cac481ad2a6564e6b8ddbc
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : analysis of data type declarations
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional
fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederanalyse alternatives of data types
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedermodule HasCASL.DataAna
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder ( DataPat(..)
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , anaAlts
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , makeDataSelEqs
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder , inVarTypeArg
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder ) where
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Data.Maybe
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Id
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Result
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.AS_Annotation
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport HasCASL.As
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport HasCASL.Le
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport HasCASL.TypeAna
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederimport HasCASL.AsUtils
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport HasCASL.Builtin
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederimport HasCASL.Unify
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder-- | description of polymorphic data types
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederdata DataPat = DataPat Id [TypeArg] RawKind Type
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- make type argument invariant
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaederinVarTypeArg :: TypeArg -> TypeArg
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaederinVarTypeArg (TypeArg i _ vk rk c o p) = (TypeArg i InVar vk rk c o p)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkSelId :: Range -> String -> Int -> Int -> Id
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedermkSelId p str n m = mkId
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder [Token (str ++ "_" ++ show n ++ "_" ++ show m) p]
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedermkSelVar :: Int -> Int -> Type -> VarDecl
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkSelVar n m ty = VarDecl (mkSelId (getRange ty) "x" n m) ty Other nullRange
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergenTuple :: Int -> Int -> [Selector] -> [VarDecl]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedergenTuple _ _ [] = []
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedergenTuple n m (Select _ ty _ : sels) =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder mkSelVar n m ty : genTuple n (m + 1) sels
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedergenSelVars _ [] = []
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedergenSelVars n (ts:sels) =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder genTuple n 1 ts : genSelVars (n + 1) sels
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermakeSelTupleEqs :: DataPat -> Term -> Int -> Int -> [Selector] -> [Named Term]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedermakeSelTupleEqs dt@(DataPat _ tArgs _ rt) ct n m (Select mi ty p : sels) =
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder let sc = TypeScheme (map inVarTypeArg tArgs) (getSelType rt p ty) nullRange
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder in (case mi of
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Just i -> let
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder vt = QualVar $ mkSelVar n m ty
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder eq = mkEqTerm eqId nullRange
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder (mkApplTerm (mkOpTerm i sc) [ct]) vt
c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder in [makeNamed ("ga_select_" ++ show i) eq]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder _ -> [])
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder ++ makeSelTupleEqs dt ct n (m + 1) sels
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermakeSelTupleEqs _ _ _ _ [] = []
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermakeSelEqs :: DataPat -> Term -> Int -> [[Selector]] -> [Named Term]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedermakeSelEqs dt ct n (sel:sels) =
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder makeSelTupleEqs dt ct n 1 sel
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder ++ makeSelEqs dt ct (n + 1) sels
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermakeSelEqs _ _ _ _ = []
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedermakeAltSelEqs dt@(DataPat _ args _ rt) (Construct mc ts p sels) =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder case mc of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Nothing -> []
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder Just c -> let sc = TypeScheme (map inVarTypeArg args)
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder (getFunType rt p ts) nullRange
3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder newSc = sc
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder vars = genSelVars 1 sels
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder ars = map ( \ vs -> mkTupleTerm (map QualVar vs) nullRange)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder vars
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder ct = mkApplTerm (mkOpTerm c newSc) ars
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder in map (mapNamed (mkForall (map GenTypeVarDecl args
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ++ map GenVarDecl (concat vars))))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $ makeSelEqs dt ct 1 sels
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- | create selector equations for a data type
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedermakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedermakeDataSelEqs (DataEntry _ i _ args rk alts) rt =
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder map (mapNamed Formula) $
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder concatMap (makeAltSelEqs $ DataPat i args rk rt) $ Set.toList alts
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- | analyse the alternatives of a data type
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederanaAlts :: [DataPat] -> DataPat -> [Alternative] -> Env -> Result [AltDefn]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederanaAlts tys dt alts te =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do l <- mapM (anaAlt tys dt te) alts
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Result (checkUniqueness $ catMaybes $
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder map ( \ (Construct i _ _ _) -> i) l) $ Just ()
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder return l
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederanaAlt :: [DataPat] -> DataPat -> Env -> Alternative
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder -> Result AltDefn
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederanaAlt _ _ te (Subtype ts _) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do l <- mapM ( \ t -> anaStarTypeM t te) ts
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder return $ Construct Nothing (map snd l) Partial []
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederanaAlt tys dt te (Constructor i cs p _) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do newCs <- mapM (anaComps tys dt te) cs
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let sels = map snd newCs
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Result (checkUniqueness $ catMaybes $
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return $ Construct (Just i) (map fst newCs) p sels
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederanaComps :: [DataPat] -> DataPat -> Env -> [Component]
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder -> Result (Type, [Selector])
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaComps tys rt te cs =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do newCs <- mapM (anaComp tys rt te) cs
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (mkProductType $ map fst newCs, map snd newCs)
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederanaComp :: [DataPat] -> DataPat -> Env -> Component
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Result (Type, Selector)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaederanaComp tys rt te (Selector s _ t _ _) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do ct <- anaCompType tys rt t te
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder let (p, nct) = case getTypeAppl ct of
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (TypeName i _ _, [lt]) | i == lazyTypeId -> (Partial, lt)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder _ -> (Total, ct)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder return (nct, Select (Just s) nct p)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaComp tys rt te (NoSelector t) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do ct <- anaCompType tys rt t te
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return (ct, Select Nothing ct Partial)
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederanaCompType :: [DataPat] -> DataPat -> Type -> Env -> Result Type
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederanaCompType tys (DataPat _ tArgs _ _) t te = do
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder (_, ct) <- anaStarTypeM t te
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder let ds = unboundTypevars True tArgs ct
1738d16957389457347bee85075d3d33d002158fChristian Maeder if null ds then return () else Result ds Nothing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mapM (checkMonomorphRecursion ct te) tys
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder return $ generalize tArgs ct
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercheckMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercheckMonomorphRecursion t te (DataPat i _ _ rt) =
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder $ findSubTypes (typeMap te) i t of
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder [] -> return ()
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder ++ expected rt ty) $ getRange ty] Nothing
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederfindSubTypes :: TypeMap -> Id -> Type -> [Type]
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederfindSubTypes tm i t = case getTypeAppl t of
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder (TypeName j _ _, args) -> if relatedTypeIds tm i j then [t]
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder else concatMap (findSubTypes tm i) args
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder (topTy, args) -> concatMap (findSubTypes tm i) $ topTy : args
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederrelatedTypeIds :: TypeMap -> Id -> Id -> Bool
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederrelatedTypeIds tm i1 i2 =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederallRelIds :: TypeMap -> Id -> Set.Set Id
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederallRelIds tm i = Set.union (superIds tm i) $ subIds tm i
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedersubIds :: TypeMap -> Id -> Set.Set Id
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedersubIds tm i = foldr ( \ j s ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if Set.member i $ superIds tm j then
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Set.insert j s else s) Set.empty $ Map.keys tm