----------------------------------------------------------------------------- -- Copyright 2013, 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 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 ok (\_ -> templateGenerator 1) , testGenerator = Just arbitrary } stepsRemaining :: Int -> RelAlg -> Maybe Int stepsRemaining i = lengthMax i . derivationTree False toCNF . inContext cnfExercise {- 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