{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Algebra.Heyting.Free.Expr (
    Expr (..),
    proofSearch,
    ) where

import Prelude ()
import Prelude.Compat

import Control.Monad             (ap)
import Control.Monad.Trans.State (State, evalState, get, put)
import Data.Data                 (Data, Typeable)
import Data.Set                  (Set)
import GHC.Generics              (Generic, Generic1)

import qualified Data.Set as Set

-------------------------------------------------------------------------------
-- Expr
-------------------------------------------------------------------------------

-- | Heyting algebra expression.
--
-- /Note:/ this type doesn't have 'Algebra.Heyting.Heyting' instance,
-- as its 'Eq' and 'Ord' are structural.
--
data Expr a
    = Var a
    | Bottom
    | Top
    | Expr a :/\: Expr a
    | Expr a :\/: Expr a
    | Expr a :=>: Expr a
  deriving (Expr a -> Expr a -> Bool
(Expr a -> Expr a -> Bool)
-> (Expr a -> Expr a -> Bool) -> Eq (Expr a)
forall a. Eq a => Expr a -> Expr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr a -> Expr a -> Bool
$c/= :: forall a. Eq a => Expr a -> Expr a -> Bool
== :: Expr a -> Expr a -> Bool
$c== :: forall a. Eq a => Expr a -> Expr a -> Bool
Eq, Eq (Expr a)
Eq (Expr a)
-> (Expr a -> Expr a -> Ordering)
-> (Expr a -> Expr a -> Bool)
-> (Expr a -> Expr a -> Bool)
-> (Expr a -> Expr a -> Bool)
-> (Expr a -> Expr a -> Bool)
-> (Expr a -> Expr a -> Expr a)
-> (Expr a -> Expr a -> Expr a)
-> Ord (Expr a)
Expr a -> Expr a -> Bool
Expr a -> Expr a -> Ordering
Expr a -> Expr a -> Expr a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Expr a)
forall a. Ord a => Expr a -> Expr a -> Bool
forall a. Ord a => Expr a -> Expr a -> Ordering
forall a. Ord a => Expr a -> Expr a -> Expr a
min :: Expr a -> Expr a -> Expr a
$cmin :: forall a. Ord a => Expr a -> Expr a -> Expr a
max :: Expr a -> Expr a -> Expr a
$cmax :: forall a. Ord a => Expr a -> Expr a -> Expr a
>= :: Expr a -> Expr a -> Bool
$c>= :: forall a. Ord a => Expr a -> Expr a -> Bool
> :: Expr a -> Expr a -> Bool
$c> :: forall a. Ord a => Expr a -> Expr a -> Bool
<= :: Expr a -> Expr a -> Bool
$c<= :: forall a. Ord a => Expr a -> Expr a -> Bool
< :: Expr a -> Expr a -> Bool
$c< :: forall a. Ord a => Expr a -> Expr a -> Bool
compare :: Expr a -> Expr a -> Ordering
$ccompare :: forall a. Ord a => Expr a -> Expr a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Expr a)
Ord, Int -> Expr a -> ShowS
[Expr a] -> ShowS
Expr a -> String
(Int -> Expr a -> ShowS)
-> (Expr a -> String) -> ([Expr a] -> ShowS) -> Show (Expr a)
forall a. Show a => Int -> Expr a -> ShowS
forall a. Show a => [Expr a] -> ShowS
forall a. Show a => Expr a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr a] -> ShowS
$cshowList :: forall a. Show a => [Expr a] -> ShowS
show :: Expr a -> String
$cshow :: forall a. Show a => Expr a -> String
showsPrec :: Int -> Expr a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Expr a -> ShowS
Show, a -> Expr b -> Expr a
(a -> b) -> Expr a -> Expr b
(forall a b. (a -> b) -> Expr a -> Expr b)
-> (forall a b. a -> Expr b -> Expr a) -> Functor Expr
forall a b. a -> Expr b -> Expr a
forall a b. (a -> b) -> Expr a -> Expr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Expr b -> Expr a
$c<$ :: forall a b. a -> Expr b -> Expr a
fmap :: (a -> b) -> Expr a -> Expr b
$cfmap :: forall a b. (a -> b) -> Expr a -> Expr b
Functor, Expr a -> Bool
(a -> m) -> Expr a -> m
(a -> b -> b) -> b -> Expr a -> b
(forall m. Monoid m => Expr m -> m)
-> (forall m a. Monoid m => (a -> m) -> Expr a -> m)
-> (forall m a. Monoid m => (a -> m) -> Expr a -> m)
-> (forall a b. (a -> b -> b) -> b -> Expr a -> b)
-> (forall a b. (a -> b -> b) -> b -> Expr a -> b)
-> (forall b a. (b -> a -> b) -> b -> Expr a -> b)
-> (forall b a. (b -> a -> b) -> b -> Expr a -> b)
-> (forall a. (a -> a -> a) -> Expr a -> a)
-> (forall a. (a -> a -> a) -> Expr a -> a)
-> (forall a. Expr a -> [a])
-> (forall a. Expr a -> Bool)
-> (forall a. Expr a -> Int)
-> (forall a. Eq a => a -> Expr a -> Bool)
-> (forall a. Ord a => Expr a -> a)
-> (forall a. Ord a => Expr a -> a)
-> (forall a. Num a => Expr a -> a)
-> (forall a. Num a => Expr a -> a)
-> Foldable Expr
forall a. Eq a => a -> Expr a -> Bool
forall a. Num a => Expr a -> a
forall a. Ord a => Expr a -> a
forall m. Monoid m => Expr m -> m
forall a. Expr a -> Bool
forall a. Expr a -> Int
forall a. Expr a -> [a]
forall a. (a -> a -> a) -> Expr a -> a
forall m a. Monoid m => (a -> m) -> Expr a -> m
forall b a. (b -> a -> b) -> b -> Expr a -> b
forall a b. (a -> b -> b) -> b -> Expr 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 :: Expr a -> a
$cproduct :: forall a. Num a => Expr a -> a
sum :: Expr a -> a
$csum :: forall a. Num a => Expr a -> a
minimum :: Expr a -> a
$cminimum :: forall a. Ord a => Expr a -> a
maximum :: Expr a -> a
$cmaximum :: forall a. Ord a => Expr a -> a
elem :: a -> Expr a -> Bool
$celem :: forall a. Eq a => a -> Expr a -> Bool
length :: Expr a -> Int
$clength :: forall a. Expr a -> Int
null :: Expr a -> Bool
$cnull :: forall a. Expr a -> Bool
toList :: Expr a -> [a]
$ctoList :: forall a. Expr a -> [a]
foldl1 :: (a -> a -> a) -> Expr a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Expr a -> a
foldr1 :: (a -> a -> a) -> Expr a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Expr a -> a
foldl' :: (b -> a -> b) -> b -> Expr a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Expr a -> b
foldl :: (b -> a -> b) -> b -> Expr a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Expr a -> b
foldr' :: (a -> b -> b) -> b -> Expr a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Expr a -> b
foldr :: (a -> b -> b) -> b -> Expr a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Expr a -> b
foldMap' :: (a -> m) -> Expr a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Expr a -> m
foldMap :: (a -> m) -> Expr a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Expr a -> m
fold :: Expr m -> m
$cfold :: forall m. Monoid m => Expr m -> m
Foldable, Functor Expr
Foldable Expr
Functor Expr
-> Foldable Expr
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Expr a -> f (Expr b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Expr (f a) -> f (Expr a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Expr a -> m (Expr b))
-> (forall (m :: * -> *) a. Monad m => Expr (m a) -> m (Expr a))
-> Traversable Expr
(a -> f b) -> Expr a -> f (Expr 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 => Expr (m a) -> m (Expr a)
forall (f :: * -> *) a. Applicative f => Expr (f a) -> f (Expr a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Expr a -> m (Expr b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Expr a -> f (Expr b)
sequence :: Expr (m a) -> m (Expr a)
$csequence :: forall (m :: * -> *) a. Monad m => Expr (m a) -> m (Expr a)
mapM :: (a -> m b) -> Expr a -> m (Expr b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Expr a -> m (Expr b)
sequenceA :: Expr (f a) -> f (Expr a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Expr (f a) -> f (Expr a)
traverse :: (a -> f b) -> Expr a -> f (Expr b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Expr a -> f (Expr b)
$cp2Traversable :: Foldable Expr
$cp1Traversable :: Functor Expr
Traversable, (forall x. Expr a -> Rep (Expr a) x)
-> (forall x. Rep (Expr a) x -> Expr a) -> Generic (Expr a)
forall x. Rep (Expr a) x -> Expr a
forall x. Expr a -> Rep (Expr a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Expr a) x -> Expr a
forall a x. Expr a -> Rep (Expr a) x
$cto :: forall a x. Rep (Expr a) x -> Expr a
$cfrom :: forall a x. Expr a -> Rep (Expr a) x
Generic, (forall a. Expr a -> Rep1 Expr a)
-> (forall a. Rep1 Expr a -> Expr a) -> Generic1 Expr
forall a. Rep1 Expr a -> Expr a
forall a. Expr a -> Rep1 Expr 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 Expr a -> Expr a
$cfrom1 :: forall a. Expr a -> Rep1 Expr a
Generic1, Typeable (Expr a)
DataType
Constr
Typeable (Expr a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Expr a -> c (Expr a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Expr a))
-> (Expr a -> Constr)
-> (Expr a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Expr a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Expr a)))
-> ((forall b. Data b => b -> b) -> Expr a -> Expr a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Expr a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Expr a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Expr a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Expr a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Expr a -> m (Expr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Expr a -> m (Expr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Expr a -> m (Expr a))
-> Data (Expr a)
Expr a -> DataType
Expr a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Expr a))
(forall b. Data b => b -> b) -> Expr a -> Expr a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr a -> c (Expr a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Expr a)
forall a. Data a => Typeable (Expr a)
forall a. Data a => Expr a -> DataType
forall a. Data a => Expr a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Expr a -> Expr a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Expr a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Expr a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Expr a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr a -> c (Expr a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Expr a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Expr 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) -> Expr a -> u
forall u. (forall d. Data d => d -> u) -> Expr a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Expr a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr a -> c (Expr a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Expr a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Expr a))
$c:=>: :: Constr
$c:\/: :: Constr
$c:/\: :: Constr
$cTop :: Constr
$cBottom :: Constr
$cVar :: Constr
$tExpr :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
gmapMp :: (forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
gmapM :: (forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Expr a -> m (Expr a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Expr a -> u
gmapQ :: (forall d. Data d => d -> u) -> Expr a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Expr a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr a -> r
gmapT :: (forall b. Data b => b -> b) -> Expr a -> Expr a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Expr a -> Expr a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Expr a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Expr a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Expr a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Expr a))
dataTypeOf :: Expr a -> DataType
$cdataTypeOf :: forall a. Data a => Expr a -> DataType
toConstr :: Expr a -> Constr
$ctoConstr :: forall a. Data a => Expr a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Expr a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Expr a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr a -> c (Expr a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr a -> c (Expr a)
$cp1Data :: forall a. Data a => Typeable (Expr a)
Data, Typeable)

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

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

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

    Var a
x      >>= :: Expr a -> (a -> Expr b) -> Expr b
>>= a -> Expr b
k = a -> Expr b
k a
x
    Expr a
Bottom     >>= a -> Expr b
_ = Expr b
forall a. Expr a
Bottom
    Expr a
Top        >>= a -> Expr b
_ = Expr b
forall a. Expr a
Top
    (Expr a
x :/\: Expr a
y) >>= a -> Expr b
k = (Expr a
x Expr a -> (a -> Expr b) -> Expr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k) Expr b -> Expr b -> Expr b
forall a. Expr a -> Expr a -> Expr a
:/\: (Expr a
y Expr a -> (a -> Expr b) -> Expr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k)
    (Expr a
x :\/: Expr a
y) >>= a -> Expr b
k = (Expr a
x Expr a -> (a -> Expr b) -> Expr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k) Expr b -> Expr b -> Expr b
forall a. Expr a -> Expr a -> Expr a
:\/: (Expr a
y Expr a -> (a -> Expr b) -> Expr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k)
    (Expr a
x :=>: Expr a
y) >>= a -> Expr b
k = (Expr a
x Expr a -> (a -> Expr b) -> Expr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k) Expr b -> Expr b -> Expr b
forall a. Expr a -> Expr a -> Expr a
:=>: (Expr a
y Expr a -> (a -> Expr b) -> Expr b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k)

-------------------------------------------------------------------------------
-- LJT proof search
-------------------------------------------------------------------------------

-- | Decide whether @x :: 'Expr' a@ is provable.
--
-- /Note:/ this doesn't construct a proof term, but merely returns a 'Bool'.
--
proofSearch :: forall a. Ord a => Expr a -> Bool
proofSearch :: Expr a -> Bool
proofSearch Expr a
tyGoal = State Int Bool -> Int -> Bool
forall s a. State s a -> s -> a
evalState (Ctx a
forall l. Ctx l
emptyCtx Ctx a -> Expr (Am a) -> State Int Bool
|- (a -> Am a) -> Expr a -> Expr (Am a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Am a
forall a. a -> Am a
R Expr a
tyGoal) Int
0
  where
    freshVar :: StateT Int Identity (Am a)
freshVar = do
        Int
n <- StateT Int Identity Int
forall (m :: * -> *) s. Monad m => StateT s m s
get
        Int -> StateT Int Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
        Am a -> StateT Int Identity (Am a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Am a
forall a. Int -> Am a
L Int
n)

    infix 4 |-
    infixr 3 .&&

    (.&&) :: Monad m => m Bool -> m Bool -> m Bool
    m Bool
x .&& :: m Bool -> m Bool -> m Bool
.&& m Bool
y = do
        Bool
x' <- m Bool
x
        if Bool
x'
        then m Bool
y
        else Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    (|-) :: Ctx a -> Expr (Am a) -> State Int Bool

    -- Ctx ats ai ii xs |- _
    --     | traceShow (length ats, length ai, length ii, length xs) False
    --     = return False

    -- T-R
    Ctx a
_ctx |- :: Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
Top
        = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    -- T-L
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Expr (Am a)
Top : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [Expr (Am a)]
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- F-L
    Ctx Set (Am a)
_ Set (AtomImpl a)
_ Set (ImplImpl a)
_ (Expr (Am a)
Bottom : [Expr (Am a)]
_ctx) |- Expr (Am a)
_ty
        = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    -- Id-atoms
    Ctx Set (Am a)
ats Set (AtomImpl a)
_ai Set (ImplImpl a)
_ii [] |- Var Am a
a
        | Am a -> Set (Am a) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Am a
a Set (Am a)
ats
        = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    -- Id
    Ctx Set (Am a)
_ats Set (AtomImpl a)
_ai Set (ImplImpl a)
_ii (Expr (Am a)
x : [Expr (Am a)]
_ctx) |- Expr (Am a)
ty
        | Expr (Am a)
x Expr (Am a) -> Expr (Am a) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr (Am a)
ty
        = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    -- Move atoms to atoms part of context
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Var Am a
a : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx (Am a -> Set (Am a) -> Set (Am a)
forall a. Ord a => a -> Set a -> Set a
Set.insert Am a
a Set (Am a)
ats) Set (AtomImpl a)
ai Set (ImplImpl a)
ii [Expr (Am a)]
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-R
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [Expr (Am a)]
ctx |- (Expr (Am a)
a :=>: Expr (Am a)
b)
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Expr (Am a)
a Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
b

    -- /\-L
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
x :/\: Expr (Am a)
y) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Expr (Am a)
x Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: Expr (Am a)
y Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-L-extra (Top)
    --
    -- \Gamma, C      |- G
    -- --------------------------
    -- \Gamma, 1 -> C |- G
    --
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
Top :=>: Expr (Am a)
c) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Expr (Am a)
c Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-L-extra (Bottom)
    --
    -- \Gamma         |- G
    -- --------------------------
    -- \Gamma, 0 -> C |- G
    --
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
Bottom :=>: Expr (Am a)
_) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [Expr (Am a)]
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-L2 (Conj)
    --
    -- \Gamma, A -> (B -> C) |- G
    -- --------------------------
    -- \Gamma, (A /\ B) -> C |- G
    --
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
a :/\: Expr (Am a)
b :=>: Expr (Am a)
c) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
a Expr (Am a) -> Expr (Am a) -> Expr (Am a)
forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
b Expr (Am a) -> Expr (Am a) -> Expr (Am a)
forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
c) Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-L3 (Disj)
    --
    -- \Gamma, A -> C, B -> C |- G
    -- ---------------------------
    -- \Gamma, (A \/ B) -> C  |- G
    --
    -- or with fresh var: (P = A \/ B, but an atom)
    --
    -- \Gamma, A -> P, B -> P, P -> C |- G
    -- -----------------------------------
    -- \Gamma, (A \/ B) -> C          |- G
    --
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
a :\/: Expr (Am a)
b :=>: Expr (Am a)
c) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty = do
        Expr (Am a)
p <- Am a -> Expr (Am a)
forall a. a -> Expr a
Var (Am a -> Expr (Am a))
-> StateT Int Identity (Am a) -> StateT Int Identity (Expr (Am a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT Int Identity (Am a)
forall a. StateT Int Identity (Am a)
freshVar
        Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
p Expr (Am a) -> Expr (Am a) -> Expr (Am a)
forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
c) Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: (Expr (Am a)
a Expr (Am a) -> Expr (Am a) -> Expr (Am a)
forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
p) Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: (Expr (Am a)
b Expr (Am a) -> Expr (Am a) -> Expr (Am a)
forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
p) Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-L4 preparation
    --
    -- \Gamma, B -> C, A |- B    \Gamma, C |- G
    -- ------------------------------------------
    -- \Gamma, (A -> B) -> C |- G
    --
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (((Expr (Am a)
a :=>: Expr (Am a)
b) :=>: Expr (Am a)
c) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai (ImplImpl a -> Set (ImplImpl a) -> Set (ImplImpl a)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Expr (Am a) -> Expr (Am a) -> Expr (Am a) -> ImplImpl a
forall a. Expr (Am a) -> Expr (Am a) -> Expr (Am a) -> ImplImpl a
ImplImpl Expr (Am a)
a Expr (Am a)
b Expr (Am a)
c) Set (ImplImpl a)
ii) [Expr (Am a)]
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- =>-L1 preparation
    --
    -- \Gamma, X, B      |- G
    -- ----------------------
    -- \Gamma, X, X -> B |- G
    --
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Var Am a
x :=>: Expr (Am a)
b) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats (AtomImpl a -> Set (AtomImpl a) -> Set (AtomImpl a)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Am a -> Expr (Am a) -> AtomImpl a
forall a. Am a -> Expr (Am a) -> AtomImpl a
AtomImpl Am a
x Expr (Am a)
b) Set (AtomImpl a)
ai) Set (ImplImpl a)
ii [Expr (Am a)]
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- These two rules, (\/-L) and (/\-R), are pushed to the last, as they branch.

    -- \/-L
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii ((Expr (Am a)
x :\/: Expr (Am a)
y) : [Expr (Am a)]
ctx) |- Expr (Am a)
ty
        =   Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Expr (Am a)
x Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty
        State Int Bool -> State Int Bool -> State Int Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
.&& Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii (Expr (Am a)
y Expr (Am a) -> [Expr (Am a)] -> [Expr (Am a)]
forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

    -- /\-R
    Ctx a
ctx |- (Expr (Am a)
a :/\: Expr (Am a)
b)
        =   Ctx a
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
a
        State Int Bool -> State Int Bool -> State Int Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
.&& Ctx a
ctx Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
b

    -- Last rules
    Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [] |- Expr (Am a)
ty
        -- L1 completion
        | ((Expr (Am a)
y, Set (AtomImpl a)
ai') : [(Expr (Am a), Set (AtomImpl a))]
_) <- [(Expr (Am a), Set (AtomImpl a))]
match
        = Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai' Set (ImplImpl a)
ii [Expr (Am a)
y] Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty

        -- \/-R and =>-L4
        | Bool -> Bool
not ([Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest) = [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> State Int Bool
iter [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest
      where
        match :: [(Expr (Am a), Set (AtomImpl a))]
match =
            [ (Expr (Am a)
y, AtomImpl a -> Set (AtomImpl a) -> Set (AtomImpl a)
forall a. Ord a => a -> Set a -> Set a
Set.delete AtomImpl a
ai' Set (AtomImpl a)
ai)
            | ai' :: AtomImpl a
ai'@(AtomImpl Am a
x Expr (Am a)
y) <- Set (AtomImpl a) -> [AtomImpl a]
forall a. Set a -> [a]
Set.toList Set (AtomImpl a)
ai
            , Am a
x Am a -> Set (Am a) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Am a)
ats
            ]

        -- try in order
        iter :: [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> State Int Bool
iter [] = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        iter (Right (Ctx a
ctx', Expr (Am a)
ty') : [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest') = do
            Bool
res <- Ctx a
ctx' Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty'
            if Bool
res
            then Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            else [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> State Int Bool
iter [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest'

        iter (Left (Ctx a
ctxa, Expr (Am a)
a, Ctx a
ctxb, Expr (Am a)
b) : [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest') = do
            Bool
res <- Ctx a
ctxa Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
a State Int Bool -> State Int Bool -> State Int Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
.&& Ctx a
ctxb Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
b
            if Bool
res
            then Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            else [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> State Int Bool
iter [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest'

        rest :: [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
rest = [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
forall a. [Either a (Ctx a, Expr (Am a))]
disj [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> [Either
      (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
-> [Either
      (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
forall a. [a] -> [a] -> [a]
++ [Either
   (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) (Ctx a, Expr (Am a))]
forall b. [Either (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) b]
implImpl

        -- =>-L4
        implImpl :: [Either (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) b]
implImpl =
            [ (Ctx a, Expr (Am a), Ctx a, Expr (Am a))
-> Either (Ctx a, Expr (Am a), Ctx a, Expr (Am a)) b
forall a b. a -> Either a b
Left (Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii' [Expr (Am a)
x, Expr (Am a)
y Expr (Am a) -> Expr (Am a) -> Expr (Am a)
forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
z], Expr (Am a)
y, Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii' [Expr (Am a)
z], Expr (Am a)
ty)
            | entry :: ImplImpl a
entry@(ImplImpl Expr (Am a)
x Expr (Am a)
y Expr (Am a)
z) <- Set (ImplImpl a) -> [ImplImpl a]
forall a. Set a -> [a]
Set.toList Set (ImplImpl a)
ii
            , let ii' :: Set (ImplImpl a)
ii' = ImplImpl a -> Set (ImplImpl a) -> Set (ImplImpl a)
forall a. Ord a => a -> Set a -> Set a
Set.delete ImplImpl a
entry Set (ImplImpl a)
ii
            ]

        -- \/-R
        disj :: [Either a (Ctx a, Expr (Am a))]
disj = case Expr (Am a)
ty of
            Expr (Am a)
a :\/: Expr (Am a)
b ->
                [ (Ctx a, Expr (Am a)) -> Either a (Ctx a, Expr (Am a))
forall a b. b -> Either a b
Right (Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [], Expr (Am a)
a)
                , (Ctx a, Expr (Am a)) -> Either a (Ctx a, Expr (Am a))
forall a b. b -> Either a b
Right (Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [], Expr (Am a)
b)
                ]
            Expr (Am a)
_ -> []

    Ctx Set (Am a)
_ Set (AtomImpl a)
_ Set (ImplImpl a)
_ [] |- (Expr (Am a)
_ :\/: Expr (Am a)
_)
        = String -> State Int Bool
forall a. HasCallStack => String -> a
error String
"panic! @proofSearch should be matched before"

    Ctx Set (Am a)
_ Set (AtomImpl a)
_ Set (ImplImpl a)
_ [] |- Var Am a
_
        = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    Ctx Set (Am a)
_ Set (AtomImpl a)
_ Set (ImplImpl a)
_ [] |- Expr (Am a)
Bottom
        = Bool -> State Int Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-------------------------------------------------------------------------------
-- Context
-------------------------------------------------------------------------------

data Am a
    = L !Int
    | R a
  deriving (Am a -> Am a -> Bool
(Am a -> Am a -> Bool) -> (Am a -> Am a -> Bool) -> Eq (Am a)
forall a. Eq a => Am a -> Am a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Am a -> Am a -> Bool
$c/= :: forall a. Eq a => Am a -> Am a -> Bool
== :: Am a -> Am a -> Bool
$c== :: forall a. Eq a => Am a -> Am a -> Bool
Eq, Eq (Am a)
Eq (Am a)
-> (Am a -> Am a -> Ordering)
-> (Am a -> Am a -> Bool)
-> (Am a -> Am a -> Bool)
-> (Am a -> Am a -> Bool)
-> (Am a -> Am a -> Bool)
-> (Am a -> Am a -> Am a)
-> (Am a -> Am a -> Am a)
-> Ord (Am a)
Am a -> Am a -> Bool
Am a -> Am a -> Ordering
Am a -> Am a -> Am a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Am a)
forall a. Ord a => Am a -> Am a -> Bool
forall a. Ord a => Am a -> Am a -> Ordering
forall a. Ord a => Am a -> Am a -> Am a
min :: Am a -> Am a -> Am a
$cmin :: forall a. Ord a => Am a -> Am a -> Am a
max :: Am a -> Am a -> Am a
$cmax :: forall a. Ord a => Am a -> Am a -> Am a
>= :: Am a -> Am a -> Bool
$c>= :: forall a. Ord a => Am a -> Am a -> Bool
> :: Am a -> Am a -> Bool
$c> :: forall a. Ord a => Am a -> Am a -> Bool
<= :: Am a -> Am a -> Bool
$c<= :: forall a. Ord a => Am a -> Am a -> Bool
< :: Am a -> Am a -> Bool
$c< :: forall a. Ord a => Am a -> Am a -> Bool
compare :: Am a -> Am a -> Ordering
$ccompare :: forall a. Ord a => Am a -> Am a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Am a)
Ord, Int -> Am a -> ShowS
[Am a] -> ShowS
Am a -> String
(Int -> Am a -> ShowS)
-> (Am a -> String) -> ([Am a] -> ShowS) -> Show (Am a)
forall a. Show a => Int -> Am a -> ShowS
forall a. Show a => [Am a] -> ShowS
forall a. Show a => Am a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Am a] -> ShowS
$cshowList :: forall a. Show a => [Am a] -> ShowS
show :: Am a -> String
$cshow :: forall a. Show a => Am a -> String
showsPrec :: Int -> Am a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Am a -> ShowS
Show)

data Ctx a = Ctx
    { Ctx a -> Set (Am a)
ctxAtoms      :: Set (Am a)
    , Ctx a -> Set (AtomImpl a)
ctxAtomImpl   :: Set (AtomImpl a)
    , Ctx a -> Set (ImplImpl a)
ctxImplImpl   :: Set (ImplImpl a)
    , Ctx a -> [Expr (Am a)]
ctxHypothesis :: [Expr (Am a)]
    }
  deriving Int -> Ctx a -> ShowS
[Ctx a] -> ShowS
Ctx a -> String
(Int -> Ctx a -> ShowS)
-> (Ctx a -> String) -> ([Ctx a] -> ShowS) -> Show (Ctx a)
forall a. Show a => Int -> Ctx a -> ShowS
forall a. Show a => [Ctx a] -> ShowS
forall a. Show a => Ctx a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ctx a] -> ShowS
$cshowList :: forall a. Show a => [Ctx a] -> ShowS
show :: Ctx a -> String
$cshow :: forall a. Show a => Ctx a -> String
showsPrec :: Int -> Ctx a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Ctx a -> ShowS
Show

emptyCtx :: Ctx l
emptyCtx :: Ctx l
emptyCtx = Set (Am l)
-> Set (AtomImpl l) -> Set (ImplImpl l) -> [Expr (Am l)] -> Ctx l
forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am l)
forall a. Set a
Set.empty Set (AtomImpl l)
forall a. Set a
Set.empty Set (ImplImpl l)
forall a. Set a
Set.empty []

-- [[ AtomImpl a b ]] = a => b
data AtomImpl a = AtomImpl (Am a) (Expr (Am a))
  deriving (AtomImpl a -> AtomImpl a -> Bool
(AtomImpl a -> AtomImpl a -> Bool)
-> (AtomImpl a -> AtomImpl a -> Bool) -> Eq (AtomImpl a)
forall a. Eq a => AtomImpl a -> AtomImpl a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AtomImpl a -> AtomImpl a -> Bool
$c/= :: forall a. Eq a => AtomImpl a -> AtomImpl a -> Bool
== :: AtomImpl a -> AtomImpl a -> Bool
$c== :: forall a. Eq a => AtomImpl a -> AtomImpl a -> Bool
Eq, Eq (AtomImpl a)
Eq (AtomImpl a)
-> (AtomImpl a -> AtomImpl a -> Ordering)
-> (AtomImpl a -> AtomImpl a -> Bool)
-> (AtomImpl a -> AtomImpl a -> Bool)
-> (AtomImpl a -> AtomImpl a -> Bool)
-> (AtomImpl a -> AtomImpl a -> Bool)
-> (AtomImpl a -> AtomImpl a -> AtomImpl a)
-> (AtomImpl a -> AtomImpl a -> AtomImpl a)
-> Ord (AtomImpl a)
AtomImpl a -> AtomImpl a -> Bool
AtomImpl a -> AtomImpl a -> Ordering
AtomImpl a -> AtomImpl a -> AtomImpl a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (AtomImpl a)
forall a. Ord a => AtomImpl a -> AtomImpl a -> Bool
forall a. Ord a => AtomImpl a -> AtomImpl a -> Ordering
forall a. Ord a => AtomImpl a -> AtomImpl a -> AtomImpl a
min :: AtomImpl a -> AtomImpl a -> AtomImpl a
$cmin :: forall a. Ord a => AtomImpl a -> AtomImpl a -> AtomImpl a
max :: AtomImpl a -> AtomImpl a -> AtomImpl a
$cmax :: forall a. Ord a => AtomImpl a -> AtomImpl a -> AtomImpl a
>= :: AtomImpl a -> AtomImpl a -> Bool
$c>= :: forall a. Ord a => AtomImpl a -> AtomImpl a -> Bool
> :: AtomImpl a -> AtomImpl a -> Bool
$c> :: forall a. Ord a => AtomImpl a -> AtomImpl a -> Bool
<= :: AtomImpl a -> AtomImpl a -> Bool
$c<= :: forall a. Ord a => AtomImpl a -> AtomImpl a -> Bool
< :: AtomImpl a -> AtomImpl a -> Bool
$c< :: forall a. Ord a => AtomImpl a -> AtomImpl a -> Bool
compare :: AtomImpl a -> AtomImpl a -> Ordering
$ccompare :: forall a. Ord a => AtomImpl a -> AtomImpl a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (AtomImpl a)
Ord, Int -> AtomImpl a -> ShowS
[AtomImpl a] -> ShowS
AtomImpl a -> String
(Int -> AtomImpl a -> ShowS)
-> (AtomImpl a -> String)
-> ([AtomImpl a] -> ShowS)
-> Show (AtomImpl a)
forall a. Show a => Int -> AtomImpl a -> ShowS
forall a. Show a => [AtomImpl a] -> ShowS
forall a. Show a => AtomImpl a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AtomImpl a] -> ShowS
$cshowList :: forall a. Show a => [AtomImpl a] -> ShowS
show :: AtomImpl a -> String
$cshow :: forall a. Show a => AtomImpl a -> String
showsPrec :: Int -> AtomImpl a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> AtomImpl a -> ShowS
Show)

-- [[ ImplImpl a b c ]] = (a ==> b) ==> c
data ImplImpl a = ImplImpl !(Expr (Am a)) !(Expr (Am a)) !(Expr (Am a))
  deriving (ImplImpl a -> ImplImpl a -> Bool
(ImplImpl a -> ImplImpl a -> Bool)
-> (ImplImpl a -> ImplImpl a -> Bool) -> Eq (ImplImpl a)
forall a. Eq a => ImplImpl a -> ImplImpl a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ImplImpl a -> ImplImpl a -> Bool
$c/= :: forall a. Eq a => ImplImpl a -> ImplImpl a -> Bool
== :: ImplImpl a -> ImplImpl a -> Bool
$c== :: forall a. Eq a => ImplImpl a -> ImplImpl a -> Bool
Eq, Eq (ImplImpl a)
Eq (ImplImpl a)
-> (ImplImpl a -> ImplImpl a -> Ordering)
-> (ImplImpl a -> ImplImpl a -> Bool)
-> (ImplImpl a -> ImplImpl a -> Bool)
-> (ImplImpl a -> ImplImpl a -> Bool)
-> (ImplImpl a -> ImplImpl a -> Bool)
-> (ImplImpl a -> ImplImpl a -> ImplImpl a)
-> (ImplImpl a -> ImplImpl a -> ImplImpl a)
-> Ord (ImplImpl a)
ImplImpl a -> ImplImpl a -> Bool
ImplImpl a -> ImplImpl a -> Ordering
ImplImpl a -> ImplImpl a -> ImplImpl a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (ImplImpl a)
forall a. Ord a => ImplImpl a -> ImplImpl a -> Bool
forall a. Ord a => ImplImpl a -> ImplImpl a -> Ordering
forall a. Ord a => ImplImpl a -> ImplImpl a -> ImplImpl a
min :: ImplImpl a -> ImplImpl a -> ImplImpl a
$cmin :: forall a. Ord a => ImplImpl a -> ImplImpl a -> ImplImpl a
max :: ImplImpl a -> ImplImpl a -> ImplImpl a
$cmax :: forall a. Ord a => ImplImpl a -> ImplImpl a -> ImplImpl a
>= :: ImplImpl a -> ImplImpl a -> Bool
$c>= :: forall a. Ord a => ImplImpl a -> ImplImpl a -> Bool
> :: ImplImpl a -> ImplImpl a -> Bool
$c> :: forall a. Ord a => ImplImpl a -> ImplImpl a -> Bool
<= :: ImplImpl a -> ImplImpl a -> Bool
$c<= :: forall a. Ord a => ImplImpl a -> ImplImpl a -> Bool
< :: ImplImpl a -> ImplImpl a -> Bool
$c< :: forall a. Ord a => ImplImpl a -> ImplImpl a -> Bool
compare :: ImplImpl a -> ImplImpl a -> Ordering
$ccompare :: forall a. Ord a => ImplImpl a -> ImplImpl a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (ImplImpl a)
Ord, Int -> ImplImpl a -> ShowS
[ImplImpl a] -> ShowS
ImplImpl a -> String
(Int -> ImplImpl a -> ShowS)
-> (ImplImpl a -> String)
-> ([ImplImpl a] -> ShowS)
-> Show (ImplImpl a)
forall a. Show a => Int -> ImplImpl a -> ShowS
forall a. Show a => [ImplImpl a] -> ShowS
forall a. Show a => ImplImpl a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ImplImpl a] -> ShowS
$cshowList :: forall a. Show a => [ImplImpl a] -> ShowS
show :: ImplImpl a -> String
$cshow :: forall a. Show a => ImplImpl a -> String
showsPrec :: Int -> ImplImpl a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ImplImpl a -> ShowS
Show)