{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------------
-- 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 Logic (Logic(..), isDNF, foldLogic, size, height, metaVars, matchLogic, (|->)) where

import Data.List
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Map as M
import Test.QuickCheck
import Control.Monad
import Data.Char

import Generics.Regular.Rewriting

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

-- | The data type Logic is the abstract syntax for the domain
-- | of logic expressions.
data Logic = Var 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)

-- | 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
         Var 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
      Var _       -> True
      Not (Var _) -> 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]

size :: Logic -> Int
size = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)
 where bin x y = x+y+1

height :: Logic -> Int
height = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)
 where bin x y = 1 + (x `max` y)
 
-- | 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 $ (Var "a" :||: Var "b") :||: (Var "c" :||: Var "d" :||: Var "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
      (Var x, Var 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

-- sized, no nested equivalences
-- arbLogic :: Bool -> Int -> Gen Logic
arbLogic b n
   | n <= 1 = frequency
        [ (1, oneof $ map return [F, T])
        , (3, oneof $ map (return . Var) ["p", "q", "r"])
        ]
   | otherwise = frequency
        [ (4, arbLogic b 0)
        , (2, bin (:->:))
        , (i, liftM2 (:<->:) recF recF)
        , (3, bin (:&&:))
        , (3, bin (:||:))
        , (3, liftM Not rec)
        ]
 where
   i     = if b then 1 else 0
   rec   = arbLogic b (n `div` 2)
   recF  = arbLogic False (n `div` 2)
   bin f = liftM2 f rec rec

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

type Substitution = M.Map Char Logic

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

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

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


-----------------------------------------------------------
--- QuickCheck generator

instance Arbitrary Logic where
   arbitrary = sized (arbLogic True)
   coarbitrary logic = 
      case logic of
         Var x     -> variant 0 . coarbitrary (map ord x)
         p :->: q  -> variant 1 . coarbitrary p . coarbitrary q
         p :<->: q -> variant 2 . coarbitrary p . coarbitrary q
         p :&&: q  -> variant 3 . coarbitrary p . coarbitrary q
         p :||: q  -> variant 4 . coarbitrary p . coarbitrary q
         Not p     -> variant 5 . coarbitrary p
         T         -> variant 6  
         F         -> variant 7

#ifdef FixView
type instance PF Logic =
    (((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))
    :+:
    ((I :*: I :+: I) :+: (U :+: U))

instance Regular Logic where
  from (Var x)     = L (L (L (K x)))
  from (p :<->: q) = L (L (R ((I (from p)) :*: (I (from q)))))
  from (p :->: q)  = L (R (L ((I (from p)) :*: (I (from q)))))
  from (p :&&: q)  = L (R (R ((I (from p)) :*: (I (from q)))))
  from (p :||: q)  = R (L (L ((I (from p)) :*: (I (from q)))))
  from (Not p)     = R (L (R (I (from p))))
  from T           = R (R (L U))
  from F           = R (R (R U))

  to (L (L (L (K x))))               = Var x
  to (L (L (R ((I p) :*: (I q))))) = to p :<->: to q
  to (L (R (L ((I p) :*: (I q))))) = to p :->: to q
  to (L (R (R ((I p) :*: (I q))))) = to p :&&: to q
  to (R (L (L ((I p) :*: (I q))))) = to p :||: to q
  to (R (L (R (I p))))              = Not (to p)
  to (R (R (L U)))                = T
  to (R (R (R U)))                = F
#else
type instance PF Logic =
    (((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))
    :+:
    ((I :*: I :+: I) :+: (U :+: U))

instance Regular Logic where
  from (Var x)     = L (L (L (K x)))
  from (p :<->: q) = L (L (R ((I p) :*: (I q))))
  from (p :->: q)  = L (R (L ((I p) :*: (I q))))
  from (p :&&: q)  = L (R (R ((I p) :*: (I q))))
  from (p :||: q)  = R (L (L ((I p) :*: (I q))))
  from (Not p)     = R (L (R (I p)))
  from T           = R (R (L U))
  from F           = R (R (R U))

  to (L (L (L (K x))))               = Var x
  to (L (L (R ((I p) :*: (I q))))) = p :<->: q
  to (L (R (L ((I p) :*: (I q))))) = p :->: q
  to (L (R (R ((I p) :*: (I q))))) = p :&&: q
  to (R (L (L ((I p) :*: (I q))))) = p :||: q
  to (R (L (R (I p))))              = Not p
  to (R (R (L U)))                = T
  to (R (R (R U)))                = F
#endif

instance Rewrite Logic