content: {-#LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}
  module Carnap.Languages.PurePropositional.Logic.Belot
      ( belotSDCalc, belotSDPlusCalc, BelotSD(..), BelotSDPlus(..), parseBelotSD, parseBelotSDPlus) where
  
  import Text.Parsec
  import Data.Char (toLower)
  import Carnap.Core.Data.Types (Form)
  import Carnap.Languages.PurePropositional.Syntax
  import Carnap.Languages.PurePropositional.Parser
  import Carnap.Calculi.Util
  import Carnap.Calculi.NaturalDeduction.Syntax
  import Carnap.Calculi.NaturalDeduction.Parser
  import Carnap.Calculi.NaturalDeduction.Checker
  import Carnap.Languages.ClassicalSequent.Syntax
  import Carnap.Languages.ClassicalSequent.Parser
  import Carnap.Languages.PurePropositional.Logic.Rules
  import Carnap.Languages.Util.LanguageClasses
  
  data BelotSD = ConjIntro  
               | ConjElim1  | ConjElim2
               | CondIntro1 | CondIntro2
               | CondElim
               | NegeIntro1 | NegeIntro2
               | NegeIntro3 | NegeIntro4
               | NegeElim1  | NegeElim2
               | NegeElim3  | NegeElim4
               | DisjIntro1 | DisjIntro2
               | DisjElim1  | DisjElim2
               | DisjElim3  | DisjElim4
               | BicoIntro1 | BicoIntro2 
               | BicoIntro3 | BicoIntro4
               | BicoElim1  | BicoElim2
               | Reiterate  | AS String
               | Pr (Maybe [(ClassicalSequentOver PurePropLexicon (Sequent (Form Bool)))])
             deriving Eq
  
  instance Show BelotSD where
          show ConjIntro  = "(&I)"
          show ConjElim1  = "(&E)"
          show ConjElim2  = "(&E)"
          show CondIntro1 = "(⊃I)"
          show CondIntro2 = "(⊃I)"
          show CondElim   = "(⊃E)"
          show NegeIntro1 = "(~I)"
          show NegeIntro2 = "(~I)"
          show NegeIntro3 = "(~I)"
          show NegeIntro4 = "(~I)"
          show NegeElim1  = "(~E)" 
          show NegeElim2  = "(~E)"
          show NegeElim3  = "(~E)"
          show NegeElim4  = "(~E)"
          show DisjElim1  = "(∨E)"
          show DisjElim2  = "(∨E)"
          show DisjElim3  = "(∨E)"
          show DisjElim4  = "(∨E)"
          show DisjIntro1 = "(∨I)"
          show DisjIntro2 = "(∨I)"
          show BicoIntro1 = "(≡I)"
          show BicoIntro2 = "(≡I)"
          show BicoIntro3 = "(≡I)"
          show BicoIntro4 = "(≡I)"
          show BicoElim1  = "(≡E)"
          show BicoElim2  = "(≡E)"
          show Reiterate  = "R"
          show (Pr _)     = "A"
          show (AS s)     = "A " ++ s ++ ""
  
  instance Inference BelotSD PurePropLexicon (Form Bool) where
      ruleOf Reiterate  = identityRule
      ruleOf CondElim   = modusPonens
      ruleOf CondIntro1 = conditionalProofVariations !! 0 
      ruleOf CondIntro2 = conditionalProofVariations !! 1
      ruleOf ConjIntro  = adjunction
      ruleOf NegeIntro1 = constructiveReductioVariations !! 0
      ruleOf NegeIntro2 = constructiveReductioVariations !! 1
      ruleOf NegeIntro3 = constructiveReductioVariations !! 2
      ruleOf NegeIntro4 = constructiveReductioVariations !! 3
      ruleOf NegeElim1  = nonConstructiveReductioVariations !! 0
      ruleOf NegeElim2  = nonConstructiveReductioVariations !! 1
      ruleOf NegeElim3  = nonConstructiveReductioVariations !! 2
      ruleOf NegeElim4  = nonConstructiveReductioVariations !! 3
      ruleOf DisjIntro1 = additionVariations !! 0
      ruleOf DisjIntro2 = additionVariations !! 1
      ruleOf DisjElim1  = proofByCasesVariations !! 0
      ruleOf DisjElim2  = proofByCasesVariations !! 1
      ruleOf DisjElim3  = proofByCasesVariations !! 2
      ruleOf DisjElim4  = proofByCasesVariations !! 3
      ruleOf ConjElim1  = simplificationVariations !! 0
      ruleOf ConjElim2  = simplificationVariations !! 1
      ruleOf BicoIntro1 = biconditionalProofVariations !! 0
      ruleOf BicoIntro2 = biconditionalProofVariations !! 1
      ruleOf BicoIntro3 = biconditionalProofVariations !! 2
      ruleOf BicoIntro4 = biconditionalProofVariations !! 3
      ruleOf (Pr _)     = axiom
      ruleOf (AS _)     = axiom
      ruleOf BicoElim1  = biconditionalPonensVariations !! 0
      ruleOf BicoElim2  = biconditionalPonensVariations !! 1
  
      indirectInference x
          | x `elem` [CondIntro1,CondIntro2, BicoIntro1, BicoIntro2
                     , BicoIntro3, BicoIntro4 , DisjElim1, DisjElim2
                     , DisjElim3, DisjElim4 ] = Just PolyProof
          | x `elem` [ NegeIntro1, NegeIntro2 , NegeIntro3, NegeIntro4
                     , NegeElim1, NegeElim2, NegeElim3, NegeElim4
                     ] = Just doubleProof
          | otherwise = Nothing
  
      isAssumption (AS _) = True
      isAssumption _ = False
  
      isPremise (Pr _) = True
      isPremise _ = False
  
      globalRestriction (Left ded) n CondIntro1 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
      globalRestriction (Left ded) n CondIntro2 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2])]
      globalRestriction (Left ded) n NegeIntro1 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeIntro2 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeIntro3 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeIntro4 = Just $ fitchAssumptionCheck n ded [([phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeElim1 = Just $ 
          fitchAssumptionCheck n ded [([lneg $ phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeElim2 = Just $ 
          fitchAssumptionCheck n ded [([lneg $ phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeElim3 = Just $ 
          fitchAssumptionCheck n ded [([lneg $ phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n NegeElim4 = Just $ 
          fitchAssumptionCheck n ded [([lneg $ phin 1], [phin 2, lneg $ phin 2])]
      globalRestriction (Left ded) n DisjElim1 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 3]), ([phin 2], [phin 3])]
      globalRestriction (Left ded) n DisjElim2 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 3]), ([phin 2], [phin 3])]
      globalRestriction (Left ded) n DisjElim3 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 3]), ([phin 2], [phin 3])]
      globalRestriction (Left ded) n DisjElim4 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 3]), ([phin 2], [phin 3])]
      globalRestriction (Left ded) n BicoIntro1 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 2]), ([phin 2], [phin 1])]
      globalRestriction (Left ded) n BicoIntro2 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 2]), ([phin 2], [phin 1])]
      globalRestriction (Left ded) n BicoIntro3 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 2]), ([phin 2], [phin 1])]
      globalRestriction (Left ded) n BicoIntro4 = Just $ 
          fitchAssumptionCheck n ded [([phin 1], [phin 2]), ([phin 2], [phin 1])]
      globalRestriction _ _ _ = Nothing
  
      restriction (Pr prems) = Just (premConstraint prems)
      restriction _ = Nothing
  
  parseBelotSD :: RuntimeDeductionConfig PurePropLexicon (Form Bool) -> Parsec String u [BelotSD]
  parseBelotSD rtc = do let mainInferences = choice (map (try . string) [ "&I","/\\I", "∧I","&E","/\\E","∧E","CI","->I","→I", ">I", "⊃I","→E", "⊃E","CE","->E"
                                                        , "→E" , ">E" ,"~I","-I", "¬I","~E","-E","¬E" ,"vI","\\/I","∨I", "vE","\\/E", "∨E","BI","<->I", "<>I", "↔I"
                                                        , "≡I" , "BE", "<->E", "<>E", "↔E", "≡E"])
                        r <- (char '(' *> mainInferences <* char ')') 
                              <|> try ((++) <$> string "A/" <*> many (noneOf ")")) 
                              <|> choice (map (try . string) ["R", "A","PR"])
                        return $ case r of
                          r | r `elem` ["A/>I", "A/->I"] -> [AS "/⊃I"]
                            | r `elem` ["A/=I"] -> [AS "/≡I"]
                            | r `elem` ["A","PR"] -> [Pr (problemPremises rtc)]
                            | r `elem` ["&I","/\\I","∧I"] -> [ConjIntro]
                            | r `elem` ["&E","/\\E","∧E"] -> [ConjElim1, ConjElim2]
                            | r `elem` ["CI","->I","→I",">I", "⊃I"] -> [CondIntro1,CondIntro2]
                            | r `elem` ["CE","->E","→E",">E", "⊃E"] -> [CondElim]
                            | r `elem` ["~I","¬I","-I"]  -> [NegeIntro1, NegeIntro2, NegeIntro3, NegeIntro4]
                            | r `elem` ["~E","¬E","-E"]  -> [NegeElim1, NegeElim2, NegeElim3, NegeElim4]
                            | r `elem` ["vI","\\/I","∨I"] -> [DisjIntro1, DisjIntro2]
                            | r `elem` ["vE","\\/E","∨E"] -> [DisjElim1, DisjElim2,DisjElim3, DisjElim4]
                            | r `elem` ["BI","<->I", "<>I" ,"↔I","≡I"] -> [BicoIntro1, BicoIntro2, BicoIntro3, BicoIntro4]
                            | r `elem` ["BE","<->E", "<>E", "↔E","≡E"] -> [BicoElim1, BicoElim2]
                          'A':'/':rest -> [AS (" / " ++ rest)]
                          "R" -> [Reiterate]
  
  parseBelotSDProof :: RuntimeDeductionConfig PurePropLexicon (Form Bool) -> String -> [DeductionLine BelotSD PurePropLexicon (Form Bool)]
  parseBelotSDProof ders = toDeductionFitch (parseBelotSD ders) (purePropFormulaParser belotOpts)
  
  data BelotSDPlus = SD BelotSD | MT | HS 
                       | DS1  | DS2 
                       | Com1 | Com2 | Com3 | Com4
                       | Assoc1 | Assoc2 | Assoc3 | Assoc4
                       | Impl1 | Impl2
                       | DN1  | DN2
                       | DeM1 | DeM2 | DeM3 | DeM4
                       | Idem1 | Idem2 | Idem3 | Idem4
                       | Trans1 | Trans2
                       | Exp1 | Exp2
                       | Dist1 | Dist2 | Dist3 | Dist4
                       | Equiv1 | Equiv2 | Equiv3 | Equiv4
      deriving Eq
  
  instance Show BelotSDPlus where
          show (SD x) = show x
          show MT = "MT"
          show HS = "HS"
          show DS1 = "DS"
          show DS2 = "DS"
          show Com1 = "Com"
          show Com2 = "Com"
          show Assoc1 = "Assoc"
          show Assoc2 = "Assoc"
          show Assoc3 = "Assoc"
          show Assoc4 = "Assoc"
          show Impl1 = "Impl"
          show Impl2 = "Impl"
          show DN1 = "DN"
          show DN2 = "DN"
          show DeM1 = "DeM"
          show DeM2 = "DeM"
          show DeM3 = "DeM"
          show DeM4 = "DeM"
          show Idem1 = "Idem"
          show Idem2 = "Idem"
          show Idem3 = "Idem"
          show Idem4 = "Idem"
          show Trans1 = "Trans"
          show Trans2 = "Trans"
          show Exp1 = "Exp"
          show Exp2 = "Exp"
          show Dist1 = "Dist"
          show Dist2 = "Dist"
          show Dist3 = "Dist"
          show Dist4 = "Dist"
          show Equiv1 = "Equiv"
          show Equiv2 = "Equiv"
          show Equiv3 = "Equiv"
          show Equiv4 = "Equiv"
  
  instance Inference BelotSDPlus PurePropLexicon (Form Bool) where
      ruleOf (SD r) = ruleOf r
      ruleOf MT = modusTollens
      ruleOf HS = hypotheticalSyllogism
      ruleOf DS1 = modusTollendoPonensVariations !! 0
      ruleOf DS2 = modusTollendoPonensVariations !! 1
      ruleOf Com1 = andCommutativity !! 0
      ruleOf Com2 = orCommutativity !! 0
      ruleOf Assoc1 = andAssociativity !! 0
      ruleOf Assoc2 = andAssociativity !! 1 
      ruleOf Assoc3 = orAssociativity !! 0  
      ruleOf Assoc4 = orAssociativity !! 1  
      ruleOf Impl1 = materialConditional !! 0
      ruleOf Impl2 = materialConditional !! 1
      ruleOf DN1 = doubleNegation !! 0
      ruleOf DN2 = doubleNegation !! 1
      ruleOf DeM1 = deMorgansLaws !! 0 
      ruleOf DeM2 = deMorgansLaws !! 1
      ruleOf DeM3 = deMorgansLaws !! 2
      ruleOf DeM4 = deMorgansLaws !! 3
      ruleOf Idem1 = andIdempotence !! 0
      ruleOf Idem2 = andIdempotence !! 1
      ruleOf Idem3 = orIdempotence !! 0
      ruleOf Idem4 = orIdempotence !! 1
      ruleOf Trans1 = contraposition !! 0
      ruleOf Trans2 = contraposition !! 1
      ruleOf Exp1 = exportation !! 0
      ruleOf Exp2 = exportation !! 1
      ruleOf Dist1 = distribution !! 0
      ruleOf Dist2 = distribution !! 1
      ruleOf Dist3 = distribution !! 4
      ruleOf Dist4 = distribution !! 5
      ruleOf Equiv1 = biconditionalExchange !! 0
      ruleOf Equiv2 = biconditionalExchange !! 1
      ruleOf Equiv3 = biconditionalCases !! 0
      ruleOf Equiv4 = biconditionalCases !! 1
  
      indirectInference (SD x) = indirectInference x
      indirectInference _ = Nothing
  
      isAssumption (SD x) = isAssumption x
      isAssumption _ = False
  
      isPremise (SD x) = isPremise x
      isPremise _ = False
  
      restriction (SD x ) = restriction x
      restriction _ = Nothing
  
  parseBelotSDPlus :: RuntimeDeductionConfig PurePropLexicon (Form Bool) -> Parsec String u [BelotSDPlus]
  parseBelotSDPlus rtc = try (map SD <$> parseBelotSD rtc) <|> parsePlus
      where parsePlus = do _ <- char '('
                           r <- choice (map (try . string) ["MT","HS","DS","Com","Assoc","Impl", "DN", "DeM", "Idem", "Trans", "Exp", "Dist", "Equiv"])
                           _ <- char ')'
                           return $ case r of
                                      r | r == "MT" -> [MT]
                                        | r == "HS" -> [HS]
                                        | r == "DS" -> [DS1,DS2]
                                        | r == "Com" -> [Com1,Com2]
                                        | r == "Assoc" -> [Assoc1,Assoc2,Assoc3,Assoc4]
                                        | r == "Impl" -> [Impl1,Impl2]
                                        | r == "DN" -> [DN1, DN2]
                                        | r == "DeM" -> [DeM1,DeM2, DeM3, DeM4]
                                        | r == "Idem" -> [Idem1, Idem2, Idem3, Idem4]
                                        | r == "Trans" -> [Trans1, Trans2]
                                        | r == "Exp" -> [Exp1, Exp2]
                                        | r == "Dist" -> [Dist1, Dist2, Dist3, Dist4]
                                        | r == "Equiv" -> [Equiv1, Equiv2, Equiv3, Equiv4]
  
  parseBelotSDPlusProof :: RuntimeDeductionConfig PurePropLexicon (Form Bool) -> String -> [DeductionLine BelotSDPlus PurePropLexicon (Form Bool)]
  parseBelotSDPlusProof ders = toDeductionFitchAlt (parseBelotSDPlus ders) (purePropFormulaParser belotOpts)
  
  belotNotation :: String -> String 
  belotNotation x = case runParser altParser 0 "" x of
                          Left e -> show e
                          Right s -> s
      where altParser = do s <- handleCon <|> try handleAtom <|> fallback
                           rest <- (eof >> return "") <|> altParser
                           return $ s ++ rest
            handleCon = (char '∧' >> return "&") 
                        <|> (char '¬' >> return "~") 
                        <|> (char '→' >> return "⊃")
                        <|> (char '↔' >> return "≡")
                        <|> (char '⊤' >> return " ")
            handleAtom = do c <- oneOf "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
                            return $ [toLower c]
            fallback = do c <- anyChar 
                          return [c]
  
  belotSDCalc = mkNDCalc
      { ndRenderer = FitchStyle StandardFitch
      , ndProcessLine = hoProcessLineFitch
      , ndProcessLineMemo = Just hoProcessLineFitchMemo
      , ndParseProof = parseBelotSDProof
      , ndParseSeq = parseSeqOver (purePropFormulaParser belotOpts)
      , ndParseForm = purePropFormulaParser belotOpts
      , ndNotation = belotNotation
      }
  
  belotSDPlusCalc = mkNDCalc 
      { ndRenderer = FitchStyle StandardFitch
      , ndProcessLine = hoProcessLineFitch
      , ndProcessLineMemo = Just hoProcessLineFitchMemo
      , ndParseProof = parseBelotSDPlusProof 
      , ndParseSeq = parseSeqOver (purePropFormulaParser belotOpts)
      , ndParseForm = purePropFormulaParser belotOpts
      , ndNotation = belotNotation
      }
  