{- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/SysS.hs
 -  Description : Implementation of logic instance of 'System S'
 -  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 'System S'.
 -}

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}

module GMP.Logics.SysS where
import Data.List
import Data.Ratio
import Data.Maybe

import Debug.Trace
import Text.ParserCombinators.Parsec

import GMP.Logics.Generic
import GMP.Parser

{- ------------------------------------------------------------------------------
instance of System S and needed functions
------------------------------------------------------------------------------ -}

data SysS a = SysS [Formula a] deriving (Eq, Show)

instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature SysS b c d where
-- compute all Gamma 0, construct all cStructures over each Gamma 0
    nefMatch flags seq =
      let g0s = sysCGammaZeros seq
          cStructuress = map cStructures g0s
-- for any structure <m> and any equivalence class <inds> on it, compute <deltaM inds>
      in if flags !! 1 then
          trace ("  <All G0s for current sequent:>                " ++
                 show (map pretty_list g0s) ++ "\n")
          [ trace "\n  <Starting a new G0...>\n" $ sysCprems strucs |
            strucs <- cStructuress ]
         else [ sysCprems strucs | strucs <- cStructuress ]

    nefPretty d = genfPretty d "[SysS]"
    nefFeatureFromSignature sig = SysS
    nefFeatureFromFormula phi = SysS
    nefStripFeature (SysS phis) = phis
    nefSeparator sig = "=>"

{- ------------------------------------------------------------------------------
additional functions for the matching function of this logic
------------------------------------------------------------------------------ -}

pretty_c :: (Feature SysS (a (b c))) => ([Int], [(Int, Int)], [Formula (SysS (a (b c)))]) -> String
pretty_c (worlds, rel, seq) = show worlds ++ show rel ++ pretty_list seq


sysCprems :: (SigFeature a b c, Eq (a (b c)), Eq (b c)) => [([Int], [(Int, Int)],
              [Formula (SysS (a (b c)))])] -> [[Sequent]]
sysCprems strucs = [ trace ("  Structure M (for g0=" ++ pretty_list sequ ++
                     "): <worlds> " ++ show worlds ++ " <rel> " ++ show rel) $
                     orOverInds m (nu m) | m@(worlds, rel, sequ) <- strucs ]

orOverInds :: (SigFeature a b c, Eq (a (b c)), Eq (b c)) => ([Int], [(Int, Int)],
               [Formula (SysS (a (b c)))]) -> [[Int]] -> [Sequent]
orOverInds struc [] = []
orOverInds struc (inds : indss) = trace ("  <deltaM(ec) (ec=" ++ show inds ++
   "):> " ++ pretty_seq (deltaM struc inds)) $
   deltaM struc inds : orOverInds struc indss


{- -----------------------------------------------------------------------------
compute deltaM(inds)
two cases, either the head of the input equivalence class is equivalent
wrt. the 'less remote than' relation to 0, or not. refer to paper for
more details...
----------------------------------------------------------------------------- -}
deltaM :: (SigFeature a b c, Eq (a (b c))) => ([Int], [(Int, Int)],
           [Formula (SysS (a (b c)))]) -> [Int] -> Sequent
deltaM struc@(worlds, rel, seq) ec = Sequent $ if (head ec, 0) `elem` rel &&
                                                  (0, head ec) `elem` rel
                                        -- equivalence class contains 0
  then concat [ [Neg ante, Neg conseq] |
           Neg (Mod (SysS (ante : conseq : _))) <- seqswAt seq ec] ++
          concat [ [Neg ante, conseq] | (Mod (SysS (ante : conseq : _))) <-
           [head seq] ] ++ [ ante | Neg (Mod (SysS (ante : conseq : _))) <-
            seqsAt seq ([0 .. length seq - 1] \\ worlds)]
                                        -- equivalence class does not contain 0
  else concat [ [Neg ante, Neg conseq] |
            Neg (Mod (SysS (ante : conseq : _))) <- seqsAt seq ec] ++
           [ ante | Neg (Mod (SysS (ante : conseq : _))) <-
            seqsAt seq ([0 .. length seq - 1] \\ worlds)] ++
           [ ante | Neg (Mod (SysS (ante : conseq : _))) <-
            seqsAt seq (biggerInds struc (head ec))] ++
           [ ante | Mod (SysS (ante : conseq : _)) <-
            seqsAt seq (biggerInds struc (head ec))]

{- -----------------------------------------------------------------------------
return those indices of a cStructure which are 'strictly bigger' wrt. to the
'less remote than' relation than the input integer
----------------------------------------------------------------------------- -}
biggerInds :: ([Int], [(Int, Int)], [Formula (SysS a)]) -> Int -> [Int]
biggerInds struc@(worlds, rel, seq) i = [ j | j <- [0 .. length seq],
 (i, j) `elem` rel && (j, i) `notElem` rel ]

{- -----------------------------------------------------------------------------
keep only the indexed parts of sequents (w/wo 0)
----------------------------------------------------------------------------- -}
seqswAt :: [Formula (SysS a)] -> [Int] -> [Formula (SysS a)]
seqswAt [] inds = []
seqswAt seq [] = []
seqswAt seq (ind : inds) = if ind == 0 then seqsAt seq inds
                           else seq !! ind : seqsAt seq inds

seqsAt :: [Formula (SysS a)] -> [Int] -> [Formula (SysS a)]
seqsAt [] inds = []
seqsAt seq [] = []
seqsAt seq (ind : inds) = seq !! ind : seqsAt seq inds

{- -----------------------------------------------------------------------------
given a sequent, return the big disjunction of this sequent
----------------------------------------------------------------------------- -}
orIfy :: [Formula (SysS a)] -> Formula (SysS a)
orIfy [] = F
orIfy (phi : []) = phi
orIfy (phi : phis) = Or phi (orIfy phis)

{- -----------------------------------------------------------------------------
compute all possible sequents of the form "\Gamma 0" that may be built
from the input sequent seq
----------------------------------------------------------------------------- -}
sysCGammaZeros :: [Formula (SysS a)] -> [[Formula (SysS a)]]
sysCGammaZeros seq =
  let negNegMods = [ Neg (Mod (SysS phis)) | Neg (Mod (SysS phis)) <- seq]
      posMods = [ Mod (SysS phis) | Mod (SysS phis) <- seq]
{- use this for complete application of the rule (i.e. all combinations of
negative literals)
allNegs    = powerList negNegMods
use this for maximal application of the rule (i.e. only consider all
negative literals at once) -}
      allNegs = [negNegMods]
  in [pos : negs | negs <- allNegs, pos <- posMods ]

{- -----------------------------------------------------------------------------
let nu return all equivalence classes for the input cStructure
----------------------------------------------------------------------------- -}
nu :: ([Int], [(Int, Int)], [Formula (SysS a)]) -> [[Int]]
nu struc@(worlds, rel, seq) = equivClasses worlds rel

{- -----------------------------------------------------------------------------
given a set of worlds and a transitive and reflexive relation over this set
of worlds, compute the equivalence classes according to this relation
----------------------------------------------------------------------------- -}
equivClasses :: (Eq a) => [a] -> [(a, a)] -> [[a]]
equivClasses [] rel = []
equivClasses (world : worlds) rel =
  let ec = equivClass world worlds rel
  in ec : equivClasses (worlds \\ ec) rel

equivClass :: (Eq a) => a -> [a] -> [(a, a)] -> [a]
equivClass world worlds rel = world : [ w |
 w <- worlds, (w, world) `elem` rel && (world, w) `elem` rel]

{- -----------------------------------------------------------------------------
for any set of worlds, compute all possible cStructures over it, i.e.
endow this set of worlds with any possible 'less remote than' relation
----------------------------------------------------------------------------- -}
cStructures :: [Formula (SysS a)] -> [([Int], [(Int, Int)], [Formula (SysS a)])]
cStructures seq = [ (worlds, rel, seq) | (worlds, rel) <-
 cStructs2 (powerList [0 .. length seq - 1])]

cStructs2 :: [[Int]] -> [([Int], [(Int, Int)])]
cStructs2 worldss = concat [ cStructs worlds | worlds <- worldss ]

cStructs :: [Int] -> [([Int], [(Int, Int)])]
cStructs worlds = [ (worlds, rel) | rel <- allRels worlds ]

{- -----------------------------------------------------------------------------
get all 'less remote than' relations, i.e. all linear pre-orders with
greatest element 0
----------------------------------------------------------------------------- -}

allRels :: [Int] -> [[(Int, Int)]]
allRels worlds = nub $ map sort (buildRels worlds (allPairs worlds)
  (diagonal worlds)) \\ [[]]

-- is a binary relation over worlds transitive, linear and has greatest element 0?
okRel :: [Int] -> [(Int, Int)] -> Bool
okRel worlds rel = null (transBreakers worlds rel) &&
 null (linearBreakers worlds rel) && null (great0Breakers worlds rel)

{- given a relation, add pairs to it in a consistent manner
(i.e. closing of under transitivity, linearity and 0 being
greatest element). continue with the remaining pairs. -}
buildRels :: [Int] -> [(Int, Int)] -> [(Int, Int)] -> [[(Int, Int)]]
buildRels worlds [] rel = -- trace ("finishing: " ++ show rel) $
                          [rel | okRel worlds rel]
buildRels worlds pairs [] = []
buildRels worlds (pair : pairs) rel = -- trace ("building: " ++ show (pair:pairs) ++ show rel) $
  if pair `elem` rel then buildRels worlds pairs rel
  else let closedRel = closeRel worlds pair rel
       in closedRel ++ concatMap (buildRels worlds pairs) closedRel ++
                       buildRels worlds pairs rel

{- add pairs to a relation until it is transitive, linear and has greatest element 0. if that's not
possible, return [] -}
closeRel :: [Int] -> (Int, Int) -> [(Int, Int)] -> [[(Int, Int)]]
closeRel worlds pair@(x, y) rel = -- trace ("closing: " ++ show worlds ++ show pair ++ show rel) $
  if pair `elem` rel then [rel | okRel worlds rel]
  else case transBreakers worlds (pair : rel) of
        w : ws -> closeRel worlds w (pair : rel)
        [] -> case linearBreakers worlds (pair : rel) of
                (v, w) : ws -> closeRel worlds v (pair : rel) ++
                               closeRel worlds w (pair : rel)
                [] -> case great0Breakers worlds (pair : rel) of
                        w : ws -> closeRel worlds w (pair : rel)
                        [] -> [pair : rel]

-- return the diagonal relation over worlds
diagonal :: [Int] -> [(Int, Int)]
diagonal = map (\ w -> (w, w))

-- return the set of pairs that break transitivity
transBreakers :: [Int] -> [(Int, Int)] -> [(Int, Int)]
transBreakers worlds rel = [ (x, z) | z <- worlds, y <- worlds, x <- worlds,
  (x, y) `elem` rel && (y, z) `elem` rel && (x, z) `notElem` rel ]

-- return the set of pairs of pairs the break linearity
linearBreakers :: [Int] -> [(Int, Int)] -> [((Int, Int), (Int, Int))]
linearBreakers worlds rel = [ ((x, z), (z, x)) | z <- worlds, x <- worlds,
  (x, z) `notElem` rel && (z, x) `notElem` rel ]

-- return the set of pairs that violate that 0 is greatest element
great0Breakers :: [Int] -> [(Int, Int)] -> [(Int, Int)]
great0Breakers worlds rel = [ (z, 0) | z <- worlds, (z, 0) `notElem` rel ]

-- return all combinations of worlds
allPairs :: [Int] -> [(Int, Int)]
allPairs worlds = [(x, y) | x <- worlds, y <- worlds]

{- ------------------------------------------------------------------------------
instance of sigFeature for 'System S'
------------------------------------------------------------------------------ -}

instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature SysS b c d where
  neGoOn = genericPGoOn
