{-# LANGUAGE FlexibleContexts #-}
-----------------------------------------------------------------------------
-- 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 LogicStrategies where

import Prelude hiding (repeat)
import Logic
import LogicRules hiding (main)
import System.Random
import Test.QuickCheck hiding (label)

import Generics.Regular.Rewriting


type Strategy a = a -> [a]

label _ = id
(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
alternatives = foldr (<|>) (const [])
notS s a = if null (s a) then [a] else []

rewriteMl :: Rewrite a => [Rule a] -> Strategy a 
rewriteMl = alternatives . map rewriteM

eliminateConstants :: Strategy (Logic)
eliminateConstants = repeat $ once $
   alternatives $
      [ rewriteMl ruleFalseZeroOr
      , rewriteMl ruleTrueZeroOr
      , rewriteMl ruleTrueZeroAnd
      , rewriteMl ruleFalseZeroAnd
      , rewriteMl ruleNotBoolConst
      , rewriteMl ruleFalseInEquiv
      , rewriteMl ruleTrueInEquiv
      , rewriteMl ruleFalseInImpl
      , rewriteMl ruleTrueInImpl
      ]

eliminateImplEquiv :: Strategy (Logic)
eliminateImplEquiv = repeat $ once $
          rewriteM ruleDefImpl
      <|> rewriteM ruleDefEquiv
      
eliminateNots :: Strategy (Logic)
eliminateNots = repeat $ once $ 
          rewriteM ruleDeMorganAnd
      <|> rewriteM ruleDeMorganOr
      <|> rewriteM ruleNotNot
      
orToTop :: Strategy (Logic)
orToTop = repeat $ once $ rewriteMl ruleAndOverOr

toDNF :: Strategy (Logic)
toDNF =  label "Bring to dnf"
      $  label "Eliminate constants"                 eliminateConstants
     <*> label "Eliminate implications/equivalences" eliminateImplEquiv
     <*> label "Eliminate nots"                      eliminateNots 
     <*> label "Move ors to top"                     orToTop
     
propSound :: Logic -> Bool
propSound p = 
   case toDNF p of
      x:_ -> isDNF x
      _   -> False
      
propView :: Logic -> Bool
propView p = p == to (from p)

checks :: IO ()
checks = do
   quickCheck propView
   quickCheck propSound

main :: IO ()
main = print $ all checkOne [0..250]
 where
   checkOne n =
      propSound (generate n (mkStdGen n) arbitrary)