Commit 3fd38871 authored by Sven Keidel's avatar Sven Keidel

move powersets and galois connections to lib

parent 83b52d4d
......@@ -2,7 +2,7 @@
let
hsEnv = pkgs.haskellPackages.ghcWithPackages(p: with p; [
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion fgl
]);
in pkgs.stdenv.mkDerivation {
......
......@@ -10,7 +10,6 @@ import Prelude hiding (map,(.),id)
import Control.Category
import Control.Applicative
import Control.Monad
import Control.Monad.Deduplicate
import Data.Sequence (Seq)
import Data.Hashable
......@@ -25,9 +24,7 @@ newtype Pow a = Pow (Seq a) deriving (Eq, Functor, Applicative, Monad, Alternati
instance (Eq a, Hashable a) => PreOrd (Pow a) where
as bs = all (`H.member` toHashSet as) (toHashSet bs)
instance (Eq a, Hashable a) => PartOrd (Pow a)
instance (Eq a, Hashable a) => Lattice (Pow a) where
instance (Eq a, Hashable a) => Complete (Pow a) where
as bs = as `union` bs
instance Show a => Show (Pow a) where
......@@ -53,7 +50,6 @@ fromFoldable = foldMap return
size :: Foldable f => f a -> Int
size = length
instance MonadDeduplicate Pow where
dedup = fromFoldable . toHashSet
dedup :: (Hashable a, Eq a) => Pow a -> Pow a
dedup = fromFoldable . toHashSet
......@@ -18,14 +18,20 @@ library
exposed-modules: Data.Order,
Data.Boolean,
Data.Interval,
Data.Powerset,
Data.Sign,
Data.GaloisConnection,
Data.Error,
Data.FreeCompletion,
Data.FreeCoCompletion,
Control.Arrow.Fail
-- other-modules:
build-depends: base,
containers,
numeric-limits,
unordered-containers,
hashable,
mtl
hs-source-dirs: src/
default-language: Haskell2010
......
......@@ -165,32 +165,6 @@ instance IsTerm Term Interp where
numberLiteral = arr NumberLiteral
stringLiteral = arr StringLiteral
instance PreOrd Term where
t1 t2 = case (t1,t2) of
(Cons c ts,Cons c' ts') -> c == c' && ts ts'
(StringLiteral s, StringLiteral s') -> s == s'
(NumberLiteral n, NumberLiteral n') -> n == n'
(_, _) -> False
instance PartOrd Term
instance Lattice (Complete Term) where
t1 t2 = case (t1,t2) of
(Complete (Cons c ts), Complete (Cons c' ts'))
| c == c' ->
Cons c <$> (Complete ts Complete ts')
| otherwise -> Top
(Complete (StringLiteral s), Complete (StringLiteral s'))
| s == s' -> Complete (StringLiteral s)
| otherwise -> Top
(Complete (NumberLiteral n), Complete (NumberLiteral n'))
| n == n' -> Complete (NumberLiteral n)
| otherwise -> Top
(_, _) -> Top
instance BoundedLattice (Complete Term) where
top = Top
instance TermUtils Term where
convertToList ts = case ts of
(x:xs) -> Cons "Cons" [x,convertToList xs]
......@@ -205,12 +179,6 @@ instance TermUtils Term where
height (StringLiteral _) = 1
height (NumberLiteral _) = 1
instance Lattice Term where
() = undefined
instance BoundedLattice Term where
top = undefined
instance Show Term where
show (Cons c ts) = show c ++ if null ts then "" else show ts
show (StringLiteral s) = show s
......
......@@ -10,7 +10,7 @@ import Control.Monad.Reader
import Control.Monad.State (StateT(..))
import Data.Order
class (Lattice s,Monad m) => MonadJoin s m | m -> s where
class (Complete s,Monad m) => MonadJoin s m | m -> s where
get :: m s
get = state (\s -> (s,s))
......@@ -49,7 +49,7 @@ instance Monad m => Monad (JoinT s m) where
(a,s') <- f s
runJoinT (k a) s'
instance (Lattice s, Monad m) => MonadJoin s (JoinT s m) where
instance (Complete s, Monad m) => MonadJoin s (JoinT s m) where
state f = JoinT (\s -> return (f s))
instance MonadTrans (JoinT s) where
......
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Monad.Powerset where
import Data.Powerset
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Deduplicate
import Control.Monad.Join (MonadJoin)
import qualified Control.Monad.Join as J
newtype PowT m a = PowT { runPowT :: m (Pow a) }
mapPowT :: (m (Pow a) -> n (Pow b)) -> PowT m a -> PowT n b
mapPowT f (PowT p) = PowT (f p)
{-# INLINE mapPowT #-}
instance Functor m => Functor (PowT m) where
fmap f = mapPowT (fmap (fmap f))
instance Monad m => Applicative (PowT m) where
pure = return
(<*>) = ap
instance Monad m => Monad (PowT m) where
return x = PowT (return (return x))
(PowT f) >>= k = PowT $ do
r <- f
join <$> mapM (runPowT . k) r
instance MonadTrans PowT where
lift = PowT . fmap return
instance MonadState s m => MonadState s (PowT m) where
state f = lift (state f)
instance MonadReader r m => MonadReader r (PowT m) where
ask = lift ask
local = mapPowT . local
instance Monad m => Alternative (PowT m) where
empty = mzero
(<|>) = mplus
instance Monad m => MonadPlus (PowT m) where
mzero = PowT $ return mzero
mplus (PowT f) (PowT g) = PowT $ mplus <$> f <*> g
instance MonadJoin j m => MonadJoin j (PowT m) where
state f = lift (J.state f)
instance Monad m => MonadDeduplicate (PowT m) where
dedup = mapPowT (fmap dedup)
......@@ -72,8 +72,6 @@ instance MonadDeduplicate m => MonadDeduplicate (ResultT m) where
instance PreOrd (m (Result a)) => PreOrd (ResultT m a) where
(ResultT m1) (ResultT m2) = m1 m2
instance PartOrd (m (Result a)) => PartOrd (ResultT m a) where
instance Lattice (m (Result a)) => Lattice (ResultT m a) where
instance Complete (m (Result a)) => Complete (ResultT m a) where
(ResultT m1) (ResultT m2) = ResultT (m1 m2)
......@@ -20,9 +20,7 @@ instance Show a => Show (Pow a) where
instance PreOrd a => PreOrd (Pow a) where
as bs = all (\x -> any (x ) bs) as
instance PartOrd a => PartOrd (Pow a)
instance PartOrd a => Lattice (Pow a) where
instance PreOrd a => Complete (Pow a) where
as bs = as `P.union` bs
instance MonadDeduplicate Pow where
......
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Order where
import Prelude hiding ((.),map)
import Control.Arrow
import Control.Monad.Reader
import Control.Monad.State
import Data.Complete
-- REMINDER TO SELF: DO NOT ADD EXTRA PARAMETER FOR STATIC INFORMATION TO ORDERING FUNCTION!!!
-- IT MAKES THE CODE MUCH MORE COMPLICATED.
-- | Reflexive, transitive order
class PreOrd x where
() :: x -> x -> Bool
-- | Reflexive, transitive and anti-symmetric order
class PreOrd x => PartOrd x
-- | Reflexive, transitive, anti-symmetric and complete order
class PartOrd x => Lattice x where
() :: x -> x -> x
class Lattice x => BoundedLattice x where
top :: x
lub :: (Foldable f, Lattice x) => f x -> x
lub = foldr1 ()
instance PreOrd x => PreOrd (Complete x) where
c1 c2 = case (c1,c2) of
(_,Top) -> True
(Complete x, Complete y) -> x y
(_,_) -> False
instance PartOrd x => PartOrd (Complete x) where
instance (PartOrd x, Lattice (Complete x),
PartOrd y, Lattice (Complete y)) => Lattice (Complete (x,y)) where
c d = case (c,d) of
(Complete (x1,y1), Complete (x2,y2)) ->
let (z1,z2) = (Complete x1,Complete y1) (Complete x2,Complete y2)
in (,) <$> z1 <*> z2
_ -> Top
instance (PreOrd a,PreOrd b) => PreOrd (a,b) where
(a1,b1) (a2,b2) = a1 a2 && b1 b2
instance (PartOrd a, PartOrd b) => PartOrd (a,b)
instance (Lattice a, Lattice b) => Lattice (a,b) where
(a1,b1) (a2,b2) = (a1 a2,b1 b2)
instance PreOrd a => PreOrd [a] where
l1 l2 = case (l1,l2) of
(a:as,b:bs) -> a b && as bs
([],[]) -> True
(_,_) -> False
instance PartOrd a => PartOrd [a] where
-- wrapComplete :: ArrowChoice c => c (x,y) (Complete z) -> c (Complete x, Complete y) (Complete z)
-- wrapComplete f = proc xs -> case xs of
-- (Complete x, Complete y) -> f -< (x,y)
-- _ -> returnA -< Top
instance (PartOrd x, Lattice (Complete x)) => Lattice (Complete [x]) where
l1 l2 = case (l1,l2) of
(Complete (a: as), Complete (b:bs)) ->
let c = Complete a Complete b
cs = Complete as Complete bs
in (:) <$> c <*> cs
(Complete [], Complete []) -> Complete []
(_,_) -> Top
instance PreOrd a => PreOrd (Maybe a) where
m1 m2 = case (m1,m2) of
(Just x,Just y) -> x y
(Nothing, Nothing) -> True
(_,_) -> False
instance PartOrd a => PartOrd (Maybe a)
instance PreOrd Int where
x y = x <= y
instance PartOrd Int
instance PreOrd () where
() () = True
instance PartOrd ()
instance Lattice () where
() () = ()
instance Lattice (Complete ()) where
c1 c2 = case (c1,c2) of
(_,Top) -> Top
(Top,_) -> Top
(Complete (),Complete ()) -> Complete ()
instance PreOrd (m b) => PreOrd (Kleisli m a b) where
_ _ = error "pointwise ordering on function space"
instance PartOrd (m b) => PartOrd (Kleisli m a b) where
instance Lattice (m b) => Lattice (Kleisli m a b) where
Kleisli f Kleisli g = Kleisli $ \x -> f x g x
instance PreOrd (m a) => PreOrd (ReaderT r m a) where
_ _ = error "pointwise ordering on function space"
instance PartOrd (m a) => PartOrd (ReaderT r m a) where
instance Lattice (m a) => Lattice (ReaderT r m a) where
ReaderT f ReaderT g = ReaderT $ \r -> f r g r
instance PreOrd (m (a,s)) => PreOrd (StateT s m a) where
_ _ = error "pointwise ordering on function space"
instance PartOrd (m (a,s)) => PartOrd (StateT s m a) where
instance Lattice (m (a,s)) => Lattice (StateT s m a) where
StateT f StateT g = StateT $ \s -> f s g s
......@@ -83,8 +83,6 @@ instance PreOrd a => PreOrd (Result a) where
(Fail, Fail) -> True
(_,_) -> False
instance (PartOrd a) => PartOrd (Result a)
instance Galois x y => Galois (Result x) (Result y) where
alpha = fmap alpha
gamma = fmap gamma
......@@ -60,9 +60,7 @@ instance PreOrd a => PreOrd (UncertainResult a) where
(Fail, SuccessOrFail _) -> True
(_, _) -> False
instance PartOrd a => PartOrd (UncertainResult a)
instance Lattice a => Lattice (UncertainResult a) where
instance Complete a => Complete (UncertainResult a) where
m1 m2 = case (m1,m2) of
(Success x, Success y) -> Success (x y)
(Success x, Fail) -> SuccessOrFail x
......
......@@ -28,7 +28,6 @@ import Control.Monad.Result
import Control.Monad.State hiding (fail,sequence)
import Control.Monad.Deduplicate
import Data.Complete
import Data.Constructor
import Data.Foldable (foldr')
import Data.HashMap.Lazy (HashMap)
......@@ -36,6 +35,7 @@ import qualified Data.HashMap.Lazy as M
import Data.Hashable
import Data.Order
import Data.GaloisConnection
import Data.FreeCompletion
import Data.Powerset hiding (size)
import qualified Data.Powerset as P
import qualified Data.AbstractPowerset as A
......@@ -56,7 +56,7 @@ data Term
newtype TermEnv = TermEnv (HashMap TermVar Term) deriving (Show,Eq,Hashable)
newtype Interp a b = Interp (Kleisli (ReaderT (StratEnv,Int) (StateT TermEnv (ResultT A.Pow))) a b)
deriving (Category,Arrow,ArrowChoice,ArrowApply,ArrowTry,ArrowZero,ArrowPlus,ArrowDeduplicate,PreOrd,PartOrd,Lattice)
deriving (Category,Arrow,ArrowChoice,ArrowApply,ArrowTry,ArrowZero,ArrowPlus,ArrowDeduplicate,PreOrd,Complete)
runInterp :: Interp a b -> Int -> StratEnv -> TermEnv -> a -> A.Pow (Result (b,TermEnv))
runInterp (Interp f) i senv tenv a = runResultT (runStateT (runReaderT (runKleisli f a) (senv,i)) tenv)
......@@ -182,7 +182,7 @@ instance IsTerm Term Interp where
numberLiteral = arr NumberLiteral
stringLiteral = arr StringLiteral
instance BoundedLattice (Interp () Term) where
instance UpperBounded (Interp () Term) where
top = proc () -> success failA -< Wildcard
instance ArrowFix Interp Term where
......@@ -203,7 +203,7 @@ instance Soundness Interp where
abst = dedup $ runInterp g i senv (alpha (fmap snd xs)) (alpha (fmap fst xs))
in counterexample (printf "%s ⊑/ %s" (show con) (show abst)) $ con abst
instance BoundedLattice Term where
instance UpperBounded Term where
top = Wildcard
instance TermUtils Term where
......@@ -230,13 +230,11 @@ instance PreOrd Term where
(NumberLiteral n, NumberLiteral n') -> n == n'
(_, _) -> False
instance PartOrd Term
instance Lattice Term where
instance Complete Term where
t1 t2 = case (t1,t2) of
(Cons c ts, Cons c' ts')
| c == c' -> case Complete ts Complete ts' of
Complete ts'' -> Cons c ts''
| c == c' -> case Lower ts Lower ts' of
Lower ts'' -> Cons c ts''
_ -> Wildcard
| otherwise -> Wildcard
(StringLiteral s, StringLiteral s')
......@@ -249,11 +247,6 @@ instance Lattice Term where
(_, Wildcard) -> Wildcard
(_, _) -> Wildcard
instance Lattice (Complete Term) where
x y = case (x,y) of
(Complete t1, Complete t2) -> Complete (t1 t2)
(_,_) -> Top
instance Galois (P.Pow C.Term) Term where
alpha = lub . fmap go
where
......@@ -322,9 +315,7 @@ instance PreOrd TermEnv where
TermEnv env1 TermEnv env2 =
Prelude.all (\v -> M.lookup v env1 M.lookup v env2) (dom env2)
instance PartOrd TermEnv
instance Lattice TermEnv where
instance Complete TermEnv where
TermEnv env1' TermEnv env2' = go (dom env1') env1' env2' M.empty
where
go vars env1 env2 env3 = case vars of
......
......@@ -26,16 +26,12 @@ library
Control.Arrow.Deduplicate,
Control.Monad.Deduplicate,
Control.Monad.Join,
Control.Monad.Powerset,
Control.Monad.Result,
Control.Monad.Try,
Data.ATerm,
Data.Constructor,
Data.Powerset,
Data.AbstractPowerset,
Data.Result,
Data.Order,
Data.GaloisConnection,
Data.Complete,
Data.TypedResult,
Data.Term,
......@@ -52,13 +48,12 @@ library
Soundness
build-depends: base,
sturdy-lib,
arrows,
deepseq,
QuickCheck,
attoparsec,
containers,
fgl,
hashable,
fgl,
unordered-containers,
mtl,
pretty,
......@@ -69,7 +64,6 @@ library
Executable case-studies
ghc-options: -Wall
Build-Depends: base,
arrows,
deepseq,
QuickCheck,
attoparsec,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment