{-# 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
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)
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 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Ctx Set (Am a)
ats Set (AtomImpl a)
ai Set (ImplImpl a)
ii [] |- Expr (Am a)
ty
| ((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
| 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
]
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
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
]
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
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 []
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)
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)