DataAna.hs revision 3f69b6948966979163bdfe8331c38833d5d90ecd
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
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
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule HasCASL.DataAna 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
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- * creating selector equations
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) =
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski let sc = TypeScheme tArgs (getSelType rt p ty) nullRange in
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder (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 -> []
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Just c -> let sc = TypeScheme args (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
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedermakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedermakeDataSelEqs (DataEntry _ i _ args rk alts) rt =
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder map (mapNamed Formula) $
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder concatMap (makeAltSelEqs $ DataPat i args rk rt) alts
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- * analysis of alternatives
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaAlts :: [DataPat] -> DataPat -> [Alternative] -> TypeEnv -> 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
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederanaAlt :: [DataPat] -> DataPat -> TypeEnv -> 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
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaComps :: [DataPat] -> DataPat -> TypeEnv -> [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
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederanaComp :: [DataPat] -> DataPat -> TypeEnv -> Component
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Result (Type, Selector)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaComp tys rt te (Selector s p t _ _) =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do ct <- anaCompType tys rt t te
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder return (ct, Select (Just s) ct 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
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaCompType :: [DataPat] -> DataPat -> Type -> TypeEnv -> 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
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercheckMonomorphRecursion :: Type -> TypeEnv -> 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
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederfindSubTypes :: TypeMap -> TypeId -> 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
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederrelatedTypeIds :: TypeMap -> TypeId -> TypeId -> Bool
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederrelatedTypeIds tm i1 i2 =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederallRelIds :: TypeMap -> TypeId -> Set.Set TypeId
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