-- |
-- Module      : AutoProof.Internal.Intuitionistic.Proof.Cut
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Functions related to cuts in proofs.
module AutoProof.Internal.Intuitionistic.Proof.Cut (findCut, hasCut) where

import AutoProof.Internal.AST (children)
import AutoProof.Internal.Proof.Types
  ( Proof
      ( AndElimL,
        AndElimR,
        AndIntr,
        IffElimL,
        IffElimR,
        IffIntr,
        ImpElim,
        ImpIntr,
        NotElim,
        NotIntr,
        OrElim,
        OrIntrL,
        OrIntrR
      ),
  )
import Control.Applicative ((<|>))
import Data.Maybe (isJust)

-- | Find the cut nearest the root of a proof, if any. This functions assumes
-- the proof is valid.
findCut :: Proof a -> Maybe (Proof a)
findCut :: Proof a -> Maybe (Proof a)
findCut p :: Proof a
p@(ImpElim _ ImpIntr {} _) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(NotElim _ NotIntr {} _) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(OrElim _ OrIntrL {} _ _) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(OrElim _ OrIntrR {} _ _) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(AndElimL _ AndIntr {}) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(AndElimR _ AndIntr {}) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(IffElimL _ IffIntr {}) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p@(IffElimR _ IffIntr {}) = Proof a -> Maybe (Proof a)
forall a. a -> Maybe a
Just Proof a
p
findCut p :: Proof a
p = (Proof a -> Maybe (Proof a) -> Maybe (Proof a))
-> Maybe (Proof a) -> [Proof a] -> Maybe (Proof a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Maybe (Proof a) -> Maybe (Proof a) -> Maybe (Proof a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Maybe (Proof a) -> Maybe (Proof a) -> Maybe (Proof a))
-> (Proof a -> Maybe (Proof a))
-> Proof a
-> Maybe (Proof a)
-> Maybe (Proof a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof a -> Maybe (Proof a)
forall a. Proof a -> Maybe (Proof a)
findCut) Maybe (Proof a)
forall a. Maybe a
Nothing (Proof a -> [Proof a]
forall t. AST t => t -> [t]
children Proof a
p)

-- | Check if a proof has a cut.
hasCut :: Proof a -> Bool
hasCut :: Proof a -> Bool
hasCut = Maybe (Proof a) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Proof a) -> Bool)
-> (Proof a -> Maybe (Proof a)) -> Proof a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof a -> Maybe (Proof a)
forall a. Proof a -> Maybe (Proof a)
findCut