 ...

Commits (5)
 ... ... @@ -3,9 +3,9 @@ module Data.Abstract.Narrowing where import Data.Order class PreOrd a => Narrowing a where -- | For △ holds that, i.e. if x ⊑ y then y ⊑ x ▽ y ⊑ x. -- | For △ holds that, i.e. if x ⊑ y then x ⊑ (x △ y) ⊑ y. -- Furthermore, iterating ▽ on an descending chain has to stabilize: -- Let x1, x2, ... xn be an infinite descending chain, then x1, x1 ▽ x2, (x1 ▽ x2) ▽ x3, ... has a limit. -- Let x1, x2, ... xn be an infinite descending chain, then x1, x1 △ x2, (x1 △ x2) △ x3, ... has a limit. -- Notice that widening and narrowing are *not* dual. (△) :: a -> a -> a ... ...
This diff is collapsed.
 {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE RecordWildCards #-} module Data.Abstract.TreeGrammar.ClosedSet where import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as M import Data.HashSet (HashSet) import qualified Data.HashSet as H import Data.IntSet(IntSet) import qualified Data.IntSet as S import Data.IntMap(IntMap) import qualified Data.IntMap as IM import Data.Identifiable data ClosedSet a = ClosedSet { fresh :: Int , upper :: HashMap a IntSet , lower :: IntMap (HashSet a) } deriving (Show) empty :: ClosedSet a empty = ClosedSet 0 M.empty IM.empty elems :: ClosedSet a -> [HashSet a] elems c = IM.elems (lower c) insert :: (Identifiable a) => HashSet a -> ClosedSet a -> ClosedSet a insert l u = let n = fresh u in u { fresh = n+1 , upper = foldl (\m a -> M.insertWith (const (S.insert n)) a (S.singleton n) m) (upper u) l , lower = IM.insert n l (lower u) } insertUpper :: (Identifiable a) => HashSet a -> ClosedSet a -> ClosedSet a insertUpper l u | memberUpper l u = u | otherwise = insert l u insertLower :: (Identifiable a) => HashSet a -> ClosedSet a -> ClosedSet a insertLower l u | memberLower l u = u | otherwise = insert l u member :: (Identifiable a) => (HashSet a -> Bool) -> HashSet a -> ClosedSet a -> Bool member p l (ClosedSet {..}) = let u = foldl (\s a -> S.union s (M.lookupDefault S.empty a upper)) S.empty l in any (\n -> p (IM.findWithDefault H.empty n lower)) (S.toList u) memberUpper :: (Identifiable a) => HashSet a -> ClosedSet a -> Bool memberUpper l = member (`subset` l) l memberLower :: (Identifiable a) => HashSet a -> ClosedSet a -> Bool memberLower l u = member (l `subset`) l u subset :: Identifiable a => HashSet a -> HashSet a -> Bool subset xs ys = all (`H.member` ys) xs
 ... ... @@ -9,7 +9,7 @@ import Data.Text(Text,pack,unpack) import Data.Hashable import Text.Printf class NonTerminal n where class Show n => NonTerminal n where type Gen n :: * fresh :: Maybe String -> State (Gen n) n generate :: forall (g :: * -> (* -> *) -> *) t. ... ...
 module Data.Abstract.TreeGrammar.OrdMap ( OrdMap , empty , insertLeq , insertNotLeq , leq , upper ) where import Prelude hiding (Ordering,compare) import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as M import Data.HashSet (HashSet) import Data.Identifiable import qualified Data.Abstract.Boolean as A import Data.Abstract.TreeGrammar.ClosedSet (ClosedSet) import qualified Data.Abstract.TreeGrammar.ClosedSet as C -- | Datatype that describes a subset of a heterogenous order with -- fast access to the lower and upper sets of elements. data OrdMap n1 n2 = OrdMap (HashMap n1 (Boundary n2)) deriving (Show) data Boundary n = Boundary { comparable :: ClosedSet n, incomparable :: ClosedSet n } deriving (Show) empty :: OrdMap n1 n2 empty = OrdMap M.empty insertLeq :: (Identifiable n1, Identifiable n2) => n1 -> HashSet n2 -> OrdMap n1 n2 -> OrdMap n1 n2 insertLeq n1 n2 (OrdMap o) = OrdMap \$ M.insertWith (const (\b -> b {comparable = C.insertUpper n2 (comparable b)})) n1 (Boundary (C.insert n2 C.empty) C.empty) o insertNotLeq :: (Identifiable n1, Identifiable n2) => n1 -> HashSet n2 -> OrdMap n1 n2 -> OrdMap n1 n2 insertNotLeq n1 n2 (OrdMap o) = OrdMap \$ M.insertWith (const (\b -> b {incomparable = C.insertLower n2 (incomparable b)})) n1 (Boundary C.empty (C.insert n2 C.empty)) o leq :: (Identifiable n1, Identifiable n2) => n1 -> HashSet n2 -> OrdMap n1 n2 -> A.Bool leq n1 n2 (OrdMap o) = case M.lookup n1 o of Just bounds | C.memberUpper n2 (comparable bounds) -> A.True | C.memberLower n2 (incomparable bounds) -> A.False _ -> A.Top upper :: Identifiable n1 => n1 -> OrdMap n1 n2 -> [HashSet n2] upper n1 (OrdMap o) = case M.lookup n1 o of Just bounds -> C.elems (comparable bounds) Nothing -> []
 ... ... @@ -24,7 +24,6 @@ import qualified Data.Hashable as Hash import qualified Data.Traversable as T import qualified Data.List as L import Data.Functor.Identity import qualified Data.Abstract.Either as A import GHC.Exts (IsList(..)) import Text.Printf ... ... @@ -36,11 +35,11 @@ class Terminal t where productive :: Identifiable n => HashSet n -> t n -> Bool filter :: (n -> Bool) -> t n -> t n determinize :: (Identifiable n, Identifiable n', Applicative f) => (HashSet n -> f n') -> t n -> f (t n') subsetOf :: (Identifiable n, Identifiable n', MonadPlus f) => ([(n,n')] -> f ()) -> t n -> t n' -> f () subsetOf :: (Identifiable n, Identifiable n', MonadPlus f) => ((HashSet [n],HashSet [n']) -> f ()) -> t n -> t n' -> f () intersection :: (Identifiable n1, Identifiable n2, Identifiable n', Applicative f) => ((n1,n2) -> f n') -> t n1 -> t n2 -> f (t n') union :: (Identifiable n1, Identifiable n2, Identifiable n', Applicative f) => (A.Either n1 n2 -> f n') -> t n1 -> t n2 -> f (t n') traverse :: (Identifiable n', Applicative f) => (n -> f n') -> t n -> f (t n') hashWithSalt :: (Identifiable n, Monad f) => (Int -> n -> f Int) -> Int -> t n -> f Int difference :: t n -> t n -> Int map :: (Identifiable n', Terminal t) => (n -> n') -> t n -> t n' map f t = runIdentity (traverse (Identity . f) t) ... ... @@ -82,18 +81,8 @@ instance Terminal Constr where guard (m1 `subsetKeys` m2) forM_ (M.intersectionWith (,) m1 m2) \$ \(a1,a2) -> do guard (a1 `subsetKeys'` a2) forM_ (IM.intersectionWith (,) a1 a2) \$ \(l1,l2)-> do forM_ l1 \$ \as -> msum [ leq (zip as bs) | bs <- H.toList l2 ] union f (Constr m1) (Constr m2) = fmap Constr \$ T.traverse (T.traverse (\u -> case u of A.Left cs1 -> traverseHashSet (T.traverse (f . A.Left)) cs1 A.Right cs2 -> traverseHashSet (T.traverse (f . A.Right)) cs2 A.LeftRight cs1 cs2 -> H.fromList <\$> T.traverse (T.traverse (f . uncurry A.LeftRight)) (cross cs1 cs2))) \$ M.unionWith (IM.unionWith (\(A.Left cs1) (A.Right cs2) -> A.LeftRight cs1 cs2)) (M.map (IM.map A.Left) m1) (M.map (IM.map A.Right) m2) forM_ (IM.intersectionWith (,) a1 a2) \$ \(l1,l2) -> do leq (l1, l2) intersection f (Constr m1) (Constr m2) = fmap Constr \$ T.traverse (T.traverse (fmap H.fromList . T.traverse (T.traverse f))) ... ... @@ -102,6 +91,8 @@ instance Terminal Constr where traverse f (Constr m) = Constr <\$> T.traverse (T.traverse (traverseHashSet (T.traverse f))) m hashWithSalt f s m = foldM (\s' (c,ts) -> foldM f (s' `Hash.hashWithSalt` c) ts) s (toList m) difference _ _ = 0 traverseHashSet :: (Applicative f, Identifiable b) => (a -> f b) -> HashSet a -> f (HashSet b) traverseHashSet f h = H.fromList <\$> T.traverse f (H.toList h) ... ...