AsToLe.hs revision f353be6210f67ffd4a46967bba749afc968cee52
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiMaintainer : hets@tzi.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder conversion from As to Le
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Set as Set
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- | basic analysis
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederbasicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Result (BasicSpec, Env, Env, [Named Term])
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaederbasicAnalysis (b, e, ga) =
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder let (nb, ne) = runState (anaBasicSpec ga b) e
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich ce = cleanEnv ne
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder in Result (reverse $ envDiags ne) $
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Just (nb, diffEnv ce e, ce, reverse $ sentences ne)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | compute difference of signatures
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskidiffEnv :: Env -> Env -> Env
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederdiffEnv e1 e2 = let tm = typeMap e2 in
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder { classMap = Map.differenceWith diffClass (classMap e1) (classMap e2)
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder , typeMap = Map.differenceWith diffType (typeMap e1) tm
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , assumps = Map.differenceWith (diffAss tm) (assumps e1) (assumps e2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | compute difference of class infos
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdiffClass :: ClassInfo -> ClassInfo -> Maybe ClassInfo
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederdiffClass _ _ = Nothing
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | compute difference of type infos
16e124196c6b204769042028c74f533509c9b5d3Christian MaederdiffType :: TypeInfo -> TypeInfo -> Maybe TypeInfo
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederdiffType _ _ = Nothing
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- | Check if two OpTypes are equal except from totality or partiality
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedercompatibleOpTypes :: TypeScheme -> TypeScheme -> Bool
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedercompatibleOpTypes = isUnifiable Map.empty 0
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder-- | compute difference of overloaded operations
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederdiffAss :: TypeMap -> OpInfos -> OpInfos -> Maybe OpInfos
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederdiffAss tm (OpInfos l1) (OpInfos l2) =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder let l3 = diffOps l1 l2 in
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder if null l3 then Nothing else Just (OpInfos l3)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder where diffOps [] _ = []
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder diffOps (o:os) ps =
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder let rs = diffOps os ps in
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder if any (\ p -> isUnifiable tm 0 (opType o) (opType p)) ps
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder then rs else o:rs
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder-- | clean up finally accumulated environment
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaedercleanEnv :: Env -> Env
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaedercleanEnv e = diffEnv initialEnv
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder { classMap = classMap e
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , typeMap = Map.filter (not . isTypeVarDefn) (typeMap e)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , assumps = filterAssumps (not . isVarDefn) (assumps e) }
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder-- | environment with predefined types and operations
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederpreEnv = initialEnv { typeMap = addUnit Map.empty
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , assumps = addOps Map.empty }
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederaddPreIds :: (PrecMap, Set.Set Id) -> State Env ()
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederaddPreIds r = do e <- get
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder put e { preIds = r }
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- | analyse basic spec
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederanaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederanaBasicSpec ga b@(BasicSpec l) = do
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder tm <- gets typeMap
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder as <- gets assumps
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder putTypeMap $ addUnit tm
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder putAssumps $ addOps as
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newAs <- gets assumps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder case opDefn oi of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder NoOpDefn Pred -> True
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Definition Pred _ -> True
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> False) . opInfos) newAs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder newPreds = idsOfBasicSpec b
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder rels = Set.union preds newPreds
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder newGa = addBuiltins ga
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder precs = mkPrecIntMap $ prec_annos newGa
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski addPreIds (precs, rels)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ul <- mapAnM (anaBasicItem newGa) l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ BasicSpec ul
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | analyse basic item
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaBasicItem :: GlobalAnnos -> BasicItem -> State Env BasicItem
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederanaBasicItem ga (SigItems i) = fmap SigItems $ anaSigItems ga Loose i
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederanaBasicItem ga (ClassItems inst l ps) =
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder do ul <- mapAnM (anaClassItem ga inst) l
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ ClassItems inst ul ps
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaBasicItem _ (GenVarItems l ps) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapM anaGenVarDecl l
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ GenVarItems (catMaybes ul) ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaBasicItem ga (ProgItems l ps) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do ul <- mapAnM (anaProgEq ga) l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ ProgItems ul ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaBasicItem _ (FreeDatatype l ps) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder do al <- mapAnMaybe ana1Datatype l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let tys = map (dataPatToType . item) al
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ul <- mapAnM (anaDatatype Free Plain tys) al
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ FreeDatatype ul ps
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederanaBasicItem ga (GenItems l ps) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder do ul <- mapAnM (anaSigItems ga Generated) l
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder return $ GenItems ul ps
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaBasicItem ga (AxiomItems decls fs ps) =
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder do tm <- gets typeMap -- save type map
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder as <- gets assumps -- save vars
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ds <- mapM anaGenVarDecl decls
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ts <- mapM (anaFormula ga) fs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder putTypeMap tm -- restore
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putAssumps as -- restore
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let newFs = catMaybes ts
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sens = map ( \ f -> NamedSen (getRLabel f) $ item f) newFs
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder appendSentences sens
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ AxiomItems (catMaybes ds) newFs ps
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederanaBasicItem ga (Internal l ps) =
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder do ul <- mapAnM (anaBasicItem ga) l
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder return $ Internal ul ps
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | add sentences
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederappendSentences :: [Named Term] -> State Env ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederappendSentences fs =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder put $ e {sentences = sentences e ++ fs}
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | analyse sig items
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaSigItems :: GlobalAnnos -> GenKind -> SigItems -> State Env SigItems
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaSigItems ga gk (TypeItems inst l ps) =
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder do ul <- anaTypeItems ga gk inst l
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ TypeItems inst ul ps
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzanaSigItems ga _ (OpItems b l ps) =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz do ul <- mapAnM (anaOpItem ga b) l
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return $ OpItems b ul ps
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- | analyse a class item
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzanaClassItem :: GlobalAnnos -> Instance -> ClassItem
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz -> State Env ClassItem
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzanaClassItem ga _ (ClassItem d l ps) =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz do cd <- anaClassDecls d
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder ul <- mapAnM (anaBasicItem ga) l
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder return $ ClassItem cd ul ps