-- |
-- Module      : AutoProof.Internal.Judgement
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines the 'Judgement' type and related functions.
module AutoProof.Internal.Judgement
  ( -- * Types and constructors
    Context,
    Judgement (Judgement, antecedents, succedent),
    (|-),

    -- * Pretty-printing
    prettyJudgement,

    -- * Operations on judgements
    weakenJudgement,
  )
where

import AutoProof.Internal.Formula (Formula)
import AutoProof.Internal.Utils.PrettyPrintable
  ( PrettyPrintable (pretty),
    prettySeq,
  )
import AutoProof.Internal.Utils.PrettyPrintable.Symbols (turnstileS)
import AutoProof.Internal.Utils.SetUtils (toSet)
import Data.Set (Set)
import qualified Data.Set as Set

-- | A set of propositional formulas, used as antecedents of a judgement.
type Context a = Set (Formula a)

-- | @(Judgement c a)@ represents the judgement or sequent \(c \vdash a\).
--
-- >>> Judgement Set.empty (Imp (And (Var 'a') (Var 'b')) (Var 'a'))
-- [] |- Imp (And (Var 'a') (Var 'b')) (Var 'a')
data Judgement a = Judgement
  { -- | The antecedents (or hypotheses).
    Judgement a -> Context a
antecedents :: Context a,
    -- | The succedent (or consequent, or conclusion).
    Judgement a -> Formula a
succedent :: Formula a
  }
  deriving (Judgement a -> Judgement a -> Bool
(Judgement a -> Judgement a -> Bool)
-> (Judgement a -> Judgement a -> Bool) -> Eq (Judgement a)
forall a. Eq a => Judgement a -> Judgement a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Judgement a -> Judgement a -> Bool
$c/= :: forall a. Eq a => Judgement a -> Judgement a -> Bool
== :: Judgement a -> Judgement a -> Bool
$c== :: forall a. Eq a => Judgement a -> Judgement a -> Bool
Eq)

-- | Infix judgement constructor. @(c '|-' a)@ represents the judgement
-- \(c \vdash a\).
--
-- >>> [Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'
-- [Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b'
--
-- /Note:/ If @c@ is already a 'Data.Set.Set', then it is recommended to use
-- @(Judgement c a)@ in favor of @(c '|-' a)@, since the latter will create a
-- new set and fill it with the values in @c@.
(|-) :: (Ord a, Foldable f) => f (Formula a) -> Formula a -> Judgement a
c :: f (Formula a)
c |- :: f (Formula a) -> Formula a -> Judgement a
|- a :: Formula a
a = Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement (f (Formula a) -> Context a
forall a (t :: * -> *). (Ord a, Foldable t) => t a -> Set a
toSet f (Formula a)
c) Formula a
a

infix 5 |-

-- Compare judgements based on the consequent first
instance Ord a => Ord (Judgement a) where
  compare :: Judgement a -> Judgement a -> Ordering
compare (Judgement g :: Context a
g a :: Formula a
a) (Judgement g' :: Context a
g' a' :: Formula a
a') = case Formula a -> Formula a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Formula a
a Formula a
a' of
    EQ -> Context a -> Context a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Context a
g Context a
g'
    x :: Ordering
x -> Ordering
x

instance Show a => Show (Judgement a) where
  showsPrec :: Int -> Judgement a -> ShowS
showsPrec d :: Int
d (Judgement c :: Context a
c a :: Formula a
a) =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
turnstilePrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      Int -> [Formula a] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
turnstilePrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (Context a -> [Formula a]
forall a. Set a -> [a]
Set.toList Context a
c)
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " |- "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Formula a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
turnstilePrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Formula a
a
    where
      turnstilePrec :: Int
turnstilePrec = 5

instance (Ord a, Read a) => Read (Judgement a) where
  readsPrec :: Int -> ReadS (Judgement a)
readsPrec d :: Int
d = Bool -> ReadS (Judgement a) -> ReadS (Judgement a)
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
turnstilePrec) ReadS (Judgement a)
forall a. (Read a, Ord a) => String -> [(Judgement a, String)]
readJudgement
    where
      turnstilePrec :: Int
turnstilePrec = 5
      readJudgement :: String -> [(Judgement a, String)]
readJudgement s :: String
s =
        [ ([Formula a]
g [Formula a] -> Formula a -> Judgement a
forall a (f :: * -> *).
(Ord a, Foldable f) =>
f (Formula a) -> Formula a -> Judgement a
|- Formula a
a, String
v)
          | (g :: [Formula a]
g, t :: String
t) <- ReadS [Formula a]
forall a. Read a => ReadS [a]
readList String
s,
            ("|-", u :: String
u) <- ReadS String
lex String
t,
            (a :: Formula a
a, v :: String
v) <- Int -> ReadS (Formula a)
forall a. Read a => Int -> ReadS a
readsPrec (Int
turnstilePrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
u
        ]

instance PrettyPrintable a => PrettyPrintable (Judgement a) where
  pretty :: Judgement a -> String
pretty (Judgement c :: Context a
c a :: Formula a
a) = case Context a -> String
forall (t :: * -> *) a.
(Foldable t, PrettyPrintable a) =>
t a -> String
prettySeq Context a
c of
    "" -> String
turnstileS String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Formula a -> String
forall a. PrettyPrintable a => a -> String
pretty Formula a
a
    c' :: String
c' -> String
c' String -> ShowS
forall a. [a] -> [a] -> [a]
++ (' ' Char -> ShowS
forall a. a -> [a] -> [a]
: String
turnstileS) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Formula a -> String
forall a. PrettyPrintable a => a -> String
pretty Formula a
a

-- | Get a pretty-printed representation of a judgement.
--
-- ==== __Examples__
--
-- >>> prettyJudgement $ [Var "a", Imp (Var "a") (Var "b")] |- Var "b"
-- "a, a → b ⊢ b"
prettyJudgement :: PrettyPrintable a => Judgement a -> String
prettyJudgement :: Judgement a -> String
prettyJudgement = Judgement a -> String
forall a. PrettyPrintable a => a -> String
pretty

-- | Weaken a judgement by inserting a formula into its hypotheses.
--
-- >>> weakenJudgement ([Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b') (Var 'c')
-- [Var 'a',Var 'c',Imp (Var 'a') (Var 'b')] |- Var 'b'
weakenJudgement :: Ord a => Judgement a -> Formula a -> Judgement a
weakenJudgement :: Judgement a -> Formula a -> Judgement a
weakenJudgement (Judgement c :: Context a
c a :: Formula a
a) b :: Formula a
b = Context a -> Formula a -> Judgement a
forall a. Context a -> Formula a -> Judgement a
Judgement (Formula a -> Context a -> Context a
forall a. Ord a => a -> Set a -> Set a
Set.insert Formula a
b Context a
c) Formula a
a