{-# LANGUAGE CPP #-}

-- |
-- Module      : AutoProof.Internal.Utils.PrettyPrintable.Symbols
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines string constants ("symbols") used for pretty-printing.
module AutoProof.Internal.Utils.PrettyPrintable.Symbols
  ( -- * Formula symbols
    falseS,
    trueS,
    notS,
    impS,
    orS,
    andS,
    iffS,

    -- * Judgement symbols
    turnstileS,

    -- * Proof symbols
    axiomS,
    falseElimS,
    trueIntrS,
    notElimS,
    notIntrS,
    impElimS,
    impIntrS,
    orElimS,
    orIntrLS,
    orIntrRS,
    andElimLS,
    andElimRS,
    andIntrS,
    iffElimLS,
    iffElimRS,
    iffIntrS,

    -- * Proof pretty-printing
    vertS,
    cornerS,
    branchS,
  )
where

-- Propositional literals, connectives, and judgement turnstile

-- | Falsity symbol.
falseS :: String
falseS :: String
falseS = String -> String -> String
forall a. a -> a -> a
ifWindows "false" "⊥"

-- | Truth symbol.
trueS :: String
trueS :: String
trueS = String -> String -> String
forall a. a -> a -> a
ifWindows "true" "⊤"

-- | Negation symbol.
notS :: String
notS :: String
notS = String -> String -> String
forall a. a -> a -> a
ifWindows "~" "¬"

-- | Implication symbol.
impS :: String
impS :: String
impS = String -> String -> String
forall a. a -> a -> a
ifWindows "->" "→"

-- | Disjunction symbol.
orS :: String
orS :: String
orS = String -> String -> String
forall a. a -> a -> a
ifWindows "|" "∨"

-- | Conjunction symbol.
andS :: String
andS :: String
andS = String -> String -> String
forall a. a -> a -> a
ifWindows "&" "∧"

-- | Equivalence symbol.
iffS :: String
iffS :: String
iffS = String -> String -> String
forall a. a -> a -> a
ifWindows "<->" "↔"

-- | Judgement turnstile symbol.
turnstileS :: String
turnstileS :: String
turnstileS = String -> String -> String
forall a. a -> a -> a
ifWindows "|-" "⊢"

-- Inference rule symbols

-- | Axiom symbol.
axiomS :: String
axiomS :: String
axiomS = "(Ax)"

-- | Falsity elimination symbol.
falseElimS :: String
falseElimS :: String
falseElimS = String -> String
elim String
falseS

-- | Truth introduction symbol.
trueIntrS :: String
trueIntrS :: String
trueIntrS = String -> String
intr String
trueS

-- | Negation elimination symbol.
notElimS :: String
notElimS :: String
notElimS = String -> String
elim String
notS

-- | Negation introduction symbol.
notIntrS :: String
notIntrS :: String
notIntrS = String -> String
intr String
notS

-- | Implication elimination symbol.
impElimS :: String
impElimS :: String
impElimS = String -> String
elim String
impS

-- | Implication introduction symbol.
impIntrS :: String
impIntrS :: String
impIntrS = String -> String
intr String
impS

-- | Disjunction elimination symbol.
orElimS :: String
orElimS :: String
orElimS = String -> String
elim String
orS

-- | Disjunction introduction (left) symbol.
orIntrLS :: String
orIntrLS :: String
orIntrLS = String -> String
intrL String
orS

-- | Disjunction introduction (right) symbol.
orIntrRS :: String
orIntrRS :: String
orIntrRS = String -> String
intrR String
orS

-- | Conjunction elimination (left) symbol.
andElimLS :: String
andElimLS :: String
andElimLS = String -> String
elimL String
andS

-- | Conjunction elimination (right) symbol.
andElimRS :: String
andElimRS :: String
andElimRS = String -> String
elimR String
andS

-- | Conjunction introduction symbol.
andIntrS :: String
andIntrS :: String
andIntrS = String -> String
intr String
andS

-- | Equivalence elimination (left) symbol.
iffElimLS :: String
iffElimLS :: String
iffElimLS = String -> String
elimL String
iffS

-- | Equivalence elimination (right) symbol.
iffElimRS :: String
iffElimRS :: String
iffElimRS = String -> String
elimR String
iffS

-- | Equivalence introduction symbol.
iffIntrS :: String
iffIntrS :: String
iffIntrS = String -> String
intr String
iffS

-- Inference rule symbol helper functions

elim :: String -> String
elim :: String -> String
elim s :: String
s = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "E)"

elimL :: String -> String
elimL :: String -> String
elimL s :: String
s = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "EL)"

elimR :: String -> String
elimR :: String -> String
elimR s :: String
s = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "ER)"

intr :: String -> String
intr :: String -> String
intr s :: String
s = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "I)"

intrL :: String -> String
intrL :: String -> String
intrL s :: String
s = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "IL)"

intrR :: String -> String
intrR :: String -> String
intrR s :: String
s = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "IR)"

-- Pretty-printed proof components

-- | Vertical bar symbol used in pretty-printing proofs.
vertS :: String
vertS :: String
vertS = String -> String -> String
forall a. a -> a -> a
ifWindows "|" "│"

-- | Corner symbol used in pretty-printing proofs.
cornerS :: String
cornerS :: String
cornerS = String -> String -> String
forall a. a -> a -> a
ifWindows "+-- " "┌── "

-- | Branch symbol used in pretty-printing proofs.
branchS :: String
branchS :: String
branchS = String -> String -> String
forall a. a -> a -> a
ifWindows "+-- " "├── "

-- Use first choice if Windows, use second choice if other OS
-- TODO: figure out if Windows is actually the problem with printing certain
-- characters
ifWindows :: a -> a -> a

#ifdef mingw32_HOST_OS
ifWindows a _ = a
#else
ifWindows :: a -> a -> a
ifWindows _ a :: a
a = a
a
#endif