----------------------------------------------------------------------------- -- | License : GPL -- -- Maintainer : helium@cs.uu.nl -- Stability : provisional -- Portability : portable -- -- An equivalence group is a graph-like structure containing type variables and -- type constants that should all be equivalent. The edges explain why they should -- be equal. -- ----------------------------------------------------------------------------- module Top.Implementation.TypeGraph.EquivalenceGroup ( EquivalenceGroup , emptyGroup, insertVertex, insertEdge, insertClique, combineGroups , vertices, constants, edges, equalPaths , removeEdge, removeClique, splitGroup , typeOfGroup, consistent, checkGroup ) where import Top.Implementation.TypeGraph.Path import Top.Implementation.TypeGraph.Basics import Top.Types import Data.List import Data.Maybe import qualified Data.Set as S ----------------------------------------------------------------------- -- * Representation of an equivalence group data EquivalenceGroup info = EQGroup { vertices :: [(VertexId, VertexInfo)] -- ^ vertices in this equivalence group , edges :: [(EdgeId, info)] -- ^ (initial) edges in this equivalence group , cliques :: [Clique] -- ^ (implied) cliques in this equivalence group } -- first sort the items of an equivalence group instance Show (EquivalenceGroup info) where show eqgroup = unlines $ [ "[Vertices]:" , " " ++ concatMap show (sort (vertices eqgroup)) , "[Edges]:" , " " ++ concatMap show (sort [ a | (a, _) <- edges eqgroup ]) , "[Cliques ]:" ] ++ map ((" "++) . show) (sort (cliques eqgroup)) ----------------------------------------------------------------------- -- * Constructing an equivalence group emptyGroup :: EquivalenceGroup info emptyGroup = EQGroup { vertices = [], edges = [], cliques = [] } insertVertex :: VertexId -> VertexInfo -> EquivalenceGroup info -> EquivalenceGroup info insertVertex i info eqgroup = eqgroup { vertices = (i, info) : vertices eqgroup } insertEdge :: EdgeId -> info -> EquivalenceGroup info -> EquivalenceGroup info insertEdge edge info eqgroup = eqgroup { edges = (edge, info) : edges eqgroup } insertClique :: Clique -> EquivalenceGroup info -> EquivalenceGroup info insertClique clique eqgroup = eqgroup { cliques = newCliques } where newCliques = mergeCliques (clique : cs2) : cs1 (cs1, cs2) = partition (isDisjointClique clique) (cliques eqgroup) {- msg = unlines [ "------------------insert clique -------------------------" , show eqgroup , "---- new cliques ----" , show newCliques ] -} combineGroups :: EquivalenceGroup info -> EquivalenceGroup info -> EquivalenceGroup info combineGroups eqgroup1 eqgroup2 = EQGroup { vertices = vertices eqgroup1 ++ vertices eqgroup2 , edges = edges eqgroup1 ++ edges eqgroup2 , cliques = cliques eqgroup1 `combineCliqueList` cliques eqgroup2 } ---------------------------------------------------------------------- -- * Removing parts from an equivalence group removeEdge :: EdgeId -> EquivalenceGroup info -> EquivalenceGroup info removeEdge edge eqgroup = let p (e, _) = edge /= e in eqgroup { edges = filter p (edges eqgroup) } removeClique :: Clique -> EquivalenceGroup info -> EquivalenceGroup info removeClique clique eqgroup = eqgroup { cliques = filter (not . (`isSubsetClique` clique)) (cliques eqgroup) } splitGroup :: EquivalenceGroup info -> [EquivalenceGroup info] splitGroup eqgroup = let (vs, es, cs) = (vertices eqgroup, edges eqgroup, cliques eqgroup) eqcs = map (\(a, b) -> insertVertex a b emptyGroup) vs addClique clique groups = let is = childrenInClique clique (gs1, gs2) = partition (any ((`elem` is) . fst) . vertices) groups in insertClique clique (foldr combineGroups emptyGroup gs1) : gs2 addEdge (edge@(EdgeId v1 v2 _), info) groups = let is = [v1, v2] (gs1, gs2) = partition (any ((`elem` is) . fst) . vertices) groups in insertEdge edge info (foldr combineGroups emptyGroup gs1) : gs2 in foldr addEdge (foldr addClique eqcs cs) es ---------------------------------------------------------------------- -- * Interrogating an equivalence group constants :: EquivalenceGroup info -> [String] constants eqgroup = nub [ s | (_, (VCon s, _)) <- vertices eqgroup ] consistent :: EquivalenceGroup info -> Bool consistent eqgroup = case constants eqgroup of [] -> True [_] -> null [ () | (_, (VApp _ _, _)) <- vertices eqgroup ] _ -> False equalPaths :: S.Set VertexId -> VertexId -> [VertexId] -> EquivalenceGroup info -> TypeGraphPath info equalPaths without start targets eqgroup = reduceNumberOfPaths $ tailSharingBy (\(e1, _) (e2, _) -> e1 `compare` e2) $ rec start (edgeList, cliqueList) where -- msg = "Path from "++show start++" to "++show targets++" without "++show (S.elems without) edgeList = let p (EdgeId v1 v2 _, _) = not (v1 `S.member` without) && not (v2 `S.member` without) in filter p (edges eqgroup) cliqueList = let f = filter (not . (`S.member` without) . child) . triplesInClique in map f (cliques eqgroup) targetSet = S.fromList targets -- Allow a second visit of a clique in a path? secondCliqueVisit = False rec :: VertexId -> ([(EdgeId, info)], [[ParentChild]]) -> TypeGraphPath info rec v1 (es, cs) | v1 `S.member` targetSet = Empty | otherwise = let (edges1,es' ) = partition (\(EdgeId a _ _, _) -> v1 == a) es (edges2,es'') = partition (\(EdgeId _ a _, _) -> v1 == a) es' (neighbourCliques, otherCliques) = partition ((v1 `elem`) . map child) cs rest@(_, restCliques) | secondCliqueVisit = (es'', removeFromClique v1 neighbourCliques ++ otherCliques) | otherwise = (es'', otherCliques) in altList $ map (\(EdgeId _ neighbour edgeNr, info) -> Step (EdgeId v1 neighbour edgeNr, Initial info) :+: rec neighbour rest) edges1 ++ map (\(EdgeId neighbour _ edgeNr, info) -> Step (EdgeId v1 neighbour edgeNr, Initial info) :+: rec neighbour rest) edges2 ++ concatMap (\list -> let (sources, others) = partition ((v1==) . child) list sourceParents = map parent sources neighbours = nub (map child others) f neighbour = altList [ beginPath :+: restPath | pc <- others , child pc == neighbour , let beginPath = altList1 (map g sourceParents) restPath | secondCliqueVisit = rec neighbour (es'', map (filter (/= pc)) restCliques) | otherwise = rec neighbour rest g sp = Step ( EdgeId v1 neighbour impliedEdgeNr , Implied (childSide pc) sp (parent pc) ) ] in if null sources then [] else map f neighbours) neighbourCliques removeFromClique :: VertexId -> [[ParentChild]] -> [[ParentChild]] removeFromClique vid = let p = (> 1) . length f = filter ((/=vid) . child) in filter p . map f typeOfGroup :: OrderedTypeSynonyms -> EquivalenceGroup info -> Maybe Tp typeOfGroup synonyms eqgroup | length allConstants > 1 = Nothing | not (null allConstants) && not (null allApplies) = Nothing | not (null allOriginals) = Just (theBestType synonyms allOriginals) | not (null allConstants) = Just (TCon (head allConstants)) | not (null allApplies) = Just $ let (VertexId l, VertexId r) = head allApplies in (TApp (TVar l) (TVar r)) | otherwise = Just (TVar (head allVariables)) where allVariables = [ i | (VertexId i, _) <- vertices eqgroup ] allConstants = nub [ s | (_, (VCon s, _)) <- vertices eqgroup ] allApplies = [ (l, r) | (_, (VApp l r, _)) <- vertices eqgroup ] allOriginals = [ tp | (_, (_, Just tp)) <- vertices eqgroup ] -- If I cannot select a best type at this point, an arbitary type is returned. -- This is because I cannot see "inside" the types -- Todo: improve theBestType :: OrderedTypeSynonyms -> Tps -> Tp theBestType synonyms tps = let f t1 t2 = fromMaybe t1 (equalUnderTypeSynonyms synonyms t1 t2) in foldr1 f tps -- Check for some invariants: identity if everything is okay, otherwise an internal error checkGroup :: EquivalenceGroup info -> EquivalenceGroup info checkGroup = test c2 . test c1 where test p eqGroup = if p eqGroup then error "Check failed for equivalence group" else eqGroup c1 eqGroup = hasDouble (concatMap triplesInClique $ cliques eqGroup) c2 eqGroup = any ((<2) . length . triplesInClique) (cliques eqGroup) hasDouble [] = False hasDouble (x:xs) = x `elem` xs || hasDouble xs