{-# 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 LogicGenerator
import LogicRules hiding (main)
import System.Random
import Test.QuickCheck hiding (label)

import Base
import Rewriting 
import Representations
import Rules
import Strategies


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 :: (Crush (PF a), PFView a, Zip (PF 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..1000]
 where
   checkOne n = 
      propSound (generate n (mkStdGen n) generateLogic)