{- | 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.
 -}
{-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses,
             FunctionalDependencies, FlexibleInstances,
             FlexibleContexts, UndecidableInstances #-}
module GMP.Logics.Generic where

import Data.List
import Data.Ratio
import Data.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 = evalState get []
  fPutCache :: a b -> [Formula (a b)] -> (GMPState [Formula (a b)]) ()
  fPutCache sig = put

newtype GMPState s a = GMPState { runState :: s -> (a, s) }

evalState :: GMPState b a -> b -> a
evalState m s = fst (runState m 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 $ const ((), 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 = genfNext
  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 = fMatch

-- 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
  fFeatureFromSignature = error $ "fFeatureFromSignature not implemented for" ++
                                  " instance Feature a ()"
  fFeatureFromFormula = error $ "fFeatureFromFormula not implemented for" ++
                                " instance Feature a ()"
  fStripFeature = error $ "fStripFeature not implemented for" ++
                          " instance Feature a ()"
  fNext = error "fNext not implemented for instance Feature a ()"
  fParser = error "fParser not implemented for instance Feature a ()"
  fSeparator = error "fSeparator not implemented for instance Feature a ()"

-- 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
  fFeatureFromSignature = error $ "fFeatureFromSignature not implemented for" ++
                                  " instance Feature a (b ())"
  fFeatureFromFormula = error $ "fFeatureFromFormula not implemented for" ++
                                " instance Feature a (b ())"
  fStripFeature = error $ "fStripFeature not implemented for" ++
                          " instance Feature a (b ())"
  fNext = error "fNext not implemented for instance Feature a (b ())"
  fParser = error "fParser not implemented for instance Feature a (b ())"
  fSeparator = error "fSeparator not implemented for instance Feature a (b ())"

-- 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 = filter (\ phi -> case phi of Mod _ -> True; _ -> False)

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

{- 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 = map (map emptifys)

{- ------------------------------------------------------------------------------
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 = Neg

{- ------------------------------------------------------------------------------
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 -}
