-----------------------------------------------------------------------------
-- 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.Strategies where

import Prelude hiding (repeat)
import Logic.Rules
import Logic.Formula
import Logic.Generator
import Test.QuickCheck hiding (label)
import System.Random
import Rewriting 
import Representations

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 []

-- applies a strategy at one location
-- see http://ideas.cs.uu.nl/trac/browser/Feedback/trunk/src/Common/Strategy.hs
somewhere :: Rewrite a => Strategy a -> Strategy a
somewhere = once

lift0 :: Rewrite a => Rule0 a -> Strategy a
lift0 = rewrite0

lift0l :: Rewrite a => [Rule a] -> Strategy a 
lift0l = alternatives . map lift0

lift1 :: Rewrite a => Rule1 a -> Strategy a
lift1 = rewrite1

lift1l :: Rewrite a => [Rule1 a] -> Strategy a
lift1l = alternatives . map lift1

lift2 :: Rewrite a => Rule2 a -> Strategy a
lift2 = rewrite2

lift3l :: Rewrite a => [Rule3 a] -> Strategy a
lift3l = alternatives . map rewrite3

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

eliminateImplEquiv :: Strategy (Logic)
eliminateImplEquiv = repeat $ somewhere $
          lift2 ruleDefImpl
      <|> lift2 ruleDefEquiv
      
eliminateNots :: Strategy (Logic)
eliminateNots = repeat $ somewhere $ 
          lift2 ruleDeMorganAnd
      <|> lift2 ruleDeMorganOr
      <|> lift1 ruleNotNot
      
orToTop :: Strategy (Logic)
orToTop = repeat $ somewhere $ lift3l 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..1000]
 where
   checkOne n = 
      propSound (generate n (mkStdGen n) generateLogic)