{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Algebra.Lattice.Free (
    Free (..),
    liftFree,
    lowerFree,
    substFree,
    retractFree,
    toExpr,
    ) where

import Prelude ()
import Prelude.Compat

import Algebra.Lattice
import Algebra.PartialOrd

import Control.Applicative          (liftA2)
import Control.Monad                (ap)
import Data.Data                    (Data, Typeable)
import GHC.Generics                 (Generic, Generic1)
import Math.NumberTheory.Logarithms (intLog2)

import qualified Algebra.Heyting.Free.Expr as E
import qualified Test.QuickCheck           as QC

-- $setup
-- >>> import Algebra.Lattice

-------------------------------------------------------------------------------
-- Free
-------------------------------------------------------------------------------

-- | Free distributive lattice.
--
-- `Eq` and `PartialOrd` instances aren't structural.
--
-- >>> (Var 'x' /\ Var 'y') == (Var 'y' /\ Var 'x' /\ Var 'x')
-- True
--
-- >>> Var 'x' == Var 'y'
-- False
--
-- This is /distributive/ lattice.
--
-- >>> import Algebra.Lattice.M3 -- non distributive lattice
-- >>> let x = M3a; y = M3b; z = M3c
-- >>> let lhs = Var x \/ (Var y /\ Var z)
-- >>> let rhs = (Var x \/ Var y) /\ (Var x \/ Var z)
--
-- 'Free' is distributive so
--
-- >>> lhs == rhs
-- True
--
-- but when retracted, values are inequal
--
-- >>> retractFree lhs == retractFree rhs
-- False
--
-- >>> (retractFree lhs, retractFree rhs)
-- (M3a,M3i)
--
data Free a
    = Var a
    | Free a :/\: Free a
    | Free a :\/: Free a
  deriving (Int -> Free a -> ShowS
forall a. Show a => Int -> Free a -> ShowS
forall a. Show a => [Free a] -> ShowS
forall a. Show a => Free a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Free a] -> ShowS
$cshowList :: forall a. Show a => [Free a] -> ShowS
show :: Free a -> String
$cshow :: forall a. Show a => Free a -> String
showsPrec :: Int -> Free a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Free a -> ShowS
Show, forall a b. a -> Free b -> Free a
forall a b. (a -> b) -> Free a -> Free b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Free b -> Free a
$c<$ :: forall a b. a -> Free b -> Free a
fmap :: forall a b. (a -> b) -> Free a -> Free b
$cfmap :: forall a b. (a -> b) -> Free a -> Free b
Functor, forall a. Eq a => a -> Free a -> Bool
forall a. Num a => Free a -> a
forall a. Ord a => Free a -> a
forall m. Monoid m => Free m -> m
forall a. Free a -> Bool
forall a. Free a -> Int
forall a. Free a -> [a]
forall a. (a -> a -> a) -> Free a -> a
forall m a. Monoid m => (a -> m) -> Free a -> m
forall b a. (b -> a -> b) -> b -> Free a -> b
forall a b. (a -> b -> b) -> b -> Free a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Free a -> a
$cproduct :: forall a. Num a => Free a -> a
sum :: forall a. Num a => Free a -> a
$csum :: forall a. Num a => Free a -> a
minimum :: forall a. Ord a => Free a -> a
$cminimum :: forall a. Ord a => Free a -> a
maximum :: forall a. Ord a => Free a -> a
$cmaximum :: forall a. Ord a => Free a -> a
elem :: forall a. Eq a => a -> Free a -> Bool
$celem :: forall a. Eq a => a -> Free a -> Bool
length :: forall a. Free a -> Int
$clength :: forall a. Free a -> Int
null :: forall a. Free a -> Bool
$cnull :: forall a. Free a -> Bool
toList :: forall a. Free a -> [a]
$ctoList :: forall a. Free a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Free a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Free a -> a
foldr1 :: forall a. (a -> a -> a) -> Free a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Free a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Free a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Free a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Free a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Free a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Free a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Free a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Free a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Free a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Free a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Free a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Free a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Free a -> m
fold :: forall m. Monoid m => Free m -> m
$cfold :: forall m. Monoid m => Free m -> m
Foldable, Functor Free
Foldable Free
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Free (m a) -> m (Free a)
forall (f :: * -> *) a. Applicative f => Free (f a) -> f (Free a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Free a -> m (Free b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Free a -> f (Free b)
sequence :: forall (m :: * -> *) a. Monad m => Free (m a) -> m (Free a)
$csequence :: forall (m :: * -> *) a. Monad m => Free (m a) -> m (Free a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Free a -> m (Free b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Free a -> m (Free b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Free (f a) -> f (Free a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Free (f a) -> f (Free a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Free a -> f (Free b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Free a -> f (Free b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Free a) x -> Free a
forall a x. Free a -> Rep (Free a) x
$cto :: forall a x. Rep (Free a) x -> Free a
$cfrom :: forall a x. Free a -> Rep (Free a) x
Generic, forall a. Rep1 Free a -> Free a
forall a. Free a -> Rep1 Free a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Free a -> Free a
$cfrom1 :: forall a. Free a -> Rep1 Free a
Generic1, Free a -> DataType
Free a -> Constr
forall {a}. Data a => Typeable (Free a)
forall a. Data a => Free a -> DataType
forall a. Data a => Free a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Free a -> Free a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Free a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Free a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Free a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Free a -> c (Free a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Free a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Free a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Free a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Free a -> c (Free a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Free a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Free a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Free a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Free a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Free a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
gmapT :: (forall b. Data b => b -> b) -> Free a -> Free a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Free a -> Free a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Free a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Free a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Free a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Free a))
dataTypeOf :: Free a -> DataType
$cdataTypeOf :: forall a. Data a => Free a -> DataType
toConstr :: Free a -> Constr
$ctoConstr :: forall a. Data a => Free a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Free a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Free a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Free a -> c (Free a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Free a -> c (Free a)
Data, Typeable)

infixr 6 :/\:
infixr 5 :\/:

liftFree :: a -> Free a
liftFree :: forall a. a -> Free a
liftFree = forall a. a -> Free a
Var

retractFree :: Lattice a => Free a -> a
retractFree :: forall a. Lattice a => Free a -> a
retractFree = forall b a. Lattice b => (a -> b) -> Free a -> b
lowerFree forall a. a -> a
id

substFree :: Free a -> (a -> Free b) -> Free b
substFree :: forall a b. Free a -> (a -> Free b) -> Free b
substFree Free a
z a -> Free b
k = Free a -> Free b
go Free a
z where
    go :: Free a -> Free b
go (Var a
x)    = a -> Free b
k a
x
    go (Free a
x :/\: Free a
y) = Free a -> Free b
go Free a
x forall a. Lattice a => a -> a -> a
/\ Free a -> Free b
go Free a
y
    go (Free a
x :\/: Free a
y) = Free a -> Free b
go Free a
x forall a. Lattice a => a -> a -> a
\/ Free a -> Free b
go Free a
y

lowerFree :: Lattice b => (a -> b) -> Free a -> b
lowerFree :: forall b a. Lattice b => (a -> b) -> Free a -> b
lowerFree a -> b
f = Free a -> b
go where
    go :: Free a -> b
go (Var a
x)    = a -> b
f a
x
    go (Free a
x :/\: Free a
y) = Free a -> b
go Free a
x forall a. Lattice a => a -> a -> a
/\ Free a -> b
go Free a
y
    go (Free a
x :\/: Free a
y) = Free a -> b
go Free a
x forall a. Lattice a => a -> a -> a
\/ Free a -> b
go Free a
y

toExpr :: Free a -> E.Expr a
toExpr :: forall a. Free a -> Expr a
toExpr (Var a
a)    = forall a. a -> Expr a
E.Var a
a
toExpr (Free a
x :/\: Free a
y) = forall a. Free a -> Expr a
toExpr Free a
x forall a. Expr a -> Expr a -> Expr a
E.:/\: forall a. Free a -> Expr a
toExpr Free a
y
toExpr (Free a
x :\/: Free a
y) = forall a. Free a -> Expr a
toExpr Free a
x forall a. Expr a -> Expr a -> Expr a
E.:\/: forall a. Free a -> Expr a
toExpr Free a
y

-------------------------------------------------------------------------------
-- Monad
-------------------------------------------------------------------------------

instance Applicative Free where
    pure :: forall a. a -> Free a
pure = forall a. a -> Free a
liftFree
    <*> :: forall a b. Free (a -> b) -> Free a -> Free b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Free where
    return :: forall a. a -> Free a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: forall a b. Free a -> (a -> Free b) -> Free b
(>>=)  = forall a b. Free a -> (a -> Free b) -> Free b
substFree

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

instance Lattice (Free a) where
    Free a
x /\ :: Free a -> Free a -> Free a
/\ Free a
y = Free a
x forall a. Free a -> Free a -> Free a
:/\: Free a
y
    Free a
x \/ :: Free a -> Free a -> Free a
\/ Free a
y = Free a
x forall a. Free a -> Free a -> Free a
:\/: Free a
y

instance Ord a => Eq (Free a) where
    == :: Free a -> Free a -> Bool
(==) = forall a. PartialOrd a => a -> a -> Bool
partialOrdEq

instance Ord a => PartialOrd (Free a) where
    leq :: Free a -> Free a -> Bool
leq Free a
x Free a
y = forall a. Ord a => Expr a -> Bool
E.proofSearch (forall a. Free a -> Expr a
toExpr Free a
x forall a. Expr a -> Expr a -> Expr a
E.:=>: forall a. Free a -> Expr a
toExpr Free a
y)

-------------------------------------------------------------------------------
-- Other instances
-------------------------------------------------------------------------------

instance QC.Arbitrary a => QC.Arbitrary (Free a) where
    arbitrary :: Gen (Free a)
arbitrary = forall a. (Int -> Gen a) -> Gen a
QC.sized Int -> Gen (Free a)
arb where
        arb :: Int -> Gen (Free a)
arb Int
n | Int
n forall a. Ord a => a -> a -> Bool
<= Int
0    = Gen (Free a)
prim
              | Bool
otherwise = forall a. [Gen a] -> Gen a
QC.oneof (Gen (Free a)
prim forall a. a -> [a] -> [a]
: [Gen (Free a)]
compound)
          where
            arb' :: Gen (Free a)
arb' = Int -> Gen (Free a)
arb (Int -> Int
intLog2 (forall a. Ord a => a -> a -> a
max Int
1 Int
n))

            compound :: [Gen (Free a)]
compound =
                [ forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Free a -> Free a -> Free a
(:/\:) Gen (Free a)
arb' Gen (Free a)
arb'
                , forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Free a -> Free a -> Free a
(:\/:) Gen (Free a)
arb' Gen (Free a)
arb'
                ]

        prim :: Gen (Free a)
prim = forall a. a -> Free a
Var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
QC.arbitrary

    shrink :: Free a -> [Free a]
shrink (Var a
c)    = forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Free a
Var (forall a. Arbitrary a => a -> [a]
QC.shrink a
c)
    shrink (Free a
x :/\: Free a
y) = Free a
x forall a. a -> [a] -> [a]
: Free a
y forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Free a -> Free a -> Free a
(:/\:)) (forall a. Arbitrary a => a -> [a]
QC.shrink (Free a
x, Free a
y))
    shrink (Free a
x :\/: Free a
y) = Free a
x forall a. a -> [a] -> [a]
: Free a
y forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Free a -> Free a -> Free a
(:\/:)) (forall a. Arbitrary a => a -> [a]
QC.shrink (Free a
x, Free a
y))