{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RecordWildCards            #-}
module RSTT.Tope.Proof where

import           Control.Applicative  (Alternative (..))
import           Data.Bifunctor
#if __GLASGOW_HASKELL__ < 808
import           Control.Monad.Fail   (MonadFail)
#endif
import           Control.Monad.Logic
import           Control.Monad.Reader
import           Data.List            (inits, intercalate, tails, nub)
import           Data.Void

import           RSTT.Cube
import           RSTT.Tope

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import RSTT.Tope

-- * Tope sequent

-- | Tope sequent \( \Xi \mid \Phi \vdash \psi \).
data Sequent = Sequent
  { Sequent -> CubeContext
sequentCubeContext :: CubeContext -- ^ Cube context \(\Xi\).
  , Sequent -> TopeContext
sequentTopeContext :: TopeContext -- ^ Tope context \(\Phi\).
  , Sequent -> Tope
sequentTope        :: Tope        -- ^ A tope \(\psi\) on the right hand side.
  } deriving (Sequent -> Sequent -> Bool
(Sequent -> Sequent -> Bool)
-> (Sequent -> Sequent -> Bool) -> Eq Sequent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sequent -> Sequent -> Bool
$c/= :: Sequent -> Sequent -> Bool
== :: Sequent -> Sequent -> Bool
$c== :: Sequent -> Sequent -> Bool
Eq, Int -> Sequent -> ShowS
[Sequent] -> ShowS
Sequent -> [Char]
(Int -> Sequent -> ShowS)
-> (Sequent -> [Char]) -> ([Sequent] -> ShowS) -> Show Sequent
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Sequent] -> ShowS
$cshowList :: [Sequent] -> ShowS
show :: Sequent -> [Char]
$cshow :: Sequent -> [Char]
showsPrec :: Int -> Sequent -> ShowS
$cshowsPrec :: Int -> Sequent -> ShowS
Show)

-- | Pretty-print a 'Sequent'.
--
-- >>> points = [("t", "I"), ("s", "J")]
-- >>> topes = [("φ" `TopeOr` "ζ") `TopeAnd` ("ψ" `TopeOr` "χ"), ("t" `TopeEQ` "s")]
-- >>> putStrLn (ppSequent (Sequent points topes ("s" `TopeEQ` "t")))
-- t : I, s : J | (φ ∨ ζ) ∧ (ψ ∨ χ), t ≡ s ⊢ s ≡ t
ppSequent :: Sequent -> String
ppSequent :: Sequent -> [Char]
ppSequent Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} =
  CubeContext -> [Char]
ppCubeContext CubeContext
sequentCubeContext [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" | " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<>
  TopeContext -> [Char]
ppTopeContext TopeContext
sequentTopeContext [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" ⊢ " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<>
  Tope -> [Char]
ppTope Tope
sequentTope

-- * Rules

-- | A name of a (tope inference) rule.
type RuleName = String

-- | A collection of tope inference rules.
-- Intuitively, @'Rules'@ is a non-deterministic function
-- from 'Sequent' to @('RuleName', ['Sequent'])@.
type Rules = RulesM (RuleName, [Sequent])

-- | A collection of generalized tope inference rules.
-- Intuitively, @'RulesM' a@ is a non-deterministic function from 'Sequent' to @a@.
newtype RulesM a = RulesM
  { forall a. RulesM a -> ReaderT Sequent (LogicT Identity) a
applyRulesM :: ReaderT Sequent Logic a }
  deriving ((forall a b. (a -> b) -> RulesM a -> RulesM b)
-> (forall a b. a -> RulesM b -> RulesM a) -> Functor RulesM
forall a b. a -> RulesM b -> RulesM a
forall a b. (a -> b) -> RulesM a -> RulesM 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 -> RulesM b -> RulesM a
$c<$ :: forall a b. a -> RulesM b -> RulesM a
fmap :: forall a b. (a -> b) -> RulesM a -> RulesM b
$cfmap :: forall a b. (a -> b) -> RulesM a -> RulesM b
Functor, Functor RulesM
Functor RulesM
-> (forall a. a -> RulesM a)
-> (forall a b. RulesM (a -> b) -> RulesM a -> RulesM b)
-> (forall a b c.
    (a -> b -> c) -> RulesM a -> RulesM b -> RulesM c)
-> (forall a b. RulesM a -> RulesM b -> RulesM b)
-> (forall a b. RulesM a -> RulesM b -> RulesM a)
-> Applicative RulesM
forall a. a -> RulesM a
forall a b. RulesM a -> RulesM b -> RulesM a
forall a b. RulesM a -> RulesM b -> RulesM b
forall a b. RulesM (a -> b) -> RulesM a -> RulesM b
forall a b c. (a -> b -> c) -> RulesM a -> RulesM b -> RulesM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. RulesM a -> RulesM b -> RulesM a
$c<* :: forall a b. RulesM a -> RulesM b -> RulesM a
*> :: forall a b. RulesM a -> RulesM b -> RulesM b
$c*> :: forall a b. RulesM a -> RulesM b -> RulesM b
liftA2 :: forall a b c. (a -> b -> c) -> RulesM a -> RulesM b -> RulesM c
$cliftA2 :: forall a b c. (a -> b -> c) -> RulesM a -> RulesM b -> RulesM c
<*> :: forall a b. RulesM (a -> b) -> RulesM a -> RulesM b
$c<*> :: forall a b. RulesM (a -> b) -> RulesM a -> RulesM b
pure :: forall a. a -> RulesM a
$cpure :: forall a. a -> RulesM a
Applicative, Applicative RulesM
Applicative RulesM
-> (forall a b. RulesM a -> (a -> RulesM b) -> RulesM b)
-> (forall a b. RulesM a -> RulesM b -> RulesM b)
-> (forall a. a -> RulesM a)
-> Monad RulesM
forall a. a -> RulesM a
forall a b. RulesM a -> RulesM b -> RulesM b
forall a b. RulesM a -> (a -> RulesM b) -> RulesM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> RulesM a
$creturn :: forall a. a -> RulesM a
>> :: forall a b. RulesM a -> RulesM b -> RulesM b
$c>> :: forall a b. RulesM a -> RulesM b -> RulesM b
>>= :: forall a b. RulesM a -> (a -> RulesM b) -> RulesM b
$c>>= :: forall a b. RulesM a -> (a -> RulesM b) -> RulesM b
Monad, Applicative RulesM
Applicative RulesM
-> (forall a. RulesM a)
-> (forall a. RulesM a -> RulesM a -> RulesM a)
-> (forall a. RulesM a -> RulesM [a])
-> (forall a. RulesM a -> RulesM [a])
-> Alternative RulesM
forall a. RulesM a
forall a. RulesM a -> RulesM [a]
forall a. RulesM a -> RulesM a -> RulesM a
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
many :: forall a. RulesM a -> RulesM [a]
$cmany :: forall a. RulesM a -> RulesM [a]
some :: forall a. RulesM a -> RulesM [a]
$csome :: forall a. RulesM a -> RulesM [a]
<|> :: forall a. RulesM a -> RulesM a -> RulesM a
$c<|> :: forall a. RulesM a -> RulesM a -> RulesM a
empty :: forall a. RulesM a
$cempty :: forall a. RulesM a
Alternative, Monad RulesM
Alternative RulesM
Alternative RulesM
-> Monad RulesM
-> (forall a. RulesM a)
-> (forall a. RulesM a -> RulesM a -> RulesM a)
-> MonadPlus RulesM
forall a. RulesM a
forall a. RulesM a -> RulesM a -> RulesM a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
mplus :: forall a. RulesM a -> RulesM a -> RulesM a
$cmplus :: forall a. RulesM a -> RulesM a -> RulesM a
mzero :: forall a. RulesM a
$cmzero :: forall a. RulesM a
MonadPlus, Monad RulesM
Monad RulesM -> (forall a. [Char] -> RulesM a) -> MonadFail RulesM
forall a. [Char] -> RulesM a
forall (m :: * -> *).
Monad m -> (forall a. [Char] -> m a) -> MonadFail m
fail :: forall a. [Char] -> RulesM a
$cfail :: forall a. [Char] -> RulesM a
MonadFail)
  deriving (MonadReader Sequent, Monad RulesM
Alternative RulesM
Monad RulesM
-> Alternative RulesM
-> (forall a. RulesM a -> RulesM (Maybe (a, RulesM a)))
-> (forall a. RulesM a -> RulesM a -> RulesM a)
-> (forall a b. RulesM a -> (a -> RulesM b) -> RulesM b)
-> (forall a. RulesM a -> RulesM a)
-> (forall a. RulesM a -> RulesM ())
-> (forall a b.
    RulesM a -> (a -> RulesM b) -> RulesM b -> RulesM b)
-> MonadLogic RulesM
forall a. RulesM a -> RulesM a
forall a. RulesM a -> RulesM (Maybe (a, RulesM a))
forall a. RulesM a -> RulesM ()
forall a. RulesM a -> RulesM a -> RulesM a
forall a b. RulesM a -> (a -> RulesM b) -> RulesM b
forall a b. RulesM a -> (a -> RulesM b) -> RulesM b -> RulesM b
forall (m :: * -> *).
Monad m
-> Alternative m
-> (forall a. m a -> m (Maybe (a, m a)))
-> (forall a. m a -> m a -> m a)
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a. m a -> m a)
-> (forall a. m a -> m ())
-> (forall a b. m a -> (a -> m b) -> m b -> m b)
-> MonadLogic m
ifte :: forall a b. RulesM a -> (a -> RulesM b) -> RulesM b -> RulesM b
$cifte :: forall a b. RulesM a -> (a -> RulesM b) -> RulesM b -> RulesM b
lnot :: forall a. RulesM a -> RulesM ()
$clnot :: forall a. RulesM a -> RulesM ()
once :: forall a. RulesM a -> RulesM a
$conce :: forall a. RulesM a -> RulesM a
>>- :: forall a b. RulesM a -> (a -> RulesM b) -> RulesM b
$c>>- :: forall a b. RulesM a -> (a -> RulesM b) -> RulesM b
interleave :: forall a. RulesM a -> RulesM a -> RulesM a
$cinterleave :: forall a. RulesM a -> RulesM a -> RulesM a
msplit :: forall a. RulesM a -> RulesM (Maybe (a, RulesM a))
$cmsplit :: forall a. RulesM a -> RulesM (Maybe (a, RulesM a))
MonadLogic)

instance Semigroup (RulesM a) where
  RulesM ReaderT Sequent (LogicT Identity) a
f <> :: RulesM a -> RulesM a -> RulesM a
<> RulesM ReaderT Sequent (LogicT Identity) a
g = ReaderT Sequent (LogicT Identity) a -> RulesM a
forall a. ReaderT Sequent (LogicT Identity) a -> RulesM a
RulesM (ReaderT Sequent (LogicT Identity) a
f ReaderT Sequent (LogicT Identity) a
-> ReaderT Sequent (LogicT Identity) a
-> ReaderT Sequent (LogicT Identity) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT Sequent (LogicT Identity) a
g)

instance Monoid (RulesM a) where
  mempty :: RulesM a
mempty = ReaderT Sequent (LogicT Identity) a -> RulesM a
forall a. ReaderT Sequent (LogicT Identity) a -> RulesM a
RulesM ReaderT Sequent (LogicT Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Rules, collected by type.
data DefinedRules = DefinedRules
  { DefinedRules -> Rules
invertibleRules    :: Rules   -- ^ Invertible rules that simplify sequents.
  , DefinedRules -> Rules
tableauxRules      :: Rules   -- ^ Non-invertible tableaux rules.
  , DefinedRules -> Rules
invertibleCutRules :: Rules   -- ^ Invertible rules that add more topes in context.
  , DefinedRules -> Rules
tableauxCutRules   :: Rules   -- ^ Non-invertible tableaux rules that add more topes in context.
  }

instance Semigroup DefinedRules where
  DefinedRules Rules
r1 Rules
r2 Rules
r3 Rules
r4 <> :: DefinedRules -> DefinedRules -> DefinedRules
<> DefinedRules Rules
r1' Rules
r2' Rules
r3' Rules
r4'
    = Rules -> Rules -> Rules -> Rules -> DefinedRules
DefinedRules (Rules
r1 Rules -> Rules -> Rules
forall a. Semigroup a => a -> a -> a
<> Rules
r1') (Rules
r2 Rules -> Rules -> Rules
forall a. Semigroup a => a -> a -> a
<> Rules
r2') (Rules
r3 Rules -> Rules -> Rules
forall a. Semigroup a => a -> a -> a
<> Rules
r3') (Rules
r4 Rules -> Rules -> Rules
forall a. Semigroup a => a -> a -> a
<> Rules
r4')

instance Monoid DefinedRules where
  mempty :: DefinedRules
mempty = Rules -> Rules -> Rules -> Rules -> DefinedRules
DefinedRules Rules
forall a. Monoid a => a
mempty Rules
forall a. Monoid a => a
mempty Rules
forall a. Monoid a => a
mempty Rules
forall a. Monoid a => a
mempty

fromDefinedRules :: DefinedRules -> Rules
fromDefinedRules :: DefinedRules -> Rules
fromDefinedRules DefinedRules{Rules
tableauxCutRules :: Rules
invertibleCutRules :: Rules
tableauxRules :: Rules
invertibleRules :: Rules
tableauxCutRules :: DefinedRules -> Rules
invertibleCutRules :: DefinedRules -> Rules
tableauxRules :: DefinedRules -> Rules
invertibleRules :: DefinedRules -> Rules
..}
  = Rules -> Rules
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once Rules
invertibleRules Rules -> Rules -> Rules
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
`orElse`
      (Rules
tableauxRules Rules -> Rules -> Rules
forall a. Semigroup a => a -> a -> a
<>
        (Rules -> Rules
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once Rules
invertibleCutRules Rules -> Rules -> Rules
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
`orElse` Rules
tableauxCutRules))

-- ** Sets of rules

-- | Rules for intuitionistic tope logic:
--
-- * 'axiom' rule
-- * \(\land\)-rules ('leftAnd' and 'rightAnd')
-- * \(\lor\)-rules ('leftOr', 'rightOrL', and 'rightOrR')
-- * \(\Rightarrow\)-rules ('leftImplies', 'rightImplies')
rulesLJ :: DefinedRules
rulesLJ :: DefinedRules
rulesLJ = DefinedRules :: Rules -> Rules -> Rules -> Rules -> DefinedRules
DefinedRules
  { invertibleRules :: Rules
invertibleRules = [Rules] -> Rules
forall a. Monoid a => [a] -> a
mconcat
      [ Rules
axiom
      , Rules
leftAnd, Rules
rightAnd
      , Rules
leftOr
      , Rules
ruleTop
      , Rules
ruleBottom
      , Rules
rightImplies
      ]
  , invertibleCutRules :: Rules
invertibleCutRules = Rules
forall a. Monoid a => a
mempty
  , tableauxRules :: Rules
tableauxRules = [Rules] -> Rules
forall a. Monoid a => [a] -> a
mconcat
      [ Rules
rightOrL, Rules
rightOrR
      , Rules
leftImplies
      ]
  , tableauxCutRules :: Rules
tableauxCutRules = Rules
forall a. Monoid a => a
mempty
  }

-- | Rules for tope equality:
--
-- * reflexivity ('reflEQ')
-- * symmetry ('symEQ')
-- * transitivity ('transEQ')
-- * substitution ('substEQ')
rulesEQ :: DefinedRules
rulesEQ :: DefinedRules
rulesEQ = DefinedRules :: Rules -> Rules -> Rules -> Rules -> DefinedRules
DefinedRules
  { invertibleRules :: Rules
invertibleRules     = [Rules] -> Rules
forall a. Monoid a => [a] -> a
mconcat [ Rules
reflEQ, Rules
transEQ, Rules
symEQ ]
  , invertibleCutRules :: Rules
invertibleCutRules  = Rules
forall a. Monoid a => a
mempty
  , tableauxRules :: Rules
tableauxRules       = [Rules] -> Rules
forall a. Monoid a => [a] -> a
mconcat [ Rules
substEQ ]
  , tableauxCutRules :: Rules
tableauxCutRules    = Rules
forall a. Monoid a => a
mempty
  }

-- | Rules for intuitionistic tope logic with equality:
--
-- * intuitionistic rules 'rulesLJ'
-- * equality tope rules 'rulesEQ'
rulesLJE :: DefinedRules
rulesLJE :: DefinedRules
rulesLJE = DefinedRules
rulesLJ DefinedRules -> DefinedRules -> DefinedRules
forall a. Semigroup a => a -> a -> a
<> DefinedRules
rulesEQ

-- | Rules for inequality tope (not built-in).
--
-- * reflexivity ('reflLEQ')
-- * antisymmetry ('antisymLEQ')
-- * transitivity ('transLEQ')
-- * excluded middle ('lemLEQ')
-- * infimum ('zeroLEQ')
-- * supremum ('oneLEQ')
-- * distinctness of 0 and 1 ('distinctLEQ')
rulesLEQ :: Rules
rulesLEQ :: Rules
rulesLEQ = [Rules] -> Rules
forall a. Monoid a => [a] -> a
mconcat
  [ Rules
reflLEQ
  , Rules
transLEQ
  , Rules
antisymLEQ
  , Rules
lemLEQ
  , Rules
zeroLEQ
  , Rules
oneLEQ
  , Rules
distinctLEQ
  ]

-- ** Intuitionistic logic rules (LJ)

ruleTop :: Rules
ruleTop :: Rules
ruleTop = do
  Tope
TopeTop <- (Sequent -> Tope) -> RulesM Tope
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"⊤R", [])

ruleBottom :: Rules
ruleBottom :: Rules
ruleBottom = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (Tope
TopeBottom, TopeContext
_) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"⊥L", [])

leftAnd :: Rules
leftAnd :: Rules
leftAnd = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeAnd Tope
l Tope
r, TopeContext
topes) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"∧L", [Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTopeContext :: TopeContext
sequentTopeContext = Tope
l Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: Tope
r Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
topes, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}])

leftOr :: Rules
leftOr :: Rules
leftOr = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeOr Tope
l Tope
r, TopeContext
topes) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"∨L",
    [ Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTopeContext :: TopeContext
sequentTopeContext = Tope
l Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
topes, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}
    , Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTopeContext :: TopeContext
sequentTopeContext = Tope
r Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
topes, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..} ])

leftImplies :: Rules
leftImplies :: Rules
leftImplies = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeImplies Tope
l Tope
r, TopeContext
topes) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Tope
r Tope -> TopeContext -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` TopeContext
topes)
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"⇒L",
    [ Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTopeContext :: TopeContext
sequentTopeContext = Tope
r Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}
    , Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTope :: Tope
sequentTope = Tope
l, CubeContext
TopeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..} ])

rightImplies :: Rules
rightImplies :: Rules
rightImplies = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  TopeImplies Tope
l Tope
r <- Tope -> RulesM Tope
forall (m :: * -> *) a. Monad m => a -> m a
return Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"⇒R",
    [ Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTope :: Tope
sequentTope = Tope
r, sequentTopeContext :: TopeContext
sequentTopeContext = Tope
l Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext, CubeContext
sequentCubeContext :: CubeContext
sequentCubeContext :: CubeContext
..} ])

rightAnd :: Rules
rightAnd :: Rules
rightAnd = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  TopeAnd Tope
l Tope
r <- Tope -> RulesM Tope
forall (m :: * -> *) a. Monad m => a -> m a
return Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"∧R",
    [ Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTope :: Tope
sequentTope = Tope
l, CubeContext
TopeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..}
    , Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTope :: Tope
sequentTope = Tope
r, CubeContext
TopeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..} ])

rightOrL :: Rules
rightOrL :: Rules
rightOrL = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  TopeOr Tope
l Tope
_ <- Tope -> RulesM Tope
forall (m :: * -> *) a. Monad m => a -> m a
return Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"∨R₁", [ Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTope :: Tope
sequentTope = Tope
l, CubeContext
TopeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..} ])

rightOrR :: Rules
rightOrR :: Rules
rightOrR = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  TopeOr Tope
_ Tope
r <- Tope -> RulesM Tope
forall (m :: * -> *) a. Monad m => a -> m a
return Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"∨R₂", [ Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{ sequentTope :: Tope
sequentTope = Tope
r, CubeContext
TopeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..} ])

axiom :: Rules
axiom :: Rules
axiom = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Tope
sequentTope Tope -> TopeContext -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TopeContext
sequentTopeContext)
  ([Char], [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
"Ax", [])

-- ** Equality tope \((\equiv)\) rules

-- | Transitivity rule for equality tope (see 'TopeEQ').
--
-- @
-- ———————————
--  ⋅ ⊢ x ≡ x
-- @
reflEQ :: Rules
reflEQ :: Rules
reflEQ = do
  TopeEQ Point
l Point
r <- (Sequent -> Tope) -> RulesM Tope
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> Tope
sequentTope
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
l Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
r)
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≡R(refl)", [])

-- | Transitivity rule for equality tope (see 'TopeEQ').
--
-- @
--      x ≡ y, y ≡ z ⊢ φ
-- —————————————————————————
--  x ≡ y, y ≡ z, x ≡ z ⊢ φ
-- @
transEQ :: Rules
transEQ :: Rules
transEQ = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeEQ Point
x Point
y, TopeContext
ts) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  (TopeEQ Point
y' Point
z, TopeContext
_) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
ts
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
y Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
y' Bool -> Bool -> Bool
&& Point
x Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
/= Point
z Bool -> Bool -> Bool
&& Point -> Point -> Tope
TopeEQ Point
x Point
z Tope -> TopeContext -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` TopeContext
sequentTopeContext)
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≡L(trans)", [Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{sequentTopeContext :: TopeContext
sequentTopeContext = Point -> Point -> Tope
TopeEQ Point
x Point
z Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}])

-- | Symmetry rule for equality tope (see 'TopeEQ').
--
-- @
--     x ≡ y ⊢ φ
-- ——————————————————
--  x ≡ y, y ≡ x ⊢ φ
-- @
symEQ :: Rules
symEQ :: Rules
symEQ = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeEQ Point
x Point
y, TopeContext
ts) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
x Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
/= Point
y Bool -> Bool -> Bool
&& Point -> Point -> Tope
TopeEQ Point
y Point
x Tope -> TopeContext -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` TopeContext
ts)
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≡L(sym)", [Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{sequentTopeContext :: TopeContext
sequentTopeContext = Point -> Point -> Tope
TopeEQ Point
y Point
x Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}])

-- | Substitution rule for equality tope (see 'TopeEQ').
--
-- @
--    Г, x ≡ y ⊢ φ
-- —————————————————
--  Г[y/x] ⊢ φ[y/x]
-- @
--
-- NOTE: limited to replacing a variable, not an arbitrary point subterm.
substEQ :: Rules
substEQ :: Rules
substEQ = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeEQ Point
x Point
y, TopeContext
ts) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point -> Bool
isVar Point
x) -- TODO: generalize
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Point
x Point -> Point -> Bool
`subPointOf` Point
y))
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≡L(subst)", [Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent
    { sequentTopeContext :: TopeContext
sequentTopeContext = TopeContext -> TopeContext
forall a. Eq a => [a] -> [a]
nub ((Tope -> Tope) -> TopeContext -> TopeContext
forall a b. (a -> b) -> [a] -> [b]
map (Point -> Point -> Tope -> Tope
replacePointInTope Point
x Point
y) TopeContext
ts)
    , sequentTope :: Tope
sequentTope = Point -> Point -> Tope -> Tope
replacePointInTope Point
x Point
y Tope
sequentTope
    , CubeContext
sequentCubeContext :: CubeContext
sequentCubeContext :: CubeContext
.. }])
  where
    isVar :: Point -> Bool
isVar PointVar{} = Bool
True
    isVar Point
_          = Bool
False

-- ** Inequality tope \((\leq)\) rules

reflLEQ :: Rules
reflLEQ :: Rules
reflLEQ = do
  TopeCon (Label [Char]
"≤") [Point
x, Point
y] <- (Sequent -> Tope) -> RulesM Tope
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> Tope
sequentTope
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
x Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
y)
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤R(refl)", [])

transLEQ :: Rules
transLEQ :: Rules
transLEQ = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeCon (Label [Char]
"≤") [Point
x, Point
y], TopeContext
ts) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  (TopeCon (Label [Char]
"≤") [Point
y', Point
z], TopeContext
_) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
ts
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
y Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
y' Bool -> Bool -> Bool
&& Label -> [Point] -> Tope
TopeCon ([Char] -> Label
Label [Char]
"≤") [Point
x, Point
z] Tope -> TopeContext -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` TopeContext
sequentTopeContext)
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤L(trans)", [Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{sequentTopeContext :: TopeContext
sequentTopeContext = Label -> [Point] -> Tope
TopeCon ([Char] -> Label
Label [Char]
"≤") [Point
x, Point
z] Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}])

antisymLEQ :: Rules
antisymLEQ :: Rules
antisymLEQ = do
  Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  (TopeCon (Label [Char]
"≤") [Point
x, Point
y], TopeContext
ts) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
sequentTopeContext
  (TopeCon (Label [Char]
"≤") [Point
y', Point
x'], TopeContext
_) <- TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne TopeContext
ts
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
y Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
y' Bool -> Bool -> Bool
&& Point
x Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
x')
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤L(antisym)", [Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Sequent{sequentTopeContext :: TopeContext
sequentTopeContext = Point -> Point -> Tope
TopeEQ Point
x Point
y Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}])

lemLEQ :: Rules
lemLEQ :: Rules
lemLEQ = do
  TopeOr (TopeCon (Label [Char]
"≤") [Point
x, Point
y]) (TopeCon (Label [Char]
"≤") [Point
y', Point
x']) <- (Sequent -> Tope) -> RulesM Tope
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> Tope
sequentTope
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Point
x Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
x' Bool -> Bool -> Bool
&& Point
y Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
y')
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤R(lem)", [])

zeroLEQ :: Rules
zeroLEQ :: Rules
zeroLEQ = do
  TopeCon (Label [Char]
"≤") [PointCon Label
"𝟬" [], Point
_] <- (Sequent -> Tope) -> RulesM Tope
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤R(zero)", [])

oneLEQ :: Rules
oneLEQ :: Rules
oneLEQ = do
  TopeCon (Label [Char]
"≤") [Point
_, PointCon Label
"𝟭" []] <- (Sequent -> Tope) -> RulesM Tope
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> Tope
sequentTope
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤R(one)", [])

distinctLEQ :: Rules
distinctLEQ :: Rules
distinctLEQ = do
  (TopeEQ (PointCon Label
"𝟬" []) (PointCon Label
"𝟭" []), TopeContext
_) <- (Sequent -> TopeContext) -> RulesM TopeContext
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Sequent -> TopeContext
sequentTopeContext RulesM TopeContext
-> (TopeContext -> RulesM (Tope, TopeContext))
-> RulesM (Tope, TopeContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TopeContext -> RulesM (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne
  ([Char], [Sequent]) -> Rules
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"≤L(distinct)", [])

-- ** Helpers

-- | Try the second computation only if the first one fails (i.e. no backtracking).
--
-- The following examples show the difference between 'orElse' and 'mplus' for 'Logic':
--
-- >>> observeAll (pure 1 `orElse` pure 2)
-- [1]
-- >>> observeAll (pure 1 `mplus` pure 2)
-- [1,2]
--
-- >>> observeAll $ do { x <- pure 1 `orElse` pure 2; guard (even x); return x }
-- []
-- >>> observeAll $ do { x <- pure 1 `mplus` pure 2; guard (even x); return x }
-- [2]
orElse :: MonadLogic m => m a -> m a -> m a
orElse :: forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
orElse m a
mx m a
my =
  m a -> m (Maybe (a, m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit m a
mx m (Maybe (a, m a)) -> (Maybe (a, m a) -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (a, m a)
Nothing      -> m a
my
    Just (a
x, m a
xs) -> a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m a
xs

-- | Nondeterministically select exactly \(N\) elements from a given list,
-- also returning the remaining part of the list.
selectN :: Alternative f => Int -> [a] -> f ([a], [a])
selectN :: forall (f :: * -> *) a. Alternative f => Int -> [a] -> f ([a], [a])
selectN Int
n = [([a], [a])] -> f ([a], [a])
forall (f :: * -> *) a. Alternative f => [a] -> f a
choose ([([a], [a])] -> f ([a], [a]))
-> ([a] -> [([a], [a])]) -> [a] -> f ([a], [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [a] -> [([a], [a])]
forall {t} {a}. (Ord t, Num t) => t -> [a] -> [([a], [a])]
splits Int
n
  where
    splits :: t -> [a] -> [([a], [a])]
splits t
k [a]
as
      | t
k t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0 = [([], [a]
as)]
      | Bool
otherwise =
          [ (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys, [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
zs')
          | ([a]
xs, a
y:[a]
zs) <- [[a]] -> [[a]] -> [([a], [a])]
forall a b. [a] -> [b] -> [(a, b)]
zip ([a] -> [[a]]
forall a. [a] -> [[a]]
inits [a]
as) ([a] -> [[a]]
forall a. [a] -> [[a]]
tails [a]
as)
          , ([a]
ys, [a]
zs') <- t -> [a] -> [([a], [a])]
splits (t
k t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [a]
zs
          ]

-- | Nondeterministically select exactly one element from a given list,
-- also returning the remaining part of the list.
selectOne :: (Alternative f, MonadFail f) => [a] -> f (a, [a])
selectOne :: forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
selectOne [a]
xs = do
  ([a
y], [a]
zs) <- Int -> [a] -> f ([a], [a])
forall (f :: * -> *) a. Alternative f => Int -> [a] -> f ([a], [a])
selectN Int
1 [a]
xs
  (a, [a]) -> f (a, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (a
y, [a]
zs)

-- | Nondeterministically select exactly one element from a given list.
choose :: Alternative f => [a] -> f a
choose :: forall (f :: * -> *) a. Alternative f => [a] -> f a
choose = (f a -> f a -> f a) -> f a -> [f a] -> f a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) f a
forall (f :: * -> *) a. Alternative f => f a
empty ([f a] -> f a) -> ([a] -> [f a]) -> [a] -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> [a] -> [f a]
forall a b. (a -> b) -> [a] -> [b]
map a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- * Proof tree

-- | A complete proof is a proof tree without any unfinished parts.
type Proof = ProofTree Void

-- | A proof tree parametrized by the type of leaves (unfinished proofs).
data ProofTree a
  = Leaf a
  -- ^ A leaf represents an unfinished part of a proof.
  | Node Sequent RuleName [ProofTree a]
  -- ^ A node in a proof tree corresponds to a single rule application.
  deriving (ProofTree a -> ProofTree a -> Bool
(ProofTree a -> ProofTree a -> Bool)
-> (ProofTree a -> ProofTree a -> Bool) -> Eq (ProofTree a)
forall a. Eq a => ProofTree a -> ProofTree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofTree a -> ProofTree a -> Bool
$c/= :: forall a. Eq a => ProofTree a -> ProofTree a -> Bool
== :: ProofTree a -> ProofTree a -> Bool
$c== :: forall a. Eq a => ProofTree a -> ProofTree a -> Bool
Eq, Int -> ProofTree a -> ShowS
[ProofTree a] -> ShowS
ProofTree a -> [Char]
(Int -> ProofTree a -> ShowS)
-> (ProofTree a -> [Char])
-> ([ProofTree a] -> ShowS)
-> Show (ProofTree a)
forall a. Show a => Int -> ProofTree a -> ShowS
forall a. Show a => [ProofTree a] -> ShowS
forall a. Show a => ProofTree a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ProofTree a] -> ShowS
$cshowList :: forall a. Show a => [ProofTree a] -> ShowS
show :: ProofTree a -> [Char]
$cshow :: forall a. Show a => ProofTree a -> [Char]
showsPrec :: Int -> ProofTree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ProofTree a -> ShowS
Show, (forall a b. (a -> b) -> ProofTree a -> ProofTree b)
-> (forall a b. a -> ProofTree b -> ProofTree a)
-> Functor ProofTree
forall a b. a -> ProofTree b -> ProofTree a
forall a b. (a -> b) -> ProofTree a -> ProofTree 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 -> ProofTree b -> ProofTree a
$c<$ :: forall a b. a -> ProofTree b -> ProofTree a
fmap :: forall a b. (a -> b) -> ProofTree a -> ProofTree b
$cfmap :: forall a b. (a -> b) -> ProofTree a -> ProofTree b
Functor, (forall m. Monoid m => ProofTree m -> m)
-> (forall m a. Monoid m => (a -> m) -> ProofTree a -> m)
-> (forall m a. Monoid m => (a -> m) -> ProofTree a -> m)
-> (forall a b. (a -> b -> b) -> b -> ProofTree a -> b)
-> (forall a b. (a -> b -> b) -> b -> ProofTree a -> b)
-> (forall b a. (b -> a -> b) -> b -> ProofTree a -> b)
-> (forall b a. (b -> a -> b) -> b -> ProofTree a -> b)
-> (forall a. (a -> a -> a) -> ProofTree a -> a)
-> (forall a. (a -> a -> a) -> ProofTree a -> a)
-> (forall a. ProofTree a -> [a])
-> (forall a. ProofTree a -> Bool)
-> (forall a. ProofTree a -> Int)
-> (forall a. Eq a => a -> ProofTree a -> Bool)
-> (forall a. Ord a => ProofTree a -> a)
-> (forall a. Ord a => ProofTree a -> a)
-> (forall a. Num a => ProofTree a -> a)
-> (forall a. Num a => ProofTree a -> a)
-> Foldable ProofTree
forall a. Eq a => a -> ProofTree a -> Bool
forall a. Num a => ProofTree a -> a
forall a. Ord a => ProofTree a -> a
forall m. Monoid m => ProofTree m -> m
forall a. ProofTree a -> Bool
forall a. ProofTree a -> Int
forall a. ProofTree a -> [a]
forall a. (a -> a -> a) -> ProofTree a -> a
forall m a. Monoid m => (a -> m) -> ProofTree a -> m
forall b a. (b -> a -> b) -> b -> ProofTree a -> b
forall a b. (a -> b -> b) -> b -> ProofTree 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 => ProofTree a -> a
$cproduct :: forall a. Num a => ProofTree a -> a
sum :: forall a. Num a => ProofTree a -> a
$csum :: forall a. Num a => ProofTree a -> a
minimum :: forall a. Ord a => ProofTree a -> a
$cminimum :: forall a. Ord a => ProofTree a -> a
maximum :: forall a. Ord a => ProofTree a -> a
$cmaximum :: forall a. Ord a => ProofTree a -> a
elem :: forall a. Eq a => a -> ProofTree a -> Bool
$celem :: forall a. Eq a => a -> ProofTree a -> Bool
length :: forall a. ProofTree a -> Int
$clength :: forall a. ProofTree a -> Int
null :: forall a. ProofTree a -> Bool
$cnull :: forall a. ProofTree a -> Bool
toList :: forall a. ProofTree a -> [a]
$ctoList :: forall a. ProofTree a -> [a]
foldl1 :: forall a. (a -> a -> a) -> ProofTree a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ProofTree a -> a
foldr1 :: forall a. (a -> a -> a) -> ProofTree a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> ProofTree a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> ProofTree a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ProofTree a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ProofTree a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ProofTree a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ProofTree a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ProofTree a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ProofTree a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> ProofTree a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> ProofTree a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ProofTree a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ProofTree a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ProofTree a -> m
fold :: forall m. Monoid m => ProofTree m -> m
$cfold :: forall m. Monoid m => ProofTree m -> m
Foldable, Functor ProofTree
Foldable ProofTree
Functor ProofTree
-> Foldable ProofTree
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ProofTree a -> f (ProofTree b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    ProofTree (f a) -> f (ProofTree a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ProofTree a -> m (ProofTree b))
-> (forall (m :: * -> *) a.
    Monad m =>
    ProofTree (m a) -> m (ProofTree a))
-> Traversable ProofTree
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 =>
ProofTree (m a) -> m (ProofTree a)
forall (f :: * -> *) a.
Applicative f =>
ProofTree (f a) -> f (ProofTree a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ProofTree a -> m (ProofTree b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ProofTree a -> f (ProofTree b)
sequence :: forall (m :: * -> *) a.
Monad m =>
ProofTree (m a) -> m (ProofTree a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
ProofTree (m a) -> m (ProofTree a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ProofTree a -> m (ProofTree b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ProofTree a -> m (ProofTree b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
ProofTree (f a) -> f (ProofTree a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
ProofTree (f a) -> f (ProofTree a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ProofTree a -> f (ProofTree b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ProofTree a -> f (ProofTree b)
Traversable)

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

instance Monad ProofTree where
  return :: forall a. a -> ProofTree a
return = a -> ProofTree a
forall a. a -> ProofTree a
Leaf
  Leaf a
x >>= :: forall a b. ProofTree a -> (a -> ProofTree b) -> ProofTree b
>>= a -> ProofTree b
f      = a -> ProofTree b
f a
x
  Node Sequent
s [Char]
r [ProofTree a]
ts >>= a -> ProofTree b
f = Sequent -> [Char] -> [ProofTree b] -> ProofTree b
forall a. Sequent -> [Char] -> [ProofTree a] -> ProofTree a
Node Sequent
s [Char]
r ((ProofTree a -> ProofTree b) -> [ProofTree a] -> [ProofTree b]
forall a b. (a -> b) -> [a] -> [b]
map (ProofTree a -> (a -> ProofTree b) -> ProofTree b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProofTree b
f) [ProofTree a]
ts)

-- | Convert a proof tree into a complete proof if possible.
close :: Alternative f => ProofTree a -> f Proof
close :: forall (f :: * -> *) a. Alternative f => ProofTree a -> f Proof
close = (a -> f Void) -> ProofTree a -> f Proof
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (f Void -> a -> f Void
forall a b. a -> b -> a
const f Void
forall (f :: * -> *) a. Alternative f => f a
empty)

-- ** ASCII rendering

-- | Pretty print a proof tree (in ASCII form).
ppProof :: Proof -> String
ppProof :: Proof -> [Char]
ppProof = [(Int, [Char])] -> [Char]
ppNodesWithDepth ([(Int, [Char])] -> [Char])
-> (Proof -> [(Int, [Char])]) -> Proof -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> [(Int, [Char])]
proofNodesWithDepth

-- | Extract proof nodes with corresponding depths.
proofNodesWithDepth :: Proof -> [(Int, String)]
proofNodesWithDepth :: Proof -> [(Int, [Char])]
proofNodesWithDepth = Int -> Proof -> [(Int, [Char])]
forall {t}. Num t => t -> Proof -> [(t, [Char])]
go Int
0
  where
    go :: t -> Proof -> [(t, [Char])]
go t
i = \case
      Node Sequent
s [Char]
r [Proof]
ts -> (t
i, [Char]
"[" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
r [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"]" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"  " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Sequent -> [Char]
ppSequent Sequent
s) (t, [Char]) -> [(t, [Char])] -> [(t, [Char])]
forall a. a -> [a] -> [a]
: (Proof -> [(t, [Char])]) -> [Proof] -> [(t, [Char])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (t -> Proof -> [(t, [Char])]
go (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1)) [Proof]
ts
      Leaf Void
x      -> Void -> [(t, [Char])]
forall a. Void -> a
absurd Void
x

-- | Pretty-print depth-annotated nodes as a ASCII tree-like structure.
--
-- >>> putStr $ ppNodesWithDepth (zip [0,1,2,1,2,3,3,2,3] (map show [0..]))
-- 0
-- ├─ 1
-- │  └─ 2
-- └─ 3
--    ├─ 4
--    │  ├─ 5
--    │  └─ 6
--    └─ 7
--       └─ 8
ppNodesWithDepth :: [(Int, String)] -> String
ppNodesWithDepth :: [(Int, [Char])] -> [Char]
ppNodesWithDepth [(Int, [Char])]
xs = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
  ([Char] -> (Int, [Char]) -> [Char])
-> [[Char]] -> [(Int, [Char])] -> [[Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[Char]
t (Int, [Char])
x -> Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
3 ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [Char]
t [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Int, [Char]) -> [Char]
forall a b. (a, b) -> b
snd (Int, [Char])
x) ([Int] -> [[Char]]
depthsTree (((Int, [Char]) -> Int) -> [(Int, [Char])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [Char]) -> Int
forall a b. (a, b) -> a
fst [(Int, [Char])]
xs)) [(Int, [Char])]
xs

-- | Pretty-print an ASCII tree-like structure based on depth list.
--
-- >>> mapM_ putStrLn $ depthsTree [0,1,2,1,2,3,3,2,3]
-- └─
--    ├─
--    │  └─
--    └─
--       ├─
--       │  ├─
--       │  └─
--       └─
--          └─
depthsTree :: [Int] -> [String]
depthsTree :: [Int] -> [[Char]]
depthsTree = ShowS -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"─") ([[Char]] -> [[Char]]) -> ([Int] -> [[Char]]) -> [Int] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> ShowS) -> [[Char]] -> [[Char]]
forall a. (a -> a -> a) -> [a] -> [a]
scanr1 [Char] -> ShowS
prev ([[Char]] -> [[Char]]) -> ([Int] -> [[Char]]) -> [Int] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> [Char]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Int -> [Char]
defaultLine
  where
    defaultLine :: Int -> [Char]
defaultLine Int
i = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
i) Char
' ' [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"└"

    prev :: [Char] -> ShowS
prev [Char]
i []   = [Char]
i
    prev [Char]
i [Char]
next = (Char -> Char -> Char) -> [Char] -> ShowS
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Char -> Char -> Char
g [Char]
i ([Char]
next [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> [Char]
forall a. a -> [a]
repeat Char
' ')
      where
        g :: Char -> Char -> Char
g Char
' ' Char
'│' = Char
'│'
        g Char
' ' Char
'└' = Char
'│'
        g Char
'─' Char
'└' = Char
'┬'
        g Char
'└' Char
'│' = Char
'├'
        g Char
'└' Char
'└' = Char
'├'
        g Char
'─' Char
'├' = Char
'┬'
        g Char
c Char
_     = Char
c

-- * Provers

-- | A simple DFS proof search algorithm for a given set of rules.
proveWithDFS
  :: Int                        -- ^ Maximum search depth.
  -> Rules                      -- ^ Set of rules.
  -> Sequent                    -- ^ Starting sequent (one to prove).
  -> Logic (ProofTree Sequent)  -- ^ A proof tree, possibly with unproven sequents in leaves
                                -- (for when maximum search depth is insufficient).
proveWithDFS :: Int -> Rules -> Sequent -> Logic (ProofTree Sequent)
proveWithDFS Int
maxDepth Rules
rules Sequent
sequent =
  ProofTree (ProofTree Sequent) -> ProofTree Sequent
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ProofTree (ProofTree Sequent) -> ProofTree Sequent)
-> LogicT Identity (ProofTree (ProofTree Sequent))
-> Logic (ProofTree Sequent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Sequent -> Logic (ProofTree Sequent))
-> ProofTree Sequent
-> LogicT Identity (ProofTree (ProofTree Sequent))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Int -> Sequent -> Logic (ProofTree Sequent)
forall {t}.
(Ord t, Num t) =>
t -> Sequent -> Logic (ProofTree Sequent)
f Int
maxDepth) (Sequent -> ProofTree Sequent
forall a. a -> ProofTree a
Leaf Sequent
sequent)
  where
    f :: t -> Sequent -> Logic (ProofTree Sequent)
f t
n Sequent
s
      | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0 = ProofTree Sequent -> Logic (ProofTree Sequent)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sequent -> ProofTree Sequent
forall a. a -> ProofTree a
Leaf Sequent
s)
      | Bool
otherwise = do
          ([Char]
r, [Sequent]
ss) <- ReaderT Sequent (LogicT Identity) ([Char], [Sequent])
-> Sequent -> Logic ([Char], [Sequent])
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Rules -> ReaderT Sequent (LogicT Identity) ([Char], [Sequent])
forall a. RulesM a -> ReaderT Sequent (LogicT Identity) a
applyRulesM Rules
rules) Sequent
s
          [ProofTree Sequent]
ss' <- (Sequent -> Logic (ProofTree Sequent))
-> [Sequent] -> Logic [ProofTree Sequent]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (t -> Sequent -> Logic (ProofTree Sequent)
f (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1)) [Sequent]
ss
          ProofTree Sequent -> Logic (ProofTree Sequent)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sequent -> [Char] -> [ProofTree Sequent] -> ProofTree Sequent
forall a. Sequent -> [Char] -> [ProofTree a] -> ProofTree a
Node Sequent
s [Char]
r [ProofTree Sequent]
ss')

-- | A simple k-depth proof search algorithm for a given set of rules.
proveWithBFSviaDFS
  :: Int          -- ^ Maximum number of limited DFS iterations.
  -> Int          -- ^ Maximum depth per one DFS iteration.
  -> Rules        -- ^ A set of rules.
  -> Sequent      -- ^ A starting sequent (one to prove).
  -> Logic Proof
proveWithBFSviaDFS :: Int -> Int -> Rules -> Sequent -> Logic Proof
proveWithBFSviaDFS Int
maxDepth Int
k Rules
rules Sequent
sequent =
  Int -> Logic (ProofTree Sequent) -> Logic Proof
forall {t}.
(Ord t, Num t) =>
t -> Logic (ProofTree Sequent) -> Logic Proof
go (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
maxDepth) (ProofTree Sequent -> Logic (ProofTree Sequent)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sequent -> ProofTree Sequent
forall a. a -> ProofTree a
Leaf Sequent
sequent))
  where
    go :: t -> Logic (ProofTree Sequent) -> Logic Proof
go t
n Logic (ProofTree Sequent)
t
      | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0 = Logic Proof
forall (f :: * -> *) a. Alternative f => f a
empty
      | Bool
otherwise = do
          Logic (ProofTree Sequent)
-> Logic (Either [ProofTree Sequent] Proof)
forall a. Logic (ProofTree a) -> Logic (Either [ProofTree a] Proof)
tryClose Logic (ProofTree Sequent)
t Logic (Either [ProofTree Sequent] Proof)
-> (Either [ProofTree Sequent] Proof -> Logic Proof) -> Logic Proof
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Right Proof
proof -> Proof -> Logic Proof
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proof
proof
            Left [] -> Logic Proof
forall (f :: * -> *) a. Alternative f => f a
empty
            Left [ProofTree Sequent]
incompletes -> {- trace (unlines $
              [ "Trying at level " <> show (maxDepth - n + 1) <> " (with k=" <> show k <> "), having " <> show (length incompletes) <> " partial proofs:"
              , unlines (map (ppProof . markIncomplete) $ take 10 incompletes)
              ]) $ -}
              t -> Logic (ProofTree Sequent) -> Logic Proof
go (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Logic (ProofTree Sequent) -> Logic Proof)
-> Logic (ProofTree Sequent) -> Logic Proof
forall a b. (a -> b) -> a -> b
$ do
                ProofTree (ProofTree Sequent) -> ProofTree Sequent
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ProofTree (ProofTree Sequent) -> ProofTree Sequent)
-> LogicT Identity (ProofTree (ProofTree Sequent))
-> Logic (ProofTree Sequent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([ProofTree Sequent] -> Logic (ProofTree Sequent)
forall (f :: * -> *) a. Alternative f => [a] -> f a
choose [ProofTree Sequent]
incompletes Logic (ProofTree Sequent)
-> (ProofTree Sequent
    -> LogicT Identity (ProofTree (ProofTree Sequent)))
-> LogicT Identity (ProofTree (ProofTree Sequent))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Sequent -> Logic (ProofTree Sequent))
-> ProofTree Sequent
-> LogicT Identity (ProofTree (ProofTree Sequent))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Int -> Rules -> Sequent -> Logic (ProofTree Sequent)
proveWithDFS Int
k Rules
rules))

markIncomplete :: ProofTree Sequent -> Proof
markIncomplete :: ProofTree Sequent -> Proof
markIncomplete = \case
  Leaf Sequent
x         -> Sequent -> [Char] -> [Proof] -> Proof
forall a. Sequent -> [Char] -> [ProofTree a] -> ProofTree a
Node Sequent
x [Char]
"incomplete" []
  Node Sequent
x [Char]
name [ProofTree Sequent]
ts -> Sequent -> [Char] -> [Proof] -> Proof
forall a. Sequent -> [Char] -> [ProofTree a] -> ProofTree a
Node Sequent
x [Char]
name (ProofTree Sequent -> Proof
markIncomplete (ProofTree Sequent -> Proof) -> [ProofTree Sequent] -> [Proof]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProofTree Sequent]
ts)

tryClose :: Logic (ProofTree a) -> Logic (Either [ProofTree a] Proof)
tryClose :: forall a. Logic (ProofTree a) -> Logic (Either [ProofTree a] Proof)
tryClose Logic (ProofTree a)
m =
  Logic (ProofTree a)
-> LogicT Identity (Maybe (ProofTree a, Logic (ProofTree a)))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit Logic (ProofTree a)
m LogicT Identity (Maybe (ProofTree a, Logic (ProofTree a)))
-> (Maybe (ProofTree a, Logic (ProofTree a))
    -> LogicT Identity (Either [ProofTree a] Proof))
-> LogicT Identity (Either [ProofTree a] Proof)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (ProofTree a, Logic (ProofTree a))
Nothing      -> Either [ProofTree a] Proof
-> LogicT Identity (Either [ProofTree a] Proof)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ProofTree a] -> Either [ProofTree a] Proof
forall a b. a -> Either a b
Left [])
    Just (ProofTree a
x, Logic (ProofTree a)
xs) ->
          (Proof -> Either [ProofTree a] Proof)
-> Logic Proof -> LogicT Identity (Either [ProofTree a] Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof -> Either [ProofTree a] Proof
forall a b. b -> Either a b
Right (ProofTree a -> Logic Proof
forall (f :: * -> *) a. Alternative f => ProofTree a -> f Proof
close ProofTree a
x)
      LogicT Identity (Either [ProofTree a] Proof)
-> LogicT Identity (Either [ProofTree a] Proof)
-> LogicT Identity (Either [ProofTree a] Proof)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Either [ProofTree a] Proof -> Either [ProofTree a] Proof)
-> LogicT Identity (Either [ProofTree a] Proof)
-> LogicT Identity (Either [ProofTree a] Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([ProofTree a] -> [ProofTree a])
-> Either [ProofTree a] Proof -> Either [ProofTree a] Proof
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ProofTree a
xProofTree a -> [ProofTree a] -> [ProofTree a]
forall a. a -> [a] -> [a]
:)) (Logic (ProofTree a) -> LogicT Identity (Either [ProofTree a] Proof)
forall a. Logic (ProofTree a) -> Logic (Either [ProofTree a] Proof)
tryClose Logic (ProofTree a)
xs)

-- | Search for a proof using simple DFS algorithm (see 'proveWithDFS').
proveWithDFS'
  :: Int                        -- ^ Maximum search depth.
  -> Rules                      -- ^ Set of rules.
  -> Sequent                    -- ^ Starting sequent (one to prove).
  -> Maybe Proof
proveWithDFS' :: Int -> Rules -> Sequent -> Maybe Proof
proveWithDFS' Int
maxDepth Rules
rules Sequent
sequent =
  case Int -> Logic Proof -> [Proof]
forall a. Int -> Logic a -> [a]
observeMany Int
1 (Int -> Rules -> Sequent -> Logic (ProofTree Sequent)
proveWithDFS Int
maxDepth Rules
rules Sequent
sequent Logic (ProofTree Sequent)
-> (ProofTree Sequent -> Logic Proof) -> Logic Proof
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProofTree Sequent -> Logic Proof
forall (f :: * -> *) a. Alternative f => ProofTree a -> f Proof
close) of
    []  -> Maybe Proof
forall a. Maybe a
Nothing
    Proof
p:[Proof]
_ -> Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
p

-- | Search for a proof using a combination of BFS and DFS algorithms (see 'proveWithBFS').
proveWithBFSviaDFS'
  :: Int          -- ^ Maximum number of limited DFS iterations.
  -> Int          -- ^ Maximum depth per one DFS iteration.
  -> Rules        -- ^ A set of rules.
  -> Sequent      -- ^ A starting sequent (one to prove).
  -> Maybe Proof
proveWithBFSviaDFS' :: Int -> Int -> Rules -> Sequent -> Maybe Proof
proveWithBFSviaDFS' Int
maxDepth Int
k Rules
rules Sequent
sequent =
  case Int -> Logic Proof -> [Proof]
forall a. Int -> Logic a -> [a]
observeMany Int
1 (Int -> Int -> Rules -> Sequent -> Logic Proof
proveWithBFSviaDFS Int
maxDepth Int
k Rules
rules Sequent
sequent) of
    []  -> Maybe Proof
forall a. Maybe a
Nothing
    Proof
p:[Proof]
_ -> Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
p

-- ** With printers

-- | Search for a proof using BFS and print proof tree (see 'ppProof').
proveAndPrintBFS
  :: Int                        -- ^ Maximum search depth.
  -> Rules                      -- ^ Set of rules.
  -> Sequent                    -- ^ Starting sequent (one to prove).
  -> IO ()
proveAndPrintBFS :: Int -> Rules -> Sequent -> IO ()
proveAndPrintBFS Int
maxDepth = Int -> Int -> Rules -> Sequent -> IO ()
proveAndPrintBFSviaDFS Int
maxDepth Int
1

-- | Search for a proof using a combination of BFS and DFS
-- and print proof tree (see 'ppProof').
proveAndPrintBFSviaDFS :: Int -> Int -> Rules -> Sequent -> IO ()
proveAndPrintBFSviaDFS :: Int -> Int -> Rules -> Sequent -> IO ()
proveAndPrintBFSviaDFS Int
maxDepth Int
k Rules
rules Sequent
sequent = do
  case Int -> Int -> Rules -> Sequent -> Maybe Proof
proveWithBFSviaDFS' Int
maxDepth Int
k Rules
rules Sequent
sequent of
    Just Proof
p  -> [Char] -> IO ()
putStrLn (Proof -> [Char]
ppProof Proof
p)
    Maybe Proof
Nothing -> [Char] -> IO ()
putStrLn ([Char]
"The sequent is not provable: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Sequent -> [Char]
ppSequent Sequent
sequent)

-- | Search for a proof using DFS and print proof tree (see 'ppProof').
proveAndPrintDFS :: Int -> Rules -> Sequent -> IO ()
proveAndPrintDFS :: Int -> Rules -> Sequent -> IO ()
proveAndPrintDFS Int
maxDepth Rules
rules Sequent
sequent = do
  case Int -> Rules -> Sequent -> Maybe Proof
proveWithDFS' Int
maxDepth Rules
rules Sequent
sequent of
    Just Proof
p  -> [Char] -> IO ()
putStrLn (Proof -> [Char]
ppProof Proof
p)
    Maybe Proof
Nothing -> [Char] -> IO ()
putStrLn ([Char]
"The sequent is not provable: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Sequent -> [Char]
ppSequent Sequent
sequent)

-- * Examples

-- |
-- >>> putStrLn (ppSequent ex1)
-- ⋅ | (φ ∨ ζ) ∧ (ψ ∨ χ) ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--
-- >>> proveAndPrintBFS 8 (fromDefinedRules rulesLJ) ex1
-- [∧L]  ⋅ | (φ ∨ ζ) ∧ (ψ ∨ χ) ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
-- └─ [∨L]  ⋅ | φ ∨ ζ, ψ ∨ χ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--    ├─ [∨L]  ⋅ | φ, ψ ∨ χ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--    │  ├─ [∨R₁]  ⋅ | ψ, φ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--    │  │  └─ [∧R]  ⋅ | ψ, φ ⊢ φ ∧ ψ
--    │  │     ├─ [Ax]  ⋅ | ψ, φ ⊢ φ
--    │  │     └─ [Ax]  ⋅ | ψ, φ ⊢ ψ
--    │  └─ [∨R₂]  ⋅ | χ, φ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--    │     └─ [∨R₂]  ⋅ | χ, φ ⊢ ζ ∧ ψ ∨ χ
--    │        └─ [Ax]  ⋅ | χ, φ ⊢ χ
--    └─ [∨L]  ⋅ | ζ, ψ ∨ χ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--       ├─ [∨R₂]  ⋅ | ψ, ζ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--       │  └─ [∨R₁]  ⋅ | ψ, ζ ⊢ ζ ∧ ψ ∨ χ
--       │     └─ [∧R]  ⋅ | ψ, ζ ⊢ ζ ∧ ψ
--       │        ├─ [Ax]  ⋅ | ψ, ζ ⊢ ζ
--       │        └─ [Ax]  ⋅ | ψ, ζ ⊢ ψ
--       └─ [∨R₂]  ⋅ | χ, ζ ⊢ φ ∧ ψ ∨ ζ ∧ ψ ∨ χ
--          └─ [∨R₂]  ⋅ | χ, ζ ⊢ ζ ∧ ψ ∨ χ
--             └─ [Ax]  ⋅ | χ, ζ ⊢ χ
ex1 :: Sequent
ex1 :: Sequent
ex1 = CubeContext -> TopeContext -> Tope -> Sequent
Sequent []
  [ (Tope
"φ" Tope -> Tope -> Tope
`TopeOr` Tope
"ζ") Tope -> Tope -> Tope
`TopeAnd` (Tope
"ψ" Tope -> Tope -> Tope
`TopeOr` Tope
"χ") ]
  ((Tope
"φ" Tope -> Tope -> Tope
`TopeAnd` Tope
"ψ") Tope -> Tope -> Tope
`TopeOr` ((Tope
"ζ" Tope -> Tope -> Tope
`TopeAnd` Tope
"ψ") Tope -> Tope -> Tope
`TopeOr` Tope
"χ"))

-- |
-- >>> putStrLn (ppSequent ex2)
-- ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ (φ ∨ ζ) ∧ (ψ ∨ χ)
--
-- >>> proveAndPrintBFS 8 (fromDefinedRules rulesLJ) ex2
-- [∧R]  ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ (φ ∨ ζ) ∧ (ψ ∨ χ)
-- ├─ [∨L]  ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ φ ∨ ζ
-- │  ├─ [∧L]  ⋅ | φ ∧ ψ ⊢ φ ∨ ζ
-- │  │  └─ [∨R₁]  ⋅ | φ, ψ ⊢ φ ∨ ζ
-- │  │     └─ [Ax]  ⋅ | φ, ψ ⊢ φ
-- │  └─ [∧L]  ⋅ | ζ ∧ χ ⊢ φ ∨ ζ
-- │     └─ [∨R₂]  ⋅ | ζ, χ ⊢ φ ∨ ζ
-- │        └─ [Ax]  ⋅ | ζ, χ ⊢ ζ
-- └─ [∨L]  ⋅ | φ ∧ ψ ∨ ζ ∧ χ ⊢ ψ ∨ χ
--    ├─ [∧L]  ⋅ | φ ∧ ψ ⊢ ψ ∨ χ
--    │  └─ [∨R₁]  ⋅ | φ, ψ ⊢ ψ ∨ χ
--    │     └─ [Ax]  ⋅ | φ, ψ ⊢ ψ
--    └─ [∧L]  ⋅ | ζ ∧ χ ⊢ ψ ∨ χ
--       └─ [∨R₂]  ⋅ | ζ, χ ⊢ ψ ∨ χ
--          └─ [Ax]  ⋅ | ζ, χ ⊢ χ
ex2 :: Sequent
ex2 :: Sequent
ex2 = CubeContext -> TopeContext -> Tope -> Sequent
Sequent []
  [ (Tope
"φ" Tope -> Tope -> Tope
`TopeAnd` Tope
"ψ") Tope -> Tope -> Tope
`TopeOr` (Tope
"ζ" Tope -> Tope -> Tope
`TopeAnd` Tope
"χ") ]
  ((Tope
"φ" Tope -> Tope -> Tope
`TopeOr` Tope
"ζ") Tope -> Tope -> Tope
`TopeAnd` (Tope
"ψ" Tope -> Tope -> Tope
`TopeOr` Tope
"χ"))

-- |
-- >>> putStrLn (ppSequent ex3)
-- ⋅ | x ≡ y ∧ y ≡ z ⊢ z ≡ x
--
-- >>> proveAndPrintBFS 35 (fromDefinedRules rulesLJE) ex3
-- [∧L]  ⋅ | x ≡ y ∧ y ≡ z ⊢ z ≡ x
-- └─ [≡L(trans)]  ⋅ | x ≡ y, y ≡ z ⊢ z ≡ x
--    └─ [≡L(sym)]  ⋅ | x ≡ z, x ≡ y, y ≡ z ⊢ z ≡ x
--       └─ [Ax]  ⋅ | z ≡ x, x ≡ z, x ≡ y, y ≡ z ⊢ z ≡ x
ex3 :: Sequent
ex3 :: Sequent
ex3 = CubeContext -> TopeContext -> Tope -> Sequent
Sequent []
  [ Point -> Point -> Tope
TopeEQ Point
"x" Point
"y" Tope -> Tope -> Tope
`TopeAnd` Point -> Point -> Tope
TopeEQ Point
"y" Point
"z" ]
  (Point -> Point -> Tope
TopeEQ Point
"z" Point
"x")

-- |
-- >>> putStrLn (ppSequent ex4)
-- ⋅ | (t ≡ s ∨ t ≡ u) ∧ s ≡ u ⊢ t ≡ s
--
-- >>> proveAndPrintBFS 8 (fromDefinedRules rulesLJE) ex4
-- [∧L]  ⋅ | (t ≡ s ∨ t ≡ u) ∧ s ≡ u ⊢ t ≡ s
-- └─ [∨L]  ⋅ | t ≡ s ∨ t ≡ u, s ≡ u ⊢ t ≡ s
--    ├─ [Ax]  ⋅ | t ≡ s, s ≡ u ⊢ t ≡ s
--    └─ [≡L(sym)]  ⋅ | t ≡ u, s ≡ u ⊢ t ≡ s
--       └─ [≡L(trans)]  ⋅ | u ≡ t, t ≡ u, s ≡ u ⊢ t ≡ s
--          └─ [≡L(sym)]  ⋅ | s ≡ t, u ≡ t, t ≡ u, s ≡ u ⊢ t ≡ s
--             └─ [Ax]  ⋅ | t ≡ s, s ≡ t, u ≡ t, t ≡ u, s ≡ u ⊢ t ≡ s
ex4 :: Sequent
ex4 :: Sequent
ex4 = CubeContext -> TopeContext -> Tope -> Sequent
Sequent []
  [ (Point -> Point -> Tope
TopeEQ Point
"t" Point
"s" Tope -> Tope -> Tope
`TopeOr` Point -> Point -> Tope
TopeEQ Point
"t" Point
"u") Tope -> Tope -> Tope
`TopeAnd` Point -> Point -> Tope
TopeEQ Point
"s" Point
"u" ]
  (Point -> Point -> Tope
TopeEQ Point
"t" Point
"s")

-- |
-- >>> putStrLn (ppSequent ex5)
-- ⋅ | (≤(t, s) ∨ ≤(s, u)) ∧ ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
--
-- >>> proveAndPrintBFS 5 (fromDefinedRules rulesLJE) ex5
-- [∧L]  ⋅ | (≤(t, s) ∨ ≤(s, u)) ∧ ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
-- └─ [∨L]  ⋅ | ≤(t, s) ∨ ≤(s, u), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
--    ├─ [∨R₁]  ⋅ | ≤(t, s), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
--    │  └─ [∨R₁]  ⋅ | ≤(t, s), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t)
--    │     └─ [Ax]  ⋅ | ≤(t, s), ≤(t, u) ⊢ ≤(t, u)
--    └─ [∨R₁]  ⋅ | ≤(s, u), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t) ∨ ≤(u, s)
--       └─ [∨R₁]  ⋅ | ≤(s, u), ≤(t, u) ⊢ ≤(t, u) ∨ ≤(s, t)
--          └─ [Ax]  ⋅ | ≤(s, u), ≤(t, u) ⊢ ≤(t, u)
ex5 :: Sequent
ex5 :: Sequent
ex5 = CubeContext -> TopeContext -> Tope -> Sequent
Sequent []
  [ (Label -> [Point] -> Tope
TopeCon Label
"≤" [Point
"t", Point
"s"] Tope -> Tope -> Tope
`TopeOr` Label -> [Point] -> Tope
TopeCon Label
"≤" [Point
"s", Point
"u"]) Tope -> Tope -> Tope
`TopeAnd` Label -> [Point] -> Tope
TopeCon Label
"≤" [Point
"t", Point
"u"] ]
  (Label -> [Point] -> Tope
TopeCon Label
"≤" [Point
"t", Point
"u"] Tope -> Tope -> Tope
`TopeOr` Label -> [Point] -> Tope
TopeCon Label
"≤" [Point
"s", Point
"t"] Tope -> Tope -> Tope
`TopeOr` Label -> [Point] -> Tope
TopeCon Label
"≤" [Point
"u", Point
"s"])