...
 
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)
......
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
module Data.Abstract.TreeGrammar.Widening where
-- import Control.Monad.State
-- import Control.Monad.Reader
-- import Control.Monad.Writer
-- import Data.HashMap.Lazy (HashMap)
-- import qualified Data.HashMap.Lazy as M
-- import Data.HashSet (HashSet)
-- import qualified Data.HashSet as H
-- import Data.Abstract.TreeGrammar (Grammar,IsGrammar,ProdMap)
-- import qualified Data.Abstract.TreeGrammar as G
-- import qualified Data.Abstract.TreeGrammar.Terminal as T
-- import Data.Abstract.TreeGrammar.OrdMap (OrdMap)
-- import qualified Data.Abstract.TreeGrammar.OrdMap as O
-- import Data.Abstract.Widening (Widening,Stable(..))
-- import Data.Order
-- import Data.Identifiable
-- import Data.Semigroup
-- import Data.Maybe
-- import Data.Foldable
-- import Data.Ord (comparing)
-- import qualified Data.List as L
-- widening :: forall n t. (IsGrammar n t,Eq (t n))
-- => (Grammar n t -> Grammar n t -> Grammar n t)
-- -> Widening (Grammar n t)
-- widening w g1 g2
-- | g2 ⊑ g1 = (Stable,g1)
-- | g1 ⊑ g2 = (Instable,w g1 g2)
-- | otherwise = (Instable,w g1 (G.minimize (g1 `G.union` g2)))
-- widening' :: IsGrammar n2 t => Grammar n2 t -> Grammar n2 t
-- widening' = _
-- where
-- go = _
-- data WidenState n1 n2 t = WidenState
-- { ordN1N2 :: OrdMap [n1] [n2]
-- , ordN2N2 :: OrdMap [n2] [n2]
-- , result :: Grammar n2 t
-- }
-- widening' :: forall n1 n2 t. (IsGrammar n1 t, IsGrammar n2 t)
-- => Grammar n1 t -> Grammar n2 t -> Grammar n2 t
-- widening' g1 g2 =
-- let Just s = execStateT (runReaderT (go H.empty (G.start g1)) []) (WidenState O.empty O.empty g2)
-- in result s
-- where
-- go :: (MonadReader [HashSet n2] m, MonadState (WidenState n1 n2 t) m, MonadPlus m) => HashSet n1 -> n1 -> m ()
-- go seen n1
-- | H.member n1 seen = return ()
-- | otherwise = do
-- ord <- gets ordN1N2
-- let n2s = flatten $ O.upper [n1] ord
-- if depth n1 d1 == 0
-- then mapM_ removeClash (H.filter (\n2 -> depth n2 d2 > 0) n2s)
-- else local (n2s:) $ mapM_ (go (H.insert n1 seen)) (T.nonTerminals (G.lookup n1 g1))
-- d1 = calcDepth g1
-- d2 = calcDepth g2
-- removeClash :: (MonadReader [HashSet n2] m, MonadState (WidenState n1 n2 t) m, MonadPlus m) => n2 -> m ()
-- removeClash n = do
-- ancestors <- ask
-- let ancestors' = L.sortBy (comparing (\x -> depth x d2))
-- $ filter (\x -> depth x d2 > depth n d2)
-- $ H.toList (mconcat ancestors)
-- replaceArc n ancestors' `mplus` unionNodes n ancestors'
-- replaceArc :: (MonadReader [HashSet n2] m, MonadState (WidenState n1 n2 t) m, MonadPlus m) => n2 -> [n2] -> m ()
-- replaceArc n ancestors = do
-- ancestor <- findGreaterAncestor n ancestors
-- modifyResult $ M.insert n (G.Rhs mempty [ancestor])
-- findGreaterAncestor :: (MonadState (WidenState n1 n2 t) m, MonadPlus m) => n2 -> [n2] -> m n2
-- findGreaterAncestor _ [] = mzero
-- findGreaterAncestor n (x:xs) = do
-- subset <- modifyN2N2 (g2 {G.start = n } `G.subsetOf'` g2 {G.start = x})
-- if subset
-- then return x
-- else findGreaterAncestor n xs
-- unionNodes :: (MonadReader [HashSet n2] m, MonadState (WidenState n1 n2 t) m, MonadPlus m) => n2 -> [n2] -> m ()
-- unionNodes n ancestors = do
-- ancestor <- findGoodAncestor n ancestors
-- modifyResult $ \ps -> M.insertWith (<>) ancestor (fold (M.lookup n ps))
-- $ M.insert n (G.Rhs mempty [ancestor]) ps
-- findGoodAncestor :: (MonadState (WidenState n1 n2 t) m) => n2 -> [n2] -> m n2
-- findGoodAncestor _ [] = error "findGoodAncestor n2 []"
-- findGoodAncestor n2 xs = do
-- g <- gets result
-- return $ minimumBy (comparing (\x -> T.difference (G.lookup n2 g) (G.lookup x g))) xs
-- modifyN1N2 :: MonadState (WidenState n1 n2 t) m => (OrdMap [n1] [n2] -> OrdMap [n1] [n2]) -> m ()
-- modifyN1N2 f = modify $ \s -> s { ordN1N2 = f (ordN1N2 s)}
-- modifyN2N2 :: MonadState (WidenState n1 n2 t) m => (OrdMap [n2] [n2] -> (a,OrdMap [n2] [n2])) -> m a
-- modifyN2N2 f = do
-- s <- get
-- let (a,o') = f (ordN2N2 s)
-- put $ s { ordN2N2 = o' }
-- return a
-- modifyResult :: MonadState (WidenState n1 n2 t) m => (ProdMap n2 t -> ProdMap n2 t) -> m ()
-- modifyResult f = modify $ \s ->
-- let g = (result s)
-- in s { result = g { G.productions = f (G.productions g) }}
-- flatten :: Identifiable x => [HashSet [x]] -> HashSet x
-- flatten x1 = H.fromList [ x | x2 <- x1, x3 <- H.toList x2, x <- x3 ]
-- depth :: forall n. Identifiable n => n -> HashMap n (Max Int) -> Max Int
-- depth n = depth' ([n] :: [n])
-- depth' :: (Foldable f, Identifiable n) => f n -> HashMap n (Max Int) -> Max Int
-- depth' xs d = foldMap (\n -> fromMaybe 0 (M.lookup n d)) xs
-- -- deepest :: (Foldable f, Identifiable n) => f n -> HashMap n (Max Int) -> n
-- -- deepest xs d = case foldl' (\m n -> m <> fmap (fmap (`Arg` n)) (M.lookup n d)) Nothing xs of
-- -- Just (Max (Arg _ n)) -> n
-- -- _ -> error "called function deepest on empty list"
-- calcDepth :: forall n t. IsGrammar n t => Grammar n t -> HashMap n (Max Int)
-- calcDepth g = execState (go H.empty (G.start g)) M.empty
-- where
-- go :: MonadState (HashMap n (Max Int)) m => HashSet n -> n -> m (Max Int)
-- go seen n
-- | H.member n seen = return 0
-- | otherwise = do
-- d <- execWriterT $ T.traverse (\n' -> tell =<< go (H.insert n seen) n')
-- $ G.lookup n g
-- let d' = d + 1
-- modify $ M.insert n d'
-- return d'
-- -- widthWidening :: (MonadState (WidenState n1 n2 t) m, MonadPlus m) => n1 -> m ()
-- -- widthWidening n1 = do
-- -- ord <- gets ordN1N2
-- -- let n2s = flatten $ O.upper [n1] ord
-- -- cs <- widenConstr _ union (G.lookup n1 g1) (G.lookup' n2s g2)
-- -- n2 <- union n2s
-- -- modifyResult $ M.insert n2 (G.Rhs cs mempty)
-- -- union :: (MonadState (WidenState n1 n2 t) m, MonadPlus m) => HashSet n2 -> m n2
-- -- union [x] = return x
-- -- union xs = do
-- -- m <- get
-- -- case M.lookup xs (unionMap m) of
-- -- Just n2 -> return n2
-- -- Nothing -> do
-- -- n2 <- fresh
-- -- modifyResult $ M.insert n2 (G.Rhs mempty xs)
-- -- return n2
module Data.OrdMap
( OrdMap
, empty
, insert
, compare
, Ordering (..)
)
where
import Prelude hiding (Ordering,compare)
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Identifiable
import Data.Order
import qualified Data.Abstract.Boolean as A
-- | 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,n2) Ordering)
data Ordering = LessThanEquals | Equivalent | GreaterThanEquals
| NotLessThanEquals | Incomparable | NotGreaterThanEquals
| StrictLessThan | StrictGreaterThan
deriving (Eq)
instance PreOrd Ordering where
LessThanEquals Equivalent = True
GreaterThanEquals Equivalent = True
NotLessThanEquals Incomparable = True
NotGreaterThanEquals Incomparable = True
LessThanEquals StrictLessThan = True
NotGreaterThanEquals StrictLessThan = True
GreaterThanEquals StrictGreaterThan = True
NotLessThanEquals StrictGreaterThan = True
x y = x == y
instance Complete Ordering where
LessThanEquals GreaterThanEquals = Equivalent
GreaterThanEquals LessThanEquals = Equivalent
NotLessThanEquals NotGreaterThanEquals = Incomparable
NotGreaterThanEquals NotLessThanEquals = Incomparable
LessThanEquals NotGreaterThanEquals = StrictLessThan
NotGreaterThanEquals LessThanEquals = StrictLessThan
GreaterThanEquals NotLessThanEquals = StrictGreaterThan
NotLessThanEquals GreaterThanEquals = StrictGreaterThan
x y | x y = y
| y x = x
| otherwise = error "The ordering is inconcistent"
empty :: OrdMap n1 n2
empty = OrdMap M.empty
insert :: (Identifiable n1, Identifiable n2) => n1 -> n2 -> Ordering -> OrdMap n1 n2 -> OrdMap n1 n2
insert n1 n2 ord (OrdMap m) = OrdMap $ M.insertWith () (n1,n2) ord m
compare :: (Identifiable n1,Identifiable n2) => n1 -> n2 -> Ordering -> OrdMap n1 n2 -> A.Bool
compare n1 n2 o1 (OrdMap m) = case M.lookup (n1,n2) m of
Just o2
| o1 o2 -> A.True
| o2 o1 -> A.Top
| otherwise -> A.False
Nothing -> A.Top
instance (Identifiable n1, Identifiable n2) => Semigroup (OrdMap n1 n2) where
(OrdMap m1) <> (OrdMap m2) = OrdMap (M.unionWith () m1 m2)
instance (Identifiable n1, Identifiable n2) => Monoid (OrdMap n1 n2) where
mempty = empty
mappend = (<>)
......@@ -2,13 +2,25 @@
module Data.Utils
( maybeHead
, fromMaybe
, pow
, powComplement
, powComplementPick
, powComplementN
, forAll
, exists
, module Data.Empty
, module Data.Singleton
)
where
import Data.Empty
import Data.Singleton
import Control.Arrow
import Control.Monad
-- import Data.Maybe
import qualified Data.IntMap as IM
import Data.Sequence (Seq)
import Data.Foldable(toList)
import Data.Empty
import Data.Singleton
fromMaybe :: (IsEmpty (f a), IsSingleton (f a), Elem (f a) ~ a) => Maybe a -> f a
fromMaybe (Just a) = singleton a
......@@ -17,3 +29,37 @@ fromMaybe Nothing = empty
maybeHead :: [a] -> Maybe a
maybeHead (a:_) = Just a
maybeHead [] = Nothing
pow :: [a] -> Seq [a]
pow = foldl (\xs x -> fmap (x:) xs<> xs) mempty
-- @powComplement M@ computes for a set M, the set { (X,M\X) | X in P(M) }
powComplement :: [a] -> Seq ([a], [a])
powComplement = foldl (\ys x -> (first (x:) <$> ys) <> (second (x:) <$> ys)) (pure ([],[]))
-- @powComplementN n M@ computes for a set M, the set { [X1,X2,X3] | X1 ⊆ M\∅, X2 ⊆ M\X1, X3 ⊆ M\(X1 ∪ X2) ... }
powComplementN :: Int -> [a] -> Seq [[a]]
powComplementN = go
where
go i notSeen
| i > 1 = do
(seen',notSeen') <- powComplement notSeen
rest <- go (i-1) notSeen'
return (seen':rest)
| otherwise = return [notSeen]
powComplementPick :: [[a]] -> Seq [[a]]
powComplementPick [] = return []
powComplementPick ([]:_) = return [[]]
powComplementPick l@(x:_) = do
ixs <- powComplementN (length l) [0..(length x - 1)]
return $ zipWith (\ix m -> IM.elems (IM.intersection m (IM.fromList [ (i,()) | i <- ix])))
ixs elements
where
elements = map (IM.fromList . zip [0..]) l
forAll :: (Foldable f, MonadPlus m) => f a -> (a -> m ()) -> m ()
forAll = forM_
exists :: (Foldable f, MonadPlus m) => f a -> (a -> m ()) -> m ()
exists l f = msum [ f x | x <- toList l ]
This diff is collapsed.
module UtilsSpec(main, spec) where
import Control.Arrow
import Data.List(sort)
import Data.Utils
import GHC.Exts
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec =
describe "Powersets" $ do
it "powComplement [1,2,3]" $
map (sort *** sort) (toList (powComplement [1,2,3::Int])) `shouldMatchList`
[ ([1,2,3],[])
, ([2,3],[1])
, ([1,3],[2])
, ([3],[1,2])
, ([1,2],[3])
, ([2],[1,3])
, ([1],[2,3])
, ([],[1,2,3])
]
it "powComplementN 3 [1,2]" $
map (map sort) (toList (powComplementN 3 [1,2::Int])) `shouldMatchList`
[ [[1,2],[],[]]
, [[1],[2],[]]
, [[1],[],[2]]
, [[2],[1],[]]
, [[2],[],[1]]
, [[],[1,2],[]]
, [[],[1],[2]]
, [[],[2],[1]]
, [[],[],[1,2]]
]
it "powComplementPick [[A,B],[C,D],[E,F]]" $
map (map sort) (toList (powComplementPick [["A","B"],["C","D"],["E","F"]])) `shouldMatchList`
[ [["A","B"],[],[]]
, [["A"],["D"],[]]
, [["A"],[],["F"]]
, [["B"],["C"],[]]
, [["B"],[],["E"]]
, [[],["C","D"],[]]
, [[],["C"],["F"]]
, [[],["D"],["E"]]
, [[],[],["E","F"]]
]
it "powComplementPick [[A,B]]" $
map (map sort) (toList (powComplementPick [["A","B"]])) `shouldMatchList` [[["A","B"]]]
it "powComplementPick [[]]" $
toList (powComplementPick [[] :: [Int]]) `shouldMatchList` [[[]]]
This diff is collapsed.
This diff is collapsed.