{-#LANGUAGE  FlexibleContexts,  FlexibleInstances, MultiParamTypeClasses #-}
module Carnap.Languages.PureFirstOrder.Logic.EbelsDuggan (ebelsDugganFOLCalc,parseEbelsDugganFOL) where

import Data.Map as M (lookup, Map,empty)
import Text.Parsec
import Carnap.Core.Data.Types (Form)
import Carnap.Languages.PureFirstOrder.Syntax
import Carnap.Languages.PureFirstOrder.Parser
import qualified Carnap.Languages.PurePropositional.Logic as P
import Carnap.Calculi.NaturalDeduction.Syntax
import Carnap.Calculi.NaturalDeduction.Parser
import Carnap.Calculi.NaturalDeduction.Checker (hoProcessLineFitchMemo, hoProcessLineFitch)
import Carnap.Languages.ClassicalSequent.Syntax
import Carnap.Languages.ClassicalSequent.Parser
import Carnap.Languages.Util.LanguageClasses
import Carnap.Languages.Util.GenericConstructors
import Carnap.Languages.PureFirstOrder.Logic.Rules
import Carnap.Languages.PurePropositional.Logic.Rules (premConstraint,axiom)
import Carnap.Languages.PureFirstOrder.Logic.ThomasBolducAndZach
import Carnap.Languages.PurePropositional.Logic.EbelsDuggan

data EbelsDugganFOL = EDTFL P.EbelsDugganTFL | TBZFOL ThomasBolducAndZachFOL | EQS | EQT

instance Show EbelsDugganFOL where
        show (EDTFL x) = show x
        show (TBZFOL x) = show x
        show EQS = "=S"
        show EQT = "=T"

instance Inference EbelsDugganFOL PureLexiconFOL (Form Bool) where

         ruleOf (TBZFOL x) = ruleOf x
         ruleOf r@(EDTFL x) = premisesOf r ∴ conclusionOf r
         ruleOf EQS = eqSymmetry
         ruleOf EQT = eqTransitivity

         premisesOf (EDTFL x) = map liftSequent (premisesOf x)
         premisesOf r = upperSequents (ruleOf r)
         
         conclusionOf (EDTFL x) = liftSequent (conclusionOf x)
         conclusionOf r = lowerSequent (ruleOf r)

         indirectInference (EDTFL x) = indirectInference x
         indirectInference (TBZFOL x) = indirectInference x
         indirectInference x = Nothing

         restriction (TBZFOL x) = restriction x
         restriction _     = Nothing

         isAssumption (EDTFL x) = isAssumption x
         isAssumption (TBZFOL x) = isAssumption x
         isAssumption _ = False

         isPremise (EDTFL x) = isPremise x
         isPremise (TBZFOL x) = isPremise x
         isPremise _ = False

parseEbelsDugganFOL rtc = try (map TBZFOL <$> parseThomasBolducAndZachFOL rtc) 
                      <|> try (map EDTFL <$> parseEbelsDugganTFL (RuntimeNaturalDeductionConfig mempty mempty))
                      <|> do r <- choice (map (try . string) ["=S", "=T"])
                             return $ case r of "=S" -> [EQS]
                                                "=T" -> [EQT]

parseEbelsDugganFOLProof :: RuntimeNaturalDeductionConfig PureLexiconFOL (Form Bool) -> String -> [DeductionLine EbelsDugganFOL PureLexiconFOL (Form Bool)]
parseEbelsDugganFOLProof ders = toDeductionFitch (parseEbelsDugganFOL ders) thomasBolducAndZachFOLFormulaParser

ebelsDugganFOLCalc = mkNDCalc
    { ndRenderer = FitchStyle StandardFitch
    , ndParseProof = parseEbelsDugganFOLProof
    , ndProcessLine = hoProcessLineFitch
    , ndProcessLineMemo = Just hoProcessLineFitchMemo
    , ndParseSeq = parseSeqOver thomasBolducAndZachFOLFormulaParser
    , ndParseForm = thomasBolducAndZachFOLFormulaParser
    , ndNotation = ndNotation P.thomasBolducAndZachTFLCalc
    }
