AsToLe.hs revision fa45d098e1c9d468f128be9505eb7e5b2705b304
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{- HetCATS/HasCASL/AsToLe.hs
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder $Id$
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Authors: Christian Maeder
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Year: 2002
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder conversion of As.hs to Le.hs
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-}
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermodule AsToLe where
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport AS_Annotation
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport As
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport ClassAna
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport ClassDecl
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport FiniteMap
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Id
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Le
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Lexer
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Maybe
d48085f765fca838c1d972d2123601997174583dChristian Maederimport Monad
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederimport MonadState
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport OpDecl
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Result
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederimport PrintAs
d48085f765fca838c1d972d2123601997174583dChristian Maederimport TypeAna
76647324ed70f33b95a881b536d883daccf9568dChristian Maederimport TypeDecl
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian Maeder----------------------------------------------------------------------------
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- analysis
d48085f765fca838c1d972d2123601997174583dChristian Maeder-----------------------------------------------------------------------------
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian MaederanaBasicSpec :: BasicSpec -> State Env ()
d48085f765fca838c1d972d2123601997174583dChristian MaederanaBasicSpec (BasicSpec l) = mapM_ anaBasicItem $ map item l
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian MaederanaBasicItem :: BasicItem -> State Env ()
d48085f765fca838c1d972d2123601997174583dChristian MaederanaBasicItem (SigItems i) = anaSigItems Loose i
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederanaBasicItem (ClassItems inst l _) = mapM_ (anaAnnotedClassItem inst) l
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederanaBasicItem (GenVarItems l _) = mapM_ anaGenVarDecl l
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederanaBasicItem t@(ProgItems _ p) = missingAna t p
76647324ed70f33b95a881b536d883daccf9568dChristian MaederanaBasicItem (FreeDatatype l _) = mapM_ (anaDatatype Free Plain) $ map item l
d48085f765fca838c1d972d2123601997174583dChristian MaederanaBasicItem (GenItems l _) = mapM_ (anaSigItems Generated) $ map item l
d48085f765fca838c1d972d2123601997174583dChristian MaederanaBasicItem t@(AxiomItems _ _ p) = missingAna t p
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian MaederanaSigItems :: GenKind -> SigItems -> State Env ()
d48085f765fca838c1d972d2123601997174583dChristian MaederanaSigItems gk (TypeItems inst l _) = mapM_ (anaTypeItem gk inst) $ map item l
d48085f765fca838c1d972d2123601997174583dChristian MaederanaSigItems _ (OpItems l _) = mapM_ anaOpItem $ map item l
d48085f765fca838c1d972d2123601997174583dChristian MaederanaSigItems _ l@(PredItems _ p) = missingAna l p
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder----------------------------------------------------------------------------
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- GenVarDecl
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-----------------------------------------------------------------------------
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederanaGenVarDecl :: GenVarDecl -> State Env ()
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederanaGenVarDecl(GenVarDecl v) = optAnaVarDecl v
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederanaGenVarDecl(GenTypeVarDecl t) = anaTypeVarDecl t
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederisSimpleId :: Id -> Bool
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederisSimpleId (Id ts _ _) = null (tail ts) && head (tokStr (head ts))
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder `elem` caslLetters
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToClass :: ClassMap -> Type -> Result Class
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToClass cMap (TypeToken t) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder if tokStr t == "Type" then Result [] (Just $ universe) else
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let ci = simpleIdToId t
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder ds = anaClassId cMap ci
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder in if null ds then
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Result [] (Just $ Intersection [ci] [])
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder else Result [mkDiag Hint "not a class" ci] Nothing
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToClass cMap (BracketType Parens ts ps) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder do cs <- mapM (convertTypeToClass cMap) ts
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder return $ Intersection (concatMap iclass cs) ps
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToClass _ t = Result [mkDiag Hint "not a class" t] Nothing
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToKind :: ClassMap -> Type -> Result Kind
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToKind cMap (ProductType ts ps) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder do ks <- mapM (convertTypeToKind cMap) ts
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder return $ ProdClass ks ps
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToKind cMap (FunType t1 FunArr t2 ps) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder do k1 <- convertTypeToKind cMap t1
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder k2 <- convertTypeToKind cMap t2
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder return $ KindAppl k1 k2 ps
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToKind cMap (BracketType Parens [t] _) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder do k <- convertTypeToKind cMap t
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder return $ k
d48085f765fca838c1d972d2123601997174583dChristian Maeder
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederconvertTypeToKind cMap (MixfixType [t1, TypeToken t]) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder let s = tokStr t
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder v = case s of
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder "+" -> CoVar
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder "-" -> ContraVar
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder _ -> InVar
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder in case v of
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder InVar -> Result [] Nothing
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder _ -> do k1 <- convertTypeToKind cMap t1
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder return $ ExtClass k1 v [tokPos t]
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaederconvertTypeToKind cMap t = convertTypeToClass cMap t >>= (return . PlainClass)
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian MaederoptAnaVarDecl, anaVarDecl :: VarDecl -> State Env ()
d48085f765fca838c1d972d2123601997174583dChristian MaederoptAnaVarDecl vd@(VarDecl v t s q) =
d48085f765fca838c1d972d2123601997174583dChristian Maeder if isSimpleId v then
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder do cMap <- getClassMap
d48085f765fca838c1d972d2123601997174583dChristian Maeder let Result ds mc = convertTypeToKind cMap t
d48085f765fca838c1d972d2123601997174583dChristian Maeder case mc of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Just c -> anaTypeVarDecl(TypeArg v c s q)
d48085f765fca838c1d972d2123601997174583dChristian Maeder Nothing -> anaVarDecl vd
d48085f765fca838c1d972d2123601997174583dChristian Maeder appendDiags ds
d48085f765fca838c1d972d2123601997174583dChristian Maeder else anaVarDecl vd
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian MaederanaVarDecl(VarDecl v oldT _ _) =
d48085f765fca838c1d972d2123601997174583dChristian Maeder do (mk, t) <- anaType oldT
d48085f765fca838c1d972d2123601997174583dChristian Maeder case mk of
d48085f765fca838c1d972d2123601997174583dChristian Maeder Nothing -> return ()
d48085f765fca838c1d972d2123601997174583dChristian Maeder Just k -> if eqKind Compatible k star
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder then return ()
d48085f765fca838c1d972d2123601997174583dChristian Maeder else addDiag $
d48085f765fca838c1d972d2123601997174583dChristian Maeder mkDiag Error
d48085f765fca838c1d972d2123601997174583dChristian Maeder ("wrong kind '" ++ showPretty k
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder "' of type for variable") v
d48085f765fca838c1d972d2123601997174583dChristian Maeder as <- getAssumps
d48085f765fca838c1d972d2123601997174583dChristian Maeder let l = lookupWithDefaultFM as [] v
d48085f765fca838c1d972d2123601997174583dChristian Maeder ts = simpleTypeScheme t in
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder if ts `elem` l then
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder addDiag $ mkDiag Warning
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder "repeated variable '" v
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder else putAssumps $ addToFM as v (ts:l)
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian Maeder
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- ----------------------------------------------------------------------------
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ClassItem
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder-- ----------------------------------------------------------------------------
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederanaAnnotedClassItem :: Instance -> Annoted ClassItem -> State Env ()
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederanaAnnotedClassItem _ aci =
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder let ClassItem d l _ = item aci in
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder do anaClassDecls d
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder mapM_ anaBasicItem $ map item l
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian Maeder