{-# 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
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)

-------------------------------------------------------------------------------
-- 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 :: 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 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
        = 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
        = 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
        = 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
        | 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

    -- 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 forall a. Eq a => a -> a -> Bool
== Expr (Am a)
ty
        = 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
        = 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

    -- =>-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)
        = 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

    -- /\-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
        = 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

    -- =>-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
        = 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

    -- =>-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
        = 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
        = 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

    -- =>-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 <- 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

    -- =>-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
        = 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

    -- =>-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
        = 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

    -- 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
        =   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

    -- /\-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
        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
        = 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 (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
            ]

        -- try in order
        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

        -- =>-L4
        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
            ]

        -- \/-R
        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

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

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 []

-- [[ AtomImpl a b ]] = a => b
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)

-- [[ 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
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)