content: {- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/CKCM.hs
   -  Description : Implementation of logic instance of CK+CM
   -  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 matching functions of CK+CM.
   -}
  {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
  module GMP.Logics.CKCM where
  import Data.List hiding (isInfixOf)
  import Data.Ratio
  import Data.Maybe
  
  import Debug.Trace
  import Text.ParserCombinators.Parsec
  
  import GMP.Logics.Generic
  import GMP.Parser
  
  {- ------------------------------------------------------------------------------
  instance of feature for the feature of CK+CM
  ------------------------------------------------------------------------------ -}
  
  data CKCM a = CKCM [Formula a] deriving (Eq, Show)
  
  instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature CKCM b c d where
      nefMatch flags seq =
        let g0 = gZeros seq
            compGraphs = map constructCompGraphs g0
        in if flags !! 1 then
            [ trace ("Matching <g0>: " ++ pretty_list gZ ++ " Using <graph>: " ++
                     show cG) $
                      let sss = ckcmPremise gZ cG
                      in trace ("Premise: " ++ show (map (map pretty_seq) sss) )
                                sss | (gZ, cGs) <- compGraphs, cG <- cGs ]
           else [ ckcmPremise gZ cG | (gZ, cGs) <- compGraphs, cG <- cGs ]
      nefPretty d = genfPretty d "[CK+CM]"
      nefFeatureFromSignature sig = CKCM
      nefFeatureFromFormula phi = CKCM
      nefStripFeature (CKCM phis) = phis
      nefSeparator sig = "=>"
  
  gZeros :: [Formula (CKCM (b c))] -> [[Formula (CKCM (b c))]]
  gZeros seq = let poslits = [ Mod (CKCM phis) | Mod (CKCM phis) <- seq]
                   neglits = [ Neg (Mod (CKCM phis)) |
                               Neg (Mod (CKCM phis)) <- seq]
               in [ neglits ++ [poslit] | poslit <- poslits ]
  
  constructCompGraphs :: [Formula (a (b c))] -> ([Formula (a (b c))], [([[Int]],
                          [([Int], [Int])])])
  constructCompGraphs gZ = (gZ, allCompGraphs (length gZ - 2 ))
  
  allCompGraphs :: Int -> [([[Int]], [([Int], [Int])])]
  allCompGraphs i = removeDuplicates (iteratedLayerAdding [([[0 .. i]], [])])
  
  removeDuplicates :: [([[Int]], [([Int], [Int])])] -> [([[Int]], [([Int], [Int])])]
  removeDuplicates [] = []
  removeDuplicates (g : gs) = if appearsIn g gs then removeDuplicates gs
                                                else g : removeDuplicates gs
  
  appearsIn :: ([[Int]], [([Int], [Int])]) -> [([[Int]], [([Int], [Int])])] -> Bool
  appearsIn graph = foldr (\ g -> (||) (graph == g)) False
  
  iteratedLayerAdding :: [([[Int]], [([Int], [Int])])] -> [([[Int]], [([Int], [Int])])]
  iteratedLayerAdding graphs = -- trace ("graphs: " ++ show graphs) $
    let extendedGraphs = nub (sort (concatMap addLayer graphs))
    in if nub (sort graphs) == extendedGraphs
       then graphs
       else iteratedLayerAdding (concatMap addLayer graphs)
  
  addLayer :: ([[Int]], [([Int], [Int])]) -> [([[Int]], [([Int], [Int])])]
  addLayer graph@(worlds, rel) =
    let exps = initialStates graph
    in case exps of
        [] -> -- trace ("initial states: " ++ show (exps)) $
              [graph]
        _ -> -- trace ("initial states: " ++ show (exps)) $
              graph : [ -- trace ("expansion: " ++ show (nub stateSetExpansion)) $
                       expandAll graph (nub stateSetExpansion) |
                       stateSetExpansion <- stateSetExpansions exps ]
  
  stateSetExpansions :: [[Int]] -> [[([Int], [[Int]])]]
  stateSetExpansions [] = [[]]
  stateSetExpansions (w : ws) = [ concatMap (decomp :) (stateSetExpansions ws) |
                                  decomp <- decompositions w ]
  
  expandAll :: ([[Int]], [([Int], [Int])]) -> [([Int], [[Int]])] ->
               ([[Int]], [([Int], [Int])])
  expandAll graph@(worlds, rel) [] = graph
  expandAll graph@(worlds, rel) ((state, expansion) : expansions) =
    expandAll (nub (sort (worlds ++ expansion)),
      nub (sort (rel ++ newPairs state expansion))) expansions
  
  newPairs :: [Int] -> [[Int]] -> [([Int], [Int])]
  newPairs state expansion = [ (newState, state) | newState <- expansion]
  
  decompositions :: [Int] -> [([Int], [[Int]])]
  decompositions world = map (\ decomp -> (world, decomp))
   (nub (concat [ sort (decomposition (first : (world \\ [first]))) |
                  first <- world ]))
  
  decomposition :: [Int] -> [[[Int]]]
  decomposition [] = []
  decomposition [x] = []
  decomposition is@(x : xs) = -- trace ("decomposing " ++ show is) $
    [ -- trace ("decomposition: " ++ show (nub decomp\\[is])) $
      nub (decomp \\ [is]) | decomp <- decompose is,
      nub (decomp \\ [is]) /= [], nub decomp /= [sort is]]
  
  isInfixOf :: (Eq a) => [a] -> [a] -> Bool
  isInfixOf needle haystack = any (isPrefixOf needle) (tails haystack)
  
  decompose :: [Int] -> [[[Int]]]
  decompose [] = [[[]]]
  decompose [x] = [[[x]]]
  decompose is@(x : xs) = [is] :
   [ {- trace ("x: " ++ show x ++ " xs:" ++ show xs ++ " cont: " ++ show contained ++
        " excl: " ++ show exclusives ++ "subD: " ++ show subDecomposition) $ -}
   (sort (x : contained) : subDecomposition) \\ [[]] |
   contained <- powerList xs, exclusives <- powerList contained,
   subDecomposition <- decompose (xs \\ exclusives),
   (xs \\ contained) /= [],
   not (any (\ w -> isInfixOf w (x : contained)) subDecomposition) ]
  
  initialStates :: ([[Int]], [([Int], [Int])]) -> [[Int]]
  initialStates graph@(worlds, rel) = filter (\ w -> length w /= 1)
    (filter (\ s -> not (any (\ p -> (p, s) `elem` rel) worlds)) worlds)
  
  initialStates2 :: ([[Int]], [([Int], [Int])]) -> [[Int]]
  initialStates2 graph@(worlds, rel) = [s | s <- worlds,
    all (\ p -> (p, s) `notElem` rel) worlds]
  
  ckcmPremise :: (SigFeature b c d, Eq (b (c d)), Eq (c d)) =>
                   [Formula (CKCM (b (c d)))] ->
                   ([[Int]], [([Int], [Int])]) -> [[Sequent]]
  ckcmPremise gZ cG@(worlds, rel) =
    let allNegConsequents = [ Neg psi | Neg (Mod (CKCM [phi, psi])) <- gZ]
        allNegAntecedents = [ Neg phi | Neg (Mod (CKCM [phi, psi])) <- gZ]
        consequent (Mod (CKCM [phi, psi])) = psi
        consequent (Neg (Mod (CKCM [phi, psi]))) = psi
        antecedent (Mod (CKCM [phi, psi])) = phi
        antecedent (Neg (Mod (CKCM [phi, psi]))) = phi
        negArgs state = [ Neg (antecedent (gZ !! ind)) | ind <- state ] ++
                        [ Neg (consequent (gZ !! ind)) | ind <- state ]
    in [ [Sequent (equiv (keep initialstate gZ))]
            | initialstate <- initialStates2 cG ] ++
        [ [Sequent (antecedent (gZ !! j) : negArgs v)]
            | v <- worlds, w <- worlds, (v, w) `elem` rel, j <- w] ++
        [ [Sequent (consequent (gZ !! (length gZ - 1)) :
                    take (length gZ - 1) allNegConsequents)] ] ++
        [ [Sequent (antecedent (gZ !! (length gZ - 1)) :
                    take (length gZ - 1) allNegConsequents
          ++ take (length gZ - 1) allNegAntecedents )] ] ++
        [ [Sequent (Neg (antecedent (gZ !! (length gZ - 1))) :
          [antecedent (gZ !! i)])] | i <- [0 .. (length gZ - 2)] ]
  
  keep :: (SigFeature b c d, Eq (b (c d)), Eq (c d)) =>
                 [Int] ->
                 [Formula (CKCM (b (c d)))] -> [Formula (CKCM (b (c d)))]
  keep [] seq = []
  keep (x : xs) seq = if x < length seq then seq !! x : keep xs seq
                      else keep xs seq
  
  equiv :: (SigFeature b c d, Eq (b (c d)), Eq (c d)) =>
                 [Formula (CKCM (b (c d)))] -> [Formula (b (c d))]
  equiv [] = -- trace ("no more element, nothing needs to be shown... ") $
             [T]
  equiv [x] = -- trace ("only one element, nothing needs to be shown... " ++ pretty x) $
              [T]
  equiv (x : y : xs) = -- trace ("equiv added...") $
    let antecedent xi = case xi of (Neg (Mod (CKCM (phi : psi : _)))) -> phi
                                   (Mod (CKCM (phi : psi : _))) -> phi
                                   _ -> F
    in And (Neg (And (Neg (antecedent x)) (antecedent y)))
        (Neg (And (Neg (antecedent y)) (antecedent x))) : equiv (y : xs)
  
  {- ------------------------------------------------------------------------------
  instance of sigFeature for CK+CM
  ------------------------------------------------------------------------------ -}
  
  instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature CKCM b c d where
    neGoOn = genericPGoOn
  