AsToLe.hs revision 05e2a3161e4589a717c6fe5c7306820273a473c5
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederModule : $Header$
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettMaintainer : maeder@tzi.de
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettStability : experimental
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettPortability : portable
020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett conversion from As to Le
020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport qualified Common.Lib.Map as Map
05b3e12808da901dccd665715cb934462290d550Andy Gimblettimport qualified Common.Lib.Set as Set
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder-- | basic analysis
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederbasicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder Result (BasicSpec, Env, Env, [Named Sentence])
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederbasicAnalysis (b, e, ga) =
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett let (nb, ne) = runState (anaBasicSpec ga b) e
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ce = cleanEnv ne
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in Result (reverse $ envDiags ne) $
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just (nb, diffEnv ce e, ce, reverse $ sentences ne)
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder-- | is the signature empty?
9f93b2a8b552789cd939d599504d39732672dc84Christian MaederisEmptyEnv :: Env -> Bool
9f93b2a8b552789cd939d599504d39732672dc84Christian MaederisEmptyEnv e = Map.isEmpty (classMap e)
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder-- | is the first argument a subsignature of the second?
9f93b2a8b552789cd939d599504d39732672dc84Christian MaederisSubEnv :: Env -> Env -> Bool
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian MaederisSubEnv e1 e2 = isEmptyEnv $ diffEnv e1 e2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- a rough equality
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maederinstance Eq Env where
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder e1 == e2 = isSubEnv e1 e2 && isSubEnv e2 e1
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly-- | compute difference of signatures
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy GimblettdiffEnv :: Env -> Env -> Env
53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy GimblettdiffEnv e1 e2 = let tm = typeMap e2 in
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett { classMap = Map.differenceWith diffClass (classMap e1) (classMap e2)
53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblett , typeMap = Map.differenceWith diffType (typeMap e1) tm
53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblett , assumps = Map.differenceWith (diffAss tm) (assumps e1) (assumps e2)
c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy Gimblett-- | compute difference of class infos
c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy GimblettdiffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy GimblettdiffClass _ _ = Nothing
b25c72845890740c2f8a21214752574990b943cfChristian Maeder-- | compute difference of type infos
b25c72845890740c2f8a21214752574990b943cfChristian MaederdiffType :: TypeInfo -> TypeInfo -> Maybe TypeInfo
c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy GimblettdiffType _ _ = Nothing
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder-- | compute difference of overloaded operations
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian MaederdiffAss :: TypeMap -> OpInfos -> OpInfos -> Maybe OpInfos
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian MaederdiffAss tm (OpInfos l1) (OpInfos l2) =
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder let l3 = diffOps l1 l2 in
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder if null l3 then Nothing else Just (OpInfos l3)
b25c72845890740c2f8a21214752574990b943cfChristian Maeder where diffOps [] _ = []
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett diffOps (o:os) ps =
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett let rs = diffOps os ps
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett n = mapOpInfo (id, expandAlias tm) o
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett in if any (instScheme tm 1 (opType n) . expand tm . opType) ps
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett then rs else n:rs
b25c72845890740c2f8a21214752574990b943cfChristian Maeder-- | environment with predefined types and operations
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy GimblettaddPreDefs :: Env -> Env
b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy GimblettaddPreDefs e = e { typeMap = addUnit $ typeMap e
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder , assumps = addOps $ assumps e }
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder-- | environment with predefined types and operations
aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy GimblettpreEnv = addPreDefs initialEnv
aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett-- | clean up finally accumulated environment
aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy GimblettcleanEnv :: Env -> Env
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy GimblettcleanEnv e = diffEnv initialEnv
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett { classMap = classMap e
197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett , typeMap = Map.filter (not . isTypeVarDefn) $ typeMap e
197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett , assumps = filterVars $ assumps e }
b25c72845890740c2f8a21214752574990b943cfChristian Maeder filterVars :: Assumps -> Assumps
b25c72845890740c2f8a21214752574990b943cfChristian Maeder filterVars = filterAssumps (not . isVarDefn)
b25c72845890740c2f8a21214752574990b943cfChristian Maeder-- | analyse basic spec
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy GimblettanaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec
fcd11c35e645b0744a308f7961a519826bbaa2f5Christian MaederanaBasicSpec ga b@(BasicSpec l) = do
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder let newAs = assumps e
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder case opDefn oi of
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder NoOpDefn Pred -> True
b25c72845890740c2f8a21214752574990b943cfChristian Maeder Definition Pred _ -> True
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder _ -> False) . opInfos) newAs
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett newPreds = idsOfBasicSpec b
fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder rels = Set.union preds newPreds
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder newGa = addBuiltins ga
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder precs = mkPrecIntMap $ prec_annos newGa
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder put (addPreDefs e) { preIds = (precs, rels) }
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett ul <- mapAnM (anaBasicItem newGa) l
b25c72845890740c2f8a21214752574990b943cfChristian Maeder return $ BasicSpec ul
b25c72845890740c2f8a21214752574990b943cfChristian Maeder-- | analyse basic item
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederanaBasicItem :: GlobalAnnos -> BasicItem -> State Env BasicItem
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy GimblettanaBasicItem ga (SigItems i) = fmap SigItems $ anaSigItems ga Loose i
b25c72845890740c2f8a21214752574990b943cfChristian MaederanaBasicItem ga (ClassItems inst l ps) =
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder do ul <- mapAnM (anaClassItem ga inst) l
b25c72845890740c2f8a21214752574990b943cfChristian Maeder return $ ClassItems inst ul ps
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederanaBasicItem _ (GenVarItems l ps) =
b25c72845890740c2f8a21214752574990b943cfChristian Maeder do ul <- mapM anaGenVarDecl l
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder return $ GenVarItems (catMaybes ul) ps
b25c72845890740c2f8a21214752574990b943cfChristian MaederanaBasicItem ga (ProgItems l ps) =
b25c72845890740c2f8a21214752574990b943cfChristian Maeder do ul <- mapAnM (anaProgEq ga) l
b25c72845890740c2f8a21214752574990b943cfChristian Maeder return $ ProgItems ul ps
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederanaBasicItem _ (FreeDatatype l ps) =
b25c72845890740c2f8a21214752574990b943cfChristian Maeder do al <- mapAnMaybe ana1Datatype l
b25c72845890740c2f8a21214752574990b943cfChristian Maeder let tys = map (dataPatToType . item) al
b25c72845890740c2f8a21214752574990b943cfChristian Maeder ul <- mapAnM (anaDatatype Free Plain tys) al
0a83f8dcd5598436966584b858313eb5efd95d5bLiam O'Reilly addDataSen tys
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ FreeDatatype ul ps
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyanaBasicItem ga (GenItems l ps) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly do ul <- mapAnM (anaSigItems ga Generated) l
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder return $ GenItems ul ps
23a073e0a3433ca80a286d46202841b569ec36fdChristian MaederanaBasicItem ga (AxiomItems decls fs ps) =
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett do tm <- gets typeMap -- save type map
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly as <- gets assumps -- save vars
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ds <- mapM anaGenVarDecl decls
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ts <- mapM (anaFormula ga) fs
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly putTypeMap tm -- restore
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett putAssumps as -- restore
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder let newFs = catMaybes ts
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder sens = map ( \ f -> NamedSen (getRLabel f) $ Formula $ item f)
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder appendSentences sens
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder return $ AxiomItems (catMaybes ds) newFs ps
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian MaederanaBasicItem ga (Internal l ps) =
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder do ul <- mapAnM (anaBasicItem ga) l
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder return $ Internal ul ps
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- | analyse sig items
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederanaSigItems :: GlobalAnnos -> GenKind -> SigItems -> State Env SigItems
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederanaSigItems ga gk (TypeItems inst l ps) =
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder do ul <- anaTypeItems ga gk inst l
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder return $ TypeItems inst ul ps
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaederanaSigItems ga _ (OpItems b l ps) =
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder do ul <- mapAnM (anaOpItem ga b) l
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder return $ OpItems b ul ps
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder-- | analyse a class item
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaederanaClassItem :: GlobalAnnos -> Instance -> ClassItem
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder -> State Env ClassItem
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaederanaClassItem ga _ (ClassItem d l ps) =
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder do cd <- anaClassDecls d
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder ul <- mapAnM (anaBasicItem ga) l
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder return $ ClassItem cd ul ps