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

import Common.Logic
import Control.Monad
import Data.Char
import Test.QuickCheck hiding (defaultConfig)
import System.Random

-----------------------------------------------------------
--- QuickCheck generator

-- sized, no nested equivalences
-- arbLogic :: Bool -> Int -> Gen Logic
arbLogic b n
   | n <= 1 = frequency
        [ (1, oneof $ map return [F, T])
        , (3, oneof $ map (return . VarL) ["p", "q", "r"])
        ]
   | otherwise = frequency
        [ (4, arbLogic b 0)
        , (2, bin (:->:))
        , (i, liftM2 (:<->:) recF recF)
        , (3, bin (:&&:))
        , (3, bin (:||:))
        , (3, liftM Not rec)
        ]
 where
   i     = if b then 1 else 0
   rec   = arbLogic b (n `div` 2)
   recF  = arbLogic False (n `div` 2)
   bin f = liftM2 f rec rec

instance Arbitrary Logic where
   arbitrary = sized (arbLogic True)
   coarbitrary logic = 
      case logic of
         VarL x    -> variant 0 . coarbitrary (map ord x)
         p :->: q  -> variant 1 . coarbitrary p . coarbitrary q
         p :<->: q -> variant 2 . coarbitrary p . coarbitrary q
         p :&&: q  -> variant 3 . coarbitrary p . coarbitrary q
         p :||: q  -> variant 4 . coarbitrary p . coarbitrary q
         Not p     -> variant 5 . coarbitrary p
         T         -> variant 6  
         F         -> variant 7

repeatM :: Monad m => m a -> m [a]
repeatM m = liftM2 (:) m (repeatM m)

formula :: [Logic]
formula = generate 100 (mkStdGen 280578) (repeatM arbitrary)