{-#LANGUAGE  FlexibleContexts,  FlexibleInstances, MultiParamTypeClasses #-}
module Carnap.Languages.PureFirstOrder.Logic.Tomassi where

import Data.Map as M (lookup, Map)
import Text.Parsec
import Control.Lens (view)
import Carnap.Core.Data.Types 
import Carnap.Core.Data.Classes
import Carnap.Core.Unification.Unification (applySub,occurs)
import Carnap.Languages.PureFirstOrder.Syntax
import Carnap.Languages.PureFirstOrder.Parser
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 (dischargeConstraint, premConstraint,axiom)
import Carnap.Languages.Util.LanguageClasses (lall)
import Carnap.Languages.PureFirstOrder.Logic.Rules
import Carnap.Languages.PurePropositional.Logic.Tomassi hiding (Pr)

{-| A system for first-order logic resembling the proof system QL
from Tomassi's Logic book
-}

data TomassiQL = PL TomassiPL
               | UI    | UE
               | EI    | EE
               | EqI   | EqE 
               | Pr (Maybe [(ClassicalSequentOver PureLexiconFOL (Sequent (Form Bool)))])
               deriving Eq

instance Show TomassiQL where
        show (PL x) = show x
        show EI = "EI"
        show EE = "EE"
        show UI = "UI"
        show UE = "UE"
        show EqI = "=I"
        show EqE = "=E"

instance Inference TomassiQL PureLexiconFOL (Form Bool) where

        ruleOf (Pr _) = axiom
        ruleOf UI  = universalGeneralization
        ruleOf UE  = universalInstantiation
        ruleOf EI  = existentialGeneralization
        ruleOf EE  = existentialDerivation !! 0
        ruleOf EqI = eqReflexivity
        ruleOf EqE = leibnizLawVariations !! 0 --do we also want reverse?
        ruleOf r = premisesOf r ∴ conclusionOf r

        premisesOf (PL x) = map liftSequent (premisesOf x)
        premisesOf x = upperSequents (ruleOf x)

        conclusionOf (PL x) = liftSequent (conclusionOf x)
        conclusionOf x = lowerSequent (ruleOf x)

        restriction UI = Just (eigenConstraint tau (SS (lall "v" $ phi' 1)) (fogamma 1))
        restriction (Pr prems) = Just (premConstraint prems)
        restriction _ = Nothing

        globalRestriction (Left ded) n EE = Just (onlyNewConstraint n ded tau' (phi' 1 tau') 
                                                 `andFurtherRestriction`
                                                  dischargeConstraint n ded (view lhs $ conclusionOf EE))
            where tau' :: FixLang PureLexiconFOL (Term Int)
                  tau' = tau
                                                 --make sure that any occurance of tau is ≥ the last occurance of phi 1 tau
        globalRestriction (Left ded) n (PL CP) = Just (dischargeConstraint n ded (view lhs $ conclusionOf (PL CP)))
        globalRestriction (Left ded) n (PL RAA1) = Just (dischargeConstraint n ded (view lhs $ conclusionOf (PL RAA1)))
        globalRestriction (Left ded) n (PL RAA2) = Just (dischargeConstraint n ded (view lhs $ conclusionOf (PL RAA2)))
        globalRestriction (Left ded) n (PL ORE) = Just (dischargeConstraint n ded (view lhs $ conclusionOf (PL ORE)))
        globalRestriction _ _ _ = Nothing

        isAssumption (Pr _) = True
        isAssumption (PL x) = isAssumption x
        isAssumption _ = False

onlyNewConstraint m ded term form sub = 
        case termOccurs of
            [] -> Just "Somehow, the term cited isn't in the proof"
            (n,_):_ | not ((n,n) `elem` theDeps) -> Just $ "The first occurance of " ++ show theTerm ++ ", on line " 
                                                     ++ show n ++ " isn't the cited assumption."
            (n,l):_ | assertionOf l /= (Just theForm) -> Just $ "The first occurance of " ++ show theTerm ++ ", on line " 
                                                            ++ show n ++ " isn't the cited assumption."
            (n,l):_ | checkRuleIn l  -> Just $ "The first occurance of " ++ show theTerm ++ ", on line "
                                             ++ show n ++ " isn't the cited assumption."
            _  -> Nothing
    where theDeps = maybe [] id (dependencies $ ded !! (m - 1))
          theTerm = applySub sub (liftToSequent term)
          theForm = applySub sub (liftToSequent form)
          termOccurs = filter (checkTermIn . snd) (zip [1 ..] ded)
          assertionOf l = liftToSequent <$> assertion l
          checkTermIn l = maybe False (\phi -> theTerm `occurs` liftToSequent phi) $ assertion l
          checkRuleIn l = maybe True (not . isAssumption . head) $ ruleOfLine l
    

parseTomassiQL rtc n annote = try parseProp <|> parseQuant
    where parseProp = map PL <$> parseTomassiPL (RuntimeNaturalDeductionConfig mempty mempty) n annote
          parseQuant = do r <- choice (map (try . string) [ "UI", "UE", "EE", "EI", "=I", "=E" ])
                          return $ case r of
                                      "UI" -> [UI]
                                      "UE" -> [UE]
                                      "EE" -> [EE]
                                      "EI" -> [EI]
                                      "=I" -> [EqI]
                                      "=E" -> [EqE]

parseTomassiQLProof :: RuntimeNaturalDeductionConfig PureLexiconFOL (Form Bool) 
                     -> String -> [DeductionLine TomassiQL PureLexiconFOL (Form Bool)]
parseTomassiQLProof rtc = toDeductionLemmonTomassi (parseTomassiQL rtc) tomassiQLFormulaParser

tomassiQLCalc = mkNDCalc
    { ndRenderer = LemmonStyle TomassiStyle
    , ndParseProof = parseTomassiQLProof
    , ndProcessLine = hoProcessLineLemmon
    , ndProcessLineMemo = Just hoProcessLineLemmonMemo
    , ndParseForm = tomassiQLFormulaParser
    , ndParseSeq = parseSeqOver tomassiQLFormulaParser
    , ndNotation = tomassiPLNotation
    }
