-----------------------------------------------------------------------------
-- 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 Common.LogicStrategies where

import Prelude hiding (repeat)
import Common.LogicRules
import Common.Logic
import Common.LogicGenerator
import Test.QuickCheck hiding (label)
import System.Random
import Common.GuardedRewriting
import Control.Monad

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

-- --------------------------------------
-- Strategies
-- --------------------------------------
-- Same monad to that in the SYB3 paper
data S m a = S a (m a)

instance MonadPlus m => Monad (S m) where
  return x = S x mzero
  (S x xs) >>= k
    = S r (rs1 `mplus` rs2)
      where
        S r rs1 = k x
        rs2 = do x <- xs
                 let S r _ = k x
                 return r

-- This is like Stratego's one.
-- It applies f to one of the immediate children of x.
{-
one :: (Rewritable a, MonadPlus m, Functor m) => (a -> m a) -> a -> m a
one f x = fmap (from . In) rs
  where
    S _ rs = fmapM try_f $ out $ to x
    try_f x = S x (f_str x)
    f_str = fmap to . f . from
-}

-- Apply f once to one of the nodes of x
-- Mirrors the corresponding definition in Stratego
once :: (Rewritable a, MonadPlus m, Functor m) => (a -> m a) -> a -> m a
once f x = f x `mplus` one (once f) x


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

lift :: Rewritable a => Rule' a -> Strategy a
lift r = (:[]) . rewrite' r

liftl :: Rewritable a => [Rule' a] -> Strategy a
liftl = alternatives . map lift

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

eliminateImplEquiv :: Strategy (Logic)
eliminateImplEquiv = repeat $ somewhere $
          lift ruleDefImpl
      <|> lift ruleDefEquiv
      
eliminateNots :: Strategy (Logic)
eliminateNots = repeat $ somewhere $ 
          lift ruleDeMorganAnd
      <|> lift ruleDeMorganOr
      <|> lift ruleNotNot
      
orToTop :: Strategy (Logic)
orToTop = repeat $ somewhere $ liftl 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 == from (to 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)