{- | Module     : $Header$
 -  Description : Implementation of generic data structures and functions
 -  Copyright   : (c) Daniel Hausmann & Georgel Calin & Lutz Schroeder, DFKI Lab Bremen,
 -                Rob Myers & Dirk Pattinson, Department of Computing, ICL 
 -  License     : GPLv2 or higher, see LICENSE.txt
 -  Maintainer  : hausmann@dfki.de
 -  Stability   : provisional
 -  Portability : portable
 -
 - Provides the implementation of the generic algorithm for checking 
 - satisfiability/provability of several types of modal logics.
 -}
module GMP.Logics.Generic where

import List
import Ratio
import Maybe
import Text.ParserCombinators.Parsec
import Debug.Trace
import Control.Monad.ST

--------------------------------------------------------------------------------
-- basic data types
--------------------------------------------------------------------------------

-- Formulae
data Formula a = F | T | And (Formula a) (Formula a) | Or (Formula a) (Formula a) | 
     	      Neg (Formula a) | Atom Int | Mod a deriving (Eq, Ord, Show)

--------------------------------------------------------------------------------
-- List of (possibly heterogenous) premises:
-- a list of premises may contain sequents with different types...
--------------------------------------------------------------------------------

-- A sequent is a list of formulae
data Sequent = forall a b c. (Feature a (b c), Eq (a (b c))) => Sequent [Formula (a (b c))]

-- A list of premises is a list of a list of sequent
type Premises = [[[Sequent]]]

data ModalOperator = Sqr | Ang | None
    deriving Eq

--------------------------------------------------------------------------------
-- feature type-class
-- the feature type-class carries the matching function...
--------------------------------------------------------------------------------

class Feature a b where
-- basic methods
  fMatch :: [Bool] -> [Formula (a b)] -> Premises 
  fPretty :: (a b) -> String
  fFeatureFromSignature :: (a b) -> [Formula e] -> a e
  fFeatureFromFormula :: Formula (a b) -> [Formula e] -> a e
  fStripFeature :: (a b) -> [Formula b]

  fDisj2Conj :: Formula (a b) -> Formula (a b)
  fNegNorm :: Formula (a b) -> Formula (a b)
  fStripFormula :: Formula (a b) -> (a b)
  fStripFormula phi = case phi of
                        T -> (fFeatureFromFormula phi) []
                        F -> (fFeatureFromFormula phi) []
                        (And psi xi) -> (fStripFormula psi)
                        (Or psi xi) -> (fStripFormula psi)
                        (Neg psi) -> (fStripFormula psi)
                        (Mod sig) -> sig
-- parsing methods
  fNext :: (a b) -> b
  fParser :: (a b) -> Parser ([Formula e] -> a e)
  fSeparator :: (a b) -> String
-- preproving methods
  fDepth :: (a b) -> Int
  fPreProve :: [Formula (a b)] -> Int -> [[Formula (a b)]] -> [[Formula (a b)]]
  fPreProve seq i ecs = []
  fMatchOptimised :: [Bool] -> [Formula (a b)] -> [[Formula (a b)]] -> Premises 
  fMatchOptimised flags seq ecs = fMatch flags seq

-- state monad stuff
  fGetCache :: (a b) -> [Formula (a b)]
  fGetCache sig = fst $ (runState get [])
  fPutCache :: (a b) -> [Formula (a b)] -> (GMPState [Formula (a b)]) ()
  fPutCache sig s = put s

newtype GMPState s a = GMPState { runState :: (s -> (a,s)) } 
 
instance Monad (GMPState s) where 
    return a           = GMPState $ \s -> (a,s)
    (GMPState x) >>= f = GMPState $ \s -> let (v,s') = x s in runState (f v) s' 

class MonadState m s | m -> s where 
    get :: m s
    put :: s -> m ()

instance MonadState (GMPState s) s where 
    get   = GMPState $ \s -> (s,s) 
    put s = GMPState $ \_ -> ((),s) 

--------------------------------------------------------------------------------
-- nonempty-features are a subclass of features
-- they have more default-functions than normal features though
--------------------------------------------------------------------------------

class (SigFeature b c d, Eq (c d)) => NonEmptyFeature a b c d where
  nefMatch :: [Bool] -> [Formula (a (b (c d)))] -> Premises 
  nefPretty :: (a (b (c d))) -> String
  nefFeatureFromSignature :: (a (b (c d))) -> [Formula e] -> a e
  nefFeatureFromFormula :: Formula (a (b (c d))) -> [Formula e] -> a e
  nefStripFeature :: (a (b (c d))) -> [Formula (b (c d))]
  nefDisj2Conj :: Formula (a (b (c d))) -> Formula (a (b (c d)))
  nefDisj2Conj = genfDisj2Conj
  nefNegNorm :: Formula (a (b (c d))) -> Formula (a (b (c d)))
  nefNegNorm = genfNegNorm
  nefNext :: (a (b (c d))) -> (b (c d))
  nefNext sig = genfNext sig
  nefDepth :: (a (b (c d))) -> Int
  nefDepth = genfDepth 
  nefParser :: (a (b (c d))) -> Parser ([Formula e] -> a e)
  nefParser sig = return (nefFeatureFromSignature sig)
  nefSeparator :: (a (b (c d))) -> String
  nefSeparator sig = ","

instance (NonEmptyFeature a b c d, Eq (c d)) => Feature a (b (c d)) where
  fMatch = nefMatch
  fDisj2Conj = nefDisj2Conj
  fNegNorm = nefNegNorm
  fDepth = nefDepth
  fNext = nefNext
  fPretty = nefPretty
  fFeatureFromSignature = nefFeatureFromSignature
  fFeatureFromFormula = nefFeatureFromFormula
  fStripFeature = nefStripFeature
  fParser = nefParser
  fSeparator = nefSeparator

--------------------------------------------------------------------------------
-- sigfeature type-class
-- the sigfeature type-class ensures correct order of features...
--------------------------------------------------------------------------------

class (Feature a (b c), Feature b c, Eq c) => SigFeature a b c where
-- basic methods
  sMatch :: (Eq c) => [Bool] -> [Formula (a (b c))] -> Premises 
  sDisj2Conj :: Formula (a (b c)) -> Formula (a (b c))
  sNegNorm :: Formula (a (b c)) -> Formula (a (b c))
  sPretty :: (a (b c)) -> String
-- parsing methods
  sParser :: (a (b c)) -> Parser ([Formula e] -> a e)
  sParser = fParser
  sNextSig :: (a (b c)) -> (b c)
  sNextSig = fNext
  pGoOn :: (a (b c)) -> ModalOperator ->  Parser (Formula (b c))
-- preproving methods
  sDepth :: Formula (a (b c)) -> Int

--------------------------------------------------------------------------------
-- nonempty-sigfeatures are a subclass of sigfeatures
-- they have more default-functions than normal sigfeatures though
--------------------------------------------------------------------------------

class (SigFeature b c d, Eq d, Feature a (b (c d)), Feature b (c d), Eq (c d)) => NonEmptySigFeature a b c d where
  neMatch :: (Eq (c d)) => [Bool] -> [Formula (a (b (c d)))] -> Premises 
  neMatch = fMatch
  neGoOn :: (a (b (c d))) -> ModalOperator ->  Parser (Formula (b (c d)))
  neDisj2Conj :: Formula (a (b (c d))) -> Formula (a (b (c d)))
  neDisj2Conj = fDisj2Conj
  neNegNorm :: Formula (a (b (c d))) -> Formula (a (b (c d)))
  neNegNorm = fNegNorm
  neDepth :: Formula (a (b (c d))) -> Int
  neDepth = genSDepth
  nePretty :: (a (b (c d))) -> String
  nePretty sig = "{NonEmpty} " ++ fPretty sig

instance (NonEmptySigFeature a b c d, Eq (c d)) => SigFeature a b (c d) where
  sMatch = neMatch
  pGoOn = neGoOn
  sDisj2Conj = neDisj2Conj
  sNegNorm = neNegNorm
  sDepth = neDepth
  sPretty = nePretty


--------------------------------------------------------------------------------
-- Generic functions for Features
--------------------------------------------------------------------------------

genfDepth :: (Feature a (b (c d)), SigFeature b c d) => (a (b (c d))) -> Int
genfDepth sig = case (fStripFeature sig) of
                  [phi] -> sDepth phi

genfNext :: (Feature a (b (c d)), SigFeature b c d) => (a (b (c d))) -> (b (c d))
genfNext sig = case fStripFeature sig of 
                      []   -> fStripFormula (F)
                      phis -> fStripFormula (head phis)

genfDisj2Conj :: (Feature a (b (c d)), SigFeature b c d) => Formula (a (b (c d))) -> Formula (a (b (c d)))
genfDisj2Conj phi = Mod ((fFeatureFromFormula phi) (map disj2conj (fStripFeature (fStripFormula phi))))

genfNegNorm :: (Feature a (b (c d)), SigFeature b c d) => Formula (a (b (c d))) -> Formula (a (b (c d)))
genfNegNorm phi = Mod ((fFeatureFromFormula phi) (map negNorm (fStripFeature (fStripFormula phi))))

genfPretty :: (Feature a (b (c d)), SigFeature b c d) => a (b (c d)) -> String -> String
genfPretty d s = case fStripFeature d of 
                    []     -> s ++ " nothing contained!"
                    (e:[]) -> s ++ (pretty e)
                    e      -> s ++ show (map pretty e)

--------------------------------------------------------------------------------
-- Generic functions for SigFeatures
--------------------------------------------------------------------------------

-- generic matching for sigfeatures (uses matching function of underlaying feature)
genSMatch :: (SigFeature a b (c d), SigFeature b c d, Eq d) => [Bool] -> [Formula (a (b (c d)))] -> Premises
genSMatch flags seq = fMatch flags seq

-- the depth of modal nesting of a list of formulae
ldepth :: (SigFeature a b c) => [Formula (a (b c))] -> Int
ldepth seq = maximum (map genSDepth seq)

-- generic depth of modal nesting of a formula
genSDepth :: (SigFeature a b c) => Formula (a (b c)) -> Int
genSDepth F = 0
genSDepth T = 0
genSDepth (Atom i) = 0
genSDepth (Neg phi) = genSDepth (phi)
genSDepth (And phi psi) = max (genSDepth phi) (genSDepth psi)
genSDepth (Or phi psi) = max (genSDepth phi) (genSDepth psi)
genSDepth (Mod xs) = 1 + (fDepth xs)

-- generic function to return all top-level modal arguments of phi
--genSGetArgs :: (SigFeature a, Feature b, Eq e) => Formula (a (b (c (d e)))) -> [Formula (c (d e))]
--genSGetArgs phi = case phi of 
--                         T -> []
--                         F -> []
--                         (Atom i) -> []
--                         (Neg psi) -> sGetArgs psi
--                         (And xi yi) -> sGetArgs xi ++ sGetArgs yi
--                         (Or xi yi) -> sGetArgs xi ++ sGetArgs yi
--                         (Mod sig) -> fStripFeat (sNextSig sig)

-- generic function to return all top-level modal arguments of phi
--genHGetArgs :: (SigFeature a, Feature b, Eq e) => Formula (a (b (c (d e)))) -> [Formula (c (d e))] :*: HNil
--genHGetArgs phi = case phi of 
--                         T -> [] .*. HNil
--                         F -> [] .*. HNil
--                         (Atom i) -> [] .*. HNil
--                         (Neg psi) -> hGetArgs psi
--                         (And xi yi) -> (hHead (hGetArgs xi) ++ hHead (hGetArgs yi)) .*. HNil
--                         (Or xi yi) -> (hHead (hGetArgs xi) ++ hHead (hGetArgs yi)) .*. HNil
--                         (Mod sig) -> fStripFeat (sNextSig sig) .*. HNil

-- generic function to return the list of all arguments of modality that
-- have nesting depth at most i
--genSGetPrems :: (SigFeature a, Feature b, SigFeature c, Feature d, Eq e) =>
--                 Int -> Formula (a (b (c (d e)))) -> [Sequent]
--genSGetPrems i phi = if (sDepth phi) <= i then
--                       let args = (sGetArgs phi)
--                       in (Sequent args) : concatMap (sGetPrems i) (args)
--                     else
--                       let args = (sGetArgs phi)
--                       in concatMap (sGetPrems i) (args)

--------------------------------------------------------------------------------
-- generic functions for preproving
--------------------------------------------------------------------------------

-- given a formula, a number i(=0) and a list of classes, compute the list of
-- preproving classes for the formula.
--genSPreProve :: (SigFeature a, Feature b, SigFeature c, Feature d, Eq g) =>
--                   Formula (a (b (c (d (e (f g)))))) -> Int -> [[Sequent]] -> [[Sequent]]
--genSPreProve phi i seqs = let eq = (genClasses (merge (collapse (sGetPrems i phi)) seqs))
--                         in if (i == (sDepth phi)-1) then eq
--                                                     else eq ++ (genSPreProve phi (i+1) eq)

-- not done yet ([[1]:A, [2]:B, [3]:C, [4]:A] -> [[1,4]:A, [2]:B, [3:C]]): 
--collapse :: [Sequent] -> [Sequent]
--collapse ((Sequent phis):seqs) = (Sequent phis):seqs

-- not done yet ([[1]:ABC, [2]:CDE],[[[3]:ABC,[4]:ABC],[[5]:CDE,[6]:CDE]] -> [([1],[[3],[4]]):ABC, ([2],[[5],[6]]):CDE]):
--merge :: [Sequent] -> [[Sequent]] -> [DoubleSequent]
--merge [] [] = []

-- given a list of pairs of sequents of the same type (the pair consisting of
-- the formulas which are to be treated and a list of already known classes),
-- return the list of the list of classes for each pair.
--genClasses :: [DoubleSequent] -> [[Sequent]]
--genClasses [] = []
--genClasses (DoubleSequent (xis,eqs):seqs) = (classes (sFilter xis) eqs) : (genClasses seqs)

-- give preproving classes of a list list of formulas using the knowledge about
-- classes ppcs.
--classes :: (SigFeature a, Feature b, Eq e) => [Formula (a (b (c (d e))))] -> [[Formula (a (b (c (d e))))]] -> [Sequent]
--classes [] ppcs = []
--classes (phi:phis) ppcs = let ppc = nub (phi:(ppClass phi phis ppcs))
--                          in (Sequent ppc) : (classes ((phi:phis) \\ ppc) (ppc:ppcs))

-- given a formula phi and a list of formulae, return the list of all formulae
-- that are in the same class as phi (using the knowledge ppcs).
--ppClass :: (SigFeature a, Feature b, Eq e) => Formula (a (b (c (d e)))) -> [Formula (a (b (c (d e))))] ->
--                                        [[Formula (a (b (c (d e))))]] -> [Formula (a (b (c (d e))))]
--ppClass phi [] ppcs = []
--ppClass phi (psi:phis) ppcs = if (sCompute phi psi ppcs) then psi:(ppClass phi phis ppcs)
--                                                         else (ppClass phi phis ppcs)

-- check whether the two input formulae are equivalent. If they are already in
-- the same preproving class, it is not necessary to prove their equivalence.
--equiv :: (SigFeature a, Feature b, Eq e) => Formula (a (b (c (d e)))) -> Formula (a (b (c (d e)))) -> [[Formula (a (b (c (d e))))]] -> Bool
--equiv phi psi ppc = -- trace ("  <Trying to show equivalence:>                 " 
--                    --        ++ show (pretty phi) ++ " = " ++ show (pretty psi)) $ 
--                    (any (\eqcls -> ((phi `elem` eqcls) && (psi `elem` eqcls))) ppc) || 
--                    provable (And (Neg (And (Neg psi) phi)) (Neg (And (Neg phi) psi)))

--------------------------------------------------------------------------------
-- generic functions of (sig)features
--------------------------------------------------------------------------------

-- generic finishing feature
instance Feature a () where
  fMatch flags seq = trace "\n  <Matching not possible, no more layers>" $ [[]]
  fDisj2Conj phi = F
  fNegNorm phi = F
  fPretty e = " nothing contained!"
  fDepth phi = 0

-- generic finishing feature
instance Feature a (b ()) where
  fMatch flags seq = trace "\n  <Matching not possible, no more layers>" $ [[]]
  fDisj2Conj phi = F
  fNegNorm phi = F
  fPretty e = " nothing Contained!"
  fDepth phi = 0

-- generic finishing sigfeature
instance SigFeature a b () where
  sMatch flags seq = trace "\n  <Matching not possible, no more layers>" $ [[]]
  sDisj2Conj phi = F
  sNegNorm phi = F
  sPretty sig = "{Last SigFeature} " ++ fPretty sig
  sDepth phi = 0
  pGoOn sig flag = trace ("finishing: " ++ sPretty sig) $ return F

--------------------------------------------------------------------------------
-- preparsing functions
--------------------------------------------------------------------------------

-- | Preparsing replaces all disjunctions by conjunctions and normalizes negations -
-- | This is the form that the sequent calculus expects
preparse :: (SigFeature a b (c d), SigFeature b c d) => Formula (a (b (c d))) -> Formula (a (b (c d)))
preparse f = negNorm $ disj2conj f

disj2conj :: (SigFeature a b c) => Formula (a (b c)) -> Formula (a (b c))
disj2conj w = case w of
                      (And x y)   -> let a = disj2conj x
                                         b = disj2conj y
                                     in And a b
                      (Or x y)    -> let a = disj2conj x
                                         b = disj2conj y
                                     in Neg (And (Neg a) (Neg b))
                      (Neg x)     -> let a = disj2conj x
                                     in Neg a
                      (Mod phi)   -> sDisj2Conj (Mod phi)
                      x           -> x

negNorm :: (SigFeature a b c) => Formula (a (b c)) -> Formula (a (b c))
negNorm w = case w of
                    (Neg (Neg x)) -> negNorm x
                    (Neg x)       -> neg $ negNorm x
                    (Mod phi)     -> sNegNorm (Mod phi)
                    (And x y)     -> let a = negNorm x
                                         b = negNorm y
                                     in And a b
                    x             -> x -- there is no need for discussing "Or"


--------------------------------------------------------------------------------
-- some auxiliary functions which are used by several features
--------------------------------------------------------------------------------

-- generate the powerlist of a list
powerList :: [a] -> [[a]]
powerList [] = [[]]
powerList (x:xs) = powerList xs ++ (map (x:) (powerList xs))

-- Remove all formulas from a container that are not positive modal literals
keep_poslits :: [Formula (a b)] -> [Formula (a b)]
keep_poslits seq = filter (\phi -> case phi of (Mod _)->True;_->False) seq

-- Remove all formulas from a container that are not negative modal literals
keep_neglits :: [Formula (a b)] -> [Formula (a b)]
keep_neglits seq = filter (\phi -> case phi of (Neg(Mod _))->True;_->False) seq

-- Get list [0..(length xs)-1]
-- Needed for 'normal-forms' of G, P
to_inds :: [a] -> [Int]
to_inds [] = []
to_inds xs = [0..(length xs)-1]

-- Get the elements of a list that are indexed by the first parameter list
-- Needed for 'normal-forms' of G, P
img :: Eq (a (b c)) => [Int] -> [Formula (a (b c))] -> [Formula (a (b c))]
img inds xs = map (xs!!) inds 

imgInt :: [Int] -> [Int] -> [Int]
imgInt inds xs = map (xs!!) inds 

andify :: Eq (a (b c)) => [Formula (a (b c))] -> Formula (a (b c))
andify [] = F
andify (phi:[]) = phi
andify (phi:phis) = And phi (andify phis)

--------------------------------------------------------------------------------
-- remove empty sequents from a list of sequents
--------------------------------------------------------------------------------

--emptifys :: [Sequent] -> [Sequent]
--emptifys seqs = case seqs of
--                  []               -> []
--                  ((Sequent x):xs) -> case x of
--                                         []   -> emptifys xs
--                                         phis -> (Sequent x) : emptifys xs

--emptifyss :: [[Sequent]] -> [[Sequent]]
--emptifyss seqs = case seqs of
--                  []     -> []
--                  (x:xs) -> emptifys x : emptifyss xs

--emptify :: Premises -> Premises
--emptify prems = trace ("emptying "++ show (map (map (map pretty_seq)) prems))$
--                  case prems of
--                  []     -> []
--                  (x:xs) -> emptifyss x : emptify xs

emptifys :: [Sequent] -> [Sequent]
emptifys []       = []
emptifys (s:seqs) = case s of
                       Sequent []     -> emptifys seqs
                       Sequent (x:xs) -> s : emptifys seqs

emptify :: Premises -> Premises
emptify prems = map (map emptifys) prems

--------------------------------------------------------------------------------
-- basic sequent functions
--------------------------------------------------------------------------------

-- expand applies all sequent rules that do not branch
expand :: [Formula (a b)] -> [Formula (a b)]
expand [] = []
expand ((Neg (Neg phi)) : as) = expand (phi:as)
expand ((Neg (And phi psi)):as) = expand ((Neg phi):(Neg psi):as)
expand (a:as) = a:(expand as)

neg :: (SigFeature a b c) => Formula (a (b c)) -> Formula (a (b c))
neg psi = (Neg psi)

--------------------------------------------------------------------------------
-- pretty printing functions
--------------------------------------------------------------------------------

-- pretty print formula
pretty :: (Feature a (b c)) => Formula (a (b c)) -> String
pretty F = "F"; pretty T = "T";
pretty (Atom k) = "Atom" ++ (show k);
pretty (Or (Neg x) y) =  "(" ++ (pretty x) ++ ") --> (" ++ (pretty y) ++ ")"
pretty (Neg x) = "!" ++  (pretty x)
pretty (Or x y) = "(" ++ (pretty x) ++ ") OR (" ++ (pretty y) ++ ")"
pretty (And x y) = "(" ++ (pretty x) ++ ") AND (" ++ (pretty y) ++ ")"
pretty (Mod a) = (fPretty a)

-- pretty print sequent
pretty_seq :: Sequent -> String
pretty_seq (Sequent seq) = pretty_list seq

-- pretty print list of formulae
pretty_list :: (Feature a (b c)) => [Formula (a (b c))] -> String
pretty_list [] = "[]"
pretty_list (x:xs) = case xs of
                      [] -> pretty x
                      (y:ys) -> pretty x ++ " , " ++ pretty_list xs 

-- pretty print list of sequents
pretty_slist :: [Sequent] -> String
pretty_slist [] = ""
pretty_slist (x:xs) = case xs of
                      [] -> pretty_seq x
                      (y:ys) -> pretty_seq x ++ " , " ++ pretty_slist xs

-- pretty print a list of lists of sequents
prettyll :: [[Sequent]] -> String
prettyll [] = ""
prettyll (x:xs) = case x of
                     []     -> "[[]]"
                     (y:ys) -> case ys of
                                 [] -> "[" ++ pretty_seq y ++ "]" ++ prettyll xs
                                 (z:zs) -> "[" ++ pretty_seq y ++ "," ++ pretty_slist ys ++ "]" ++ prettyll xs

-- pretty print a list of lists of lists of sequents
prettylll :: [[[Sequent]]] -> String
prettylll [] = ""
prettylll (x:xs) = case x of
                      []     -> "[[]]"
                      (y:ys) -> case ys of
                                  [] -> "[" ++ pretty_slist y ++ "]" ++ prettylll xs
                                  (z:zs) -> "[" ++ pretty_slist y ++ "," ++ prettyll ys ++ "]" ++ prettylll xs

--------------------------------------------------------------------------------
-- 'polymorphic equality' type-class:
-- every feature is preserving the comparability of sequents...
--------------------------------------------------------------------------------

-- not needed?

--instance Eq a => Eq (b a)
--class PolyEq f
--  where g :: a -> f a
--instance Feature a b => PolyEq a
--instance (Eq a, PolyEq f) => Eq (f a)

--class Eq2 f
--class PolyEq2 f
--  where dzdu :: a -> f a
--instance SigFeature a b c => PolyEq2 a
--instance (Eq2 a, PolyEq2 f) => Eq2 (f a)
--instance Eq2 a => Eq a

