5ba323da9f037264b4a356085e844889aedeac23Christian MaederDescription : final static analysis
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederconversion from As to Le
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport qualified Data.Map as Map
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport qualified Data.Set as Set
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- * extract predicate ids from As for mixfix analysis
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederunite :: [Ids] -> Ids
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederidsOfBasicSpec :: BasicSpec -> Ids
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederidsOfBasicSpec (BasicSpec l) = unite $ map (idsOfBasicItem . item) l
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederidsOfBasicItem :: BasicItem -> Ids
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederidsOfBasicItem bi = case bi of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder SigItems i -> idsOfSigItems i
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ClassItems _ l _ -> unite $ map (idsOfClassItem . item) l
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GenItems l _ -> unite $ map (idsOfSigItems . item) l
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Internal l _ -> unite $ map (idsOfBasicItem . item) l
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederidsOfClassItem :: ClassItem -> Ids
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederidsOfClassItem (ClassItem _ l _) = unite $ map (idsOfBasicItem . item) l
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederidsOfSigItems :: SigItems -> Ids
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederidsOfSigItems si = case si of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder OpItems b l _ -> unite $ map (idsOfOpItem b . item) l
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederidsOfOpItem :: OpBrand -> OpItem -> Ids
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederidsOfOpItem b oi = let
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder stripCompound (PolyId (Id ts _ ps) _ _) = Id ts [] ps
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder getPolyId (PolyId i _ _) = i
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder in case oi of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder OpDecl os _ _ _ -> case b of
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder Pred -> Set.union (Set.fromList $ map getPolyId os) $ Set.fromList
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder $ map stripCompound os
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder OpDefn p _ _ _ _ -> case b of
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder Pred -> Set.fromList [getPolyId p, stripCompound p]
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- * basic analysis
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | basic analysis
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederbasicAnalysis :: (BasicSpec, Env, GlobalAnnos) ->
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederbasicAnalysis (b, e, ga) =
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let (nb, ne) = runState (anaBasicSpec ga b) e
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder in Result (reverse $ envDiags ne) $
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder Just (nb, ExtSign (cleanEnv ne) $ declSymbs ne,
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder reverse $ sentences ne)
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder-- | is the first argument a subsignature of the second?
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaederisSubEnv :: Env -> Env -> Bool
167b6ed8639bce096380defb7311ded501ebb5daChristian MaederisSubEnv e1 e2 =
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder let c2 = classMap e2
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder cm = addCpoMap c2
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder t2 = typeMap e2
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder tm = addUnit cm t2
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder expTy = expand tm . opType
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder in Map.isSubmapOfBy (\ (ClassInfo _ k1) (ClassInfo _ k2) ->
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder (\ k -> Set.null $ Set.filter (flip (lesserKind cm) k) k2) k1)
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder (classMap e1) c2
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder && Map.isSubmapOfBy (\ ti1 ti2 -> let
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder k1 = otherTypeKinds ti1
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder k2 = otherTypeKinds ti2
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder in Set.null $ Set.filter (\ k -> Set.null $
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Set.filter (flip (lesserKind cm) k) k2) k1)
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder (typeMap e1) (typeMap e2)
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder all (\ t -> any (instScheme tm 1 (expTy t) . expTy)
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder $ Set.toList s1) (assumps e1) (assumps e2)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | compute difference of signatures
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederdiffEnv :: Env -> Env -> Env
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaederdiffEnv e1 e2 = let
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder tm = typeMap e2
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder cm = diffClassMap (classMap e1) $ classMap e2
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder acm = addClassMap (classMap e1) $ classMap e2
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder in initialEnv
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder { classMap = cm
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder , typeMap = diffTypeMap acm (typeMap e1) tm
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder , assumps = Map.differenceWith diffAss (assumps e1) $ assumps e2
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (\ i1 i2 -> if i1 == i2 then Nothing else Just i1)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (binders e1) $ binders e2 }
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder-- | compute difference of operations
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder -> Maybe (Set.Set OpInfo)
167b6ed8639bce096380defb7311ded501ebb5daChristian MaederdiffAss s1 s2 =
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder let s3 = Set.difference s1 s2 in
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder if Set.null s3 then Nothing else Just s3
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | clean up finally accumulated environment
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedercleanEnv :: Env -> Env
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedercleanEnv e = delPreDefs initialEnv
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder { classMap = classMap e
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , typeMap = typeMap e
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder , assumps = assumps e
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder , binders = binders e }
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | analyse basic spec
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaBasicSpec :: GlobalAnnos -> BasicSpec -> State Env BasicSpec
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaBasicSpec ga b@(BasicSpec l) = do
8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder let newAs = assumps e
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder preds = Map.keysSet $ Map.filter (not . Set.null . Set.filter ( \ oi ->
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder case opDefn oi of
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder NoOpDefn Pred -> True
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder Definition Pred _ -> True
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder _ -> False)) newAs
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder newPreds = idsOfBasicSpec b
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder rels = Set.union preds newPreds
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder newGa = addBuiltins ga
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder precs = mkPrecIntMap $ prec_annos newGa
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Result _ (Just ne) = merge preEnv e
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder put ne { preIds = (precs, rels), globAnnos = newGa }
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapAnM anaBasicItem l
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return $ BasicSpec ul
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | analyse basic item
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaBasicItem :: BasicItem -> State Env BasicItem
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaBasicItem bi = case bi of
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder SigItems i -> fmap SigItems $ anaSigItems Loose i
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ClassItems inst l ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapAnM (anaClassItem inst) l
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ ClassItems inst ul ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GenVarItems l ps -> do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ul <- mapM (anaddGenVarDecl True) l
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ GenVarItems (catMaybes ul) ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ProgItems l ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapAnMaybe anaProgEq l
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ ProgItems ul ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder FreeDatatype l ps -> do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder al <- mapAnMaybe ana1Datatype l
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder tys <- mapM (dataPatToType . item) al
f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder ul <- mapAnMaybe (anaDatatype Free tys) al
c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder addDataSen tys
fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder return $ FreeDatatype ul ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GenItems l ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapAnM (anaSigItems Generated) l
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ GenItems ul ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder AxiomItems decls fs ps -> do
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder tm <- gets localTypeVars -- save type map
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder vs <- gets localVars -- save vars
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder ds <- mapM (anaddGenVarDecl True) decls
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ts <- mapM anaFormula fs
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder putLocalVars vs -- restore
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder putLocalTypeVars tm -- restore
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder let newFs = catMaybes ts
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder newDs = catMaybes ds
021d7137df04ec1834911d99d90243a092841cedChristian Maeder sens = map ( \ (_, f) -> makeNamedSen $ replaceAnnoted (Formula
021d7137df04ec1834911d99d90243a092841cedChristian Maeder $ mkEnvForall e (item f) ps) f) newFs
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder appendSentences sens
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder return $ AxiomItems newDs (map fst newFs) ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Internal l ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapAnM anaBasicItem l
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder return $ Internal ul ps
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | analyse sig items
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaSigItems :: GenKind -> SigItems -> State Env SigItems
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaSigItems gk si = case si of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder TypeItems inst l ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- anaTypeItems gk l
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ TypeItems inst ul ps
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder OpItems b l ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapM (anaOpItem b) l
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder let al = foldr (\ i -> case item i of
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder Nothing -> id
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder Just v -> (replaceAnnoted v i :)) [] ul
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return $ OpItems b al ps
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | analyse a class item
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaClassItem :: Instance -> ClassItem -> State Env ClassItem
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaClassItem _ (ClassItem d l ps) = do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder cd <- anaClassDecls d
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ul <- mapAnM anaBasicItem l
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return $ ClassItem cd ul ps