content: {- | Module     : ./GMP/GMP-CoLoSS/GMP/Logics/IneqSolver.hs
    Description : Inequality Solver for Graded Modal Logics
    Copyright   : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
    License     : GPLv2 or higher, see LICENSE.txt
    Maintainer  : g.calin@jacobs-university.de
    Stability   : provisional
    Portability : non-portable (various -fglasgow-exts extensions)
  
    Provides an implementation for solving the system
           0 >= 1 + sum x_i*n_i + sum y_i*p_i
     with unknowns x_i and y_i within given limits.
   -}
  module GMP.Logics.IneqSolver where
  
  -- | Coefficients: negative\/positive signed grades on the left\/right.
  data Coeffs = Coeffs [Int] [Int]
      deriving (Eq, Ord, Show)
  
  -- | Datatype for negative\/positive unknowns; the second Int is the flag.
  data IntFlag = IF Int Int
      deriving (Eq, Ord)
  
  {- | Sort increasingly a list of pairs.
  The sorting is done over the first element of the pair
  -}
  sort :: Ord a => [(a, b)] -> [(a, b)]
  sort list =
    let insert x l =
          case l of
            h : t -> if fst x < fst h
                   then x : l
                   else h : insert x t
            [] -> [x]
    in case list of
         h : t -> insert h (sort t)
         [] -> []
  
  -- | Compute the minimal point-wise extremal sum of an IntFlag list.
  minSum :: [IntFlag] -> Int -> Int -> Int
  minSum l lim c =
      case l of
        IF x 0 : t -> minSum t lim c - lim * x
        IF x 1 : t -> minSum t lim c + x
        [] -> c
        _ -> error "IneqSolver.minSum"
  
  -- | Compute the maximal point-wise extremal sum of an IntFlag list.
  maxSum :: [IntFlag] -> Int -> Int -> Int
  maxSum l lim c =
      case l of
        IF x 0 : t -> maxSum t lim c - x
        IF x 1 : t -> maxSum t lim c + lim * x
        [] -> c
        _ -> error "IneqSolver.maxSum"
  
  {- | Returns the updated bound for the unknown corresponding to the negative
   - coeff. h where t holds the coefficients for the not yet set unknowns -}
  negBound :: Int -> [IntFlag] -> Int -> Int -> Int
  negBound h t lim c =
          let tmp = case h of
                      0 -> -1 -- error "div by 0 @ IneqSolver.negBound"
                      _ -> div (negate (minSum t lim c)) h
          in if tmp < 0 then min tmp (-1) else - 1
  
  {- | Returns the updated bound for the unknown corresponding to the positive
   - coeff. h where t holds the coefficients for the not yet set unknowns -}
  posBound :: Int -> [IntFlag] -> Int -> Int -> Int
  posBound h t lim c =
          let tmp = case h of
                      0 -> lim -- error "div by 0 @ IneqSolver.posBound"
                      _ -> div (negate (minSum t lim c)) h
          in if tmp > 0 then min tmp lim else lim
  
  mapAppend :: a -> [[a]] -> [[a]]
  mapAppend x = map (x :)
  
  -- | Generate all posible solutions of unknowns
  getUnknowns :: [IntFlag] -> Int -> Int -> [[Int]]
  getUnknowns list lim c =
    if maxSum list lim c <= 0
    then
      [map (\ x -> case x of
                  IF _ 0 -> -1
                  IF _ 1 -> lim
                  _ -> error "IneqSolver.getUnknowns.if"
           ) list]
    else
      case list of
        IF h 0 : t -> let aux = negBound h t lim c
                      in concatMap (\ x -> mapAppend x (getUnknowns t lim (c + x * h)))
                                     [(-lim) .. aux]
        IF h 1 : t -> let aux = posBound h t lim c
                      in concatMap (\ x -> mapAppend x (getUnknowns t lim (c + x * h)))
                                     [1 .. aux]
        [] -> []
        _ -> error "IneqSolver.getUnknowns.else"
  
  {- | Returns all solutions (x,y) with 1<=-x_i,y_j<=L for the inequality
   -              0 >= 1 + sum x_i*n_i + sum y_j*p_j
   - with coefficients n_j>0, p_j>0 known -}
  ineqSolver :: Coeffs -> Int -> [([Int], [Int])]
  ineqSolver (Coeffs n p) bound =
    let combinedList = map (`IF` 0) n ++ map (`IF` 1) p -- merge lists & add flags
        (sortedList, indexOrder) = (unzip . sort) (zip combinedList [(1 :: Int) ..]) -- sort by coefficents
        unOrdered = getUnknowns sortedList bound 1 -- get solutions for the sorted list of coefficients
        reOrder list order = (snd . unzip . sort) (zip order list) -- revert list to its initial order
        splitList l = case l of  -- split a result list in a pair as used by the implementation
                        h : t -> if h < 0 then let tmp = splitList t
                                               in (h : fst tmp, snd tmp)
                                        else ([], l)
                        [] -> ([], [])
    in map (\ l -> splitList (reOrder l indexOrder)) unOrdered
       -- for each element in the result list reorder it and split it
  