module Logic.Language.Derivation where

import Logic.Language (Language(..))

data Derivation symbol
  = Hypothesis [symbol]
  | Axiom0 Integer
  | Axiom1 Integer [symbol]
  | Axiom2 Integer [symbol] [symbol]
  | Axiom3 Integer [symbol] [symbol] [symbol]
  | Infer1 Integer Integer (Derivation symbol)
  | Infer2 Integer Integer (Derivation symbol) (Derivation symbol)
  deriving (Eq, Show)

data DerivationError s
  = SelectIndexError (DerivationSelectIndexError s)
  | ResultIndexError (DerivationResultIndexError s)
  | NotWellFormed [s]
  deriving Show

data DerivationSelectIndexError s = DerivationSelectIndexError
  { dserrSelectPlace :: DerivationSelectIndexErrorPlace
  , dserrSelectErrorIndex :: Integer
  , dserrSize :: Int
  , dserrWffs :: [[s]]
  } deriving Show

data DerivationSelectIndexErrorPlace
  = AxiomSelect
  | InferSelect
  deriving Show

data DerivationResultIndexError s = DerivationResultIndexError
  { drerrPlace :: DerivationResultIndexErrorPlace
  , drerrSelectIndex :: Integer
  , drerrResultIndex :: Integer
  , drerrResult :: [[s]]
  , drerrTheorems :: [[s]]
  } deriving Show

data DerivationResultIndexErrorPlace
  = InferResult
  deriving Show

resolveDerivation :: Language s => Derivation s -> Either (DerivationError s) [s]
resolveDerivation derivation =
  case derivation of
    (Hypothesis wff)
      | not $ isWellFormed wff -> Left $ NotWellFormed wff
      | otherwise -> Right wff
    (Axiom0 index) -> trySelect AxiomSelect axiom0 index []
    (Axiom1 index wff1)
      | not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
      | otherwise -> do
        rule <- trySelect AxiomSelect axiom1 index [wff1]
        return $ rule wff1
    (Axiom2 index wff1 wff2)
      | not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
      | not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
      | otherwise -> do
        rule <- trySelect AxiomSelect axiom2 index [wff1, wff2]
        return $ rule wff1 wff2
    (Axiom3 index wff1 wff2 wff3)
      | not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
      | not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
      | not $ isWellFormed wff3 -> Left $ NotWellFormed wff3
      | otherwise -> do
        rule <- trySelect AxiomSelect axiom3 index [wff1, wff2, wff3]
        return $ rule wff1 wff2 wff3
    (Infer1 selectIndex resultIndex deriv1) -> do
      theorem1 <- resolveDerivation deriv1
      rule <- trySelect InferSelect infer1 selectIndex [theorem1]
      let result = rule theorem1
      tryResult InferResult selectIndex resultIndex result [theorem1]
    (Infer2 selectIndex resultIndex deriv1 deriv2) -> do
      theorem1 <- resolveDerivation deriv1
      theorem2 <- resolveDerivation deriv2
      rule <- trySelect InferSelect infer2 selectIndex [theorem1, theorem2]
      let result = rule theorem1 theorem2
      tryResult InferResult selectIndex resultIndex result [theorem1, theorem2]
  where
    trySelect place list index wffs = maybe
      (Left $ SelectIndexError $ DerivationSelectIndexError place index (length list) wffs)
      Right $
      get index list

    tryResult place selectIndex resultIndex list theorems = maybe
      (Left $ ResultIndexError $ DerivationResultIndexError place selectIndex resultIndex list theorems)
      Right $
      get resultIndex list

    get :: Integer -> [a] -> Maybe a
    get 0 (x:xs) = Just x
    get index [] = Nothing
    get index (x:xs)
      | index >= 1 = get (index - 1) xs
      | otherwise = Nothing