{-# 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
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, Expr a -> Expr a -> Ordering
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
Ord, Int -> Expr a -> ShowS
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, 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
<$ :: forall a b. a -> Expr b -> Expr a
$c<$ :: forall a b. a -> Expr b -> Expr a
fmap :: forall a b. (a -> b) -> Expr a -> Expr b
$cfmap :: forall a b. (a -> b) -> Expr a -> Expr b
Functor, 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 :: forall a. Num a => Expr a -> a
$cproduct :: forall a. Num a => Expr a -> a
sum :: forall a. Num a => Expr a -> a
$csum :: forall a. Num a => Expr a -> a
minimum :: forall a. Ord a => Expr a -> a
$cminimum :: forall a. Ord a => Expr a -> a
maximum :: forall a. Ord a => Expr a -> a
$cmaximum :: forall a. Ord a => Expr a -> a
elem :: forall a. Eq a => a -> Expr a -> Bool
$celem :: forall a. Eq a => a -> Expr a -> Bool
length :: forall a. Expr a -> Int
$clength :: forall a. Expr a -> Int
null :: forall a. Expr a -> Bool
$cnull :: forall a. Expr a -> Bool
toList :: forall a. Expr a -> [a]
$ctoList :: forall a. Expr a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Expr a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Expr a -> a
foldr1 :: forall a. (a -> a -> a) -> Expr a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Expr a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Expr a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Expr a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Expr a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Expr a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Expr a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Expr a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Expr a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Expr a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Expr a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Expr a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Expr a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Expr a -> m
fold :: forall m. Monoid m => Expr m -> m
$cfold :: forall m. Monoid m => Expr m -> m
Foldable, Functor Expr
Foldable Expr
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 :: forall (m :: * -> *) a. Monad m => Expr (m a) -> m (Expr a)
$csequence :: forall (m :: * -> *) a. Monad m => Expr (m a) -> m (Expr a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Expr a -> m (Expr b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Expr a -> m (Expr b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Expr (f a) -> f (Expr a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Expr (f a) -> f (Expr a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Expr a -> f (Expr b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Expr a -> f (Expr b)
Traversable, 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. 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, Expr a -> DataType
Expr a -> Constr
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 (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))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
Data, Typeable)
infixr 6 :/\:
infixr 5 :\/:
infixr 4 :=>:
instance Applicative Expr where
pure :: forall a. a -> Expr a
pure = forall a. a -> Expr a
Var
<*> :: forall a 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 :: forall a. a -> Expr a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
Var a
x >>= :: forall a b. Expr a -> (a -> Expr b) -> Expr b
>>= a -> Expr b
k = a -> Expr b
k a
x
Expr a
Bottom >>= a -> Expr b
_ = forall a. Expr a
Bottom
Expr a
Top >>= a -> Expr b
_ = forall a. Expr a
Top
(Expr a
x :/\: Expr a
y) >>= a -> Expr b
k = (Expr a
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k) forall a. Expr a -> Expr a -> Expr a
:/\: (Expr a
y 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k) forall a. Expr a -> Expr a -> Expr a
:\/: (Expr a
y 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Expr b
k) forall a. Expr a -> Expr a -> Expr a
:=>: (Expr a
y 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 :: forall a. Ord a => Expr a -> Bool
proofSearch Expr a
tyGoal = forall s a. State s a -> s -> a
evalState (forall l. Ctx l
emptyCtx Ctx a -> Expr (Am a) -> State Int Bool
|- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Am a
R Expr a
tyGoal) Int
0
where
freshVar :: StateT Int Identity (Am a)
freshVar = do
Int
n <- forall (m :: * -> *) s. Monad m => StateT s m s
get
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
n forall a. Num a => a -> a -> a
+ Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Int -> Am a
L Int
n)
infix 4 |-
infixr 3 .&&
(.&&) :: Monad m => m Bool -> m Bool -> m Bool
m Bool
x .&& :: forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
.&& m Bool
y = do
Bool
x' <- m Bool
x
if Bool
x'
then m Bool
y
else 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
= 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
= 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
= 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
| forall a. Ord a => a -> Set a -> Bool
Set.member Am a
a Set (Am a)
ats
= 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 forall a. Eq a => a -> a -> Bool
== Expr (Am a)
ty
= 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
= forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx (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)
= 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 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
= 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 forall a. a -> [a] -> [a]
: Expr (Am a)
y 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
= 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 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
= 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
= 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 forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
b forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
c) 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 <- forall a. a -> Expr a
Var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a}. StateT Int Identity (Am a)
freshVar
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 forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
c) forall a. a -> [a] -> [a]
: (Expr (Am a)
a forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
p) forall a. a -> [a] -> [a]
: (Expr (Am a)
b forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
p) 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
= 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 (forall a. Ord a => a -> Set a -> Set a
Set.insert (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
= forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx Set (Am a)
ats (forall a. Ord a => a -> Set a -> Set a
Set.insert (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
= 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 forall a. a -> [a] -> [a]
: [Expr (Am a)]
ctx) Ctx a -> Expr (Am a) -> State Int Bool
|- Expr (Am a)
ty
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
.&& 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 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
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
= 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 (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, 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) <- forall a. Set a -> [a]
Set.toList Set (AtomImpl a)
ai
, Am a
x 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 [] = 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 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 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 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 = forall {a}. [Either a (Ctx a, Expr (Am a))]
disj forall a. [a] -> [a] -> [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 =
[ forall a b. a -> Either a b
Left (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 forall a. Expr a -> Expr a -> Expr a
:=>: Expr (Am a)
z], Expr (Am a)
y, 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) <- forall a. Set a -> [a]
Set.toList Set (ImplImpl a)
ii
, let ii' :: Set (ImplImpl a)
ii' = 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 ->
[ forall a b. b -> Either a b
Right (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)
, forall a b. b -> Either a b
Right (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)
_)
= 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
_
= 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
= forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
data Am a
= L !Int
| R a
deriving (Am a -> Am a -> Bool
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, Am a -> Am a -> Bool
Am a -> Am a -> Ordering
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
Ord, Int -> Am a -> ShowS
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
{ forall a. Ctx a -> Set (Am a)
ctxAtoms :: Set (Am a)
, forall a. Ctx a -> Set (AtomImpl a)
ctxAtomImpl :: Set (AtomImpl a)
, forall a. Ctx a -> Set (ImplImpl a)
ctxImplImpl :: Set (ImplImpl a)
, forall a. Ctx a -> [Expr (Am a)]
ctxHypothesis :: [Expr (Am a)]
}
deriving Int -> Ctx a -> ShowS
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 :: forall l. Ctx l
emptyCtx = forall a.
Set (Am a)
-> Set (AtomImpl a) -> Set (ImplImpl a) -> [Expr (Am a)] -> Ctx a
Ctx forall a. Set a
Set.empty forall a. Set a
Set.empty forall a. Set a
Set.empty []
data AtomImpl a = AtomImpl (Am a) (Expr (Am a))
deriving (AtomImpl a -> AtomImpl a -> Bool
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, AtomImpl a -> AtomImpl a -> Bool
AtomImpl a -> AtomImpl a -> Ordering
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
Ord, Int -> AtomImpl a -> ShowS
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
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, ImplImpl a -> ImplImpl a -> Bool
ImplImpl a -> ImplImpl a -> Ordering
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
Ord, Int -> ImplImpl a -> ShowS
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)