{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -cpp #-}

module Common.DNF (runStrategy, dnf1, dnf2, dnf3, dnf4, reportTick) where

import Prelude hiding (repeat)
import Common.LogicRules()
import Common.Logic
import System.IO.Unsafe
import Data.IORef

{- Which rules -}
#ifdef __PM
import PM.Rules
#endif
#ifdef __Uni
import Uni.Rules
#endif
#ifdef __Gen
import Gen.Rules
#endif


import Common.Once

counting = False


type Strategy a = a -> [a]

somewhere s = once s
(s <*> t) a = [c | b <- s a, c <- t b]
(s <|> t) a = s a ++ t a
many s = return <|> (s <*> many s)
repeat s = many s <*> notS s
try s = s <|> (notS s)
alternatives = foldr (<|>) (const [])
notS s a = if null (s a) then [a] else []

runStrategy :: Strategy a -> a -> a
runStrategy s p = case s p of
                     hd:_ -> hd
                     _    -> p      

data Count = C !Integer !Integer deriving Show

tickRef :: IORef Count
tickRef = unsafePerformIO (newIORef (C 0 0))

reportTick :: IO ()
reportTick = if counting then readIORef tickRef >>= print else return ()

tick :: (a -> [b]) -> a -> [b]
tick r a = if not counting then r a else unsafePerformIO $ do
   xs <- return (r a)
   c  <- readIORef tickRef
   seq c (writeIORef tickRef (update (null xs) c))
   return xs

update :: Bool -> Count -> Count
update b (C x y)
   | b         = C (x+1) y
   | otherwise = C x (y+1)

---------------------------------------------------------------

allRules = conRules ++ defRules ++ notRules ++ disRules
conRules = map tick [ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd, ruleFalseZeroAnd, ruleNotBoolConst, ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl]
defRules = map tick [ruleDefImpl, ruleDefEquiv]
notRules = map tick [ruleDeMorganAnd, ruleDeMorganOr, ruleNotNot]
disRules = map tick [ruleAndOverOr]

eliminateConstants :: Strategy (Logic)
eliminateConstants = repeat $ somewhere $ alternatives conRules

eliminateImplEquiv :: Strategy (Logic)
eliminateImplEquiv = repeat $ somewhere $ alternatives defRules

eliminateNots :: Strategy (Logic)
eliminateNots = repeat $ somewhere $ alternatives notRules


dnf1 :: Strategy (Logic)
dnf1 =  repeat (somewhere (alternatives allRules))

dnf2 :: Strategy (Logic)
dnf2 =  repeat (somewhere (alternatives conRules))
     <*> repeat (somewhere (alternatives defRules))
     <*> repeat (somewhere (alternatives notRules))
     <*> repeat (somewhere (alternatives disRules))

dnf3 :: Strategy (Logic)
dnf3 =  repeat (oneTD (alternatives conRules))
     <*> repeat (oneBU (alternatives defRules))
     <*> repeat (oneTD (alternatives notRules))
     <*> repeat (somewhere (alternatives disRules))

dnf4 :: Strategy (Logic)
dnf4 =   fullBU (repeat (alternatives (conRules ++ defRules)))
     <*> fullTD (repeat (alternatives notRules))
     <*> fullBU (try (alternatives disRules <*> fullTD (try (alternatives disRules))))