{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeFamilies       #-}
{-# LANGUAGE TypeOperators      #-}
{-# LANGUAGE FlexibleInstances  #-}

-----------------------------------------------------------------------------
-- Copyright 2008, Open Universiteit Nederland. This file is distributed 
-- under the terms of the GNU General Public License. For more information, 
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
module Common.Logic where

import Data.List
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Map as M
import Data.Typeable
import Data.Data
import Common.GuardedRewriting

infixr 1 :<->:
infixr 2 :->: 
infixr 3 :||: 
infixr 4 :&&:

-- | The data type Logic is the abstract syntax for the domain
-- | of logic expressions.
data Logic = VarL String
           | Logic :->:  Logic            -- implication
           | Logic :<->: Logic            -- equivalence
           | Logic :&&:  Logic            -- and (conjunction)
           | Logic :||:  Logic            -- or (disjunction)
           | Not Logic                    -- not
           | T                            -- true
           | F                            -- false
 deriving (Show, Eq, Ord, Typeable, Data)

-- | The type LogicAlg is the algebra for the data type Logic
-- | Used in the fold for Logic.
type LogicAlg a = (String -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a, a)

-- | foldLogic is the standard fold for Logic.
foldLogic :: LogicAlg a -> Logic -> a
foldLogic (var, impl, equiv, and, or, not, true, false) = rec
 where
   rec logic = 
      case logic of
         VarL x     -> var x
         p :->: q  -> rec p `impl`  rec q
         p :<->: q -> rec p `equiv` rec q
         p :&&: q  -> rec p `and`   rec q
         p :||: q  -> rec p `or`    rec q
         Not p     -> not (rec p)
         T         -> true 
         F         -> false
              
-- | evalLogic takes a function that gives a logic value to a variable,
-- | and a Logic expression, and evaluates the boolean expression.
evalLogic :: (String -> Bool) -> Logic -> Bool
evalLogic env = foldLogic (env, impl, (==), (&&), (||), not, True, False)
 where
   impl p q = not p || q

-- | eqLogic determines whether or not two Logic expression are logically 
-- | equal, by evaluating the logic expressions on all valuations.
eqLogic p q = all (\f -> evalLogic f p == evalLogic f q) fs
 where 
   xs = varsLogic p `union` varsLogic q
   fs = map (flip elem) (subsets xs) 

   subsets :: [a] -> [[a]]
   subsets = foldr op [[]]
    where op a list = list ++ map (a:) list

-- | Functions noNot, noOr, and noAnd determine whether or not a Logic 
-- | expression contains a not, or, and and constructor, respectively.
noNot, noOr, noAnd :: Logic -> Bool
noNot = foldLogic (const True, (&&), (&&), (&&), (&&), const False, True, True)
noOr  = foldLogic (const True, (&&), (&&), (&&), \_ _ -> False, id, True, True)
noAnd = foldLogic (const True, (&&), (&&), \_ _ -> False, (&&), id, True, True)

-- | A Logic expression is atomic if it is a variable or a constant True or False.
isAtomic :: Logic -> Bool
isAtomic logic = 
   case logic of
      VarL _       -> True
      Not (VarL _) -> True
      _           -> False

-- | Functions isDNF, and isCNF determine whether or not a Logix expression
-- | is in disjunctive normal form, or conjunctive normal form, respectively. 
isDNF, isCNF :: Logic -> Bool
isDNF = all isAtomic . concatMap conjunctions . disjunctions
isCNF = all isAtomic . concatMap disjunctions . conjunctions

-- | Function disjunctions returns all Logic expressions separated by an or
-- | operator at the top level.
disjunctions :: Logic -> [Logic]
disjunctions F          = []
disjunctions (p :||: q) = disjunctions p ++ disjunctions q
disjunctions logic      = [logic]

-- | Function conjunctions returns all Logic expressions separated by an and
-- | operator at the top level.
conjunctions :: Logic -> [Logic]
conjunctions T          = []
conjunctions (p :&&: q) = conjunctions p ++ conjunctions q
conjunctions logic      = [logic]

-- | Count the number of implicationsations :: Logic -> Int
countImplications :: Logic -> Int
countImplications = foldLogic (const 0, \x y -> x+y+1, (+), (+), (+), id, 0, 0)
 
-- | Count the number of equivalences
countEquivalences :: Logic -> Int
countEquivalences = foldLogic (const 0, (+), \x y -> x+y+1, (+), (+), id, 0, 0)

-- | Count the number of binary operators
countBinaryOperators :: Logic -> Int
countBinaryOperators = foldLogic (const 0, binop, binop, binop, binop, id, 0, 0)
 where binop x y = x + y + 1

-- | Count the number of double negations 
countDoubleNegations :: Logic -> Int
countDoubleNegations = fst . foldLogic (const zero, bin, bin, bin, bin, notf, zero, zero)
 where
   zero = (0, False)
   bin (n, _) (m, _) = (n+m, False)
   notf (n, b) = if b then (n+1, False) else (n, True)

-- | Function varsLogic returns the variables that appear in a Logic expression.
varsLogic :: Logic -> [String]
varsLogic = foldLogic (return, union, union, union, union, id, [], [])      

test = associativityAnd $ (VarL "a" :||: VarL "b") :||: (VarL "c" :||: VarL "d" :||: VarL "e")

associativityAnd, associativityOr :: Logic -> [Logic]
associativityAnd = associativity conjunctions (:&&:) [T]
associativityOr  = associativity disjunctions (:||:) [F]

-- Helper function (polymorphic, domain independent)
associativity :: (a -> [a]) -> (a -> a -> a) -> [a] -> a -> [a]
associativity f op nil = rec . f
 where
   rec ps
      | n == 0    = nil
      | n == 1    = ps
      | otherwise = concatMap f [1 .. n-1]
    where
      n = length ps
      f i = let (xs, ys) = splitAt i ps
            in [ x `op` y | x <- rec xs, y <- rec ys ]

eqAssociative :: Logic -> Logic -> Bool
eqAssociative p q =
   case (p, q) of
      (VarL x, VarL y)             -> x==y
      (p1 :->: p2,  q1 :->:  q2) -> eqAssociative p1 q1 && eqAssociative p2 q2
      (p1 :<->: p2, q1 :<->: q2) -> eqAssociative p1 q1 && eqAssociative p2 q2
      (_ :&&: _,  _ :&&:  _) -> and $ zipWith eqAssociative (conjunctions p) (conjunctions q)
      (_ :||: _,  _ :||:  _) -> and $ zipWith eqAssociative (disjunctions p) (disjunctions q)
      (Not p1,      Not q1     ) -> eqAssociative p1 q1
      (T,           T          ) -> True
      (F,           F          ) -> True
      _ -> False

-----------------------------------------------------------
--- Unification

type Substitution = M.Map Char Logic

isMetaVar :: Logic -> Maybe Char
isMetaVar (VarL ['_', c]) = Just c
isMetaVar _ = Nothing

metaVars :: [Logic]
metaVars = [ VarL ['_', c] | c <- ['a' .. 'z'] ]

(|->) :: Substitution -> Logic -> Logic
(|->) sub = foldLogic (var, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)
 where 
   var s = case isMetaVar (VarL s) of
              Just i -> fromMaybe (VarL s) (M.lookup i sub)
              _      -> VarL s

matchLogic :: Logic -> Logic -> Maybe Substitution
matchLogic p q =
   case isMetaVar p of
      Just i  -> return (M.singleton i q)
      Nothing ->
         case (p, q) of
            (VarL x, VarL y) | x==y      -> return M.empty
            (p1 :->: p2,  q1 :->:  q2) -> matchPairs (p1, p2) (q1, q2)
            (p1 :<->: p2, q1 :<->: q2) -> matchPairs (p1, p2) (q1, q2)
            (p1 :&&: p2,  q1 :&&: q2 ) -> matchPairs (p1, p2) (q1, q2)
            (p1 :||: p2,  q1 :||: q2 ) -> matchPairs (p1, p2) (q1, q2)
            (Not p1,      Not q1     ) -> matchLogic p1 q1
            (T,           T          ) -> return M.empty
            (F,           F          ) -> return M.empty
            _ -> Nothing
 where
  matchPairs :: (Logic, Logic) -> (Logic, Logic) -> Maybe Substitution
  matchPairs (x1, x2) (y1, y2) = do
     s1 <- matchLogic x1 y1
     s2 <- matchLogic (s1 |-> x2) y2
     return (M.union s1 s2)


instance Rewritable Logic
instance Rewritable [Char]

instance Representable Logic where
  type Rep Logic =
        Var String
    :+: Rec Logic :*: Rec Logic
    :+: Rec Logic :*: Rec Logic
    :+: Rec Logic :*: Rec Logic
    :+: Rec Logic :*: Rec Logic
    :+: Rec Logic
    :+: U
    :+: U

  from (VarL x)    = L (Var x)
  from (p :<->: q) = R (L (Rec p :*: Rec q))
  from (p :->: q)  = R (R (L (Rec p :*: Rec q)))
  from (p :&&: q)  = R (R (R (L (Rec p :*: Rec q))))
  from (p :||: q)  = R (R (R (R (L (Rec p :*: Rec q)))))
  from (Not p)     = R (R (R (R (R (L (Rec p))))))
  from T           = R (R (R (R (R (R (L U))))))
  from F           = R (R (R (R (R (R (R U))))))

  to (L (Var x))                           = VarL x
  to (R (L (Rec p :*: Rec q)))             = p :<->: q
  to (R (R (L (Rec p :*: Rec q))))         = p :->: q
  to (R (R (R (L (Rec p :*: Rec q)))))     = p :&&: q
  to (R (R (R (R (L (Rec p :*: Rec q)))))) = p :||: q
  to (R (R (R (R (R (L (Rec p)))))))       = Not p
  to (R (R (R (R (R (R (L U)))))))         = T
  to (R (R (R (R (R (R (R U)))))))         = F