{-# LANGUAGE FlexibleContexts #-}

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

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

{- OPTION 1: which rules -}
#ifdef PM
import RulesPM
#endif
#ifdef Uni
import RulesUni
#endif
#ifdef Gen
import RulesGeneric 
#endif
#ifdef FixView
import RulesGeneric
#endif

{- OPTION 2: which traversal combinators -}
#ifdef ST
import Once
#endif
#ifdef GT
import Strategies
#endif

{- OPTION 3: with or without counting rules -}
#ifdef Counting
counting = True
#else
counting = False
#endif

testje = once (\_ -> [T]) (Var "p" :||: Var "q")

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
     
orToTop :: Strategy (Logic)
orToTop = repeat $ somewhere (tick ruleAndOverOr)

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))))