{-#LANGUAGE  FlexibleContexts,  FlexibleInstances, MultiParamTypeClasses #-}
module Carnap.Languages.PurePropositional.Logic.Gamut 
    ( GamutMPND(..), gamutMPNDCalc, parseGamutMPND
    , GamutIPND(..), gamutIPNDCalc, parseGamutIPND
    , GamutPND(..), gamutPNDCalc, parseGamutPND
    , GamutPNDPlus(..), gamutPNDPlusCalc, parseGamutPNDPlus
    ) where

import Text.Parsec
import Data.Char
import Carnap.Core.Data.Types (Form)
import Carnap.Core.Data.Classes
import Carnap.Core.Unification.Unification (applySub,subst,FirstOrder)
import Carnap.Languages.PurePropositional.Syntax
import Carnap.Languages.PurePropositional.Parser
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 (parseSeqOver)
import Carnap.Languages.Util.LanguageClasses
import Carnap.Languages.Util.GenericConstructors
import Carnap.Languages.PurePropositional.Logic.Rules

data GamutMPND = InAnd  | ElimAndL | ElimAndR
               | ElimIf | InIf1    | InIf2
               | InNeg1 | InNeg2   | ElimNeg 
               | ElimOr | InOrL    | InOrR 
               | AS     | PR       | Rep
    deriving Eq

data GamutIPND = MPND GamutMPND | EFSQ
    deriving Eq

data GamutPND = IPND GamutIPND | DNE
    deriving Eq

data GamutPNDPlus = PND GamutPND 
                  | LEM | LNC | DN1 | DN2
                  | LCC  | LCD  | LAC1 | LAC2 | LAD1 | LAD2
                  | LDD1 | LDD2 | LDC1 | LDC2 | DMOR1 | DMOR2
                  | DMAND1 | DMAND2 | MT | MTP | NMTP
    deriving Eq

instance Show GamutMPND where
        show InAnd      = "I∧"
        show ElimAndL   = "E∧"
        show ElimAndR   = "E∧"
        show ElimIf     = "E→"
        show InIf1      = "I→"
        show InIf2      = "I→"
        show InNeg1     = "I¬"
        show InNeg2     = "I¬"
        show ElimNeg    = "E¬"
        show ElimOr     = "E∨"
        show InOrL      = "I∨" 
        show InOrR      = "I∨"
        show AS         = "assumption"
        show PR         = "assumption"
        show Rep        = "repeat"

instance Show GamutIPND where
        show (MPND x)   = show x
        show EFSQ       = "EFSQ"

instance Show GamutPND where
        show (IPND x)   = show x
        show DNE        = "¬¬"

instance Show GamutPNDPlus where
        show (PND x)   = show x
        show LEM = "LEM"
        show LNC = "LNC"
        show DN1 = "DN"
        show DN2 = "DN"
        show LCC = "LCC"
        show LCD = "LCD" 
        show LAC1 = "LAC"
        show LAC2 = "LAC"
        show LAD1 = "LAD"
        show LAD2 = "LAD"
        show LDD1 = "LDD"
        show LDD2 = "LDD"
        show LDC1 = "LDC"
        show LDC2 = "LDC"
        show DMOR1 = "DMOR"
        show DMOR2 = "DMOR"
        show DMAND1 = "DMAND"
        show DMAND2 = "DMAND"
        show MT = "MT"
        show MTP = "PDS" 
        show NMTP = "NDS"

instance Inference GamutMPND PurePropLexicon (Form Bool) where
        ruleOf InAnd      = adjunction
        ruleOf ElimAndL   = simplificationVariations !! 0
        ruleOf ElimAndR   = simplificationVariations !! 1
        ruleOf ElimIf     = modusPonens
        ruleOf InIf1      = conditionalProofVariations !! 0
        ruleOf InIf2      = conditionalProofVariations !! 1
        ruleOf InNeg1     = constructiveFalsumReductioVariations !! 0
        ruleOf InNeg2     = constructiveFalsumReductioVariations !! 1
        ruleOf ElimNeg    = falsumIntroduction
        ruleOf ElimOr     = dilemma
        ruleOf Rep        = identityRule
        ruleOf InOrL      = additionVariations !! 0
        ruleOf InOrR      = additionVariations !! 1
        ruleOf AS         = axiom
        ruleOf PR         = axiom

        indirectInference x
            | x `elem` [InIf1, InIf2, InNeg1, InNeg2] = Just (WithAlternate (ImplicitProof (ProofType 0 1)) (TypedProof (ProofType 0 1)))
            | otherwise = Nothing

        isAssumption AS = True
        isAssumption _ = False

        globalRestriction (Left ded) n InIf1 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n InIf2 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n InNeg1 = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction (Left ded) n InNeg2 = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction _ _ _ = Nothing

instance Inference GamutIPND PurePropLexicon (Form Bool) where
        ruleOf (MPND x) = ruleOf x
        ruleOf EFSQ     = falsumElimination

        indirectInference (MPND x) = indirectInference x
        indirectInference _ = Nothing

        isAssumption (MPND x) = isAssumption x
        isAssumption _ = False

        globalRestriction (Left ded) n (MPND InIf1) = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n (MPND InIf2) = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n (MPND InNeg1) = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction (Left ded) n (MPND InNeg2) = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction _ _ _ = Nothing

instance Inference GamutPND PurePropLexicon (Form Bool) where
        ruleOf (IPND x) = ruleOf x
        ruleOf DNE = doubleNegationElimination

        indirectInference (IPND x) = indirectInference x
        indirectInference _ = Nothing

        isAssumption (IPND x) = isAssumption x
        isAssumption _ = False

        globalRestriction (Left ded) n (IPND (MPND InIf1)) = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n (IPND (MPND InIf2)) = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n (IPND (MPND InNeg1)) = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction (Left ded) n (IPND (MPND InNeg2)) = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction _ _ _ = Nothing

instance Inference GamutPNDPlus PurePropLexicon (Form Bool) where
        ruleOf (PND x) = ruleOf x
        ruleOf LEM = [] ∴ Top :|-: SS (phin 1 .\/. (lneg $ phin 1))
        ruleOf LNC = [] ∴ Top :|-: SS (lneg (phin 1 ./\. (lneg $ phin 1)))
        ruleOf DN1 = doubleNegation !! 0
        ruleOf DN2 = doubleNegation !! 1
        ruleOf LCC = andCommutativity !! 0
        ruleOf LCD = orCommutativity !! 0
        ruleOf LAC1 = andAssociativity !! 0
        ruleOf LAC2 = andAssociativity !! 1
        ruleOf LAD1 = orAssociativity !! 0 
        ruleOf LAD2 = orAssociativity !! 1
        ruleOf LDD1 = orDistributivity !! 0
        ruleOf LDD2 = orDistributivity !! 1
        ruleOf LDC1 = andDistributivity !! 0
        ruleOf LDC2 = andDistributivity !! 1
        ruleOf DMOR1 = deMorgansLaws !! 0
        ruleOf DMOR2 = deMorgansLaws !! 1
        ruleOf DMAND1 = deMorgansLaws !! 2
        ruleOf DMAND2 = deMorgansLaws !! 3
        ruleOf MT = modusTollens
        ruleOf MTP = modusTollendoPonensVariations !! 0
        ruleOf NMTP = [ GammaV 1  :|-: SS (phin 1) 
                , GammaV 2  :|-: SS (lneg $ phin 1 .∧. phin 2)
                ] ∴ GammaV 1 :+: GammaV 2 :|-: SS (lneg $ phin 2)

        indirectInference (PND x) = indirectInference x
        indirectInference _ = Nothing

        isAssumption (PND x) = isAssumption x
        isAssumption _ = False

        globalRestriction (Left ded) n (PND (IPND (MPND InIf1))) = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n (PND (IPND (MPND InIf2))) = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
        globalRestriction (Left ded) n (PND (IPND (MPND InNeg1))) = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction (Left ded) n (PND (IPND (MPND InNeg2))) = Just $ fitchAssumptionCheck n ded [([phin 1], [lfalsum])]
        globalRestriction _ _ _ = Nothing

parseGamutMPND rtc = do r <- choice (map (try . string) 
                                [ "I∧" , "I/\\", "I^", "E∧" , "E/\\", "E^"
                                , "E→" , "E->", "I→" , "I->"
                                , "I¬" , "I~", "I-", "E¬" , "E~", "E-"
                                , "E∨" , "E\\/", "Ev",  "I∨" , "I\\/", "Iv"
                                , "repetition", "rep" , "assumption", "as"])
                        case r of 
                         r | r `elem` ["I∧" , "I/\\", "I^"] -> return [InAnd]
                           | r `elem` ["E∧" , "E/\\", "E^"] -> return [ElimAndR, ElimAndL]
                           | r `elem` ["E→" , "E->"]        -> return [ElimIf]
                           | r `elem` ["I→" , "I->"]        -> return [InIf1, InIf2]
                           | r `elem` ["I¬" , "I~", "I-"]   -> return [InNeg1, InNeg2]
                           | r `elem` ["E¬" , "E~", "E-"]   -> return [ElimNeg]
                           | r `elem` ["E∨" , "E\\/", "Ev"] -> return [ElimOr]
                           | r `elem` ["I∨" , "I\\/", "Iv"] -> return [InOrL, InOrR]
                           | r `elem` ["repetition", "rep"] -> return [Rep]
                           | r `elem` ["assumption", "as"]  -> return [AS, PR]

parseGamutIPND rtc = (map MPND <$> parseGamutMPND rtc) <|> (try (string "EFSQ") >> return [EFSQ])

parseGamutPND rtc = (map IPND <$> parseGamutIPND rtc) 
                 <|> (choice (map (try . string) ["~~","¬¬","--"]) >> return [DNE])

parseGamutPNDPlus rtc = (map PND <$> parseGamutPND rtc) 
                 <|> parsePlus
    where parsePlus = do r <- choice (map (try . string) ["LEM", "LNC", "DN", "LCC", "LCD", "LAC", "LAD", "LDD", "LDC", "DMOR", "DMAND", "MT", "PDS", "NDS"])
                         return $ case r of
                           r | r == "LEM"   -> [LEM]
                             | r == "LNC"   -> [LNC]
                             | r == "DN"    -> [DN1, DN2]
                             | r == "LCC"   -> [LCC]
                             | r == "LCD"   -> [LCD]
                             | r == "LAC"   -> [LAC1,LAC2]
                             | r == "LAD"   -> [LAD1,LAD2]
                             | r == "LDD"   -> [LDD1,LDD2]
                             | r == "LDC"   -> [LDC1,LDC2]
                             | r == "DMOR"  -> [DMOR1,DMOR2]
                             | r == "DMAND" -> [DMAND1,DMAND2]
                             | r == "MT"    -> [MT]
                             | r == "PDS"   -> [MTP]
                             | r == "NDS"   -> [NMTP]

parseGamutMPNDProof :: RuntimeNaturalDeductionConfig PurePropLexicon (Form Bool) -> String -> [DeductionLine GamutMPND PurePropLexicon (Form Bool)]
parseGamutMPNDProof rtc = toDeductionFitch (parseGamutMPND rtc) (purePropFormulaParser gamutOpts)

parseGamutIPNDProof :: RuntimeNaturalDeductionConfig PurePropLexicon (Form Bool) -> String -> [DeductionLine GamutIPND PurePropLexicon (Form Bool)]
parseGamutIPNDProof rtc = toDeductionFitch (parseGamutIPND rtc) (purePropFormulaParser gamutOpts)

parseGamutPNDProof :: RuntimeNaturalDeductionConfig PurePropLexicon (Form Bool) -> String -> [DeductionLine GamutPND PurePropLexicon (Form Bool)]
parseGamutPNDProof rtc = toDeductionFitch (parseGamutPND rtc) (purePropFormulaParser gamutOpts)

parseGamutPNDPlusProof :: RuntimeNaturalDeductionConfig PurePropLexicon (Form Bool) -> String -> [DeductionLine GamutPNDPlus PurePropLexicon (Form Bool)]
parseGamutPNDPlusProof rtc = toDeductionFitch (parseGamutPNDPlus rtc) (purePropFormulaParser gamutOpts)

gamutNotation :: String -> String
gamutNotation (x:xs) | isUpper x = toLower x : gamutNotation xs
                     | otherwise = x : gamutNotation xs
gamutNotation [] = []

gamutMPNDCalc = mkNDCalc
    { ndRenderer = NoRender
    , ndParseProof = parseGamutMPNDProof
    , ndProcessLine = hoProcessLineFitch
    , ndProcessLineMemo = Just hoProcessLineFitchMemo
    , ndParseSeq = parseSeqOver (purePropFormulaParser gamutOpts)
    , ndParseForm = purePropFormulaParser gamutOpts
    , ndNotation = gamutNotation
    }

gamutIPNDCalc = mkNDCalc
    { ndRenderer = NoRender
    , ndParseProof = parseGamutIPNDProof
    , ndProcessLine = hoProcessLineFitch
    , ndProcessLineMemo = Just hoProcessLineFitchMemo
    , ndParseSeq = parseSeqOver (purePropFormulaParser gamutOpts)
    , ndParseForm = purePropFormulaParser gamutOpts
    , ndNotation = gamutNotation
    }

gamutPNDCalc = mkNDCalc
    { ndRenderer = NoRender
    , ndParseProof = parseGamutPNDProof
    , ndProcessLine = hoProcessLineFitch
    , ndProcessLineMemo = Just hoProcessLineFitchMemo
    , ndParseSeq = parseSeqOver (purePropFormulaParser gamutOpts)
    , ndParseForm = purePropFormulaParser gamutOpts
    , ndNotation = gamutNotation
    }

gamutPNDPlusCalc = mkNDCalc
    { ndRenderer = NoRender
    , ndParseProof = parseGamutPNDPlusProof
    , ndProcessLine = hoProcessLineFitch
    , ndProcessLineMemo = Just hoProcessLineFitchMemo
    , ndParseSeq = parseSeqOver (purePropFormulaParser gamutOpts)
    , ndParseForm = purePropFormulaParser gamutOpts
    , ndNotation = gamutNotation
    }
