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

import Prelude ()
import Prelude.Compat

import Algebra.Heyting
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
-- >>> import Algebra.PartialOrd
-- >>> import Algebra.Heyting

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

-- | Free Heyting algebra.
--
-- Note: `Eq` and `PartialOrd` instances aren't structural.
--
-- >>> Top == (Var 'x' ==> Var 'x')
-- True
--
-- >>> Var 'x' == Var 'y'
-- False
--
-- You can test for taulogogies:
--
-- >>> leq Top $ (Var 'A' /\ Var 'B' ==> Var 'C') <=>  (Var 'A' ==> Var 'B' ==> Var 'C')
-- True
--
-- >>> leq Top $ (Var 'A' /\ neg (Var 'A')) <=> Bottom
-- True
--
-- >>> leq Top $ (Var 'A' \/ neg (Var 'A')) <=> Top
-- False
--
data Free a
    = Var a
    | Bottom
    | Top
    | Free a :/\: Free a
    | Free a :\/: Free a
    | Free a :=>: Free a
  deriving (Int -> Free a -> ShowS
[Free a] -> ShowS
Free a -> String
(Int -> Free a -> ShowS)
-> (Free a -> String) -> ([Free a] -> ShowS) -> Show (Free a)
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, a -> Free b -> Free a
(a -> b) -> Free a -> Free b
(forall a b. (a -> b) -> Free a -> Free b)
-> (forall a b. a -> Free b -> Free a) -> Functor Free
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
<$ :: a -> Free b -> Free a
$c<$ :: forall a b. a -> Free b -> Free a
fmap :: (a -> b) -> Free a -> Free b
$cfmap :: forall a b. (a -> b) -> Free a -> Free b
Functor, Free a -> Bool
(a -> m) -> Free a -> m
(a -> b -> b) -> b -> Free a -> b
(forall m. Monoid m => Free m -> m)
-> (forall m a. Monoid m => (a -> m) -> Free a -> m)
-> (forall m a. Monoid m => (a -> m) -> Free a -> m)
-> (forall a b. (a -> b -> b) -> b -> Free a -> b)
-> (forall a b. (a -> b -> b) -> b -> Free a -> b)
-> (forall b a. (b -> a -> b) -> b -> Free a -> b)
-> (forall b a. (b -> a -> b) -> b -> Free a -> b)
-> (forall a. (a -> a -> a) -> Free a -> a)
-> (forall a. (a -> a -> a) -> Free a -> a)
-> (forall a. Free a -> [a])
-> (forall a. Free a -> Bool)
-> (forall a. Free a -> Int)
-> (forall a. Eq a => a -> Free a -> Bool)
-> (forall a. Ord a => Free a -> a)
-> (forall a. Ord a => Free a -> a)
-> (forall a. Num a => Free a -> a)
-> (forall a. Num a => Free a -> a)
-> Foldable Free
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 :: Free a -> a
$cproduct :: forall a. Num a => Free a -> a
sum :: Free a -> a
$csum :: forall a. Num a => Free a -> a
minimum :: Free a -> a
$cminimum :: forall a. Ord a => Free a -> a
maximum :: Free a -> a
$cmaximum :: forall a. Ord a => Free a -> a
elem :: a -> Free a -> Bool
$celem :: forall a. Eq a => a -> Free a -> Bool
length :: Free a -> Int
$clength :: forall a. Free a -> Int
null :: Free a -> Bool
$cnull :: forall a. Free a -> Bool
toList :: Free a -> [a]
$ctoList :: forall a. Free a -> [a]
foldl1 :: (a -> a -> a) -> Free a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Free a -> a
foldr1 :: (a -> a -> a) -> Free a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Free a -> a
foldl' :: (b -> a -> b) -> b -> Free a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Free a -> b
foldl :: (b -> a -> b) -> b -> Free a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Free a -> b
foldr' :: (a -> b -> b) -> b -> Free a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Free a -> b
foldr :: (a -> b -> b) -> b -> Free a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Free a -> b
foldMap' :: (a -> m) -> Free a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Free a -> m
foldMap :: (a -> m) -> Free a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Free a -> m
fold :: Free m -> m
$cfold :: forall m. Monoid m => Free m -> m
Foldable, Functor Free
Foldable Free
Functor Free
-> Foldable Free
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Free a -> f (Free b))
-> (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 (m :: * -> *) a. Monad m => Free (m a) -> m (Free a))
-> Traversable Free
(a -> f b) -> Free a -> f (Free b)
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 :: Free (m a) -> m (Free a)
$csequence :: forall (m :: * -> *) a. Monad m => Free (m a) -> m (Free a)
mapM :: (a -> m b) -> Free a -> m (Free b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Free a -> m (Free b)
sequenceA :: Free (f a) -> f (Free a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Free (f a) -> f (Free a)
traverse :: (a -> f b) -> Free a -> f (Free b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Free a -> f (Free b)
$cp2Traversable :: Foldable Free
$cp1Traversable :: Functor Free
Traversable, (forall x. Free a -> Rep (Free a) x)
-> (forall x. Rep (Free a) x -> Free a) -> Generic (Free a)
forall x. Rep (Free a) x -> Free a
forall x. Free a -> Rep (Free a) x
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. Free a -> Rep1 Free a)
-> (forall a. Rep1 Free a -> Free a) -> Generic1 Free
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, Typeable (Free a)
DataType
Constr
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Free a))
-> (Free a -> Constr)
-> (Free a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Free a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Free a)))
-> ((forall b. Data b => b -> b) -> Free a -> Free a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Free a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Free a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Free a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Free a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Free a -> m (Free a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Free a -> m (Free a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Free a -> m (Free a))
-> Data (Free a)
Free a -> DataType
Free a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Free a))
(forall b. Data b => b -> b) -> Free a -> Free a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Free a -> c (Free a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Free a)
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 u. Int -> (forall d. Data d => d -> u) -> Free a -> u
forall u. (forall d. Data d => d -> u) -> Free a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Free a -> m (Free 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Free a))
$c:=>: :: Constr
$c:\/: :: Constr
$c:/\: :: Constr
$cTop :: Constr
$cBottom :: Constr
$cVar :: Constr
$tFree :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> Free a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Free a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (Free a)
Data, Typeable)

infixr 6 :/\:
infixr 5 :\/:
infixr 4 :=>:

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

substFree :: Free a -> (a -> Free b) -> Free b
substFree :: 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
Bottom     = Free b
forall a. Free a
Bottom
    go Free a
Top        = Free b
forall a. Free a
Top
    go (Free a
x :/\: Free a
y) = Free a -> Free b
go Free a
x Free b -> Free b -> Free b
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 Free b -> Free b -> Free b
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 Free b -> Free b -> Free b
forall a. Heyting a => a -> a -> a
==> Free a -> Free b
go Free a
y

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

lowerFree :: Heyting b => (a -> b) -> Free a -> b
lowerFree :: (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
Bottom     = b
forall a. BoundedJoinSemiLattice a => a
bottom
    go Free a
Top        = b
forall a. BoundedMeetSemiLattice a => a
top
    go (Free a
x :/\: Free a
y) = Free a -> b
go Free a
x b -> b -> b
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 b -> b -> b
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 b -> b -> b
forall a. Heyting a => a -> a -> a
==> Free a -> b
go Free a
y

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

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

instance Applicative Free where
    pure :: a -> Free a
pure = a -> Free a
forall a. a -> Free a
liftFree
    <*> :: Free (a -> b) -> Free a -> Free 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 :: a -> Free a
return = a -> Free a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: Free a -> (a -> Free b) -> Free b
(>>=)  = Free a -> (a -> Free b) -> Free b
forall a b. Free a -> (a -> Free b) -> Free b
substFree

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

-- instances do small local optimisations.

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

    Free a
Top    \/ :: Free a -> Free a -> Free a
\/ Free a
_      = Free a
forall a. Free a
Top
    Free a
Bottom \/ Free a
y      = Free a
y
    Free a
_      \/ Free a
Top    = Free a
forall a. Free a
Top
    Free a
x      \/ Free a
Bottom = Free a
x
    Free a
x      \/ Free a
y      = Free a
x Free a -> Free a -> Free a
forall a. Free a -> Free a -> Free a
:\/: Free a
y

instance BoundedJoinSemiLattice (Free a) where
    bottom :: Free a
bottom = Free a
forall a. Free a
Bottom

instance BoundedMeetSemiLattice (Free a) where
    top :: Free a
top = Free a
forall a. Free a
Top

instance Heyting (Free a) where
    Free a
Bottom ==> :: Free a -> Free a -> Free a
==> Free a
_   = Free a
forall a. Free a
Top
    Free a
Top    ==> Free a
y   = Free a
y
    Free a
_      ==> Free a
Top = Free a
forall a. Free a
Top
    Free a
x      ==> Free a
y   = Free a
x Free a -> Free a -> Free a
forall a. Free a -> Free a -> Free a
:=>: Free a
y

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

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

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

instance QC.Arbitrary a => QC.Arbitrary (Free a) where
    arbitrary :: Gen (Free a)
arbitrary = (Int -> Gen (Free a)) -> Gen (Free a)
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0    = Gen (Free a)
prim
              | Bool
otherwise = [Gen (Free a)] -> Gen (Free a)
forall a. [Gen a] -> Gen a
QC.oneof (Gen (Free a)
prim Gen (Free a) -> [Gen (Free a)] -> [Gen (Free a)]
forall a. a -> [a] -> [a]
: [Gen (Free a)]
compound)
          where
            arb' :: Gen (Free a)
arb' = Int -> Gen (Free a)
arb (Int -> Int
sc Int
n)
            arb'' :: Gen (Free a)
arb'' = Int -> Gen (Free a)
arb (Int -> Int
sc (Int -> Int
sc Int
n)) -- make domains be smaller.

            sc :: Int -> Int
sc = Int -> Int
intLog2 (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1

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

        prim :: Gen (Free a)
prim = [(Int, Gen (Free a))] -> Gen (Free a)
forall a. [(Int, Gen a)] -> Gen a
QC.frequency
            [ (Int
20, a -> Free a
forall a. a -> Free a
Var (a -> Free a) -> Gen a -> Gen (Free a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
QC.arbitrary)
            , (Int
1, Free a -> Gen (Free a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Free a
forall a. Free a
Bottom)
            , (Int
2, Free a -> Gen (Free a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Free a
forall a. Free a
Top)
            ]

    shrink :: Free a -> [Free a]
shrink (Var a
c)    = Free a
forall a. Free a
Top Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: (a -> Free a) -> [a] -> [Free a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Free a
forall a. a -> Free a
Var (a -> [a]
forall a. Arbitrary a => a -> [a]
QC.shrink a
c)
    shrink Free a
Bottom     = []
    shrink Free a
Top        = [Free a
forall a. Free a
Bottom]
    shrink (Free a
x :/\: Free a
y) = Free a
x Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: Free a
y Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: ((Free a, Free a) -> Free a) -> [(Free a, Free a)] -> [Free a]
forall a b. (a -> b) -> [a] -> [b]
map ((Free a -> Free a -> Free a) -> (Free a, Free a) -> Free a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Free a -> Free a -> Free a
forall a. Free a -> Free a -> Free a
(:/\:)) ((Free 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 Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: Free a
y Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: ((Free a, Free a) -> Free a) -> [(Free a, Free a)] -> [Free a]
forall a b. (a -> b) -> [a] -> [b]
map ((Free a -> Free a -> Free a) -> (Free a, Free a) -> Free a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Free a -> Free a -> Free a
forall a. Free a -> Free a -> Free a
(:\/:)) ((Free 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 Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: Free a
y Free a -> [Free a] -> [Free a]
forall a. a -> [a] -> [a]
: ((Free a, Free a) -> Free a) -> [(Free a, Free a)] -> [Free a]
forall a b. (a -> b) -> [a] -> [b]
map ((Free a -> Free a -> Free a) -> (Free a, Free a) -> Free a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Free a -> Free a -> Free a
forall a. Free a -> Free a -> Free a
(:=>:)) ((Free a, Free a) -> [(Free a, Free a)]
forall a. Arbitrary a => a -> [a]
QC.shrink (Free a
x, Free a
y))