hets/HasCASL/DataAna.hs

	DataAna.hs revision df638d53c2d5fe5e80b943a58609c8936848ed82
55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaederModule      :  $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright   :  (c) Christian Maeder and Uni Bremen 2002-2003
de6a40dbdd4712e5a9398b8519a59b1eaeab2f5aChristian MaederLicence     :  All rights reserved.
64f00fb69046070dc033eb034cdd9afd22809a63Christian Maeder
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer  :  hets@tzi.de
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaederStability   :  provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability :  non-portable (MonadState)
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederanalyse alternatives of data types
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder
aac750d0dc6a7c8f2129d357a129894c9d042e90Christian Maeder-}
aac750d0dc6a7c8f2129d357a129894c9d042e90Christian Maeder
aac750d0dc6a7c8f2129d357a129894c9d042e90Christian Maedermodule HasCASL.DataAna where
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederimport HasCASL.As
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederimport HasCASL.AsUtils
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Id
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederimport Common.Result
a209694d7694b93e56927c6aacc3f5b9366fdb8fChristian Maederimport HasCASL.Le
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederimport Data.Maybe
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederimport HasCASL.TypeAna
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maederimport HasCASL.Reader
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaederanaAlts :: Type -> [Alternative] -> ReadR (ClassMap, TypeMap) [AltDefn]
a209694d7694b93e56927c6aacc3f5b9366fdb8fChristian MaederanaAlts dt alts = do l <- foldReadR (anaAlt dt) alts
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder             lift $ Result (checkUniqueness $ map
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder                    ( \ (Construct i _ _ _) -> i) l)
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder                    $ Just l
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaederanaAlt :: Type -> Alternative -> ReadR (ClassMap, TypeMap) AltDefn
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaederanaAlt _ (Subtype ts ps) =
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder    do kts <- mapM anaType $ map ( \ t -> (star, t)) ts
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder       mapM ( \ (ki, ti) -> checkKindsR ti star ki) kts
616b72452ce5a75ade1a11ccc2c9671b3444558eChristian Maeder       lift $ Result [Diag Warning "data subtype ignored" $ firstPos ts ps]
616b72452ce5a75ade1a11ccc2c9671b3444558eChristian Maeder        $ Nothing
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaederanaAlt dt (Constructor i cs p _) =
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder    do newCs <- mapM (anaComp i dt) $ zip cs $ map (:[]) [1..]
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder       let sels = concatMap snd newCs
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder       con = Construct i (map fst newCs) p sels
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder       -- check for disjoint selectors
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder       lift $ Result (checkUniqueness $ map ( \ (Select s _ _) -> s ) sels)
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder        $ Just con
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaedergetConstrType :: Type -> Partiality -> [Type] -> Type
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian MaedergetConstrType dt p = addPartiality p .
ca5e921bbca4a90ad9adf7350bedcb7deb059e86Christian Maeder               foldr ( \ c r -> FunType c FunArr r [] ) dt
bba825b39570777866d560bfde3807731131097eKlaus Luettich
bba825b39570777866d560bfde3807731131097eKlaus Luettich
740670de3c457d7571ef6f3fe9b60c2e25fb9902Christian MaederaddPartiality :: Partiality -> Type -> Type
740670de3c457d7571ef6f3fe9b60c2e25fb9902Christian MaederaddPartiality Total t = t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddPartiality Partial t = makePartial t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
2018084d6189a68640c516ca3e340d879f40f0acChristian MaedermakePartial :: Type -> Type
aa074a906c39b63c7177040378c0073dbac4e3baChristian MaedermakePartial t =
    case t of
       FunType t1 a t2 ps ->
           case t2 of
               FunType _ _ _ _ -> FunType t1 a (makePartial t2) ps
               _ -> FunType t1 PFunArr t2 ps
       _ -> LazyType t []

anaComp :: Id -> Type -> (Components, [Int])
    -> ReadR (ClassMap, TypeMap) (Type, [Selector])
anaComp _ _ (Selector s p t _ _, _) =
    do (k, ct) <- anaType (star, t)
       checkKindsR t star k
       return (ct, [Select s ct p])
anaComp con rt (NoSelector t, i) =
    do (k, ct) <- anaType (star, t)
       checkKindsR t star k
       return (ct, [Select (simpleIdToId $ mkSimpleId
                ("%(" ++ showPretty rt "." ++
                 showId con ".sel_" ++ show i ++ ")%"))
            ct Partial])

anaComp con rt (NestedComponents cs ps, i) =
    do newCs <- mapM (anaComp con rt) $ zip cs $ map (:i) [1..]
       return (ProductType (map fst newCs) ps,
           concatMap snd newCs)

getSelType :: Type -> Partiality -> Type -> Type
getSelType dt p rt = addPartiality p $ FunType dt FunArr rt []