-----------------------------------------------------------------------------
-- Copyright 2015, 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)
--
-----------------------------------------------------------------------------
--  $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $

module Domain.RelationAlgebra.Exercises (cnfExercise) where

import Data.Maybe
import Domain.RelationAlgebra.Formula
import Domain.RelationAlgebra.Generator
import Domain.RelationAlgebra.Parser
import Domain.RelationAlgebra.Rules
import Domain.RelationAlgebra.Strategies
import Ideas.Common.Library
import Prelude hiding (repeat)
import Test.QuickCheck

cnfExercise :: Exercise RelAlg
cnfExercise = makeExercise
   { exerciseId     = describe "To conjunctive normal form" $
                         newId "relationalgebra.cnf"
   , status         = Alpha
   , parser         = parseRelAlg
   , prettyPrinter  = ppRelAlg
   , equivalence    = withoutContext probablyEqual -- isEquivalent
   , extraRules     = map liftToContext (relAlgRules ++ buggyRelAlgRules)
   , strategy       = toCNF
   , navigation     = navigator
   , ready          = predicate (myReady cnfExercise)
   , randomExercise = let ok p = let n = fromMaybe maxBound (stepsRemaining 4 p)
                                 in n >= 2 && n <= 4
                      in useGenerator (\_ -> templateGenerator 1 `suchThat` ok)
   , testGenerator  = Just arbitrary
   }

stepsRemaining :: Int -> RelAlg -> Maybe Int
stepsRemaining i = checkLength i cnfExercise

checkLength :: Int -> Exercise a -> a -> Maybe Int
checkLength n ex a = defaultDerivation ex a >>= rec 0 . steps
 where
   rec i []       = Just i
   rec i (_:xs)
      | i >= n    = Nothing
      | otherwise = rec (i+1) xs

{- cnfExerciseSimple :: Exercise RelAlg
cnfExerciseSimple = cnfExercise
   { identifier  = "cnf-simple"
   , description = description cnfExercise ++ " (simple)"
   , strategy    = label "Apply rules exhaustively" $ repeat $ somewhere $ alternatives $ ruleset cnfExercise
   } -}

myReady :: Exercise a -> a -> Bool
myReady ex = null . applyAll (alternatives $ filter (not . isBuggy) (ruleset ex))
         . inContext ex