module Logic.Language.Impl.L where

import Logic.Language (Language(..))
import Logic.Language.Derivation (Derivation(..))
import Logic.Statement (Statement(..))
import Logic.Parse
  ( Parser(..)
  , ParseError
  , Input(..)
  , eof
  , expected
  , mkInput
  , parseToken
  )

import Control.Applicative (Alternative((<|>)))
import Data.Either (isRight)
import Data.Maybe (fromJust, maybeToList)
import Text.Read (readMaybe)

-- The language L
data AlphaL
  = Arrow
  | Tilde
  | Open
  | Close
  | Variable Integer
  deriving (Eq, Show)

type StringL = [AlphaL]

instance Language AlphaL where
  isWellFormed string = isRight $ eof parseL $ mkInput string

  axiom2 = [lAxiom1, lAxiom3]
  axiom3 = [lAxiom2]
  infer2 = [lRule1]

-- (A → (B → A))
lAxiom1 :: StringL -> StringL -> StringL
lAxiom1 wff1 wff2 =
  [Open] ++
    wff1 ++
  [Arrow] ++
    [Open] ++ wff2 ++ [Arrow] ++ wff1 ++ [Close] ++
  [Close]

-- ((A → (B → C)) → ((A → B) → (A → C)))
lAxiom2 :: StringL -> StringL -> StringL -> StringL
lAxiom2 wff1 wff2 wff3 =
  [Open] ++
    [Open] ++
      wff1 ++
    [Arrow] ++
      [Open] ++ wff2 ++ [Arrow] ++ wff3 ++ [Close] ++
    [Close] ++
  [Arrow] ++
    [Open] ++
      [Open] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
    [Arrow] ++
      [Open] ++ wff1 ++ [Arrow] ++ wff3 ++ [Close] ++
    [Close] ++
  [Close]

-- ((¬A → ¬B) → ((¬A → B) → A))
lAxiom3 :: StringL -> StringL -> StringL
lAxiom3 wff1 wff2 =
  [Open] ++
    [Open, Tilde] ++ wff1 ++ [Arrow, Tilde] ++ wff2 ++ [Close] ++
  [Arrow] ++
    [Open] ++
      [Open, Tilde] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
    [Arrow] ++
      wff1 ++
    [Close] ++
  [Close]

{-
ghci> import Logic.Statement.Eval (bucket)
ghci> import Data.Either (fromRight)
ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom1 [Variable 0] [Variable 1]
Tautology
ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom2 [Variable 0] [Variable 1] [Variable 2]
Tautology
ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom3 [Variable 0] [Variable 1]
Tautology
-}

-- Modus ponens: from (A → B) and A, conclude B.
lRule1 :: StringL -> StringL -> [StringL]
lRule1 theorem1 theorem2 = maybeToList $ do
  s1 <- fromEither $ eof parseL $ mkInput theorem1
  s2 <- fromEither $ eof parseL $ mkInput theorem2
  case s1 of
    Implies s1a s1b
      | s1a == s2 -> Just $ fromJust $ serializeL s1b
      | otherwise -> Nothing
    _ -> Nothing
  where
    fromEither = either (const Nothing) Just

{-
ghci> f x = fromJust $ serializeL $ fromRight undefined $ eof stmt $ mkInput x
ghci> lRule1 (f "(0->1)") (f "0")
[[Variable 1]]
ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->2)")
[[Open,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Variable 1,Arrow,Variable 1,Close]]
ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->3)")
[]
-}

parseL :: Parser AlphaL Statement
parseL = Parser variable <|> Parser tilde <|> arrow <|> fail
  where
    variable :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
    variable input@(Input pos ((Variable n):xs)) =
      Right (Atom $ show n, Input (pos + 1) xs)
    variable input = Left $ expected "statement variable" input

    tilde :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
    tilde input@(Input pos (Tilde:xs)) =
      (\(statement, rest) -> (Not statement, rest)) <$>
      runParser parseL (Input (pos + 1) xs)
    tilde input = Left $ expected "negation" input

    arrow :: Parser AlphaL Statement
    arrow = do
      _  <- parseToken [Open]
      s1 <- parseL
      _  <- parseToken [Arrow]
      s2 <- parseL
      _  <- parseToken [Close]
      return $ Implies s1 s2

    fail :: Parser AlphaL Statement
    fail = Parser $ \input -> Left $ expected "well-formed formula" input

serializeL :: Statement -> Maybe [AlphaL]
serializeL (Atom label) = (\x -> [x]) <$> Variable <$> readMaybe label
serializeL (Not s) = (Tilde:) <$> serializeL s
serializeL (Implies s1 s2) = do
  l1 <- serializeL s1
  l2 <- serializeL s2
  return $ [Open] ++ l1 ++ [Arrow] ++ l2 ++ [Close]
serializeL _ = Nothing

deriveLExample1 :: Derivation AlphaL
deriveLExample1 = step5
  where
    step1 = Hypothesis [Open, Variable 1, Arrow, Variable 2, Close]
    step2 = Axiom2 0 [Open, Variable 1, Arrow, Variable 2, Close] [Variable 0]
    step3 = Infer2 0 0 step2 step1
    step4 = Axiom3 0 [Variable 0] [Variable 1] [Variable 2]
    step5 = Infer2 0 0 step4 step3

deriveLExample2 :: Derivation AlphaL
deriveLExample2 = step5
  where
    step1 = Axiom2 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close]
    step2 = Axiom3 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close] [Variable 0]
    step3 = Infer2 0 0 step2 step1
    step4 = Axiom2 0 [Variable 0] [Variable 0]
    step5 = Infer2 0 0 step3 step4