{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}

{-|
Module       : ATP.Pretty.FOL
Description  : Pretty-printers for formulas, theorems and proofs.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental

Pretty-printers for formulas, theorems and proofs.
-}

module ATP.Pretty.FOL (
  Pretty(..),
  pprint,
  hprint
) where

import Control.Applicative (liftA2)
import Control.Monad (foldM)
import Data.Char (digitToInt)
import Data.Foldable (toList)
import Data.Functor (($>))
import Data.List (genericIndex, find)
import Data.List.NonEmpty (NonEmpty(..), nonEmpty)
import Data.Map (Map, (!))
import qualified Data.Text as T (unpack, null)
import System.IO (Handle)

import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))

import ATP.Internal.Enumeration

import ATP.Error
import ATP.FOL


-- * Helper functions

-- | Pretty print to the standard output.
pprint :: Pretty a => a -> IO ()
pprint :: a -> IO ()
pprint = Doc -> IO ()
putDoc (Doc -> IO ()) -> (a -> Doc) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty

-- | Pretty print to an IO handle.
hprint :: Pretty a => Handle -> a -> IO ()
hprint :: Handle -> a -> IO ()
hprint Handle
h = Handle -> Doc -> IO ()
hPutDoc Handle
h (Doc -> IO ()) -> (a -> Doc) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty

prettySequent :: Pretty a => Doc -> a -> Doc
prettySequent :: Doc -> a -> Doc
prettySequent Doc
h a
f = Doc -> Doc
bold (Doc
h Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot) Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
line

prettySequents :: Pretty a => Doc -> [a] -> Doc
prettySequents :: Doc -> [a] -> Doc
prettySequents Doc
h = [Doc] -> Doc
hcat ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> a -> Doc) -> [Integer] -> [a] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Integer -> a -> Doc
forall a. Pretty a => Integer -> a -> Doc
sequent [Integer
1..]
  where sequent :: Integer -> a -> Doc
sequent Integer
i = Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
prettySequent (Doc
h Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
i)


-- * Pretty printer for formulas

prettyVar :: Var -> Doc
prettyVar :: Integer -> Doc
prettyVar Integer
v = Doc -> Doc
cyan (Doc -> Doc) -> (String -> Doc) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> Integer -> String
forall i a. Integral i => [a] -> i -> a
genericIndex [String]
variables (Integer -> Integer
forall a. Num a => a -> a
abs Integer
v)
  where
    variables :: [String]
    variables :: [String]
variables = (Integer -> String -> String) -> [Integer] -> [String] -> [String]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Integer -> String -> String
prime [Integer
0..] [String
"v", String
"x", String
"y", String
"z", String
"t"]

    prime :: Integer -> String -> String
    prime :: Integer -> String -> String
prime Integer
n String
w = String
letter String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
index
      where
        letter :: String
letter = if Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then String
w  else String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"′"
        index :: String
index  = if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then String
"" else (Int -> Char) -> [Int] -> String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"₀₁₂₃₄₅₆₇₈₉" String -> Int -> Char
forall a. [a] -> Int -> a
!!) (Integer -> [Int]
digits Integer
n)
        digits :: Integer -> [Int]
digits = (Char -> Int) -> String -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Int
digitToInt (String -> [Int]) -> (Integer -> String) -> Integer -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show

sepBy :: Doc -> NonEmpty Doc -> Doc
sepBy :: Doc -> NonEmpty Doc -> Doc
sepBy Doc
s = (Doc -> Doc -> Doc) -> NonEmpty Doc -> Doc
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (\Doc
a Doc
b -> Doc
a Doc -> Doc -> Doc
<+> Doc
s Doc -> Doc -> Doc
<+> Doc
b)

commaSep :: NonEmpty Doc -> Doc
commaSep :: NonEmpty Doc -> Doc
commaSep (Doc
d :| [Doc]
ds) = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
d Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat ((Doc -> Doc) -> [Doc] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc
comma Doc -> Doc -> Doc
<+>) [Doc]
ds)

prettyApplication :: Doc -> [Doc] -> Doc
prettyApplication :: Doc -> [Doc] -> Doc
prettyApplication Doc
s [Doc]
as
  | Just NonEmpty Doc
as' <- [Doc] -> Maybe (NonEmpty Doc)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Doc]
as = Doc
s Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (NonEmpty Doc -> Doc
commaSep NonEmpty Doc
as')
  | Bool
otherwise = Doc
s

prettyParens :: Pretty e => (e -> Bool) -> e -> Doc
prettyParens :: (e -> Bool) -> e -> Doc
prettyParens e -> Bool
simple e
e
  | e -> Bool
simple e
e  = e -> Doc
forall a. Pretty a => a -> Doc
pretty e
e
  | Bool
otherwise = Doc -> Doc
parens (e -> Doc
forall a. Pretty a => a -> Doc
pretty e
e)

instance Pretty FunctionSymbol where
  pretty :: FunctionSymbol -> Doc
pretty (FunctionSymbol Text
s) = String -> Doc
text (Text -> String
T.unpack Text
s)

instance Pretty Term where
  pretty :: Term -> Doc
pretty = \case
    Variable Integer
v    -> Integer -> Doc
prettyVar Integer
v
    Function FunctionSymbol
f [Term]
ts -> Doc -> [Doc] -> Doc
prettyApplication (FunctionSymbol -> Doc
forall a. Pretty a => a -> Doc
pretty FunctionSymbol
f) ((Term -> Doc) -> [Term] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Doc
forall a. Pretty a => a -> Doc
pretty [Term]
ts)

instance Pretty PredicateSymbol where
  pretty :: PredicateSymbol -> Doc
pretty (PredicateSymbol Text
p) = String -> Doc
text (Text -> String
T.unpack Text
p)

instance Pretty Literal where
  pretty :: Literal -> Doc
pretty = \case
    Propositional Bool
True  -> Doc -> Doc
blue Doc
"⟙"
    Propositional Bool
False -> Doc -> Doc
blue Doc
"⟘"
    Predicate PredicateSymbol
p [Term]
ts -> Doc -> [Doc] -> Doc
prettyApplication (PredicateSymbol -> Doc
forall a. Pretty a => a -> Doc
pretty PredicateSymbol
p) ((Term -> Doc) -> [Term] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Doc
forall a. Pretty a => a -> Doc
pretty [Term]
ts)
    Equality Term
a Term
b   -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
a Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
b

instance Pretty (Signed Literal) where
  pretty :: Signed Literal -> Doc
pretty = \case
    Signed Sign
Negative (Equality Term
a Term
b) -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
a Doc -> Doc -> Doc
<+> Doc
"!=" Doc -> Doc -> Doc
<+> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
b
    Signed Sign
Negative Literal
l -> Doc -> Doc
blue Doc
"￢" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
    Signed Sign
Positive Literal
l -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l

instance Pretty Clause where
  pretty :: Clause -> Doc
pretty (Literals [Signed Literal]
ls) = case [Signed Literal] -> Maybe (NonEmpty (Signed Literal))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Signed Literal]
ls of
    Maybe (NonEmpty (Signed Literal))
Nothing  -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty (Bool -> Literal
Propositional Bool
False)
    Just NonEmpty (Signed Literal)
nls -> Doc -> NonEmpty Doc -> Doc
sepBy (Connective -> Doc
forall a. Pretty a => a -> Doc
pretty Connective
Or) ((Signed Literal -> Doc)
-> NonEmpty (Signed Literal) -> NonEmpty Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Signed Literal -> Doc
forall a. Pretty a => a -> Doc
pretty NonEmpty (Signed Literal)
nls)

  prettyList :: [Clause] -> Doc
prettyList = Doc -> [Clause] -> Doc
forall a. Pretty a => Doc -> [a] -> Doc
prettySequents Doc
"Axiom"

instance Pretty Connective where
  pretty :: Connective -> Doc
pretty = Doc -> Doc
blue (Doc -> Doc) -> (Connective -> Doc) -> Connective -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Connective
And        -> Doc
"⋀"
    Connective
Or         -> Doc
"⋁"
    Connective
Implies    -> Doc
"=>"
    Connective
Equivalent -> Doc
"<=>"
    Connective
Xor        -> Doc
"<~>"

instance Pretty Quantifier where
  pretty :: Quantifier -> Doc
pretty = \case
    Quantifier
Forall -> Doc
"∀"
    Quantifier
Exists -> Doc
"∃"

instance Pretty Formula where
  pretty :: Formula -> Doc
pretty = \case
    Atomic Literal
l -> Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
    Negate (Atomic (Equality Term
a Term
b)) -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
a Doc -> Doc -> Doc
<+> Doc
"!=" Doc -> Doc -> Doc
<+> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
b
    Negate Formula
f -> Doc -> Doc
blue Doc
"￢" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (Formula -> Bool) -> Formula -> Doc
forall e. Pretty e => (e -> Bool) -> e -> Doc
prettyParens Formula -> Bool
unitary Formula
f
    Connected  Connective
c Formula
f Formula
g -> (Formula -> Bool) -> Formula -> Doc
forall e. Pretty e => (e -> Bool) -> e -> Doc
prettyParens (Connective -> Formula -> Bool
under Connective
c) Formula
f Doc -> Doc -> Doc
<+> Connective -> Doc
forall a. Pretty a => a -> Doc
pretty Connective
c
                    Doc -> Doc -> Doc
<+> (Formula -> Bool) -> Formula -> Doc
forall e. Pretty e => (e -> Bool) -> e -> Doc
prettyParens (Connective -> Formula -> Bool
under Connective
c) Formula
g
    Quantified Quantifier
q Integer
v Formula
f -> Quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty Quantifier
q Doc -> Doc -> Doc
<+> Integer -> Doc
prettyVar Integer
v Doc -> Doc -> Doc
<+> Doc
dot
                    Doc -> Doc -> Doc
<+> (Formula -> Bool) -> Formula -> Doc
forall e. Pretty e => (e -> Bool) -> e -> Doc
prettyParens Formula -> Bool
unitary Formula
f

  prettyList :: [Formula] -> Doc
prettyList = Doc -> [Formula] -> Doc
forall a. Pretty a => Doc -> [a] -> Doc
prettySequents Doc
"Axiom"

unitary :: Formula -> Bool
unitary :: Formula -> Bool
unitary = \case
  Atomic{}     -> Bool
True
  Negate{}     -> Bool
True
  Connected{}  -> Bool
False
  Quantified{} -> Bool
True

under :: Connective -> Formula -> Bool
under :: Connective -> Formula -> Bool
under Connective
c = \case
  Connected Connective
c' Formula
_ Formula
_ | Connective
c Connective -> Connective -> Bool
forall a. Eq a => a -> a -> Bool
== Connective
c' Bool -> Bool -> Bool
&& Connective -> Bool
chainable Connective
c -> Bool
True
  Quantified{} -> Bool
False
  Formula
f -> Formula -> Bool
unitary Formula
f

chainable :: Connective -> Bool
chainable :: Connective -> Bool
chainable = \case
  Connective
And        -> Bool
True
  Connective
Or         -> Bool
True
  Connective
Implies    -> Bool
False
  Connective
Equivalent -> Bool
False
  Connective
Xor        -> Bool
False

instance Pretty LogicalExpression where
  pretty :: LogicalExpression -> Doc
pretty = \case
    Clause  Clause
c -> Clause -> Doc
forall a. Pretty a => a -> Doc
pretty Clause
c
    Formula Formula
f -> Formula -> Doc
forall a. Pretty a => a -> Doc
pretty Formula
f


-- * Pretty printer for problems

instance Pretty Clauses where
  pretty :: Clauses -> Doc
pretty (Clauses [Clause]
cs) = [Clause] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [Clause]
cs

instance Pretty Theorem where
  pretty :: Theorem -> Doc
pretty (Theorem [Formula]
as Formula
c) = [Formula] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList [Formula]
as Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Formula -> Doc
forall a. Pretty a => Doc -> a -> Doc
prettySequent Doc
"Conjecture" Formula
c


-- * Pretty printer for proofs

instance Pretty l => Pretty (Rule l) where
  pretty :: Rule l -> Doc
pretty Rule l
rule = RuleName -> Doc
forall a. Pretty a => a -> Doc
pretty (Rule l -> RuleName
forall f. Rule f -> RuleName
ruleName Rule l
rule) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> case [l] -> Maybe (NonEmpty l)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty (Rule l -> [l]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Rule l
rule) of
    Just NonEmpty l
as -> Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> NonEmpty Doc -> Doc
commaSep ((l -> Doc) -> NonEmpty l -> NonEmpty Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc -> Doc
bold (Doc -> Doc) -> (l -> Doc) -> l -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. l -> Doc
forall a. Pretty a => a -> Doc
pretty) NonEmpty l
as)
    Maybe (NonEmpty l)
Nothing -> Doc
empty

instance Pretty RuleName where
  pretty :: RuleName -> Doc
pretty (RuleName Text
rn) =
    case Text
rn of
      Text
"negated conjecture" -> Doc -> Doc
underline (Doc -> Doc
yellow Doc
name)
      Text
"unknown"            -> Doc -> Doc
red Doc
name
      Text
"other"              -> Doc
name
      Text
_                    -> Doc -> Doc
yellow Doc
name
    where
      name :: Doc
name = String -> Doc
text (Text -> String
T.unpack Text
rn)

instance Pretty l => Pretty (Inference l) where
  pretty :: Inference l -> Doc
pretty (Inference Rule l
r LogicalExpression
f) = LogicalExpression -> Doc
forall a. Pretty a => a -> Doc
pretty LogicalExpression
f Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (Rule l -> Doc
forall a. Pretty a => a -> Doc
pretty Rule l
r)

instance Pretty l => Pretty (Sequent l) where
  pretty :: Sequent l -> Doc
pretty (Sequent l
c Inference l
i) = Doc -> Doc
bold (l -> Doc
forall a. Pretty a => a -> Doc
pretty l
c Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot) Doc -> Doc -> Doc
<+> Inference l -> Doc
forall a. Pretty a => a -> Doc
pretty Inference l
i

instance (Ord l, Pretty l) => Pretty (Derivation l) where
  pretty :: Derivation l -> Doc
pretty Derivation l
d = [Doc] -> Doc
vsep (Sequent Integer -> Doc
forall a. Pretty a => a -> Doc
pretty (Sequent Integer -> Doc) -> [Sequent Integer] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Derivation l -> [Sequent Integer]
forall l. Ord l => Derivation l -> [Sequent Integer]
derivation Derivation l
d) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
line

instance (Ord l, Pretty l) => Pretty (Refutation l) where
  pretty :: Refutation l -> Doc
pretty Refutation l
r = [Doc] -> Doc
vsep (Sequent Integer -> Doc
forall a. Pretty a => a -> Doc
pretty (Sequent Integer -> Doc) -> [Sequent Integer] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Refutation l -> [Sequent Integer]
forall l. Ord l => Refutation l -> [Sequent Integer]
sequents Refutation l
r) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
line

-- | List all sequents that lead to the refutation, sorted topologically
-- breadth-first on the graph of inferences.
sequents :: Ord l => Refutation l -> [Sequent Integer]
sequents :: Refutation l -> [Sequent Integer]
sequents (Refutation Derivation l
d Contradiction l
c) = Enumeration l [Sequent Integer] -> [Sequent Integer]
forall a e. Enumeration a e -> e
evalEnumeration (Enumeration l [Sequent Integer] -> [Sequent Integer])
-> Enumeration l [Sequent Integer] -> [Sequent Integer]
forall a b. (a -> b) -> a -> b
$ do
  [Sequent Integer]
ss <- Derivation l -> Enumeration l [Sequent Integer]
forall l. Ord l => Derivation l -> Enumeration l [Sequent Integer]
derivationS Derivation l
d
  Sequent Integer
s <- Integer -> Inference Integer -> Sequent Integer
forall f. f -> Inference f -> Sequent f
Sequent (Integer -> Inference Integer -> Sequent Integer)
-> EnumerationT l Identity Integer
-> EnumerationT l Identity (Inference Integer -> Sequent Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EnumerationT l Identity Integer
forall (m :: * -> *) a. Monad m => EnumerationT a m Integer
next EnumerationT l Identity (Inference Integer -> Sequent Integer)
-> EnumerationT l Identity (Inference Integer)
-> EnumerationT l Identity (Sequent Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (l -> EnumerationT l Identity Integer)
-> Inference l -> EnumerationT l Identity (Inference Integer)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse l -> EnumerationT l Identity Integer
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> EnumerationT a m Integer
enumerate (Contradiction l -> Inference l
forall f. Contradiction f -> Inference f
liftContradiction Contradiction l
c)
  [Sequent Integer] -> Enumeration l [Sequent Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Sequent Integer] -> [Sequent Integer]
forall a. [a] -> [a]
reverse (Sequent Integer
sSequent Integer -> [Sequent Integer] -> [Sequent Integer]
forall a. a -> [a] -> [a]
:[Sequent Integer]
ss))

derivation :: Ord l => Derivation l -> [Sequent Integer]
derivation :: Derivation l -> [Sequent Integer]
derivation = Enumeration l [Sequent Integer] -> [Sequent Integer]
forall a e. Enumeration a e -> e
evalEnumeration (Enumeration l [Sequent Integer] -> [Sequent Integer])
-> (Derivation l -> Enumeration l [Sequent Integer])
-> Derivation l
-> [Sequent Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Sequent Integer] -> [Sequent Integer])
-> Enumeration l [Sequent Integer]
-> Enumeration l [Sequent Integer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Sequent Integer] -> [Sequent Integer]
forall a. [a] -> [a]
reverse (Enumeration l [Sequent Integer]
 -> Enumeration l [Sequent Integer])
-> (Derivation l -> Enumeration l [Sequent Integer])
-> Derivation l
-> Enumeration l [Sequent Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation l -> Enumeration l [Sequent Integer]
forall l. Ord l => Derivation l -> Enumeration l [Sequent Integer]
derivationS

derivationS :: Ord l => Derivation l -> Enumeration l [Sequent Integer]
derivationS :: Derivation l -> Enumeration l [Sequent Integer]
derivationS Derivation l
d = ([Sequent Integer] -> Sequent l -> Enumeration l [Sequent Integer])
-> [Sequent Integer]
-> [Sequent l]
-> Enumeration l [Sequent Integer]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Map l LogicalExpression
-> [Sequent Integer]
-> Sequent l
-> Enumeration l [Sequent Integer]
forall l.
Ord l =>
Map l LogicalExpression
-> [Sequent Integer]
-> Sequent l
-> Enumeration l [Sequent Integer]
sequentsS Map l LogicalExpression
es) [] [Sequent l]
ss
  where
    ss :: [Sequent l]
ss = Derivation l -> [Sequent l]
forall f. Ord f => Derivation f -> [Sequent f]
breadthFirst Derivation l
d
    es :: Map l LogicalExpression
es = [Sequent l] -> Map l LogicalExpression
forall f. Ord f => [Sequent f] -> Map f LogicalExpression
labeling [Sequent l]
ss

sequentsS :: Ord l => Map l LogicalExpression ->
             [Sequent Integer] -> Sequent l ->
             Enumeration l [Sequent Integer]
sequentsS :: Map l LogicalExpression
-> [Sequent Integer]
-> Sequent l
-> Enumeration l [Sequent Integer]
sequentsS Map l LogicalExpression
es [Sequent Integer]
ss s :: Sequent l
s@(Sequent l
l Inference l
i) =
  case (l -> Bool) -> [l] -> Maybe l
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find l -> Bool
trivialClausification (Inference l -> [l]
forall f. Inference f -> [f]
antecedents Inference l
i) of
    Just l
a  -> l -> l -> EnumerationT l Identity ()
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> a -> EnumerationT a m ()
alias l
l l
a EnumerationT l Identity ()
-> [Sequent Integer] -> Enumeration l [Sequent Integer]
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> [Sequent Integer]
ss
    Maybe l
Nothing -> (Sequent Integer -> [Sequent Integer])
-> EnumerationT l Identity (Sequent Integer)
-> Enumeration l [Sequent Integer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sequent Integer -> [Sequent Integer] -> [Sequent Integer]
forall a. a -> [a] -> [a]
:[Sequent Integer]
ss) ((l -> EnumerationT l Identity Integer)
-> Sequent l -> EnumerationT l Identity (Sequent Integer)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse l -> EnumerationT l Identity Integer
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> EnumerationT a m Integer
enumerate Sequent l
s)
  where trivialClausification :: l -> Bool
trivialClausification l
a = Map l LogicalExpression
es Map l LogicalExpression -> l -> LogicalExpression
forall k a. Ord k => Map k a -> k -> a
! l
a LogicalExpression -> LogicalExpression -> Bool
~~= Inference l -> LogicalExpression
forall f. Inference f -> LogicalExpression
consequent Inference l
i

(~~=) :: LogicalExpression -> LogicalExpression -> Bool
Clause  Clause
c ~~= :: LogicalExpression -> LogicalExpression -> Bool
~~= Formula Formula
f = Formula -> Clause -> Bool
triviallyClausified Formula
f Clause
c
Formula Formula
f ~~= Clause  Clause
c = Formula -> Clause -> Bool
triviallyClausified Formula
f Clause
c
LogicalExpression
_ ~~= LogicalExpression
_ = Bool
False

triviallyClausified :: Formula -> Clause -> Bool
triviallyClausified :: Formula -> Clause -> Bool
triviallyClausified Formula
f Clause
c
  | Just Clause
k <- Formula -> Maybe Clause
unliftClause Formula
f = Clause
k Clause -> Clause -> Bool
forall e. FirstOrder e => e -> e -> Bool
~= Clause
c
  | Bool
otherwise = Bool
False

instance Pretty Solution where
  pretty :: Solution -> Doc
pretty = \case
    Saturation Derivation Integer
d -> [Doc] -> Doc
vsep [Doc -> Doc
yellow Doc
saturated, Derivation Integer -> Doc
forall a. Pretty a => a -> Doc
pretty Derivation Integer
d]
    Proof Refutation Integer
r      -> [Doc] -> Doc
vsep [Doc -> Doc
green Doc
proven,     Refutation Integer -> Doc
forall a. Pretty a => a -> Doc
pretty Refutation Integer
r]
    where
      saturated :: Doc
saturated = Doc
"Disproven by constructing the saturated set of clauses."
      proven :: Doc
proven = Doc
"Found a proof by refutation."

instance Pretty Error where
  pretty :: Error -> Doc
pretty Error
err = Doc -> Doc
red (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ case Maybe Doc
explanation of
                       Just Doc
ex -> [Doc] -> Doc
vsep [Doc
failure, Doc
ex]
                       Maybe Doc
Nothing -> Doc
failure
    where
      failure :: Doc
failure = Doc
"Failed to find a solution because" Doc -> Doc -> Doc
<+> Doc
reason Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."

      reason :: Doc
reason = case Error
err of
        Error
TimeLimitError    -> Doc
"the theorem prover exceeded its time limit"
        Error
MemoryLimitError  -> Doc
"the theorem prover exceeded its memory limit"
        ParsingError{}    -> Doc
"of the following parsing error"
        ProofError{}      -> Doc
"of the following problem with the proof"
        OtherError{}      -> Doc
"of the following error"
        ExitCodeError Int
c Text
_ -> Doc
"the theorem prover terminated with exit code" Doc -> Doc -> Doc
<+>
                             Doc -> Doc
bold Doc
exitCode Doc -> Doc -> Doc
<+> Doc
"and the following error message"
          where exitCode :: Doc
exitCode = String -> Doc
text (Int -> String
forall a. Show a => a -> String
show Int
c)

      explanation :: Maybe Doc
explanation = (Text -> Doc) -> Maybe Text -> Maybe Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Doc
text (String -> Doc) -> (Text -> String) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) (Maybe Text -> Maybe Doc) -> Maybe Text -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ case Error
err of
        Error
TimeLimitError    -> Maybe Text
forall a. Maybe a
Nothing
        Error
MemoryLimitError  -> Maybe Text
forall a. Maybe a
Nothing
        ParsingError Text
e    -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
e
        ProofError   Text
e    -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
e
        OtherError   Text
e    -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
e
        ExitCodeError Int
_ Text
e -> if Text -> Bool
T.null Text
e then Maybe Text
forall a. Maybe a
Nothing else Text -> Maybe Text
forall a. a -> Maybe a
Just Text
e

instance Pretty a => Pretty (Partial a) where
  pretty :: Partial a -> Doc
pretty = (Error -> Doc) -> (a -> Doc) -> Either Error a -> Doc
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Error -> Doc
forall a. Pretty a => a -> Doc
pretty a -> Doc
forall a. Pretty a => a -> Doc
pretty (Either Error a -> Doc)
-> (Partial a -> Either Error a) -> Partial a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Partial a -> Either Error a
forall a. Partial a -> Either Error a
liftPartial