-- # Software Tools for Discrete Mathematics
module Stdm06PropositionalLogic where

-- import Control.Exception (SomeException, catch)

import Stdm06LogicOperators

-- # Chapter 6.  Propositional Logic

-- # A Mini-tutorial on Using the Proof Checker for Propositional Logic

-- ## And Introduction
-- Here is a theorem and a valid proof using the And Introduction rule:
-- Theorem AI1.  q,r  |-  q&r

thAI1 = Theorem [Q, R] (Q `And` R)

prAI1 = AndI (Assume Q, Assume R) (And Q R)

-- To check that Proof prAI1 is a valid proof of Theorem thAI1,
-- execute the following expression interactively:
-- 	check_proof thAI1 prAI1
-- The next theorem is similar, but it's incorrect,
-- because Q `And` S doesn't follow from assuming Q and R.
-- Theorem AI2.  q,r  |-  q&s
-- Here are the theorem and an invalid proof of it,
-- using the And Introduction rule incorrectly.

thAI2 = Theorem [Q, R] (Q `And` S)

prAI2 =
  AndI
    (Assume Q, Assume R)
    (And Q S)

-- Try it out with the proof checker by evaluating the following interactively:
-- 	check_proof thAI2 prAI2

-- ## And Elimination (Left)
-- Here is a theorem and a valid proofs using And Elimination (Left).
-- Test it by evaluating
-- 	check_proof thAEL1 prAEL1
-- Theorem AEL1.  p&q |-  p

thAEL1 = Theorem [P `And` Q] P

prAEL1 = AndEL (Assume (And P Q)) P

-- This is a slightly more complex theorem,
-- again with a valid proof using And Elimination (Left).
-- Check it with:
-- 	check_proof thAEL2 prAEL2
-- Theorem AEL2.  (P|Q)&R |- (P|Q)

thAEL2 = Theorem [(P `Or` Q) `And` R] (P `Or` Q)

prAEL2 = AndEL (Assume (And (Or P Q) R)) (Or P Q)

-- Now we try some invalid proofs.
-- Consider the following theorem,
-- the theorem itself is valid but its proof is incorrect.
-- Check it by evaluating the expression check_AEL3; the proof checker will tell you exactly what is wrong with the proof.
-- Notice that we're moving to a slightly more concise style,
-- where we aren't naming both the theorem and the proof separately.
-- Theorem AEL3.  p&q |-  p

check_AEL3 =
  check_proof
    (Theorem [P `And` Q] P)
    (AndEL (Assume (Or P Q)) P)

-- p&q  |-  p
p6 = AndEL (Assume (And P Q)) Q

-- P&Q  |-  R
p7 = AndEL (Assume (And P Q)) R

-- ## And Elimination (Right)
-- The following theorem and proof are correct;
-- they are the mirror image of the AEL1 example above.

check_AER1 =
  check_proof
    (Theorem [P `And` Q] Q)
    (AndER (Assume (P `And` Q)) Q)

-- This example is similar;
-- the theorem is ok and the proof would be valid if it used the AndEL rule,
-- but the AndER rule does not justify the conclusion,
-- so the proof fails to establish the theorem.

check_AER2 =
  check_proof
    (Theorem [P `And` Q] Q)
    (AndER (Assume (P `And` Q)) P)

-- ## Imply Introduction
-- Theorem II1.  Q |- P => P&Q

check_II1 =
  check_proof
    (Theorem [Q] (P `Imp` (P `And` Q)))
    ( ImpI
        ( AndI
            (Assume P, Assume Q)
            (And P Q)
        )
        (Imp P (And P Q))
    )

-- Theorem II2.  |- Q => (P => (P&Q))

check_II2 =
  check_proof
    (Theorem [] (Q `Imp` (P `Imp` (P `And` Q))))
    ( ImpI
        ( ImpI
            ( AndI
                (Assume P, Assume Q)
                (And P Q)
            )
            (Imp P (And P Q))
        )
        (Imp Q (Imp P (And P Q)))
    )

-- ## Imply Elimination
-- Theorem IE1.  P, P=>Q  |-  Q

check_IE1 =
  check_proof
    (Theorem [P, P `Imp` Q] Q)
    ( ImpE
        (Assume P, Assume (Imp P Q))
        Q
    )

-- ## Or Introduction (Left)
-- Theorem OEL1.  P&Q |- P&Q \/ S&P

check_OIL1 =
  check_proof
    ( Theorem
        [P `And` Q, Q `And` R]
        ((P `And` Q) `Or` (S `And` P))
    )
    ( OrIL
        (Assume (P `And` Q))
        ((P `And` Q) `Or` (S `And` P))
    )

-- ## Or Introduction (Right)
-- Theorem OIR1.  ~S |- P \/ ~S

check_OIR1 =
  check_proof
    (Theorem [Not S] (P `Or` (Not S)))
    ( OrIR
        (Assume (Not S))
        (P `Or` (Not S))
    )

-- ## Identity
check_ID0 =
  check_proof
    (Theorem [P `And` Q] (P `And` Q))
    (Assume (P `And` Q))

-- Now the same is proved using the ID inference rule.
-- Theorem ID1.  P&Q |- P&Q

check_ID1 =
  check_proof
    (Theorem [P `And` Q] (P `And` Q))
    (ID (Assume (P `And` Q)) (P `And` Q))

-- ## Contradiction
-- Theorem CTR1.  False |- P & ~P

check_CTR1 =
  check_proof
    (Theorem [FALSE] (P `And` (Not P)))
    (CTR (Assume FALSE) (P `And` (Not P)))

-- The next theorem isn't valid,
-- because the premise P isn't enough to establish P & ~P,
-- and it isn't FALSE so the Contradiction inference rule doesn't apply.
-- Theorem CTR2.  P |- P & ~P

check_CTR2 =
  check_proof
    (Theorem [P] (P `And` (Not P)))
    (CTR (Assume P) (P `And` (Not P)))

-- ## Reductio ab Absurdum
-- Theorem RAA1.  ~~P |- P

check_RAA1 =
  check_proof
    ( Theorem
        [P `Imp` FALSE, (P `Imp` FALSE) `Imp` FALSE]
        P
    )
    ( RAA
        ( ImpE
            ( Assume (P `Imp` FALSE),
              Assume ((P `Imp` FALSE) `Imp` FALSE)
            )
            FALSE
        )
        P
    )

-- ## Examples from the book
-- Here is the theorem and  proofs that are used in the book;
-- run them like this:
--    check_proof example_theorem example_proof1     (should be valid)
--    check_proof example_theorem example_proof2     (should give error message)

example_theorem :: Theorem
example_theorem =
  Theorem
    []
    (Imp Q (Imp (And P R) (And R Q)))

example_proof1 =
  ImpI
    ( ImpI
        ( AndI
            ( ( AndER
                  (Assume (And P R))
                  R
              ),
              Assume Q
            )
            (And R Q)
        )
        (Imp (And P R) (And R Q))
    )
    (Imp Q (Imp (And P R) (And R Q)))

-- The following proof is incorrect proof,
-- because Q^R was inferred where R^Q was needed.

example_proof2 =
  ImpI
    ( ImpI
        ( AndI
            ( Assume Q,
              ( AndER
                  (Assume (And P R))
                  R
              )
            )
            (And R Q)
        )
        (Imp (And P R) (And R Q))
    )
    (Imp Q (Imp (And P R) (And R Q)))

-- # Implementation of the Proof Checker for Propositional Logic
data Prop
  = FALSE
  | TRUE
  | A
  | B
  | C
  | D
  | E
  | G
  | H
  | I
  | J
  | K
  | L
  | M
  | N
  | O
  | P
  | Q
  | R
  | S
  | U
  | V
  | W
  | X
  | Y
  | Z
  | Pvar String
  | And Prop Prop
  | Or Prop Prop
  | Not Prop
  | Imp Prop Prop
  deriving (Show)

-- Eq is not derived anymore, but completly defined

data Theorem
  = Theorem [Prop] Prop
  deriving (Eq, Show)

type TheoremDB = [String]

-- a representation of all the known theorems

data Proof
  = Assume Prop
  | AndI (Proof, Proof) Prop
  | AndEL Proof Prop
  | AndER Proof Prop
  | OrIL Proof Prop
  | OrIR Proof Prop
  | OrE (Proof, Proof, Proof) Prop
  | ImpI Proof Prop
  | ImpE (Proof, Proof) Prop
  | ID Proof Prop
  | CTR Proof Prop
  | RAA Proof Prop
  | Use Theorem [Proof] Prop
  | UseTh (Theorem, Proof) [Proof] Prop
  | UseDB Theorem [Proof] Prop
  deriving (Eq, Show)

-- When a proof is checked, several pieces of information are gathered together,
-- into a data structure called Status.

type Status =
  ( Bool,
    [String],
    [Prop],
    Prop
  )

-- True iff the proof is valid
-- messages describing errors found in the proof
-- undischarged assumptions required by the proof
-- conclusion

-- The following type is used for comparisons,
-- with the ordering on the propositions

data Comparison = Lesser | Equal | Greater deriving (Eq)

-------------------- definition of the Eq for a Prop ------------------------
-- the basic definitions for the equality:

instance Eq Prop where
  (==) FALSE FALSE = True
  (==) TRUE TRUE = True
  (==) A A = True
  (==) B B = True
  (==) C C = True
  (==) D D = True
  (==) E E = True
  (==) G G = True
  (==) H H = True
  (==) I I = True
  (==) J J = True
  (==) K K = True
  (==) L L = True
  (==) M M = True
  (==) N N = True
  (==) O O = True
  (==) P P = True
  (==) Q Q = True
  (==) R R = True
  (==) S S = True
  (==) U U = True
  (==) V V = True
  (==) W W = True
  (==) X X = True
  (==) Y Y = True
  (==) Z Z = True
  (==) (Pvar x1) (Pvar x2) = x1 == x2
  (==) (And x1 y1) (And x2 y2) = (x1 == x2) && (y1 == y2)
  (==) (Or x1 y1) (Or x2 y2) = (x1 == x2) && (y1 == y2)
  (==) (Not x) (Not y) = (x == y)
  (==) (Imp x1 y1) (Imp x2 y2) = (x1 == x2) && (y1 == y2)
  (==) TRUE y = (Imp FALSE FALSE) == y
  (==) x TRUE = x == (Imp FALSE FALSE)
  (==) (Not x) y = ((Imp x FALSE) == y)
  (==) x (Not y) = (x == (Imp y FALSE))
  (==) _ _ = False
  (/=) x y = not (x == y)

----------------------------- auxilary functions ----------------------------

--   'setelem' was deleted (use 'elem' instead)
--   'jsubset' was deleted, and it's not needed anymore

union :: (Eq a) => [a] -> [a] -> [a]
union xs ys = xs ++ [y | y <- ys, notElem y xs]

setdif :: (Eq a) => [a] -> [a] -> [a]
setdif xs ys = [x | x <- xs, notElem x ys]

putmessages :: [String] -> IO ()
putmessages [] = return ()
putmessages (x : xs) = do
  putStr (" ." ++ x)
  putmessages xs

putassumptions :: [Prop] -> IO ()
putassumptions [] = return ()
putassumptions (x : []) = do
  putStr (show x)
  putassumptions []
putassumptions (x : xs) = do
  putStr (show x ++ ", ")
  putassumptions xs

------------------------------ the proof-checker --------------------------

-- the following 'check_proof' is equivalent to the 'check_proof' of the previous versions.

check_proof :: Theorem -> Proof -> IO ()
check_proof t p =
  do
    check_proof_with_db [] t p
    return ()

-- 'check_proof_with_db' allows to use theorems stored in a data-base

check_proof_with_db :: TheoremDB -> Theorem -> Proof -> IO (Bool)
check_proof_with_db db (Theorem thas thc) proof =
  do
    let (valid, ms, uda, concl) = traverse' db proof
    let missingassum = setdif uda thas
    let uselessassum = setdif thas uda
    let allok = valid && (missingassum == []) && (concl == thc)
    if allok
      then do
        putStr "The proof is valid\n"
        if (uselessassum == [])
          then putStr ""
          else do
            putStr "notice: these assumptions are useless: "
            putassumptions uselessassum
            putStr "\n"
      else do
        putStr "*** The proof is NOT valid ***\n"
        if valid
          then do
            putStr "The proof does not match the sequent.\n"
            putStr " .what is actually proved is:\n      "
            putassumptions uda
            putStr ("  |-  " ++ show concl ++ "\n")
            if (missingassum == [])
              then putStr ""
              else do
                putStr
                  ( " .these assumptions are used"
                      ++ " but not part of the sequ"
                      ++ "ent:\n      "
                  )
                putassumptions missingassum
                putStr "\n"
          else do
            if (ms == [])
              then putStr ""
              else do
                putStr "Reported errors:\n"
                putmessages ms
    return (allok)

-- The real work is performed in the traverse' function,
-- which has a separate case for checking each inference rule.
-- Nearly all the complexity in the following code results from an attempt to provide meaningful error messages;
-- if the aim were merely to decide whether a proof is valid,
-- then the implementation could rely much more on Haskell's pattern matching mechanism,
-- and everything would be much more concise.

traverse' :: TheoremDB -> Proof -> Status
traverse' _ (Assume a) = (True, [], [a], a)
traverse' db (AndI (a, b) c) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (bvalid, bmsgs, buda, bconcl) = traverse' db b
      (ok, msg) =
        case c of
          And p q ->
            if (p == aconcl) && (q == bconcl)
              then (True, [])
              else (False, [err1])
          otherwise -> (False, [err2])
      err1 =
        "AndI: the conclusion ("
          ++ show c
          ++ ") is not the "
          ++ "logical And of the assumption ("
          ++ show aconcl
          ++ ") with the assumption ("
          ++ show bconcl
          ++ ")\n"
      err2 =
        "AndI: the conclusion ("
          ++ show c
          ++ ") is not an "
          ++ "And expression\n"
      valid = avalid && bvalid && ok
      msgs = amsgs ++ bmsgs ++ msg
      uda = auda `union` buda
   in (valid, msgs, uda, c)
traverse' db (AndEL a b) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        case aconcl of
          And p q ->
            if p == b
              then (True, [])
              else (False, [err1])
          otherwise -> (False, [err2])
      err1 =
        "AndEL: the left term of And assumption ("
          ++ show aconcl
          ++ ") doesn't match the conclusion ("
          ++ show b
          ++ ")\n"
      err2 =
        "AndEL: the assumption ("
          ++ show aconcl
          ++ ") is not an "
          ++ "And expression\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda
   in (valid, msgs, uda, b)
traverse' db (AndER a b) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        case aconcl of
          And p q ->
            if q == b
              then (True, [])
              else (False, [err1])
          otherwise -> (False, [err2])
      err1 =
        "AndER: the right term of And assumption ("
          ++ show aconcl
          ++ ") doesn't match the conclusion ("
          ++ show b
          ++ ")\n"
      err2 =
        "AndER: the assumption ("
          ++ show aconcl
          ++ ") is not an "
          ++ "And expression\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda
   in (valid, msgs, uda, b)
traverse' db (OrIL a b) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        case b of
          Or p q ->
            if aconcl == p
              then (True, [])
              else (False, [err1])
          otherwise -> (False, [err2])
      err1 =
        "OrIL: the left term of OR conclusion ("
          ++ show b
          ++ ") doesn't match the assumption ("
          ++ show aconcl
          ++ ")\n"
      err2 =
        "OrIL: the conclusion ("
          ++ show b
          ++ ") is not an Or "
          ++ "expression\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda
   in (valid, msgs, uda, b)
traverse' db (OrIR a b) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        case b of
          Or p q ->
            if aconcl == q
              then (True, [])
              else (False, [err1])
          otherwise -> (False, [err2])
      err1 =
        "OrIL: the right term of OR conclusion ("
          ++ show b
          ++ ") doesn't match the assumption ("
          ++ show aconcl
          ++ ")\n"
      err2 =
        "OrIL: the conclusion ("
          ++ show b
          ++ ") is not an Or "
          ++ "expression\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda
   in (valid, msgs, uda, b)
traverse' db (OrE (a, b, c) d) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (bvalid, bmsgs, buda, bconcl) = traverse' db b
      (cvalid, cmsgs, cuda, cconcl) = traverse' db c
      (ok, msg, uda) =
        case aconcl of
          Or p q ->
            let ok2 = p `elem` buda
                ok3 = q `elem` cuda
                ok4 = bconcl == cconcl
                ok5 = bconcl == d
             in if ok2 && ok3 && ok4 && ok5
                  then
                    ( True,
                      [],
                      auda
                        `union` (buda `setdif` [p])
                        `union` (cuda `setdif` [q])
                    )
                  else
                    ( False,
                      (if ok2 then [] else [err2 p])
                        ++ (if ok3 then [] else [err3 q])
                        ++ ( if ok4
                               then if ok5 then [] else [err5]
                               else [err4]
                           ),
                      auda `union` buda `union` cuda
                    )
          otherwise ->
            ( False,
              [err1],
              auda `union` buda `union` cuda
            )
      err1 =
        "OrE: the first term above line ("
          ++ show aconcl
          ++ ") is not an Or expression\n"
      err2 x =
        "OrE: the left term ("
          ++ show x
          ++ ") of the first "
          ++ "term above line ("
          ++ show aconcl
          ++ ") is not an "
          ++ "undischarged assumption of the  proof of the second "
          ++ "term above line ("
          ++ show bconcl
          ++ ")\n"
      err3 x =
        "OrE: the right term ("
          ++ show x
          ++ ") of the first "
          ++ "term above line ("
          ++ show aconcl
          ++ ") is not an "
          ++ "undischarged assumption of the proof of the third "
          ++ "term above line ("
          ++ show bconcl
          ++ ")\n"
      err4 =
        "OrE: the conclusion of the second term above line ("
          ++ show bconcl
          ++ ") doesn't match the conclusion of the "
          ++ "third term above line ("
          ++ show cconcl
          ++ ")\n"
      err5 =
        "OrE: the conclusion ("
          ++ show d
          ++ ") doesn't match the "
          ++ "conclusion of the second and third terms above line ("
          ++ show bconcl
          ++ ")\n"
      valid = avalid && bvalid && cvalid && ok
      msgs = amsgs ++ bmsgs ++ cmsgs ++ msg
   in (valid, msgs, uda, d)
traverse' db (ImpI a b) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) = match b
      match x =
        case x of
          Imp p q ->
            if p `elem` auda && aconcl == q
              then (True, [])
              else
                if not (p `elem` auda) && aconcl == q
                  then (False, [err2])
                  else
                    if p `elem` auda && aconcl /= q
                      then (False, [err3])
                      else (False, [err2, err3])
          Not p -> match (Imp p FALSE)
          FALSE -> match (Imp TRUE TRUE)
          otherwise -> (False, [err1])
      err1 =
        "ImpI: the conclusion ("
          ++ show b
          ++ ") is not an "
          ++ "implication\n"
      err2 =
        "ImpI: the antecedent in ("
          ++ show b
          ++ ") is not an "
          ++ "undischarged assumption above line\n"
      err3 =
        "ImpI: the conclusion in ("
          ++ show b
          ++ ") doesn't match "
          ++ "the conclusion above line ("
          ++ show aconcl
          ++ ")\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = case b of
        Imp p q -> auda `setdif` [p]
        Not p -> auda `setdif` [p]
        FALSE -> auda `setdif` [TRUE]
        otherwise -> auda
   in (valid, msgs, uda, b)
traverse' db (ImpE (a, b) c) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (bvalid, bmsgs, buda, bconcl) = traverse' db b
      (ok, msg) = match bconcl
      match x =
        case x of
          Imp p q ->
            if aconcl == p && c == q
              then (True, [])
              else
                if aconcl /= p && c == q
                  then (False, [err2])
                  else
                    if aconcl == p && c /= q
                      then (False, [err3])
                      else (False, [err2, err3])
          Not p -> match (Imp p FALSE)
          FALSE -> match (Imp TRUE TRUE)
          otherwise -> (False, [err1])
      err1 =
        "ImpE: second term above line ("
          ++ show bconcl
          ++ ") is not an implication\n"
      err2 =
        "ImpE: first term ("
          ++ show aconcl
          ++ ") doesn't match "
          ++ " the antecedent of the second term ("
          ++ show bconcl
          ++ ")\n"
      err3 =
        "ImpE: the conclusion ("
          ++ show c
          ++ ") doesn't match "
          ++ "the conclusion of the second term ("
          ++ show bconcl
          ++ ")\n"
      valid = avalid && bvalid && ok
      msgs = amsgs ++ bmsgs ++ msg
      uda = auda `union` buda
   in (valid, msgs, uda, c)
traverse' db (ID a c) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        if aconcl == c
          then (True, [])
          else (False, [err1])
      err1 =
        "ID: the conclusion ("
          ++ show c
          ++ ") doesn't match "
          ++ "the antecedent ("
          ++ show aconcl
          ++ ")\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda
   in (valid, msgs, uda, c)
traverse' db (CTR a c) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        if aconcl == FALSE
          then (True, [])
          else (False, [err1])
      err1 =
        "CTR: the antecedent ("
          ++ show aconcl
          ++ ") is not "
          ++ "FALSE\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda
   in (valid, msgs, uda, c)
traverse' db (RAA a c) =
  let (avalid, amsgs, auda, aconcl) = traverse' db a
      (ok, msg) =
        if not ((c `Imp` FALSE) `elem` auda)
          then (False, [err1])
          else
            if aconcl /= FALSE
              then (False, [err2])
              else (True, [])
      err1 =
        "RAA: the negation of the conclusion ("
          ++ show c
          ++ ") is not an undischarged assumption of the proof "
          ++ "above the line\n"
      err2 =
        "RAA: the conclusion ("
          ++ show aconcl
          ++ ") of the proof "
          ++ "above the line is not FALSE\n"
      valid = avalid && ok
      msgs = amsgs ++ msg
      uda = auda `setdif` [(c `Imp` FALSE)]
   in (valid, msgs, uda, c)
-- (everything of chapter 2 that follows has been added as 2nd extension,
-- and every line should be marked with)

----------------------- traverse' function for 'USE' -----------------------

-- Use assumes that the theorem is correct

traverse' db (Use theo assums concl) =
  let (oks, msgs, udas, concls) = checkproofs db assums
      err2 =
        "Use: the theorem "
          ++ show theo
          ++ " cannot be applied "
          ++ "with the assumptions "
          ++ show concls
          ++ " and the conclusion ("
          ++ show concl
          ++ ")\n"
   in if not oks
        then (False, msgs, udas, concl)
        else
          if (usetheorem theo concls concl)
            then (True, msgs, udas, concl)
            else (False, msgs ++ [err2], udas, concl)
-- UseTh needs the proof of a theorem to check if it's valid and then can be used.

traverse' db (UseTh (theo, proof) assums concl) =
  -- check if the theorem is valid
  let (proofvalid, _, proofuda, proofconcl) = traverse' db proof
      (Theorem thas thc) = theo
      missingassum = setdif proofuda thas
      theook = proofvalid && (missingassum == []) && (proofconcl == thc)
      -- check if the assumptions of the theorems are valid
      (oks, msgs, udas, concls) = checkproofs db assums
      err1 =
        "UseTh: the proof of the theorem "
          ++ show theo
          ++ " is not valid and then the theorem cannot be used\n"
      err2 =
        "UseTh: the theorem "
          ++ show theo
          ++ " cannot be applied "
          ++ "with the assumptions "
          ++ show concls
          ++ " and the conclusion ("
          ++ show concl
          ++ ")\n"
   in if not theook
        then (False, msgs ++ [err1], udas, concl)
        else
          if not oks
            then (False, msgs, udas, concl)
            else
              if (usetheorem theo concls concl)
                then (True, msgs, udas, concl)
                else (False, msgs ++ [err2], udas, concl)
-- UseDB checks if a theorem can be used by looking for it in a data-base

traverse' db (UseDB theo assums concl) =
  let (oks, msgs, udas, concls) = checkproofs db assums
      err1 =
        "UseDB: there is no known theorem of which name is "
          ++ show theo
          ++ "\n"
      err2 =
        "UseDB: the theorem "
          ++ show theo
          ++ " cannot be applied "
          ++ "with the assumptions "
          ++ show concls
          ++ " and the conclusion ("
          ++ show concl
          ++ ")\n"
   in if not (findtheorem db theo)
        then (False, msgs ++ [err1], udas, concl)
        else
          if not oks
            then (False, msgs, udas, concl)
            else
              if (usetheorem theo concls concl)
                then (True, msgs, udas, concl)
                else (False, msgs ++ [err2], udas, concl)

----------------------- the functions to use a theorem --------------------

-- the function 'checkproof' check the proofs of every assumptions of the theorem,
-- and return the list of the conclusions of these proofs, with their validity,
-- the error messages and the undischarged assumptions

checkproofs :: TheoremDB -> [Proof] -> (Bool, [String], [Prop], [Prop])
checkproofs _ [] = (True, [], [], [])
checkproofs db (x : xs) =
  let (okx, msgx, udasx, cclx) = traverse' db x
      (okxs, msgxs, udasxs, cclxs) = checkproofs db xs
   in (okx && okxs, msgx ++ msgxs, udasx `union` udasxs, cclx : cclxs)

-- The function 'usetheorem' checks if a theorem can be applied,
-- with the given assumption to reach the given conclusion.
-- Actually, the work is mainly performed by the functions 'unification' and 'allunifications'

usetheorem :: Theorem -> [Prop] -> Prop -> Bool
usetheorem theo assums concl =
  let (Theorem thassums thconcl) = theo
      (okconcl, _, unifconcl) = unif thconcl concl
   in (length thassums == length assums)
        && (okconcl) -- must be of same length
        && ( (unification unifconcl thassums assums) -- conclusions must match
               || (allunifications unifconcl thassums assums)
           )

-- The function 'unification' try to match the atoms of the first list of proposition,
-- with sub-propositions of the second list.
-- The propositions are taken in the order they appear within the lists.
-- The first argument is a list of already matched pairs. The 2 list are assumed to be of the same length.

unification :: [(Prop, Prop)] -> [Prop] -> [Prop] -> Bool
unification initialpairs l1 l2 =
  let (ok, _) = unifrec l1 l2 in ok
  where
    unifrec :: [Prop] -> [Prop] -> (Bool, [(Prop, Prop)])
    unifrec [] [] = (True, initialpairs)
    unifrec (x : xs) (y : ys) =
      let (okxy, _, unifxy) = unif x y
          (oks, unifs) =
            if okxy
              then (unifrec xs ys)
              else (False, [])
          (oku, unifu) =
            if oks
              then addunif unifxy unifs
              else (False, [])
       in (oku, unifu)

-- The function 'allunifiactions' is a kind of extended version of 'unification':
-- now, the order of the propositions does not matter, since every permutation may be considered.

allunifications :: [(Prop, Prop)] -> [Prop] -> [Prop] -> Bool
allunifications initialpairs l1 l2 =
  let (ok, _) = allunifrec (order l1) ([], (order l2)) initialpairs in ok
  where
    allunifrec ::
      [Prop] ->
      ([Prop], [Prop]) ->
      [(Prop, Prop)] ->
      (Bool, [(Prop, Prop)])
    allunifrec [] ([], []) pairs = (True, pairs)
    allunifrec (_ : _) (_, []) _ = (False, [])
    allunifrec (x : xs) (prev, (y : ys)) pairs =
      let (okxy, eqxy, unifxy) = unif x y
       in if okxy
            then
              let (oku, unifu) = addunif pairs unifxy
               in if not oku
                    then trynext
                    else
                      let (oks, unifs) = allunifrec xs ([], prev ++ ys) unifu
                       in if not oks then trynext else (oks, unifs)
            else
              if eqxy == Greater
                then (False, [])
                else trynext
      where
        trynext = allunifrec (x : xs) (prev ++ [y], ys) pairs
    allunifrec _ _ _ = (False, [])

-- unification of 2 propositions: the function 'unif'
-- . the Bool-value returned is True iff the unification succeeded
-- . the Comparison-value returned is the comparison between the 2 trees of the propositions (cf 'comparison')
-- . the list returned is the list of the matching pairs

unif :: Prop -> Prop -> (Bool, Comparison, [(Prop, Prop)])
unif x y =
  case x of
    TRUE ->
      if y == TRUE
        then (True, Equal, [])
        else (False, comparison x y, [])
    FALSE ->
      if y == FALSE
        then (True, Equal, [])
        else (False, comparison x y, [])
    And a b -> case y of
      And c d -> unifacbd a c b d
      otherwise -> (False, comparison x y, [])
    Or a b -> case y of
      Or c d -> unifacbd a c b d
      otherwise -> (False, comparison x y, [])
    Not a -> case y of
      Not b -> unif a b
      Imp b FALSE -> unif a b
      otherwise -> (False, comparison x y, [])
    Imp a b -> case y of
      Imp c d -> unifacbd a c b d
      Not c ->
        if b == FALSE
          then unif a c
          else (False, comparison x y, [])
      otherwise -> (False, comparison x y, [])
    _ -> (True, Equal, [(x, y)])
  where
    unifacbd a c b d =
      let (okac, eqac, unifac) = unif a c
          (okbd, eqbd, unifbd) = unif b d
          (oku, unifu) = addunif unifac unifbd
          eqacbd = if (eqac /= Equal) then eqac else eqbd
       in if oku then (True, eqacbd, unifu) else (False, eqacbd, [])

-- 'addunif' performs the union of 2 sets of matching pairs, and checks whether there is a conflict

addunif :: [(Prop, Prop)] -> [(Prop, Prop)] -> (Bool, [(Prop, Prop)])
addunif xs [] = (True, xs)
addunif xs (y : ys) =
  let (exp, val) = y
      setexp = [v | (y, v) <- xs, y == exp]
   in if setexp == []
        then addunif (y : xs) ys
        else
          if val == head setexp
            then addunif xs ys
            else (False, [])

-- comparison of 2 trees of proposition, with 3 possible values.
-- The order is:
--     And > Or > Imp > FALSE > (variable)
-- When its the same operator, the left sub-tree is considered first.
-- For TRUE and Not, their definitions are used.

comparison :: Prop -> Prop -> Comparison
comparison a b =
  case (a, b) of
    -- definitions of Not and TRUE:
    (Not x, _) -> comparison (x `Imp` FALSE) b
    (_, Not y) -> comparison a (y `Imp` FALSE)
    (TRUE, _) -> comparison (FALSE `Imp` FALSE) b
    (_, TRUE) -> comparison a (FALSE `Imp` FALSE)
    -- equality:
    (FALSE, FALSE) -> Equal
    (Imp x1 x2, Imp y1 y2) -> comparison2 x1 y1 x2 y2
    (Or x1 x2, Or y1 y2) -> comparison2 x1 y1 x2 y2
    (And x1 x2, And y1 y2) -> comparison2 x1 y1 x2 y2
    -- inequality (from the greatest to the least):
    (And _ _, _) -> Greater
    (_, And _ _) -> Lesser
    (Or _ _, _) -> Greater
    (_, Or _ _) -> Lesser
    (Imp _ _, _) -> Greater
    (_, Imp _ _) -> Lesser
    (FALSE, _) -> Greater
    (_, FALSE) -> Lesser
    -- equality of tree (2 variables):
    (_, _) -> Equal
  where
    comparison2 x1 y1 x2 y2 =
      let comp1 = comparison x1 y1
       in if (comp1 /= Equal) then comp1 else (comparison x2 y2)

-- The function 'order' sorts proposition from the greatest to the least,
-- according to the function 'comparison'
-- (note: the result depends on the initial list,
-- since 2 differents propositions may be considered equal as 'comparison' compares trees not values)

order :: [Prop] -> [Prop]
order [] = []
order (x : xs) = (order greater_egal) ++ [x] ++ (order lesser)
  where
    (lesser, greater_egal) = split xs ([], [])
    split [] (le, g) = (le, g)
    split (y : ys) (le, g) =
      split
        ys
        ( if (comparison y x == Lesser)
            then (y : le, g)
            else (le, y : g)
        )

----------------------- functions to use the data-base --------------------

-- the function 'findtheorem' looks if a theorem belongs to the data-base of known theorems.

findtheorem :: TheoremDB -> Theorem -> Bool
findtheorem db t =
  case db of
    [] -> False
    (x : xs) -> x == s || findtheorem xs t
  where
    s = namefor t

-- The function 'namefor' give a name (String) to a theorem,
-- which does not depend on the name given to the variables of the theorem.
-- For example, (Theorem [A,B] (B `And` A)) and (Theorem [C,D] (D `And` C)) will receive the same name.

namefor :: Theorem -> String
namefor t =
  let (Theorem assums concl) = t
      names = name (concl : assums)
   in write assums names ++ " |- " ++ write [concl] names
  where
    name :: [Prop] -> [(Prop, Int)]
    name xs = zip (atoms xs) [1 ..]
      where
        atoms :: [Prop] -> [Prop]
        atoms [] = []
        atoms (x : xs) =
          case x of
            TRUE -> atoms xs
            FALSE -> atoms xs
            And p q -> ((atoms [p]) `union` (atoms [q])) `union` (atoms xs)
            Or p q -> ((atoms [p]) `union` (atoms [q])) `union` (atoms xs)
            Imp p q -> ((atoms [p]) `union` (atoms [q])) `union` (atoms xs)
            Not p -> (atoms [p]) `union` (atoms xs)
            _ -> [x] `union` (atoms xs)

    write :: [Prop] -> [(Prop, Int)] -> String
    write [] _ = ""
    write (x : []) names = writeprop x names
    write (x : xs) names = writeprop x names ++ ", " ++ write xs names

    writeprop :: Prop -> [(Prop, Int)] -> String
    writeprop x names =
      case x of
        TRUE -> "T"
        FALSE -> "F"
        And p q ->
          "(And "
            ++ writeprop p names
            ++ " "
            ++ writeprop q names
            ++ ")"
        Or p q ->
          "(Or "
            ++ writeprop p names
            ++ " "
            ++ writeprop q names
            ++ ")"
        Imp p FALSE -> writeprop (Not p) names
        Imp p q ->
          "(Imp "
            ++ writeprop p names
            ++ " "
            ++ writeprop q names
            ++ ")"
        Not p -> "(Not " ++ writeprop p names ++ ")"
        _ -> show (head [s | (a, s) <- names, a == x])

-- The 2 following functions convert a String into a data-base, and vice-versa

readtheorems :: String -> TheoremDB
readtheorems = clear . lines
  where
    clear [] = []
    clear (x : xs) = if x == "" then clear xs else x : clear xs

writetheorems :: TheoremDB -> String
writetheorems [] = "\n"
writetheorems (x : xs) = x ++ "\n" ++ writetheorems xs

-------------------- user's functions for the db --------------------------

addNewTheorem :: String -> Theorem -> Proof -> IO ()
addNewTheorem filename theo proof =
  do
    filedata <- (readFile filename) -- `catch` (\_ -> return ".")
    let db = readtheorems filedata
     in do
          ok <- check_proof_with_db db theo proof
          if ok && (db == db) -- to force the complete evaluation of 'db'
            then do
              writeFile
                filename
                ( writetheorems
                    (db `union` [namefor theo])
                )
              return ()
            else return ()

checkProofUsingTheorems :: String -> Theorem -> Proof -> IO ()
checkProofUsingTheorems filename theo proof =
  do
    filedata <- (readFile filename) -- `catch` (\_ -> return ".")
    check_proof_with_db (readtheorems filedata) theo proof
    return ()