{-# 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 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
$cshowsPrec :: forall a. Show a => Int -> Free a -> ShowS
showsPrec :: Int -> Free a -> ShowS
$cshow :: forall a. Show a => Free a -> String
show :: Free a -> String
$cshowList :: forall a. Show a => [Free a] -> ShowS
showList :: [Free a] -> ShowS
Show, (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
$cfmap :: forall a b. (a -> b) -> Free a -> Free b
fmap :: forall a b. (a -> b) -> Free a -> Free b
$c<$ :: forall a b. a -> Free b -> Free a
<$ :: forall a b. a -> Free b -> Free a
Functor, (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
$cfold :: forall m. Monoid m => Free m -> m
fold :: forall m. Monoid m => Free m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Free a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Free a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Free a -> a
foldr1 :: forall a. (a -> a -> a) -> Free a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Free a -> a
foldl1 :: forall a. (a -> a -> a) -> Free a -> a
$ctoList :: forall a. Free a -> [a]
toList :: forall a. Free a -> [a]
$cnull :: forall a. Free a -> Bool
null :: forall a. Free a -> Bool
$clength :: forall a. Free a -> Int
length :: forall a. Free a -> Int
$celem :: forall a. Eq a => a -> Free a -> Bool
elem :: forall a. Eq a => a -> Free a -> Bool
$cmaximum :: forall a. Ord a => Free a -> a
maximum :: forall a. Ord a => Free a -> a
$cminimum :: forall a. Ord a => Free a -> a
minimum :: forall a. Ord a => Free a -> a
$csum :: forall a. Num a => Free a -> a
sum :: forall a. Num a => Free a -> a
$cproduct :: forall a. Num a => Free a -> a
product :: forall a. Num a => Free a -> a
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
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Free a -> f (Free b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Free a -> f (Free b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Free (f a) -> f (Free a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Free (f a) -> f (Free a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Free a -> m (Free b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Free a -> m (Free b)
$csequence :: forall (m :: * -> *) a. Monad m => Free (m a) -> m (Free a)
sequence :: forall (m :: * -> *) a. Monad m => Free (m a) -> m (Free a)
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
$cfrom :: forall a x. Free a -> Rep (Free a) x
from :: forall x. Free a -> Rep (Free a) x
$cto :: forall a x. Rep (Free a) x -> Free a
to :: forall x. Rep (Free a) x -> Free a
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
$cfrom1 :: forall a. Free a -> Rep1 Free a
from1 :: forall a. Free a -> Rep1 Free a
$cto1 :: forall a. Rep1 Free a -> Free a
to1 :: forall a. Rep1 Free a -> Free a
Generic1, Typeable (Free a)
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 -> Constr
Free a -> DataType
(forall b. Data b => b -> b) -> Free a -> Free a
forall a. Data a => Typeable (Free a)
forall a. Data a => Free a -> Constr
forall a. Data a => Free a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Free a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Free a)
$ctoConstr :: forall a. Data a => Free a -> Constr
toConstr :: Free a -> Constr
$cdataTypeOf :: forall a. Data a => Free a -> DataType
dataTypeOf :: Free a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Free a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Free a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Free a -> Free a
gmapT :: (forall b. Data b => b -> b) -> Free a -> Free a
$cgmapQl :: 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
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Free a -> r
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Free a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Free a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Free a -> m (Free a)
Data, Typeable)

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

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

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
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 :: forall a. Heyting a => 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 :: forall b a. Heyting 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
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 :: forall a. 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 :: forall a. a -> Free a
pure = a -> Free a
forall a. a -> Free a
liftFree
    <*> :: forall a b. 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 :: forall a. a -> Free a
return = a -> Free a
forall a. a -> Free a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: forall a b. 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. HasCallStack => [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 a b c. (a -> b -> c) -> Gen a -> Gen b -> Gen c
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 a b c. (a -> b -> c) -> Gen a -> Gen b -> Gen c
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 a b c. (a -> b -> c) -> Gen a -> Gen b -> Gen c
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. HasCallStack => [(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 a. a -> Gen 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 a. a -> Gen 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))