packages feed

ideas-math 1.0 → 1.1

raw patch · 111 files changed

+1586/−600 lines, 111 filesdep ~QuickCheckdep ~ideas

Dependency ranges changed: QuickCheck, ideas

Files

CREDITS.txt view
@@ -4,4 +4,4 @@  CREDITS -Harrie Passier, Arthur van Leeuwen, Josje Lodder+Harrie Passier, Arthur van Leeuwen, Josje Lodder, Eric Andrès
ideas-math.cabal view
@@ -1,5 +1,5 @@ name:                   ideas-math-version:                1.0+version:                1.1 synopsis:               Interactive domain reasoner for logic and mathematics homepage:               http://ideas.cs.uu.nl/www/ description:@@ -14,7 +14,7 @@    ActiveMath, and the GenExas logic tool.   category:               Education-copyright:              (c) 2013+copyright:              (c) 2014 license:                GPL license-file:           LICENSE.txt author:                 Bastiaan Heeren, Alex Gerdes, Johan Jeuring@@ -23,7 +23,7 @@ extra-source-files:     CREDITS.txt build-type:             Simple cabal-version:          >= 1.8.0.2-tested-with:            GHC == 7.4.1, GHC == 7.4.2, GHC == 7.6.1+tested-with:            GHC == 7.4.1, GHC == 7.6.3  -- feedback scripts extra-source-files: @@ -38,18 +38,16 @@    -------------------------------------------------------------------------------- -- Executable ideas-math   Main-is:           Main.hs   ghc-options:       -Wall   hs-source-dirs:    src   Build-Depends:     base >= 4.2 && < 5, -                     QuickCheck >= 2.4.1,+                     QuickCheck >= 2.4.1 && < 2.7,                      containers,                      random,                      parsec,-                     ideas == 1.1+                     ideas == 1.2    Other-modules:     Domain.LinearAlgebra.Checks@@ -65,15 +63,18 @@     Domain.LinearAlgebra.Vector     Domain.LinearAlgebra     Domain.Logic.BuggyRules+    Domain.Logic.Consequence     Domain.Logic.Examples     Domain.Logic.Exercises     Domain.Logic.Formula     Domain.Logic.GeneralizedRules     Domain.Logic.Generator+    Domain.Logic.InverseRules     Domain.Logic.Parser     Domain.Logic.Proofs     Domain.Logic.Rules     Domain.Logic.Strategies+    Domain.Logic.Utils     Domain.Logic.Views     Domain.Logic     Domain.Math.Approximation
scripts/logic.txt view
@@ -4,6 +4,8 @@ 
 string okay      = Well done!
 string incorrect = This is incorrect. 
+string selectedRule = The rule you have selected was not applied correctly (or you combined multiple steps).
+string selectRight  = Select the right rule.
 string multiple  = You have combined multiple steps (or made a mistake). 
 string finished  = Are you aware that you already reached disjunctive normal form?
 
@@ -14,7 +16,6 @@ 
 string youRewroteInto = You rewrote @diffbefore into @diffafter. 
 string appliedRule    = You have applied @recognized correctly.
-string pressBack      = Press the Back button and try again.
 
 string suggested 
    | @hasexpected = However, the standard strategy suggests to use @expected.
@@ -29,11 +30,16 @@    or removed parentheses (the tool supports associativity)?
 }
 
-feedback ok      = @okay @appliedRule
-feedback noteq   = @youRewroteInto @incorrect @pressBack @askForHint
-feedback unknown = @youRewroteInto @multiple @pressBack @askForHint
-feedback buggy   = @youRewroteInto @incorrect @recognized @pressBack @askForHint
+feedback ok        = @okay @appliedRule
+feedback noteq     = @youRewroteInto @incorrect @askForHint
+feedback unknown   = @youRewroteInto @multiple @askForHint
+feedback buggy     = @youRewroteInto @incorrect @recognized @askForHint
 
+feedback wrongrule 
+   | @recognizedbuggy = @youRewroteInto @recognized @askForHint
+   | @hasrecognized   = @youRewroteInto @selectRight
+   | true             = @youRewroteInto @selectedRule
+
 feedback detour 
    | @oldready         = @appliedRule @finished
    | recognize commor  = @commText
@@ -142,9 +148,10 @@    @tryto apply DeMorgan? Make sure that you replace AND by OR. 
 }
 
-text buggy.demorgan4 = {
-   @tryto apply DeMorgan? Make sure that you replace OR by AND. 
-}
+text buggy.demorgan4 
+   | motivation demorganor = Make sure that you replace OR by AND. 
+   | @hasmotivation = Did you try to apply De Morgan instead of @motivation? Make sure that you replace OR by AND. 
+   | true = @tryto apply DeMorgan? Make sure that you replace OR by AND. 
 
 text buggy.demorgan5 = {
    @tryto apply DeMorgan? Take care of the  scope of the negations.
src/Domain/LinearAlgebra.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: LinearAlgebra.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra (module Export) where
 
 import Domain.LinearAlgebra.EquationsRules as Export
src/Domain/LinearAlgebra/Checks.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Checks.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.Checks (checks) where
 
 import Data.Maybe
@@ -25,12 +27,14 @@ --- QuickCheck properties
 
 checks :: TestSuite
-checks = suite "Linear algebra" $ do
-   let thorough = stdArgs {maxSize = 500, maxSuccess = 500}
-   addPropertyWith "echelon"         thorough propEchelon
-   addPropertyWith "reduced echelon" thorough propReducedEchelon
-   addPropertyWith "sound"           thorough propSound
-   addPropertyWith "solution"        thorough propSolution
+checks = suite "Linear algebra"
+   [ usePropertyWith "echelon"         thorough propEchelon
+   , usePropertyWith "reduced echelon" thorough propReducedEchelon
+   , usePropertyWith "sound"           thorough propSound
+   , usePropertyWith "solution"        thorough propSolution
+   ]
+ where
+   thorough = stdArgs {maxSize = 500, maxSuccess = 500}
 
 propEchelon :: Matrix Rational -> Bool
 propEchelon =
src/Domain/LinearAlgebra/EquationsRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: EquationsRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.EquationsRules
    ( ruleCoverAllEquations, ruleUncoverEquation, ruleScaleEquation
    , ruleBackSubstitution, ruleIdentifyFreeVariables, ruleExchangeEquations
src/Domain/LinearAlgebra/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.Exercises
    ( gramSchmidtExercise, linearSystemExercise
    , gaussianElimExercise, systemWithMatrixExercise
@@ -64,7 +66,7 @@                                     (Just a, Just b) -> getSolution a == getSolution b
                                     _ -> False
    , extraRules     = equationsRules
-   , ruleOrdering   = ruleOrderingWithId [getId ruleScaleEquation]
+   , ruleOrdering   = ruleOrderingWith [ruleScaleEquation]
    , ready          = predicate inSolvedForm
    , strategy       = linearSystemStrategy
    , randomExercise = simpleGenerator (fmap matrixToSystem arbMatrix)
@@ -105,7 +107,7 @@                                               (_, Just m)  -> Just $ matrixToSystem (m :: Matrix Expr)
                                               _            -> Nothing
                               in case (f x, f y) of
-                                    (Just a, Just b) -> simpleEquivalence linearSystemExercise a b
+                                    (Just a, Just b) -> (equivalence linearSystemExercise `on` inContext linearSystemExercise) a b
                                     _ -> False
    , ready          = predicate (inSolvedForm . (fromExpr :: Expr -> Equations Expr))
    , strategy       = systemWithMatrixStrategy
src/Domain/LinearAlgebra/GramSchmidtRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: GramSchmidtRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.GramSchmidtRules
    ( ruleNext, ruleNextOrthogonal
    , ruleOrthogonal, ruleNormalize
src/Domain/LinearAlgebra/LinearSystem.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: LinearSystem.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.LinearSystem where
 
 import Control.Monad
src/Domain/LinearAlgebra/LinearView.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: LinearView.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.LinearView
    ( IsLinear(..), LinearMap, renameVariables
    , splitLinearExpr, evalLinearExpr, linearView
src/Domain/LinearAlgebra/Matrix.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Matrix.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.Matrix
    ( Matrix, Row, Column, isRectangular, makeMatrix, identity, mapWithPos
    , changeEntries, changeEntry, setEntries, setEntry
src/Domain/LinearAlgebra/MatrixRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: MatrixRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.MatrixRules
    ( ruleFindColumnJ, ruleExchangeNonZero, ruleScaleToOne
    , ruleZerosFP, ruleCoverRow, ruleUncoverRow, ruleZerosBP
src/Domain/LinearAlgebra/Parser.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.Parser
    ( parseMatrix, parseVectorSpace, parseSystem
    , ppMatrix, ppMatrixWith
src/Domain/LinearAlgebra/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.Strategies
    ( gaussianElimStrategy, linearSystemStrategy
    , gramSchmidtStrategy, systemWithMatrixStrategy
src/Domain/LinearAlgebra/Vector.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Vector.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.LinearAlgebra.Vector
    ( Vector, VectorSpace
    , makeVectorSpace, vectors, sameDimension, gramSchmidt
src/Domain/Logic.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Logic.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic (module Export) where
 
 import Domain.Logic.BuggyRules as Export
@@ -16,6 +18,8 @@ import Domain.Logic.Formula as Export
 import Domain.Logic.GeneralizedRules as Export
 import Domain.Logic.Generator as Export
+import Domain.Logic.InverseRules as Export
 import Domain.Logic.Parser as Export
 import Domain.Logic.Rules as Export
-import Domain.Logic.Strategies as Export+import Domain.Logic.Strategies as Export
+import Domain.Logic.Utils as Export
src/Domain/Logic/BuggyRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,10 +11,13 @@ -- Buggy rules in the logic domain, expressing common misconceptions
 --
 -----------------------------------------------------------------------------
+--  $Id: BuggyRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.BuggyRules (buggyRules) where
 
 import Domain.Logic.Formula
-import Domain.Logic.Generator()
+import Domain.Logic.Generator (equalLogicA)
+import Domain.Logic.Utils
 import Ideas.Common.Library hiding (ruleList)
 import qualified Ideas.Common.Library as C
 
@@ -28,13 +31,16 @@    , buggyParenth3, buggyAssoc, buggyAbsor
    , buggyAndSame, buggyAndCompl, buggyOrSame, buggyOrCompl
    , buggyTrueProp, buggyFalseProp, buggyDistr, buggyDistrNot
+   , buggyInvIdemImp, buggyInvIdemEqui, buggyInvDefImpl, buggyInvDeMorgan3
+   , buggyInvDeMorgan4, buggyInvDistr
+   , buggyInvAndCompl, buggyInvOrCompl, buggyInvTrueProp, buggyInvFalseProp
    ]
 
 rule :: RuleBuilder f a => String -> f -> Rule a
-rule = C.rewriteRule . ( "logic.propositional.buggy" # )
+rule s = C.rewriteRule (propositionalId # "buggy" # s)
 
 ruleList :: RuleBuilder f a => String -> [f] -> Rule a
-ruleList = C.rewriteRules . ( "logic.propositional.buggy" # )
+ruleList s = C.rewriteRules (propositionalId # "buggy" # s)
 
 -----------------------------------------------------------------------------
 -- Buggy rules
@@ -119,9 +125,10 @@ 
 buggyImplElim :: Rule SLogic
 buggyImplElim = buggy $ ruleList "ImplElim"
-   [\x y -> x :->: y :~> Not (x :||: y)
-   ,\x y -> x :->: y :~> (x :||: y)
-   ,\x y -> x :->: y :~> Not (x :&&: y)
+   [ \x y -> x :->: y :~> Not (x :||: y)
+   , \x y -> x :->: y :~> (x :||: y)
+   , \x y -> x :->: y :~> Not (x :&&: y)
+   , \x y -> x :->: y :~> (x :||: Not y)
    ]
 
 buggyImplElim1 :: Rule SLogic
@@ -223,4 +230,50 @@    , \x y z -> Not x :||: (y :&&: z)  :~>  (x :||: y) :&&: (Not x :||: z)
    , \x y z -> (x :&&: y) :||: Not z  :~>  (x :||: Not z) :&&: (y :||: z)
    , \x y z -> (x :&&: y) :||: Not z  :~>  (x :||: z) :&&: (y :||: Not z)
+   ]
+
+logicInvRule :: String -> Rule SLogic -> Rule SLogic
+logicInvRule s = makeInvRule equalLogicA (propositionalId # "buggy" # s)
+
+buggyInvAndCompl, buggyInvOrCompl, buggyInvTrueProp, buggyInvFalseProp :: Rule SLogic
+buggyInvAndCompl  = logicInvRule "AndCompl.inv" buggyAndCompl
+buggyInvOrCompl   = logicInvRule "OrCompl.inv" buggyOrCompl
+buggyInvTrueProp  = logicInvRule "TrueProp.inv" buggyTrueProp
+buggyInvFalseProp = logicInvRule "FalseProp.inv" buggyFalseProp
+
+buggyInvIdemImp :: Rule SLogic
+buggyInvIdemImp = buggy $ rule "IdemImp.inv" $
+   \x -> x  :~>  x :->: x
+
+buggyInvIdemEqui :: Rule SLogic
+buggyInvIdemEqui = buggy $ rule "IdemEquiv.inv" $
+   \x -> x  :~>  x :<->: x
+
+buggyInvDefImpl :: Rule SLogic
+buggyInvDefImpl = buggy $ ruleList "DefImpl.inv"
+   [\x y -> Not x :&&: y  :~>  x :->: y
+   ,\x y -> x :||: Not y  :~>  x :->: y
+   ,\x y -> x :&&: Not y  :~>  y :->: x
+   ,\x y -> Not x :||: y  :~>  y :->: x
+   ,\x y -> Not (x :||: y)  :~>  x :->: y
+   ]
+
+buggyInvDeMorgan3 :: Rule SLogic
+buggyInvDeMorgan3 = buggy $  rule "DeMorgan3.inv" $
+    \x y -> Not x :&&: Not y :~>  Not (x :&&:  y)
+
+buggyInvDeMorgan4 :: Rule SLogic
+buggyInvDeMorgan4 = buggy $  rule "DeMorgan4.inv" $
+     \x y -> Not x :||: Not y :~>  Not( x :||:  y)
+
+buggyInvDistr :: Rule SLogic
+buggyInvDistr = buggy $ ruleList "Distr.inv"
+   [ \x y z -> (x :&&: y) :&&: (x :&&: z)  :~>  x :&&: (y :||: z)
+   , \x y z -> (x :&&: z) :&&: (y :&&: z)  :~>  (x :||: y) :&&: z
+   , \x y z -> (x :||: y) :&&: (x :||: z)  :~>  x :&&: (y :||: z)
+   , \x y z -> (x :||: z) :&&: (y :||: z)  :~>  (x :||: y) :&&: z
+   , \x y z -> (x :||: y) :||: (x :||: z)  :~>  x :||: (y :&&: z)
+   , \x y z -> (x :||: z) :||: (y :||: z)  :~>  (x :&&: y) :||: z
+   , \x y z -> (x :&&: y) :||: (x :&&: z)  :~>  x :||: (y :&&: z)
+   , \x y z -> (x :&&: z) :||: (y :&&: z)  :~>  (x :&&: y) :||: z
    ]
+ src/Domain/Logic/Consequence.hs view
@@ -0,0 +1,384 @@+{-# LANGUAGE RankNTypes #-}
+-----------------------------------------------------------------------------
+-- Copyright 2014, 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)
+--
+-- Exercise for the logic domain: to prove two propositions equivalent
+--
+-----------------------------------------------------------------------------
+--  $Id: Consequence.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
+module Domain.Logic.Consequence (consequenceExercise) where
+
+import Control.Monad
+import Data.List
+import Data.Maybe
+import Data.Traversable
+import Domain.Logic.Formula
+import Domain.Logic.Generator (equalLogicA, normalizeLogicA)
+import Domain.Logic.Parser
+import Domain.Logic.Proofs (sortRuleOr, sortRuleAnd)
+import Domain.Logic.Rules
+import Domain.Logic.Strategies (cnfStrategyDWA)
+import Domain.Logic.Utils
+import Domain.Math.Expr ()
+import Ideas.Common.Library hiding (singleton)
+import Ideas.Common.Rewriting.AC
+import Ideas.Common.Traversal.Navigator
+import Ideas.Common.Utils
+
+consequenceExercise :: Exercise Proof
+consequenceExercise = makeExercise
+   { exerciseId     = describe "Prove that formula is a logical consequence of a set of formulas" $
+                         propositionalId # "consequence"
+   , status         = Experimental
+   , parser         = mapSecond makeProof . parseConsequence False
+   , prettyPrinter  = showProof
+   , equivalence    = equivalentProofs
+   , similarity     = similarProofs
+   , suitable       = predicate suitableProof
+   , ready          = predicate readyProof
+   , strategy       = proofStrategy
+--   , extraRules     = map use extraLogicRules ++ map use buggyRules
+   , navigation     = termNavigator
+   , examples       = exampleProofs
+   }
+
+-- (assumptions, consequence)
+type Proof = Logic ([SLogic], SLogic)
+
+makeProof :: ([SLogic], SLogic) -> Proof
+makeProof = Var
+
+proofPair :: Proof -> ([SLogic], SLogic)
+proofPair x = (map catLogic $ sequenceA (fmap fst x), catLogic (fmap snd x))
+
+initial :: Ref Term
+initial = makeRef "initial"
+
+onAssumption :: (IsStrategy f, Navigator a) => f a -> Strategy a
+onAssumption s = ruleDown <*> ruleDown <*> s <*> ruleUp <*> ruleUp
+
+onConsequence :: (IsStrategy f, Navigator a) => f a -> Strategy a
+onConsequence s = ruleDownLast <*> s <*> ruleUp
+
+getInitial :: Context Proof -> Maybe [SLogic]
+getInitial ctx =
+   ((initial ? ctx) >>= fromTerm)
+    `mplus`
+   fmap (fst . proofPair) (fromContext ctx)
+
+showProof :: Proof -> String
+showProof proof =
+   let (ps, q) = proofPair proof
+   in intercalate ", " (map ppLogicPars ps) ++ " => " ++ ppLogicPars q
+
+equivalentProofs :: Context Proof -> Context Proof -> Bool
+equivalentProofs c1 c2 = fromMaybe False $ do
+   as1     <- getInitial c1
+   as2     <- getInitial c2
+   (ps, p) <- fmap proofPair (fromContext c1)
+   (qs, q) <- fmap proofPair (fromContext c2)
+   return $ ands as1 === ands as2
+         && ands as1 ==> ands ps
+         && ands as2 ==> ands qs
+         && (ands ps :->: p) <=> (ands qs :->: q)
+         && p === q
+
+similarProofs :: Context Proof -> Context Proof -> Bool
+similarProofs c1 c2 = fromMaybe False $ do
+   as1     <- getInitial c1
+   as2     <- getInitial c2
+   (ps, p) <- fmap proofPair (fromContext c1)
+   (qs, q) <- fmap proofPair (fromContext c2)
+   let f = sort . map normalizeLogicA
+   return $ as1 == as2
+         && f ps == f qs
+         && equalLogicA p q
+
+suitableProof :: Proof -> Bool
+suitableProof proof =
+   let (ps, p) = proofPair proof
+   in ands ps ==> p && p `notElem` ps
+
+readyProof :: Proof -> Bool
+readyProof proof =
+   case proofPair proof of
+      ([p], q) -> equalLogicA p q
+      _ -> False
+
+readyProofC :: Context Proof -> Bool
+readyProofC = maybe False readyProof . fromContext
+
+proofStrategy :: LabeledStrategy (Context Proof)
+proofStrategy = label "consequence" $
+   keepInitialAssumptions
+   <*> try (use conjIntro)
+       -- use cnf for the (singleton) assumption
+   <*> repeatS (somewhere (use topIsAnd)) -- topIsAndCom
+   <*> onAssumption (useC cnfStrategyDWA)
+       -- use cnf for the consequence
+   <*> onConsequence (useC cnfStrategyDWA)
+       -- strong normalization of assumption and consequence
+   <*> repeatS (somewhere (use absorptionSubset <|> use fakeAbsorption <|> use fakeAbsorptionNot))
+   <*> repeatS (somewhere splitTop)
+   <*> use checkCNF <*> normStrategy
+ where
+   splitTop = use topIsAnd |> use topIsAndCom
+
+checkCNF :: Rule Proof
+checkCNF = minor $ makeRule "is-cnf" $ \proof -> do
+   let (ps, p) = proofPair proof
+   guard (length ps == 1 && isCNF (head ps) && isCNF p)
+   Just proof
+
+-- strong normalization for CNF
+normStrategy :: Strategy (Context Proof)
+normStrategy = untilS readyProofC $
+      use assumptionIsFalse
+   |> use conjElim
+   |> use comAndSubset
+   |> somewhere (use ruleFalseZeroAnd <|> use ruleTrueZeroOr)
+   |> somewhere (use ruleComplOr)
+   |> somewhere (
+         use ruleIdempOr   <|>
+         use ruleIdempAnd  <|>
+         use ruleOrOverAnd <|>
+         use ruleTrueZeroAnd
+      )
+   |> oncetd (use sortRuleOr)
+   |> oncetd (use sortRuleAnd)
+   -- |> oncetd eliminateVar
+   |> somewhereConjunct introduceVar
+
+keepInitialAssumptions :: Rule (Context Proof)
+keepInitialAssumptions = minorRule "initial" $ \ctx -> do
+   (ps, _) <- fmap proofPair (fromContext ctx)
+   Just $ insertRef initial (toTerm ps) ctx
+
+assumptionIsFalse :: Rule Proof
+assumptionIsFalse = makeRule "assump-false" $ \proof ->
+   case proofPair proof of
+      ([F], q) -> Just (makeProof ([F :&&: q], q))
+      _        -> Nothing
+
+comAndSubset :: Rule Proof
+comAndSubset = makeRule "command-subset" $ \proof -> do
+   let (ps, q) = proofPair proof
+   p <- singleton ps
+   let cps = conjunctions p
+       cqs = conjunctions q
+       (cps1, cps2) = partition (\x -> any (equalLogicA x) cqs) cps
+   guard (p /= q && cps /= (cqs++cps2))
+   guard (all (\x -> any (equalLogicA x) cps1) cqs)
+   Just (makeProof ([ands (cqs++cps2)], q))
+
+conjElim :: Rule Proof
+conjElim = makeRule "conj-elim" $ \proof -> do
+   let (ps, q) = proofPair proof
+   p <- singleton ps
+   let cps = conjunctions p
+       cqs = conjunctions q
+   guard (p /= q && ( isPrefixOfWith equalLogicA cqs cps
+                   || isSuffixOfWith equalLogicA cqs cps))
+   Just (makeProof ([q], q))
+
+conjIntro :: Rule Proof
+conjIntro = makeRule "conj-intro" (f . proofPair)
+ where
+   f (ps, q) | length ps > 1 =
+      Just (makeProof ([ands ps], q))
+   f _ = Nothing
+
+-- eliminate a variable in the assumption
+{-
+eliminateVar :: Strategy (Context Proof)
+eliminateVar =  check superfluous
+            <*> (liftToContext $ makeRule "jippie" (\_ -> Just $ makeProof ([pp], pp)))
+ where
+   pp = Var (ShowString "b")
+
+superfluous :: Context Proof -> Bool
+superfluous = isJust . superfluousVar
+
+superfluousVar :: Context Proof -> Maybe ShowString
+superfluousVar cp =
+   case currentTerm cp >>= fromTerm of
+      Just (ps, q) -> listToMaybe (nub (concatMap varsLogic ps) \\ varsLogic q)
+      _ -> Nothing -}
+
+introduceVar :: Strategy (Context Proof)
+introduceVar =  check missing
+            <*> use introFalseLeft
+            <*> introCompl
+
+missing :: Context Proof -> Bool
+missing = isJust . missingVar
+
+-- The variables in the current subproof
+globalVars :: Context Proof -> [ShowString]
+globalVars cp =
+   case currentTerm cp >>= fromTerm of
+      Just (ps, q) -> nub (concatMap varsLogic (q:ps))
+      _ -> maybe [] globalVars (up cp)
+
+missingVar :: Context Proof -> Maybe ShowString
+missingVar cp =
+   case currentTerm cp >>= fromTerm of
+      Just p  -> listToMaybe (globalVars cp \\ varsLogic p)
+      Nothing -> Nothing
+
+introFalseLeft :: Rule SLogic
+introFalseLeft = rewriteRule "IntroFalseLeft" $
+   \x -> x  :~>  F :||: x
+
+introCompl :: Rule (Context Proof)
+introCompl = makeRule "IntroCompl" $ \cp -> do
+   a <- missingVar cp -- focus is on conjunct
+   let f = fromTerm >=> fmap toTerm . introContradiction a
+   changeTerm f cp
+ where
+   introContradiction :: a -> Logic a -> Maybe (Logic a)
+   introContradiction a F = Just (Var a :&&: Not (Var a))
+   introContradiction a (p :||: q) =
+      fmap (:||: q) (introContradiction a p) `mplus`
+      fmap (p :||:) (introContradiction a q)
+   introContradiction _ _ = Nothing
+
+-- let op: ook commutatieve variant nog toevoegen
+topIsAnd :: Rule Proof
+topIsAnd = {- minor $                !!!!!!!!!!!!!!!!!!!!!-}
+   ruleTrans "top-is-and" $ acTopRuleFor False (collect andView)
+
+topIsAndCom :: Rule Proof
+topIsAndCom = ruleTrans "top-is-and.com" $ acTopRuleFor True (collect andView)
+
+acTopRuleFor :: Bool -> (forall a . Isomorphism (Logic a) [Logic a])
+             -> Transformation Proof
+acTopRuleFor com ep = makeTrans $ \proof -> do
+   (ps, q) <- maybeToList (getSingleton proof)
+   guard (length ps == 1)
+   let pair = (head ps, q)
+       pairings = if com then pairingsAC else pairingsA
+       ep2 = ep *** ep
+       (xs, ys) = from ep2 pair
+   guard (length xs > 1 && length ys > 1)
+   zs <- liftM (map (to ep2)) (pairings False xs ys)
+   guard (all (uncurry (==>)) zs)
+   return (to ep [ Var ([x], y) | (x, y) <- zs])
+
+-- see somewhereDisjunct in Proofs
+somewhereConjunct :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof)
+somewhereConjunct s = somewhere (check isPair <*> onPair)
+ where
+   isPair ctx = case currentTerm ctx of
+                   Just (TList [_, _]) -> True
+                   _ -> False
+   onPair =
+          onAssumption  (somewhereAndG s) -- conjunct in assumption
+      <|> onConsequence (somewhereAndG s) -- conjunct in consequence
+
+somewhereAndG :: IsStrategy g => g (Context a) -> Strategy (Context a)
+somewhereAndG s =
+   let curIsAnd a = case currentTerm a >>= (fromTerm :: Term -> Maybe SLogic) of
+                       Just (_ :&&: _) -> True
+                       _               -> False
+   in fix $ \this -> check (Prelude.not . curIsAnd) <*> s
+                 <|> check curIsAnd <*> layer [] this
+
+exampleProofs :: Examples Proof
+exampleProofs =
+   [ easy      [p :&&: Not p] q
+   , medium    [p :->: q, p :->: Not q] (Not p)
+   , medium    [Not p :->: Not q, q] p
+   , difficult [p :->: q, r :->: s] ((p :&&: r) :->: (q :&&: s))
+   , difficult [Not r :<->: q] (p :->: (q :||: r))
+   , medium    [p :->: q, p :->: r] (p :->: (q :&&: r))
+   , medium    [p :->: q, q :->: r] (p :->: r)
+   , medium    [p :->: (q :->: r), q] (p :->: r)
+   -- , medium    [p :->: (q :->: p)] p
+   , difficult [p :->: (q :&&: r)] ((p :&&: q) :<->: (p :&&: r))
+   , difficult [p :<->: r, q :<->: s] ((p :->: q) :<->: (r :->: s))
+   , difficult [p :<->: r, q :<->: s] ((p :&&: q) :<->: (r :&&: s))
+   , difficult [p :<->: r, q :<->: s] ((p :||: q) :<->: (r :||: s))
+   , difficult [q :<->: s] ((p :&&: q) :<->: (p :&&: s))
+   , easy      [p :->: (p :->: q), p] q
+   , easy      [p :->: q, p] q
+   , easy      [p :||: (q :&&:r)] (Not p :->: r)
+   , easy      [p :->: q, Not q] (Not p)
+   , difficult [q] ((p :&&: q) :<->: p)
+   , difficult [Not q] ((p :||: q) :<->: p)
+   , difficult [p :<->: q, p] q
+   , difficult [p :<->: q, Not p] (Not q)
+   , medium    [q] (p :->: (p :&&:q))
+   , medium    [Not q] ((p :||: q) :->: p)
+   , medium    [Not q, p :||: q] p
+   ]
+ where
+   easy      = make Easy
+   medium    = make Medium
+   difficult = make Difficult
+
+   make dif ps consq = (dif, makeProof (ps, consq))
+
+   p = Var (ShowString "p")
+   q = Var (ShowString "q")
+   s = Var (ShowString "s")
+   r = Var (ShowString "r")
+
+isPrefixOfWith, isSuffixOfWith :: (a -> a -> Bool) -> [a] -> [a] -> Bool
+isPrefixOfWith _ [] _ = True
+isPrefixOfWith _ _ [] = False
+isPrefixOfWith eq (x:xs) (y:ys) = eq x y && isPrefixOfWith eq xs ys
+
+isSuffixOfWith eq xs ys = isPrefixOfWith eq (reverse xs) (reverse ys)
+
+singleton :: [a] -> Maybe a
+singleton [x] = Just x
+singleton _   = Nothing
+
+-- debug
+{-
+vb :: Proof
+Right vb = parseConsequence False "p -> q, r -> s => \
+    \(~p || q || ~r || s) /\\ (~p || q || ~r || ~s) /\\ (~p || ~q || ~r || s) /\\ (p || q || ~r || s) =>\
+    \(~p || q || ~r || s) /\\ (~p || q || ~r || ~s) /\\ (~p || q || ~r || s)"
+-}
+
+-- (p \/ q) /\ ... /\ (p \/ q \/ r)    ~> (p \/ q) /\ ...
+--    (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes)
+absorptionSubset :: Rule SLogic
+absorptionSubset = ruleList "absorptionSubset" $ \p -> do
+   let xss = map disjunctions (conjunctions p)
+       yss = nub $ filter (\xs -> all (ok xs) xss) xss
+       ok xs ys = not (ys `isSubsetOf` xs) || xs == ys
+   guard (length yss < length xss)
+   return $ ands (map ors yss)
+
+-- p /\ ... /\ (~p \/ q \/ r)  ~> p /\ ... /\ (q \/ r)
+--    (p is hier een losse variabele)
+fakeAbsorption :: Rule SLogic
+fakeAbsorption = makeRule "fakeAbsorption" $ \p -> do
+   let xs = conjunctions p
+   v <- [ a | a@(Var _) <- xs ]
+   let ys  = map (ors . filter (/= Not v) . disjunctions) xs
+       new = ands ys
+   guard (p /= new)
+   return new
+
+-- ~p /\ ... /\ (p \/ q \/ r)  ~> ~p /\ ... /\ (q \/ r)
+--   (p is hier een losse variabele)
+fakeAbsorptionNot :: Rule SLogic
+fakeAbsorptionNot = makeRule "fakeAbsorptionNot" $ \p -> do
+   let xs = conjunctions p
+   v <- [ a | Not a@(Var _) <- xs ]
+   let ys  = map (ors . filter (/= v) . disjunctions) xs
+       new = ands ys
+   guard (p /= new)
+   return new
src/Domain/Logic/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- A set of example proofs
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Examples
    ( exampleProofs
    ) where
@@ -21,40 +23,41 @@ 
 exampleProofs :: [(Difficulty, (SLogic, SLogic))]
 exampleProofs =
-   [ {-  1 -} ok        (Not(p :||: (Not p :&&: q)), Not(p :||: q))
-   , {-  2 -} ok        ((p :->: q):||: Not p, (p :->: q) :||: q)
+   [ {-  1 -} medium    (Not(p :||: (Not p :&&: q)), Not(p :||: q))
+   , {-  2 -} medium    ((p :->: q):||: Not p, (p :->: q) :||: q)
    , {-  3 -} difficult ((p :&&: Not q):||:(q :&&: Not p), (p :||:q):&&:Not(p :&&: q))
-   , {-  4 -} ok        (Not(p :||: Not(p :||: Not q)), Not(p :||: q))
+   , {-  4 -} medium    (Not(p :||: Not(p :||: Not q)), Not(p :||: q))
    , {-  5 -} difficult (p :<->: q, (p :->: q) :&&: (q :->: p))
-   , {-  6 -} ok        ((p :&&: q) :->: p, T)
-   , {-  7 -} ok        ((p :->: q) :||: (q :->: p), T)
+   , {-  6 -} medium    ((p :&&: q) :->: p, T)
+   , {-  7 -} medium    ((p :->: q) :||: (q :->: p), T)
    , {-  8 -} difficult ((q :->: (Not p :->: q)) :->: p, Not p :->: (q :&&: ((p :&&: q) :&&: q)))
-   , {-  9 -} ok        ((p :->: Not q):->:q, (s :||:(s :->:(q :||: p))) :&&: q)
+   , {-  9 -} medium    ((p :->: Not q):->:q, (s :||:(s :->:(q :||: p))) :&&: q)
    , {- 10 -} difficult (p :->: (q :->: r), (p :->: q) :->: (p :->:r))
    , {- 11 -} difficult (Not((p :->: q) :->: Not(q :->: p)), p :<->: q)
-   , {- 12 -} ok        ((p :->: q):->: (p :->: s), (Not q :->: Not p) :->: (Not s :->: Not p))
-   , {- 13 -} ok        (Not((p :->:q) :->: (p:&&:q)), (p :->: q) :&&: (Not p :||: Not q))
-   , {- 14 -} ok        (Not((p :<->: q) :->: (p :||: (p :<->: q))), F)
+   , {- 12 -} medium    ((p :->: q):->: (p :->: s), (Not q :->: Not p) :->: (Not s :->: Not p))
+   , {- 13 -} medium    (Not((p :->:q) :->: (p:&&:q)), (p :->: q) :&&: (Not p :||: Not q))
+   , {- 14 -} medium    (Not((p :<->: q) :->: (p :||: (p :<->: q))), F)
    , {- 15 -} easy      (q :&&: p, p :&&: (q :||: q))
    , {- 16 -} easy      (Not(p :&&: q) :||: (s :||: Not r), (p :&&: q) :->: (r :->: s))
    , {- 17 -} easy      (Not(Not p :&&: Not(q :||: r)),  p :||: (q :||: r))
    , {- 18 -} easy      (Not (p :&&: (q :||: r)), Not p :||: (Not q :&&: Not r))
    , {- 19 -} easy      (p :&&: q, Not(p :->: Not q))
    , {- 20 -} difficult (p :<->: (q :<->: p),q)
-   , {- 21 -} ok        ((p :->: q) :->: Not p, (p :->: (q :->: Not p)))
-   , {- 22 -} ok        ((Not q :&&: p) :->: p, (Not q :<->: q) :->: p)
+   , {- 21 -} medium    ((p :->: q) :->: Not p, p :->: (q :->: Not p))
+   , {- 22 -} medium    ((Not q :&&: p) :->: p, (Not q :<->: q) :->: p)
    , {- 23 -} easy      (p :<->: q, Not p :<->: Not q)
    , {- 24 -} difficult ((p :->: q) :<->: (p :->: r), (p :->: (q :&&: r)) :||: Not(p :->: (q :||: r)))
-   , {- 25 -} ok        ((p :<->: (p :&&: q), p :->: q))
-   , {- 26 -} ok        (p :<->: (p :->: q), p :&&: q)
-   , {- 27 -} ok        ((p :->: q ) :&&: (r :->: q), (p :||: r) :->: q)
+   , {- 25 -} medium    (p :<->: (p :&&: q), p :->: q)
+   , {- 26 -} medium    (p :<->: (p :->: q), p :&&: q)
+   , {- 27 -} medium    ((p :->: q ) :&&: (r :->: q), (p :||: r) :->: q)
    , {- 28 -} difficult ((p :&&: (q :&&: r)) :||: (Not p :&&: q), (Not p :&&: (q :&&: Not r)) :||: ( q :&&: r))
    , {- 29 -} difficult (p :||: (q :&&: r), ( p :&&: Not q) :||: ( p :&&: Not r):||: ( q :&&: r))
    , {- 30 -} difficult ((p :&&: q) :||: (Not q :&&: r), ( p :&&: r) :||: ( p :&&: q :&&: Not r):||: (Not p :&&: Not q :&&: r))
+   , {- 31 -} medium    (p :&&: (q :||: s), (q :&&: Not s :&&: p) :||: (p :&&: s))
    ]
  where
    easy      x = (Easy, x)
-   ok        x = (Medium, x)
+   medium    x = (Medium, x)
    difficult x = (Difficult, x)
 
    p = Var (ShowString "p")
src/Domain/Logic/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,17 +12,23 @@ -- "Discrete Wiskunde A (DWA)"
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Exercises
-   ( dnfExercise, dnfUnicodeExercise
+   ( dnfExercise, dnfUnicodeExercise, cnfUnicodeExercise
+   , extraLogicRules
    ) where
 
 import Data.Maybe
 import Domain.Logic.BuggyRules
 import Domain.Logic.Formula
+import Domain.Logic.GeneralizedRules
 import Domain.Logic.Generator
+import Domain.Logic.InverseRules
 import Domain.Logic.Parser
 import Domain.Logic.Rules
 import Domain.Logic.Strategies
+import Domain.Logic.Utils
 import Ideas.Common.Library
 import Test.QuickCheck
 
@@ -30,43 +36,77 @@ dnfExercise :: Exercise SLogic
 dnfExercise = makeExercise
    { exerciseId     = describe "Proposition to DNF" $
-                         newId "logic.propositional.dnf"
+                         propositionalId # "dnf"
    , status         = Stable
    , parser         = parseLogicPars
    , prettyPrinter  = ppLogicPars
    , equivalence    = withoutContext eqLogic
    , similarity     = withoutContext equalLogicA
    , ready          = predicate isDNF
-   , suitable       = predicate mySuitable
+   , suitable       = predicate notTooManyEquivs
    , extraRules     = map liftToContext (extraLogicRules ++ buggyRules)
    , strategy       = dnfStrategyDWA
    , navigation     = navigator
-   , testGenerator  = Just (restrictGenerator mySuitable arbitrary)
-   , randomExercise = useGenerator (const True) logicExercise
+   , testGenerator  = Just (arbitrary `suchThat` notTooManyEquivs)
+   , randomExercise = useGenerator dnfExerciseGenerator
    }
 
 -- Direct support for unicode characters
 dnfUnicodeExercise :: Exercise SLogic
 dnfUnicodeExercise = dnfExercise
    { exerciseId    = describe "Proposition to DNF (unicode support)" $
-                        newId "logic.propositional.dnf.unicode"
+                        propositionalId # "dnf.unicode"
    , parser        = parseLogicUnicodePars
    , prettyPrinter = ppLogicUnicodePars
    }
 
-logicExercise :: Maybe Difficulty -> Gen SLogic
-logicExercise mdif =
-   let (gen, (minStep, maxStep)) = generateLevel (fromMaybe Medium mdif)
-       ok p = let i = fromMaybe maxBound (stepsRemaining maxStep p)
-              in countEquivalences p <= 2 && i >= minStep && i <= maxStep
-   in restrictGenerator ok gen
+cnfUnicodeExercise :: Exercise SLogic
+cnfUnicodeExercise = makeExercise
+   { exerciseId     = describe "Proposition to CNF (unicode support)" $
+                         propositionalId # "cnf.unicode"
+   , status         = Stable
+   , parser         = parseLogicUnicodePars
+   , prettyPrinter  = ppLogicUnicodePars
+   , equivalence    = withoutContext eqLogic
+   , similarity     = withoutContext equalLogicA
+   , ready          = predicate isCNF
+   , suitable       = predicate notTooManyEquivs
+   , extraRules     = map liftToContext (extraLogicRules ++ buggyRules)
+   , strategy       = cnfStrategyDWA
+   , navigation     = navigator
+   , testGenerator  = Just (arbitrary `suchThat` notTooManyEquivs)
+   , randomExercise = useGenerator cnfExerciseGenerator
+   }
 
-mySuitable :: SLogic -> Bool
-mySuitable = (<=2) . countEquivalences
+extraLogicRules :: [Rule SLogic]
+extraLogicRules =
+   [ ruleCommOr, ruleCommAnd, ruleAssocOr, ruleAssocAnd
+   , generalRuleOrOverAnd, ruleOrOverAnd
+   , inverseDeMorganOr, inverseDeMorganAnd
+   , inverseAndOverOr, inverseOrOverAnd
+   -- Rules that are NOT allowed in DWA
+   -- , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl
+   -- , ruleCommEquiv, ruleDefEquivImpls, ruleEquivSame, ruleImplSame
+   ]
 
-stepsRemaining :: Int -> SLogic -> Maybe Int
-stepsRemaining i =
-   lengthMax i . derivationTree False dnfStrategyDWA . inContext dnfExercise
+notTooManyEquivs :: SLogic -> Bool
+notTooManyEquivs = (<=2) . countEquivalences
+
+dnfExerciseGenerator :: Maybe Difficulty -> Gen SLogic
+dnfExerciseGenerator = exerciseGeneratorFor dnfExercise
+
+cnfExerciseGenerator :: Maybe Difficulty -> Gen SLogic
+cnfExerciseGenerator = exerciseGeneratorFor cnfUnicodeExercise
+
+exerciseGeneratorFor :: Exercise SLogic -> Maybe Difficulty -> Gen SLogic
+exerciseGeneratorFor ex mdif =
+   let (gen, (minStep, maxStep)) = generateLevel (fromMaybe Medium mdif)
+       ok p = let i = fromMaybe maxBound (stepsRemaining maxStep p)
+              in notTooManyEquivs p && i >= minStep && i <= maxStep
+   in gen `suchThat` ok
+ where
+   stepsRemaining i =
+      lengthMax i . derivationTree (strategy ex) . inContext ex
 
 -- QuickCheck property to monitor the number of steps needed
 -- to normalize a random proposition (30-40% is ok)
src/Domain/Logic/Formula.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,9 +9,10 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Formula.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Formula
-   ( module Domain.Logic.Formula
-   , conjunctions, disjunctions, ors, ands
+   ( module Domain.Logic.Formula, module Ideas.Common.Algebra.Boolean
    ) where
 
 import Control.Applicative
@@ -137,6 +138,13 @@  where
    xs = varsLogic p `union` varsLogic q
    fs = map (flip elem) (subsets xs)
+
+tautology :: Eq a => Logic a -> Bool
+tautology = eqLogic T
+
+isNot :: Logic a -> Bool
+isNot (Not _) = True
+isNot _       = False
 
 -- | A Logic expression is atomic if it is a variable or a constant True or False.
 isAtomic :: Logic a -> Bool
src/Domain/Logic/GeneralizedRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,96 +11,26 @@ -- Generalized rules, and inverse rules, for De Morgan and distributivity
 --
 -----------------------------------------------------------------------------
+--  $Id: GeneralizedRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.GeneralizedRules
    ( generalRuleDeMorganOr, generalRuleDeMorganAnd
    , generalRuleAndOverOr, generalRuleOrOverAnd
-   , inverseDeMorganOr, inverseDeMorganAnd
-   , inverseAndOverOr, inverseOrOverAnd
    ) where
 
 -- Note: the generalized rules do not take AC-unification into account,
 -- and perhaps they should.
 import Control.Monad
 import Domain.Logic.Formula
+import Domain.Logic.Utils
 import Ideas.Common.Library
-import qualified Ideas.Common.Library as C
 
-makeSimpleRule :: String -> (a -> Maybe a) -> Rule a
-makeSimpleRule s = C.makeRule ("logic.propositional." ++ s)
-
 -----------------------------------------------------------------------------
--- Inverse rules
-
--- generalized (works for multiple terms)
-inverseDeMorganOr :: Rule SLogic
-inverseDeMorganOr = makeSimpleRule "InvDeMorganOr" $ \p -> do
-   let xs = conjunctions p
-   guard (length xs > 1)
-   ys <- mapM isNot xs
-   return (Not $ ors ys)
-
--- generalized (works for multiple terms)
-inverseDeMorganAnd :: Rule SLogic
-inverseDeMorganAnd = makeSimpleRule "InvDeMorganAnd" $ \p -> do
-   let xs = disjunctions p
-   guard (length xs > 1)
-   ys <- mapM isNot xs
-   return (Not $ ands ys)
-
-inverseAndOverOr :: Rule SLogic
-inverseAndOverOr = makeSimpleRule "InvAndOverOr" $ \p -> do
-   let xs = disjunctions p
-   guard (length xs > 1)
-   do pairs <- mapM isAndHead xs
-      let (as, ys) = unzip pairs
-      guard (allSame as)
-      return (head as :&&: ors ys)
-    `mplus` do
-      pairs <- mapM isAndLast xs
-      let (ys, as) = unzip pairs
-      guard (allSame as)
-      return (ors ys :&&: head as)
-
-inverseOrOverAnd :: Rule SLogic
-inverseOrOverAnd = makeSimpleRule "InvOrOverAnd" $ \p -> do
-   let xs = conjunctions p
-   guard (length xs > 1)
-   do pairs <- mapM isOrHead xs
-      let (as, ys) = unzip pairs
-      guard (allSame as)
-      return (head as :||: ands ys)
-    `mplus` do
-      pairs <- mapM isOrLast xs
-      let (ys, as) = unzip pairs
-      guard (allSame as)
-      return (ands ys :||: head as)
-
-isNot :: SLogic -> Maybe SLogic
-isNot (Not p) = Just p
-isNot _       = Nothing
-
-isAndHead, isAndLast, isOrHead, isOrLast :: SLogic -> Maybe (SLogic, SLogic)
-isAndHead = useHead (:&&:) . conjunctions
-isAndLast = useLast (:&&:) . conjunctions
-isOrHead  = useHead (:||:) . disjunctions
-isOrLast  = useLast (:||:) . disjunctions
-
-useHead, useLast :: (a -> a -> a) -> [a] -> Maybe (a, a)
-useHead op (x:xs) | not (null xs) =
-   Just (x, foldr1 op xs)
-useHead _ _ = Nothing
-
-useLast op = fmap (\(x, y) -> (y, x)) . useHead (flip op) . reverse
-
-allSame :: Eq a => [a] -> Bool
-allSame []     = True
-allSame (x:xs) = all (==x) xs
-
------------------------------------------------------------------------------
 -- Generalized rules
 
 generalRuleDeMorganOr :: Rule SLogic
-generalRuleDeMorganOr = makeSimpleRule "GenDeMorganOr" f
+generalRuleDeMorganOr =
+   siblingOf groupDeMorgan $ makeSimpleRule "GenDeMorganOr" f
  where
    f (Not e) = do
       let xs = disjunctions e
@@ -109,7 +39,8 @@    f _ = Nothing
 
 generalRuleDeMorganAnd :: Rule SLogic
-generalRuleDeMorganAnd = makeSimpleRule "GenDeMorganAnd" f
+generalRuleDeMorganAnd =
+   siblingOf groupDeMorgan $ makeSimpleRule "GenDeMorganAnd" f
  where
    f (Not e) = do
       let xs = conjunctions e
@@ -118,7 +49,8 @@    f _ = Nothing
 
 generalRuleAndOverOr :: Rule SLogic
-generalRuleAndOverOr = makeSimpleRule "GenAndOverOr" f
+generalRuleAndOverOr =
+   siblingOf groupDistribution $ makeSimpleRule "GenAndOverOr" f
  where
    f (x :&&: y) =
       case (disjunctions x, disjunctions y) of
@@ -130,7 +62,8 @@    f _ = Nothing
 
 generalRuleOrOverAnd :: Rule SLogic
-generalRuleOrOverAnd = makeSimpleRule "GenOrOverAnd" f
+generalRuleOrOverAnd =
+   siblingOf groupDistribution $ makeSimpleRule "GenOrOverAnd" f
  where
    f (x :||: y) =
       case (conjunctions x, conjunctions y) of
src/Domain/Logic/Generator.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,8 +10,11 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Generator.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Generator
    ( generateLogic, generateLevel, equalLogicA, equalLogicACI
+   , normalizeLogicA
    ) where
 
 import Control.Monad
@@ -29,12 +32,14 @@ 
 -- | Equality modulo associativity of operators
 equalLogicA :: Eq a => Logic a -> Logic a -> Bool
-equalLogicA = (==) `on` rec
- where
-   rec a = case a of
-              _ :&&: _ -> ands (map rec (conjunctions a))
-              _ :||: _ -> ors  (map rec (disjunctions a))
-              _        -> descend rec a
+equalLogicA = (==) `on` normalizeLogicA
+
+normalizeLogicA :: Logic a -> Logic a
+normalizeLogicA a =
+   case a of
+      _ :&&: _ -> ands (map normalizeLogicA (conjunctions a))
+      _ :||: _ -> ors  (map normalizeLogicA (disjunctions a))
+      _        -> descend normalizeLogicA a
 
 -- | Equality modulo associativity/commutativity/idempotency of operators,
 --   and there units/absorbing elements
+ src/Domain/Logic/InverseRules.hs view
@@ -0,0 +1,94 @@+-----------------------------------------------------------------------------
+-- Copyright 2014, 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)
+--
+-- Generalized rules, and inverse rules, for De Morgan and distributivity
+--
+-----------------------------------------------------------------------------
+--  $Id: InverseRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
+module Domain.Logic.InverseRules
+   ( inverseDeMorganOr, inverseDeMorganAnd
+   , inverseAndOverOr, inverseOrOverAnd
+   ) where
+
+-- Note: the generalized rules do not take AC-unification into account,
+-- and perhaps they should.
+import Control.Monad
+import Domain.Logic.Formula
+import Domain.Logic.Utils
+import Ideas.Common.Library
+
+-----------------------------------------------------------------------------
+-- Inverse rules
+
+-- generalized (works for multiple terms)
+inverseDeMorganOr :: Rule SLogic
+inverseDeMorganOr = siblingOf groupDeMorgan $
+   makeSimpleRule "InvDeMorganOr" $ \p -> do
+      let xs = conjunctions p
+      guard (length xs > 1)
+      ys <- mapM isComplement xs
+      return (Not $ ors ys)
+
+-- generalized (works for multiple terms)
+inverseDeMorganAnd :: Rule SLogic
+inverseDeMorganAnd = siblingOf groupDeMorgan $
+   makeSimpleRule "InvDeMorganAnd" $ \p -> do
+      let xs = disjunctions p
+      guard (length xs > 1)
+      ys <- mapM isComplement xs
+      return (Not $ ands ys)
+
+inverseAndOverOr :: Rule SLogic
+inverseAndOverOr = siblingOf groupDistribution $
+   makeSimpleRule "InvAndOverOr" $ \p -> do
+      let xs = disjunctions p
+      guard (length xs > 1)
+      do pairs <- mapM isAndHead xs
+         let (as, ys) = unzip pairs
+         guard (allSame as)
+         return (head as :&&: ors ys)
+       `mplus` do
+         pairs <- mapM isAndLast xs
+         let (ys, as) = unzip pairs
+         guard (allSame as)
+         return (ors ys :&&: head as)
+
+inverseOrOverAnd :: Rule SLogic
+inverseOrOverAnd = siblingOf groupDistribution $
+   makeSimpleRule "InvOrOverAnd" $ \p -> do
+      let xs = conjunctions p
+      guard (length xs > 1)
+      do pairs <- mapM isOrHead xs
+         let (as, ys) = unzip pairs
+         guard (allSame as)
+         return (head as :||: ands ys)
+       `mplus` do
+         pairs <- mapM isOrLast xs
+         let (ys, as) = unzip pairs
+         guard (allSame as)
+         return (ands ys :||: head as)
+
+isAndHead, isAndLast, isOrHead, isOrLast :: SLogic -> Maybe (SLogic, SLogic)
+isAndHead = useHead (:&&:) . conjunctions
+isAndLast = useLast (:&&:) . conjunctions
+isOrHead  = useHead (:||:) . disjunctions
+isOrLast  = useLast (:||:) . disjunctions
+
+useHead, useLast :: (a -> a -> a) -> [a] -> Maybe (a, a)
+useHead op (x:xs) | not (null xs) =
+   Just (x, foldr1 op xs)
+useHead _ _ = Nothing
+
+useLast op = fmap (\(x, y) -> (y, x)) . useHead (flip op) . reverse
+
+allSame :: Eq a => [a] -> Bool
+allSame []     = True
+allSame (x:xs) = all (==x) xs
src/Domain/Logic/Parser.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,8 +9,11 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Parser
    ( parseLogic, parseLogicPars, parseLogicUnicodePars, parseLogicProof
+   , parseConsequence
    , ppLogicPars, ppLogicUnicodePars
    ) where
 
@@ -43,12 +46,37 @@    maybe (parseSimple p input) (Left . show) (balanced [('(', ')')] input)
 
 parseLogicProof :: Bool -> String -> Either String (SLogic, SLogic)
-parseLogicProof unicode = parseSimple $ do
+parseLogicProof unicode input =
+   case balanced [('(',')')] input of
+      Just msg -> Left (show msg)
+      Nothing  -> case splitIs input of
+         Just (lhs, _) ->
+            case balanced [('(',')')] lhs of
+               Just e2 -> Left (show e2)
+               Nothing -> parseLogicProof2 unicode input
+         Nothing -> Left "Expecting =="
+
+splitIs :: String -> Maybe (String, String)
+splitIs = rec []
+ where
+   rec acc ('=':'=':xs) = Just (reverse acc, xs)
+   rec acc (x:xs)       = rec (x:acc) xs
+   rec _   []           = Nothing
+
+parseLogicProof2 :: Bool -> String -> Either String (SLogic, SLogic)
+parseLogicProof2 unicode = parseSimple $ do
    p <- parserSLogic unicode True
    reservedOp "=="
    q <- parserSLogic unicode True
    return (p, q)
 
+parseConsequence :: Bool -> String -> Either String ([SLogic], SLogic)
+parseConsequence unicode = parseSimple $ do
+   ps <- commaSep1 (parserSLogic unicode True)
+   reservedOp "=>"
+   q <- parserSLogic unicode True
+   return (ps, q)
+
 -- generalized parser
 parserSLogic :: Bool -> Bool -> Parser SLogic
 parserSLogic unicode extraPars = pLogic
@@ -86,7 +114,7 @@ lexer :: P.TokenParser a
 lexer = P.makeTokenParser $ emptyDef
    { reservedNames   = ["T", "F"]
-   , reservedOpNames = ["~", "<->", "->", "||", "/\\", "=="]
+   , reservedOpNames = ["~", "<->", "->", "||", "/\\", "==", "=>"]
    , identStart      = lower
    , identLetter     = lower
    , opStart         = fail ""
@@ -95,6 +123,9 @@ 
 reservedOp :: String -> Parser ()
 reservedOp = P.reservedOp lexer
+
+commaSep1 :: Parser a -> Parser [a]
+commaSep1 = P.commaSep1 lexer
 
 -----------------------------------------------------------
 --- Helper-functions for syntax warnings
src/Domain/Logic/Proofs.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE RankNTypes #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,8 +12,11 @@ -- Exercise for the logic domain: to prove two propositions equivalent
 --
 -----------------------------------------------------------------------------
+--  $Id: Proofs.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Proofs
    ( proofExercise, proofUnicodeExercise
+   , sortRuleOr, sortRuleAnd -- fix me
    ) where
 
 import Control.Arrow
@@ -24,16 +27,17 @@ import Data.Maybe
 import Domain.Logic.BuggyRules
 import Domain.Logic.Examples
+import Domain.Logic.Exercises
 import Domain.Logic.Formula
 import Domain.Logic.GeneralizedRules
 import Domain.Logic.Generator (equalLogicA)
+import Domain.Logic.InverseRules
 import Domain.Logic.Parser
 import Domain.Logic.Rules
 import Domain.Logic.Strategies (somewhereOr)
+import Domain.Logic.Utils
 import Domain.Math.Expr ()
-import Ideas.Common.Algebra.Boolean
 import Ideas.Common.Library
-import Ideas.Common.Rewriting.AC
 import Ideas.Common.Traversal.Navigator
 import Ideas.Common.Traversal.Utils
 import Ideas.Common.Utils
@@ -51,7 +55,7 @@ proofExercise :: Exercise Proof
 proofExercise = makeExercise
    { exerciseId     = describe "Prove two propositions equivalent" $
-                         newId "logic.proof"
+                         propositionalId # "proof"
    , status         = Experimental
    , parser         = mapSecond makeProof . parseLogicProof False
    , prettyPrinter  = showProof
@@ -68,7 +72,7 @@ proofUnicodeExercise :: Exercise Proof
 proofUnicodeExercise = proofExercise
    { exerciseId    = describe "Prove two propositions equivalent (unicode support)" $
-                        newId "logic.propositional.proof.unicode"
+                        propositionalId # "proof.unicode"
    , parser        = mapSecond makeProof . parseLogicProof True
    , prettyPrinter = showProofUnicode
    }
@@ -110,17 +114,45 @@ proofStrategy = label "proof equivalent" $
    repeatS (
          somewhere splitTop
-      -- somewhere (useC commonExprAtom)   -- (tijdelijk uitgezet)
+      -- disabled: first investigate how the common subexpressions should be
+      -- communicated to the client
+      -- |> somewhere commonExprAtom
       |> useC dnfStrategyDWA
+      |> commonLiteralSpecial
+      |> useC orToTop
+      |> (use checkDNF <*> commonLiteral)
       )
       <*> use checkDNF <*> normStrategy
  where
    splitTop =  use topIsNot  <|> use topIsImpl
                -- only use commutativity if not already in desired order
            <|> (use topIsAnd |> use topIsAndCom)
-           <|> (use topIsOr |> use topIsOrCom)
+           <|> (use topIsOr  |> use topIsOrCom)
            <|> use topIsEquiv
 
+commonLiteralSpecial :: Strategy (Context Proof)
+commonLiteralSpecial =
+   repeat1 (somewhere (use ruleCommonLiteralSpecialInFront))
+   <*>
+   repeat1 (somewhere (use ruleInvDistrCommonLiteral))
+   <*>
+   repeatS (somewhere (use topIsAnd))
+
+ruleCommonLiteralSpecialInFront :: Rule Proof
+ruleCommonLiteralSpecialInFront = makeRule "command.common-literal-special" f
+ where
+   f (Var eq) =
+      [ Var x | x <- maybeToList (findInFrontLeft eq) ] ++
+      [ Var (swap x) | x <- maybeToList (findInFrontLeft (swap eq)) ]
+   f _ = []
+
+   findInFrontLeft eq@(p1 :&&: p2, q)
+      | isAtomic p1 && isDNF p2 && all (`notElem` varsLogic p2) (varsLogic p1) && isDNF q = do
+           lit <- listToMaybe (findCommonLiteral (p1, q))
+           res <- inFrontLeft lit (swap eq)
+           return (swap res)
+   findInFrontLeft _ = Nothing
+
 checkDNF :: Rule Proof
 checkDNF = minor $ makeRule "is-dnf" $ \proof -> do
    guard $ and [ isDNF p && isDNF q | (p, q) <- subProofs proof ]
@@ -174,7 +206,6 @@       |> label "Sort and simplify"                   (sortAndSimplify |> deMorganAndSimplify)
       |> label "Eliminate implications/equivalences" eliminateImplEquiv
       |> label "Eliminate nots"                      eliminateNots
-      |> label "Move ors to top"                     orToTop
       )
  where
     toplevel = useRules
@@ -189,53 +220,49 @@        ]
     sortAndSimplify = somewhere $
            use ruleAbsorpOrNot
-       <|> (use sortForIdempOr  <*> try (use ruleIdempOr))
-       <|> (use sortForIdempAnd <*> try (use ruleIdempAnd))
-       <|> (use sortForComplOr  <*> try (use ruleComplOr))
-       <|> (use sortForComplAnd <*> try (use ruleComplAnd))
+       <|> use sortForIdempOr
+       <|> use sortForIdempAnd
+       <|> use sortForComplOr
+       <|> use sortForComplAnd
     deMorganAndSimplify = somewhere $
-           (use ruleDeMorganOrNot  <*> try (oncetd (use ruleNotNot)))
-       <|> (use ruleDeMorganAndNot <*> try (oncetd (use ruleNotNot)))
+           deMorganOrNot <|> deMorganAndNot
     eliminateImplEquiv =
-           oncetd (use ruleDefImpl)
-        |> oncebu (use ruleDefEquiv)
+           somewhere (use ruleDefImpl)  -- preference: top-down!
+        |> somewhere (use ruleDefEquiv) -- preference: bottom-up!
 
     eliminateNots = somewhere $ useRules
        [ generalRuleDeMorganAnd, generalRuleDeMorganOr
        , ruleDeMorganAnd, ruleDeMorganOr
        ]
-    orToTop = somewhere $ useRules
-       [ generalRuleAndOverOr, ruleAndOverOr ]
 
+orToTop :: LabeledStrategy (Context SLogic)
+orToTop = label "Move ors to top" $ somewhere $ useRules
+   [ generalRuleAndOverOr, ruleAndOverOr ]
+
 useRules :: [Rule SLogic] -> Strategy (Context SLogic)
 useRules = alternatives . map liftToContext
 
-{-
-normLogicRule :: Rule (SLogic, SLogic)
-normLogicRule = ruleMaybe "Normalize" $ \tuple@(p, q) -> do
-   guard (p /= q)
-   let xs  = sort (varsLogic p `union` varsLogic q)
-       new = (normLogicWith xs p, normLogicWith xs q)
-   guard (tuple /= new)
-   return new -}
-
 -- disabled for now
 
 -- Find a common subexpression that can be treated as a box
 {-
-commonExprAtom :: Rule (Context (SLogic, SLogic))
-commonExprAtom = minor $ ruleTrans "commonExprAtom" $ makeTransLiftContext $ \(p, q) -> do
-   let xs = filter (same <&&> complement isAtomic) (largestCommonSubExpr p q)
-       same cse = eqLogic (sub cse p) (sub cse q)
-       new = head (logicVars \\ (varsLogic p `union` varsLogic q))
-       sub a this
-          | a == this = Var new
-          | otherwise = descend (sub a) this
-   case xs of
-      hd:_ -> do
-         xs <- substRef :? []
-         substRef := (show new, show hd):xs
-         return (sub hd p, sub hd q)
+commonExprAtom :: Rule (Context Proof)
+commonExprAtom = minor $ ruleTrans "commonExprAtom" $ makeTransLiftContext $ \proof ->
+   case proof of
+      Var (p, q) -> do
+         sub <- substRef :? []
+         let xs = filter (same <&&> complement isAtomic) (largestCommonSubExpr p q)
+             same cse = eqLogic (substitute cse p) (substitute cse q)
+             used = varsLogic p `union` varsLogic q `union` map (ShowString . fst) sub
+             new  = head (logicVars \\ used)
+             substitute a this
+                | a == this = Var new
+                | otherwise = descend (substitute a) this
+         case xs of
+            hd:_ -> do
+               substRef := (show new, show hd):sub
+               return (Var (substitute hd p, substitute hd q))
+            _ -> fail "not applicable"
       _ -> fail "not applicable"
 
 largestCommonSubExpr :: (Uniplate a, Ord a) => a -> a -> [a]
@@ -251,19 +278,7 @@ logicVars :: [ShowString]
 logicVars = [ ShowString [c] | c <- ['a'..] ]
 -}
-
-{-
-normLogic :: Ord a => Logic a -> Logic a
-normLogic p = normLogicWith (sort (varsLogic p)) p
-
-normLogicWith :: Eq a => [a] -> Logic a -> Logic a
-normLogicWith xs p = make (filter keep (subsets xs))
- where
-   keep ys = evalLogic (`elem` ys) p
-   make = ors . map atoms
-   atoms ys = ands [ f (x `elem` ys) (Var x) | x <- xs ]
-   f b = if b then id else Not
--}
+--------------------------------------------------------------------
 
 -- p \/ q \/ ~p  ~>  reorder p and ~p
 sortForComplOr :: Rule SLogic
@@ -297,64 +312,41 @@    guard (xs /= ys && not (distinct xs))
    return (ands ys)
 
-{-
--- (p /\ q) \/ ... \/ (p /\ q /\ r)    ~> (p /\ q) \/ ...
---    (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes)
-absorptionSubset :: Rule SLogic
-absorptionSubset = ruleList "absorptionSubset" $ \p -> do
-   let xss = map conjunctions (disjunctions p)
-       yss = nub $ filter (\xs -> all (ok xs) xss) xss
-       ok xs ys = not (ys `isSubsetOf` xs) || xs == ys
-   guard (length yss < length xss)
-   return $ ors (map ands yss)
-
--- p \/ ... \/ (~p /\ q /\ r)  ~> p \/ ... \/ (q /\ r)
---    (p is hier een losse variabele)
-fakeAbsorption :: Rule SLogic
-fakeAbsorption = makeRule "fakeAbsorption" $ \p -> do
-   let xs = disjunctions p
-   v <- [ a | a@(Var _) <- xs ]
-   let ys  = map (ands . filter (/= Not v) . conjunctions) xs
-       new = ors ys
-   guard (p /= new)
-   return new
-
--- ~p \/ ... \/ (p /\ q /\ r)  ~> ~p \/ ... \/ (q /\ r)
---   (p is hier een losse variabele)
-fakeAbsorptionNot :: Rule SLogic
-fakeAbsorptionNot = makeRule "fakeAbsorptionNot" $ \p -> do
-   let xs = disjunctions p
-   v <- [ a | Not a@(Var _) <- xs ]
-   let ys  = map (ands . filter (/= v) . conjunctions) xs
-       new = ors ys
-   guard (p /= new)
-   return new -}
-
 acTopRuleFor :: Bool -> (forall a . Isomorphism (Logic a) [Logic a])
              -> Transformation Proof
-acTopRuleFor com ep = makeTrans $ \proof -> do
-   pair <- maybeToList (getSingleton proof)
-   let pairings = if com then pairingsAC else pairingsA
-       ep2 = ep *** ep
-       (xs, ys) = from ep2 pair
-   guard (length xs > 1 && length ys > 1)
-   xs <- liftM (map (to ep2)) (pairings False xs ys)
-   guard (all (uncurry eqLogic) xs)
-   return (to ep (map Var xs))
+acTopRuleFor com iso = makeTrans $ \proof -> do
+   (lhs, rhs) <- maybeToList (getSingleton proof)
+   let as = from iso lhs
+       bs = from iso rhs
+       splitter = if com then divide else split
+   (as1, as2, bs1, bs2) <- splitTwoLists splitter as bs
+   let eqList xs ys = eqLogic (to iso xs) (to iso ys)
+   guard (eqList as1 bs1 && eqList as2 bs2)
+   return $ to iso
+      [ Var (to iso as1, to iso bs1)
+      , Var (to iso as2, to iso bs2)
+      ]
 
-collect :: View a (a, a) -> Isomorphism a [a]
-collect v = f <-> g
- where
-   f x = maybe [x] (\(y, z) -> f y ++ f z) (match v x)
-   g   = foldr1 (curry (build v))
+splitTwoLists :: (forall t . [t] -> [([t], [t])])
+              -> [a] -> [b] -> [([a], [a], [b], [b])]
+splitTwoLists f as bs =
+   [ (as1, as2, bs1, bs2)
+   | (as1, as2) <- f as
+   , not (null as1 || null as2)
+   , (bs1, bs2) <- f bs
+   , not (null bs1 || null bs2)
+   ]
 
-andView, orView, eqView :: View (Logic a) (Logic a, Logic a)
-andView = makeView isAnd (uncurry (<&&>))
-orView  = makeView isOr  (uncurry (<||>))
-eqView  = makeView isEq  (uncurry equivalent)
+split :: [a] -> [([a], [a])] -- associative
+split as = [ splitAt i as | i <- [1..length as-1] ]
+
+divide :: [a] -> [([a], [a])] -- associative + commutative
+divide = foldr op [([], [])]
  where
-   isEq (p :<->: q) = Just (p, q)
-   isEq _           = Nothing
+   op a xs = map addLeft xs ++ map addRight xs
+    where
+      addLeft  (ys, zs) = (a:ys, zs)
+      addRight (ys, zs) = (ys, a:zs)
 
 topIsAnd :: Rule Proof
 topIsAnd = minor $ ruleTrans "top-is-and" $ acTopRuleFor False (collect andView)
@@ -476,11 +468,11 @@ 
 somewhereOrG :: IsStrategy g => g (Context a) -> Strategy (Context a)
 somewhereOrG s =
-   let isOr a = case currentTerm a >>= (fromTerm :: Term -> Maybe SLogic) of
-                   Just (_ :||: _) -> True
-                   _               -> False
-   in fix $ \this -> check (Prelude.not . isOr) <*> s
-                 <|> check isOr <*> layer [] this
+   let curIsOr a = case currentTerm a >>= (fromTerm :: Term -> Maybe SLogic) of
+                      Just (_ :||: _) -> True
+                      _               -> False
+   in fix $ \this -> check (Prelude.not . curIsOr) <*> s
+                 <|> check curIsOr <*> layer [] this
 
 ----------------------
 
@@ -499,17 +491,25 @@    ]
 
 -- specialization of De Morgan rules with a not inside (gives higher priority)
-ruleDeMorganOrNot :: Rule SLogic
-ruleDeMorganOrNot = rewriteRules "DeMorganOrNot"
-   [ \x y -> Not (Not x :||: y)  :~>  Not (Not x) :&&: Not y
-   , \x y -> Not (x :||: Not y)  :~>  Not x :&&: Not (Not y)
-   ]
+deMorganOrNot :: Strategy (Context SLogic)
+deMorganOrNot = check p <*> (use ruleDeMorganOr <|> use generalRuleDeMorganOr)
+ where
+   p :: Context SLogic -> Bool
+   p ctx = case currentInContext ctx of
+              Just (Not x) ->
+                 let ys = disjunctions x
+                 in length ys > 1 && any isNot ys
+              _ -> False
 
-ruleDeMorganAndNot :: Rule SLogic
-ruleDeMorganAndNot = rewriteRules "DeMorganAndNot"
-   [ \x y -> Not (Not x :&&: y)  :~>  Not (Not x) :||: Not y
-   , \x y -> Not (x :&&: Not y)  :~>  Not x :||: Not (Not y)
-   ]
+deMorganAndNot :: Strategy (Context SLogic)
+deMorganAndNot = check p <*> (use ruleDeMorganAnd <|> use generalRuleDeMorganAnd)
+ where
+   p :: Context SLogic -> Bool
+   p ctx = case currentInContext ctx of
+              Just (Not x) ->
+                 let ys = conjunctions x
+                 in length ys > 1 && any isNot ys
+              _ -> False
 
 {-
 ruleAbsorpAndNot :: Rule SLogic
@@ -532,7 +532,8 @@ inverseRules :: [Rule (Context Proof)]
 inverseRules = map use [invDefImpl, invDefEquiv, invNotNot, invIdempOr, invIdempAnd,
    invTrueZeroAnd, invNotTrue, invFalseZeroOr, invNotFalse] ++
-   [invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd, invComplAnd]
+   [ invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd
+   , invComplAnd, invAndOverOr, invOrOverAnd]
 
 invDefImpl :: Rule SLogic
 invDefImpl = rewriteRule "DefImpl.inv" $
@@ -552,7 +553,7 @@ 
 invIdempAnd :: Rule SLogic
 invIdempAnd = rewriteRule "IdempAnd.inv" $
-   \x -> x :&&: x  :~>  x
+   \x -> x :~> x :&&: x
 
 invTrueZeroAnd :: Rule SLogic
 invTrueZeroAnd = rewriteRules "TrueZeroAnd.inv"
@@ -574,20 +575,83 @@ invNotFalse = rewriteRule "NotFalse.inv" $
    T  :~> Not F
 
-makeInvRule :: String -> Rule SLogic -> Rule (Context Proof)
-makeInvRule name r = addRecognizerBool eq $ makeRule name (const Nothing)
+proofInvRule :: String -> Rule SLogic -> Rule (Context Proof)
+proofInvRule = makeInvRuleWithUse (similarity proofExercise)
+
+invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd,
+   invComplAnd, invAndOverOr, invOrOverAnd :: Rule (Context Proof)
+invAbsorpOr     = proofInvRule "AbsorpOr.inv" ruleAbsorpOr
+invAbsorpAnd    = proofInvRule "AbsorpAnd.inv" ruleAbsorpAnd
+invTrueZeroOr   = proofInvRule "TrueZeroOr.inv" ruleTrueZeroOr
+invComplOr      = proofInvRule "ComplOr.inv" ruleComplOr
+invFalseZeroAnd = proofInvRule "FalseZeroAnd.inv" ruleFalseZeroAnd
+invComplAnd     = proofInvRule "ComplAnd.inv" ruleComplAnd
+invAndOverOr    = proofInvRule "AndOverOr.inv" ruleAndOverOr -- see GeneralizedRules
+invOrOverAnd    = proofInvRule "OrOverAnd.inv" ruleOrOverAnd -- see GeneralizedRules
+
+-----------------------------------------------------------------------------
+-- Heuristic
+
+{-
+vb :: Proof
+vb = makeProof
+     ( (p :&&: Not q :&&: Not r) :||: (Not p :&&: Not q)
+     , (Not p :&&: Not q :&&: r) :||: (Not q :&&: Not r)
+     )
  where
-   eq :: Context Proof -> Context Proof -> Bool
-   eq a b = or [ True
-               | c <- applyAll (somewhere (use r)) b
-               , similarity ex a c
-               ]
-   ex = proofExercise
+   (p, q, r) = (Var $ ShowString "p", Var $ ShowString "q", Var $ ShowString "r")
+-}
 
-invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd, invComplAnd :: Rule (Context Proof)
-invAbsorpOr     = makeInvRule "AbsorpOr.inv" ruleAbsorpOr
-invAbsorpAnd    = makeInvRule "AbsorpAnd.inv" ruleAbsorpAnd
-invTrueZeroOr   = makeInvRule "TrueZeroOr.inv" ruleTrueZeroOr
-invComplOr      = makeInvRule "ComplOr.inv" ruleComplOr
-invFalseZeroAnd = makeInvRule "FalseZeroAnd.inv" ruleFalseZeroAnd
-invComplAnd     = makeInvRule "ComplAnd.inv" ruleComplAnd+-- Special case: all conjunctions, on both sides, have a common literal.
+-- Move this literal to the front (on both sides). Then use inverse distribution
+-- (and top-is-and if possible).
+commonLiteral :: Strategy (Context Proof)
+commonLiteral =
+   repeatS (somewhere (use ruleCommonLiteralInFront))
+   <*>
+   repeat1 (somewhere (use ruleInvDistrCommonLiteral))
+   <*>
+   repeatS (somewhere (use topIsAnd))
+
+findCommonLiteral :: Ord a => (Logic a, Logic a) -> [Logic a]
+findCommonLiteral (p, q) = sort $
+   intersectList (map conjunctions (disjunctions p ++ disjunctions q))
+
+ruleCommonLiteralInFront :: Rule Proof
+ruleCommonLiteralInFront = makeRule "command.common-literal" f
+ where
+   f (Var eq) =
+      [ Var x | x <- maybeToList (findInFrontLeft eq) ] ++
+      [ Var (swap x) | x <- maybeToList (findInFrontLeft (swap eq)) ]
+   f _ = []
+
+   findInFrontLeft eq = do
+      lit <- listToMaybe (findCommonLiteral eq)
+      inFrontLeft lit eq
+
+inFrontLeft :: SLogic -> (SLogic, SLogic) -> Maybe (SLogic, SLogic)
+inFrontLeft lit (p, q) = do
+   let pss = map (toFront . conjunctions) (disjunctions p)
+       toFront = uncurry (++) . partition (==lit)
+       new = ors (map ands pss)
+   guard (new /= p)
+   Just (new, q)
+
+ruleInvDistrCommonLiteral :: Rule Proof
+ruleInvDistrCommonLiteral = makeRule "andoveror.inv.common-literal" f
+ where
+   f (Var eq) = [ Var x | x <- invDistr eq ] ++
+                [ Var (swap x) | x <- invDistr (swap eq) ]
+   f _ = []
+
+   invDistr eq@(p, q) = do
+      guard (not (null (findCommonLiteral eq)))
+      new <- applyAll inverseAndOverOr p
+      return (new, q)
+
+intersectList :: Eq a => [[a]] -> [a]
+intersectList [] = []
+intersectList xs = foldr1 intersect xs
+
+swap :: (a, b) -> (b, a)
+swap (x, y) = (y, x)
src/Domain/Logic/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,60 +12,55 @@ -- DWA course)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Rules
-   ( extraLogicRules, ruleAbsorpAnd, ruleAbsorpOr, ruleAndOverOr
+   ( ruleAbsorpAnd, ruleAbsorpOr, ruleAndOverOr, ruleOrOverAnd
    , ruleComplAnd, ruleComplOr, ruleDeMorganAnd, ruleDeMorganOr
-   , ruleDefEquiv, ruleDefImpl, ruleFalseInEquiv, ruleFalseInImpl
+   , ruleDefEquiv, ruleDefImpl
    , ruleFalseZeroAnd, ruleFalseZeroOr, ruleIdempAnd, ruleIdempOr
-   , ruleNotFalse, ruleNotNot, ruleNotTrue, ruleTrueInEquiv
-   , ruleTrueInImpl, ruleTrueZeroAnd, ruleTrueZeroOr
+   , ruleNotFalse, ruleNotNot, ruleNotTrue
+   , ruleTrueZeroAnd, ruleTrueZeroOr
+   , ruleCommOr, ruleCommAnd, ruleAssocOr, ruleAssocAnd
    ) where
 
 import Domain.Logic.Formula
-import Domain.Logic.GeneralizedRules
 import Domain.Logic.Generator()
+import Domain.Logic.Utils
 import Ideas.Common.Library hiding (ruleList)
-import qualified Ideas.Common.Library as C
 
-extraLogicRules :: [Rule SLogic]
-extraLogicRules =
-   [ ruleCommOr, ruleCommAnd, ruleAssocOr, ruleAssocAnd
-   , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl
-   , ruleCommEquiv, ruleDefEquivImpls, ruleEquivSame, ruleImplSame
-   , generalRuleOrOverAnd, ruleOrOverAnd
-   , inverseDeMorganOr, inverseDeMorganAnd
-   , inverseAndOverOr, inverseOrOverAnd
-   ]
-
-logic :: IsId a => a -> Id
-logic = ( # ) "logic.propositional"
-
 rule :: RuleBuilder f a => String -> f -> Rule a
-rule = C.rewriteRule . logic
+rule = rewriteRule . (propositionalId #)
 
+ruleFor :: RuleBuilder f a => Id -> String -> f -> Rule a
+ruleFor group s = siblingOf group . rule s
+
 ruleList :: RuleBuilder f a => String -> [f] -> Rule a
-ruleList = C.rewriteRules . logic
+ruleList = rewriteRules . (propositionalId #)
 
+ruleListFor :: RuleBuilder f a => Id -> String -> [f] -> Rule a
+ruleListFor group s = siblingOf group . ruleList s
+
 -----------------------------------------------------------------------------
 -- Commutativity
 
 ruleCommOr :: Rule SLogic
-ruleCommOr = rule "CommOr" $
+ruleCommOr = ruleFor groupCommutativity "CommOr" $
    \x y -> x :||: y  :~>  y :||: x
 
 ruleCommAnd :: Rule SLogic
-ruleCommAnd = rule "CommAnd" $
+ruleCommAnd = ruleFor groupCommutativity "CommAnd" $
    \x y -> x :&&: y  :~>  y :&&: x
 
 -----------------------------------------------------------------------------
 -- Associativity (implicit)
 
 ruleAssocOr :: Rule SLogic
-ruleAssocOr = minor $ rule "AssocOr" $
+ruleAssocOr = minor $ ruleFor groupAssociativity "AssocOr" $
    \x y z -> (x :||: y) :||: z  :~>  x :||: (y :||: z)
 
 ruleAssocAnd :: Rule SLogic
-ruleAssocAnd = minor $ rule "AssocAnd" $
+ruleAssocAnd = minor $ ruleFor groupAssociativity "AssocAnd" $
    \x y z -> (x :&&: y) :&&: z  :~>  x :&&: (y :&&: z)
 
 -----------------------------------------------------------------------------
@@ -73,13 +68,13 @@ 
 ruleAndOverOr :: Rule SLogic
 
-ruleAndOverOr = ruleList "AndOverOr"
+ruleAndOverOr = ruleListFor groupDistribution "AndOverOr"
    [ \x y z -> x :&&: (y :||: z)  :~>  (x :&&: y) :||: (x :&&: z)
    , \x y z -> (x :||: y) :&&: z  :~>  (x :&&: z) :||: (y :&&: z)
    ]
 
 ruleOrOverAnd :: Rule SLogic
-ruleOrOverAnd = ruleList "OrOverAnd"
+ruleOrOverAnd = ruleListFor groupDistribution "OrOverAnd"
    [ \x y z -> x :||: (y :&&: z)  :~>  (x :||: y) :&&: (x :||: z)
    , \x y z -> (x :&&: y) :||: z  :~>  (x :||: z) :&&: (y :||: z)
    ]
@@ -89,10 +84,10 @@ 
 ruleIdempOr, ruleIdempAnd :: Rule SLogic
 
-ruleIdempOr = rule "IdempOr" $
+ruleIdempOr = ruleFor groupIdempotency "IdempOr" $
    \x -> x :||: x  :~>  x
 
-ruleIdempAnd = rule "IdempAnd" $
+ruleIdempAnd = ruleFor groupIdempotency "IdempAnd" $
    \x -> x :&&: x  :~>  x
 
 -----------------------------------------------------------------------------
@@ -100,14 +95,14 @@ 
 ruleAbsorpOr, ruleAbsorpAnd :: Rule SLogic
 
-ruleAbsorpOr = ruleList "AbsorpOr"
+ruleAbsorpOr = ruleListFor groupAbsorption "AbsorpOr"
    [ \x y -> x :||: (x :&&: y)  :~>  x
    , \x y -> x :||: (y :&&: x)  :~>  x
    , \x y -> (x :&&: y) :||: x  :~>  x
    , \x y -> (y :&&: x) :||: x  :~>  x
    ]
 
-ruleAbsorpAnd = ruleList "AbsorpAnd"
+ruleAbsorpAnd = ruleListFor groupAbsorption "AbsorpAnd"
    [ \x y -> x :&&: (x :||: y)  :~>  x
    , \x y -> x :&&: (y :||: x)  :~>  x
    , \x y -> (x :||: y) :&&: x  :~>  x
@@ -171,11 +166,11 @@ -- De Morgan
 
 ruleDeMorganOr :: Rule SLogic
-ruleDeMorganOr = rule "DeMorganOr" $
+ruleDeMorganOr = ruleFor groupDeMorgan "DeMorganOr" $
    \x y -> Not (x :||: y)  :~>  Not x :&&: Not y
 
 ruleDeMorganAnd :: Rule SLogic
-ruleDeMorganAnd = rule "DeMorganAnd" $
+ruleDeMorganAnd = ruleFor groupDeMorgan "DeMorganAnd" $
    \x y -> Not (x :&&: y)  :~>  Not x :||: Not y
 
 -----------------------------------------------------------------------------
@@ -195,6 +190,7 @@ -----------------------------------------------------------------------------
 -- Additional rules, not in the DWA course
 
+{-
 ruleFalseInEquiv :: Rule SLogic
 ruleFalseInEquiv = ruleList "FalseInEquiv"
    [ \x -> F :<->: x  :~>  Not x
@@ -233,4 +229,5 @@ 
 ruleImplSame :: Rule SLogic
 ruleImplSame = rule "ImplSame" $
-   \x -> x :->: (x::SLogic)  :~>  T+   \x -> x :->: (x::SLogic)  :~>  T
+-}
src/Domain/Logic/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,8 +9,11 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Strategies
-   ( dnfStrategy, dnfStrategyDWA, somewhereOr
+   ( dnfStrategyDWA, somewhereOr
+   , cnfStrategyDWA
    ) where
 
 import Domain.Logic.Formula
@@ -54,11 +57,11 @@ -- the strategy only at (top-level) disjuncts
 somewhereOr :: IsStrategy g => g (Context SLogic) -> Strategy (Context SLogic)
 somewhereOr s =
-   let isOr a = case currentInContext a of
-                   Just (_ :||: _) -> True
-                   _               -> False
-   in fix $ \this -> check (Prelude.not . isOr) <*> s
-                 <|> check isOr <*> layer [] this
+   let curIsOr a = case currentInContext a of
+                      Just (_ :||: _) -> True
+                      _               -> False
+   in fix $ \this -> check (Prelude.not . curIsOr) <*> s
+                 <|> check curIsOr <*> layer [] this
 
 --check1, check2 :: (a -> Bool) -> Rule a
 --check1 p = minorRule $ makeSimpleRule "check1" $ \a -> if p a then Just a else Nothing
@@ -66,7 +69,7 @@ 
 -----------------------------------------------------------------------------
 -- To DNF, in four steps
-
+{-
 dnfStrategy :: LabeledStrategy (Context SLogic)
 dnfStrategy =  label "Bring to dnf"
       $  label "Eliminate constants"                 eliminateConstants
@@ -76,8 +79,8 @@  where
    eliminateConstants = repeatS $ oncetd $ useRules
       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
-      , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse, ruleFalseInEquiv
-      , ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl
+      , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
+      -- , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl
       ]
    eliminateImplEquiv = repeatS $ oncebu $ useRules
       [ ruleDefImpl, ruleDefEquiv
@@ -91,8 +94,49 @@          ]
    orToTop = repeatS $ somewhere $
       liftToContext generalRuleAndOverOr |>
-      liftToContext ruleAndOverOr
+      liftToContext ruleAndOverOr -}
 
 -- local helper function
 useRules :: [Rule SLogic] -> Strategy (Context SLogic)
-useRules = alternatives . map liftToContext+useRules = alternatives . map liftToContext
+
+-----------------------------------------------------------------
+-- Conjunctive normal form
+
+cnfStrategyDWA :: LabeledStrategy (Context SLogic)
+cnfStrategyDWA =  label "Bring to cnf (DWA)" $
+   repeatS $ toplevel <|> somewhereAnd -- CHANGED
+      (  label "Simplify"                            simpl
+      |> label "Eliminate implications/equivalences" eliminateImplEquiv
+      |> label "Eliminate nots"                      eliminateNots
+      |> label "Move ands to top"                    andToTop -- CHANGED
+      )
+ where
+    toplevel = useRules -- CHANGED
+       [ ruleFalseZeroAnd, ruleTrueZeroAnd, ruleIdempAnd
+       , ruleAbsorpAnd, ruleComplAnd
+       ]
+    simpl = somewhere $ useRules
+       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
+       , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
+       , ruleNotNot, ruleIdempOr, ruleIdempAnd, ruleAbsorpOr, ruleAbsorpAnd
+       , ruleComplOr, ruleComplAnd
+       ]
+    eliminateImplEquiv = somewhere $ useRules
+       [ ruleDefImpl, ruleDefEquiv
+       ]
+    eliminateNots = somewhere $ useRules
+       [ generalRuleDeMorganAnd, generalRuleDeMorganOr
+       , ruleDeMorganAnd, ruleDeMorganOr
+       ]
+    andToTop = somewhere $ useRules
+       [ generalRuleOrOverAnd, ruleOrOverAnd ]
+
+-- Copied from somewhereAnd (and changed)
+somewhereAnd :: IsStrategy g => g (Context SLogic) -> Strategy (Context SLogic)
+somewhereAnd s =
+   let curIsAnd a = case currentInContext a of
+                       Just (_ :&&: _) -> True
+                       _               -> False
+   in fix $ \this -> check (Prelude.not . curIsAnd) <*> s
+                 <|> check curIsAnd <*> layer [] this
+ src/Domain/Logic/Utils.hs view
@@ -0,0 +1,86 @@+-----------------------------------------------------------------------------
+-- Copyright 2014, 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)
+--
+-- Utilities for the logic domain
+--
+-----------------------------------------------------------------------------
+--  $Id: Utils.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
+module Domain.Logic.Utils
+   ( propositionalId, makeSimpleRule
+     -- groups of rules
+   , groupAbsorption, groupAssociativity, groupCommutativity, groupDeMorgan
+   , groupDistribution, groupIdempotency
+     -- other utility functions
+   , makeInvRule, makeInvRuleWithUse
+   , collect, andView, orView, eqView
+   , (===), (==>), (<=>)
+   ) where
+
+import Domain.Logic.Formula
+import Ideas.Common.Library
+
+propositionalId :: Id
+propositionalId = newId "logic.propositional"
+
+makeSimpleRule :: String -> (a -> Maybe a) -> Rule a
+makeSimpleRule s = makeRule (propositionalId # s)
+
+-----------------------------------------------------------------------------
+-- Groups of rules
+
+groupAbsorption, groupAssociativity, groupCommutativity, groupDeMorgan,
+   groupDistribution, groupIdempotency :: Id
+groupAbsorption    = makeGroup "Absorption"
+groupAssociativity = makeGroup "Associativity"
+groupCommutativity = makeGroup "Commutativity"
+groupDeMorgan      = makeGroup "DeMorgan"
+groupDistribution  = makeGroup "Distribution"
+groupIdempotency   = makeGroup "Idempotency"
+
+makeGroup :: String -> Id
+makeGroup s = describe "Group of logic rules" (propositionalId # s)
+
+-----------------------------------------------------------------------------
+-- Inverse of a rule
+
+makeInvRule :: IsId n => (a -> a -> Bool) -> n -> Rule a -> Rule a
+makeInvRule sim name r =
+   addRecognizerBool eq $ setBuggy (isBuggy r) $ makeRule name (const Nothing)
+ where
+   eq a b = any (sim a) (applyAll r b)
+
+makeInvRuleWithUse :: (IsTerm a, IsTerm b, IsId n, Show a)
+                => (Context a -> Context a -> Bool) -> n -> Rule b -> Rule (Context a)
+makeInvRuleWithUse sim name r =
+   addRecognizerBool eq $ setBuggy (isBuggy r) $ makeRule name (const Nothing)
+ where
+   eq a b = any (sim a) (applyAll (somewhere (use r)) b)
+
+collect :: View a (a, a) -> Isomorphism a [a]
+collect v = f <-> g
+ where
+   f x = maybe [x] (\(y, z) -> f y ++ f z) (match v x)
+   g   = foldr1 (curry (build v))
+
+andView, orView, eqView :: View (Logic a) (Logic a, Logic a)
+andView = makeView isAnd (uncurry (<&&>))
+orView  = makeView isOr  (uncurry (<||>))
+eqView  = makeView isEq  (uncurry equivalent)
+ where
+   isEq (p :<->: q) = Just (p, q)
+   isEq _           = Nothing
+
+infix 6 ===, ==>, <=>
+
+(===), (==>), (<=>) :: Eq a => Logic a -> Logic a -> Bool
+(===)   = eqLogic
+p ==> q = tautology (p :->: q)
+p <=> q = tautology (p :<->: q)
src/Domain/Logic/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Logic.Views
    ( (.<->.), (.->.), (.&&.), (.||.)
    , simplify, pushNot, pushNotWith
src/Domain/Math/Approximation.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Selection of numerical algorithms for approximations
 --
 -----------------------------------------------------------------------------
+--  $Id: Approximation.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Approximation where
 
 import Data.List
src/Domain/Math/CleanUp.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: CleanUp.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.CleanUp
    ( cleanUpRelations, cleanUpRelation, cleanUpExpr
    , cleanUpSimple, cleanUpView, cleanUpACView
src/Domain/Math/Data/DecimalFraction.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -13,6 +13,8 @@ -- Division in the Fractional type class is not safe.
 --
 -----------------------------------------------------------------------------
+--  $Id: DecimalFraction.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.DecimalFraction
    ( DecimalFraction(..), fromDouble, validDivisor, digits
    ) where
src/Domain/Math/Data/Interval.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -13,6 +13,8 @@ -- equality (provided that there is a valid ordering on the elements).
 --
 -----------------------------------------------------------------------------
+--  $Id: Interval.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.Interval
    ( -- * Data types
      Interval, Endpoint(..)
@@ -263,32 +265,36 @@    coarbitrary (I xs) = coarbitrary xs
 
 testMe :: TestSuite
-testMe = suite "Intervals" $ do
+testMe = suite "Intervals"
 
-   suite "Constructor functions" $ do
-     addProperty "empty"     $ op0 empty     (const False)
-     addProperty "unbounded" $ op0 unbounded (const True)
+   [ suite "Constructor functions"
+        [ useProperty "empty"     $ op0 empty     (const False)
+        , useProperty "unbounded" $ op0 unbounded (const True)
 
-     addProperty "greater than"             $ op1 greaterThan (>)
-     addProperty "greater than or equal to" $ op1 greaterThanOrEqualTo (>=)
-     addProperty "less than"                $ op1 lessThan (<)
-     addProperty "less than or equal to"    $ op1 lessThanOrEqualTo (<=)
-     addProperty "point    "                $ op1 point (==)
+        , useProperty "greater than"             $ op1 greaterThan (>)
+        , useProperty "greater than or equal to" $ op1 greaterThanOrEqualTo (>=)
+        , useProperty "less than"                $ op1 lessThan (<)
+        , useProperty "less than or equal to"    $ op1 lessThanOrEqualTo (<=)
+        , useProperty "point    "                $ op1 point (==)
 
-     addProperty "open"       $ op2 open      (<)  (<)
-     addProperty "closed"     $ op2 closed    (<=) (<=)
-     addProperty "left open"  $ op2 leftOpen  (<)  (<=)
-     addProperty "right open" $ op2 rightOpen (<=) (<)
+        , useProperty "open"       $ op2 open      (<)  (<)
+        , useProperty "closed"     $ op2 closed    (<=) (<=)
+        , useProperty "left open"  $ op2 leftOpen  (<)  (<=)
+        , useProperty "right open" $ op2 rightOpen (<=) (<)
+        ]
 
-   suite "Combinators" $ do
-      addProperty "except"     defExcept
-      addProperty "union"      defUnion
-      addProperty "intersect"  defIntersect
-      addProperty "complement" defComplement
+   , suite "Combinators"
+        [ useProperty "except"     defExcept
+        , useProperty "union"      defUnion
+        , useProperty "intersect"  defIntersect
+        , useProperty "complement" defComplement
+        ]
 
-   suite "Boolean algebra" $
-      forM_ (booleanLaws :: [Law (Interval Int)]) $ \p ->
-         addProperty (show p) p
+   , suite "Boolean algebra"
+        [ useProperty (show p) p
+        | p <- booleanLaws :: [Law (Interval Int)]
+        ]
+   ]
 
 defExcept :: Int -> Int -> Bool
 defExcept a b = isIn a (except b) == (a/=b)
src/Domain/Math/Data/MixedFraction.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -13,6 +13,8 @@ -- for example, 5[1/4] or -3[2/5]
 --
 -----------------------------------------------------------------------------
+--  $Id: MixedFraction.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.MixedFraction
    ( MixedFraction, wholeNumber, fractionPart, numerator, denominator
    ) where
src/Domain/Math/Data/OrList.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,6 +10,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: OrList.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.OrList
    ( OrList, OrSet, true, false, (<>)
    , isTrue, isFalse, fromBool, toOrList
src/Domain/Math/Data/Polynomial.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Polynomial.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.Polynomial
    ( Polynomial, toPolynomial, fromPolynomial, var, con, raise
    , degree, lowestDegree, coefficient
@@ -283,13 +285,14 @@ -- Properties
 
 testPolynomials :: TestSuite
-testPolynomials = suite "polynomial" $
-   addProperty "factorization" $ do
-      i  <- choose (0, 5)
-      as <- replicateM i $ choose (-20, 20)
-      b  <- choose (1, 30)
-      c  <- choose (-10*b, 10*b)
-      let qs = [ var - con (fromInteger a) | a <- as ]
-          p  = con (fromInteger c/fromInteger b) * product qs
-          ps = factorize p
-      return (all ((<= 1) . degree) ps && product ps == p)+testPolynomials = suite "polynomial"
+   [ useProperty "factorization" $ do
+        i  <- choose (0, 5)
+        as <- replicateM i $ choose (-20, 20)
+        b  <- choose (1, 30)
+        c  <- choose (-10*b, 10*b)
+        let qs = [ var - con (fromInteger a) | a <- as ]
+            p  = con (fromInteger c/fromInteger b) * product qs
+            ps = factorize p
+        return (all ((<= 1) . degree) ps && product ps == p)
+   ]
src/Domain/Math/Data/PrimeFactors.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: PrimeFactors.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.PrimeFactors
    ( PrimeFactors
    , splitPower, greatestPower, allPowers
src/Domain/Math/Data/Primes.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Calculating prime numbers and prime factors
 --
 -----------------------------------------------------------------------------
+--  $Id: Primes.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.Primes
    ( primes, isPrime, coprime, primeFactors, factors
    , testPrimes
@@ -153,23 +155,24 @@ primesSlow = 1 : 2 : sieveSlow [3, 5 ..]
 
 testPrimes :: TestSuite
-testPrimes = suite "primes" $ do
-   assertTrue "first 1000 primes" (take 1000 primesSlow == take 1000 primes)
-   assertTrue "isPrime" (all isPrime primes1000)
-   addProperty "product of prime factors" $
-      forAll (choose (1, 1000000)) $ \n ->
-      product (primeFactors n) == n
-   addProperty "primality of prime factors" $
-      forAll (choose (1, 1000000)) $ \n ->
-      all isPrime (primeFactors n)
-   addProperty "factoring product of two primes" $
-      forAll (elements $ tail primes1000) $ \a ->
-      forAll (elements $ tail primes1000) $ \b ->
-      primeFactors (a*b) == sort [a, b]
-   addProperty "factors" $
-      forAll (choose (1, 10000)) $ \n ->
-      all (`divisorOf` n) (factors n)
-   addProperty "factors of product" $
-      forAll (choose (1, 1000)) $ \a ->
-      forAll (choose (1, 1000)) $ \b ->
-      all (`elem` factors (a*b)) [a, b]+testPrimes = suite "primes"
+   [ assertTrue "first 1000 primes" (take 1000 primesSlow == take 1000 primes)
+   , assertTrue "isPrime" (all isPrime primes1000)
+   , useProperty "product of prime factors" $
+        forAll (choose (1, 1000000)) $ \n ->
+        product (primeFactors n) == n
+   , useProperty "primality of prime factors" $
+        forAll (choose (1, 1000000)) $ \n ->
+        all isPrime (primeFactors n)
+   , useProperty "factoring product of two primes" $
+        forAll (elements $ tail primes1000) $ \a ->
+        forAll (elements $ tail primes1000) $ \b ->
+        primeFactors (a*b) == sort [a, b]
+   , useProperty "factors" $
+        forAll (choose (1, 10000)) $ \n ->
+        all (`divisorOf` n) (factors n)
+   , useProperty "factors of product" $
+        forAll (choose (1, 1000)) $ \a ->
+        forAll (choose (1, 1000)) $ \b ->
+        all (`elem` factors (a*b)) [a, b]
+   ]
src/Domain/Math/Data/Relation.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Mathematical relations
 --
 -----------------------------------------------------------------------------
+--  $Id: Relation.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.Relation
    ( -- * Type class
      Relational(..)
src/Domain/Math/Data/SquareRoot.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: SquareRoot.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.SquareRoot
    ( SquareRoot
    , imaginary, imaginaryUnit
src/Domain/Math/Data/TestingClassLaws.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE TypeFamilies #-}
 
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: TestingClassLaws.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.TestingClassLaws where
 
 import Domain.Math.Data.DecimalFraction
src/Domain/Math/Data/WithBool.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,6 +12,8 @@ -- Values extended with boolean constants
 --
 -----------------------------------------------------------------------------
+--  $Id: WithBool.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Data.WithBool
    ( WithBool, fromWithBool, join
    ) where
@@ -22,7 +24,6 @@ import Data.Foldable
 import Data.Traversable
 import Domain.Logic.Formula
-import Ideas.Common.Algebra.Boolean
 import Ideas.Common.Classes
 import Ideas.Common.Rewriting
 import Test.QuickCheck
src/Domain/Math/Derivative/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,6 +12,8 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html.
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Derivative.Examples
    ( diffSet1, diffSet2, diffSet3, diffSet4
    , diffSet5, diffSet6, diffSet7, diffSet8
src/Domain/Math/Derivative/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Derivative.Exercises
    ( derivativeExercise, derivativePolyExercise
    , derivativeProductExercise, derivativeQuotientExercise
@@ -74,7 +76,7 @@    , suitable      = predicate isQuotientDiff
    , equivalence   = withoutContext eqQuotientDiff
    , strategy      = derivativeQuotientStrategy
-   , ruleOrdering  = ruleOrderingWithId [ruleDerivQuotient]
+   , ruleOrdering  = ruleOrderingWith [ruleDerivQuotient]
    , examples      = level Medium $ concat diffSet4
    , testGenerator = Nothing
    }
src/Domain/Math/Derivative/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Derivative.Rules where
 
 import Control.Monad
src/Domain/Math/Derivative/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Derivative.Strategies
    ( derivativeStrategy, derivativePolyStrategy
    , derivativeProductStrategy, derivativeQuotientStrategy
src/Domain/Math/Equation/BalanceRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: BalanceRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Equation.BalanceRules
    ( plusRule, minusRule, timesRule, divisionRule
    ) where
src/Domain/Math/Equation/CoverUpExercise.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: CoverUpExercise.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Equation.CoverUpExercise
    ( coverUpExercise, coverUpStrategy
    ) where
src/Domain/Math/Equation/CoverUpRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: CoverUpRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Equation.CoverUpRules
    ( coverUpRules, coverUpRulesOr
    , coverUp, coverUpOrs
src/Domain/Math/Equation/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Example exercises from the Digital Mathematics Environment (DWO)
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Equation.Examples
    ( fillInResult, coverUpEquations
    ) where
src/Domain/Math/Equation/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Equation.Views
    ( relationSolvedForm, relationsSolvedForm
    , equationSolvedForm, equationsSolvedForm, equationSolvedWith
src/Domain/Math/ExerciseList.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- All exported exercises in the mathematical domain
 --
 -----------------------------------------------------------------------------
+--  $Id: ExerciseList.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.ExerciseList
    ( exerciseList, viewList, scriptList, testSuiteList
    ) where
src/Domain/Math/Expr.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Expr.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Expr (module Export) where
 
 import Domain.Math.Expr.Clipboard as Export
src/Domain/Math/Expr/Clipboard.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -13,6 +13,8 @@ -- is part of the environment (terms that are placed in a context)
 --
 -----------------------------------------------------------------------------
+--  $Id: Clipboard.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Expr.Clipboard
    ( -- * Data type
      Clipboard
src/Domain/Math/Expr/Data.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,6 +10,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Data.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Expr.Data
    ( Expr(..), toExpr, fromExpr, fromDouble
    ) where
src/Domain/Math/Expr/Parser.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Expr.Parser
    ( parseExpr, parseExprM
    , parseEqExpr, parseBoolEqExpr, parseRelExpr
src/Domain/Math/Expr/Symbols.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Exports relevant OpenMath symbols
 --
 -----------------------------------------------------------------------------
+--  $Id: Symbols.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Expr.Symbols
    ( -- OpenMath dictionary symbols
      plusSymbol, timesSymbol, minusSymbol, divideSymbol, rationalSymbol
src/Domain/Math/Expr/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Expr.Views
    ( module Domain.Math.Expr.Views
    , (.+.), (.-.), neg, (.*.), (./.)
src/Domain/Math/Fraction/Exercises.hs view
@@ -1,3 +1,16 @@+-----------------------------------------------------------------------------
+-- Copyright 2014, 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 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Fraction.Exercises
    ( simpleFractionAddition
    ) where
src/Domain/Math/Fraction/Rules.hs view
@@ -1,10 +1,20 @@+-----------------------------------------------------------------------------
+-- Copyright 2014, 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: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Fraction.Rules where
 
 import Control.Monad
 import Domain.Math.Expr
-import Domain.Math.Expr.Clipboard
-import Domain.Math.Numeric.Rules (calcPlusWith, calcMinusWith, calcTimesWith, calcDivisionWith)
-import Domain.Math.Numeric.Views
 import Ideas.Common.Library
 
 expandFractionSymbol :: Symbol
@@ -45,9 +55,9 @@ expandToLCM = makeRule "expandToLCM" $ \ctx -> do
                  expr <- currentInContext ctx
                  (Nat a,Nat b) <- match fractionView expr
-                 lcm <- lookupClipboardG "lcm" ctx
-                 guard (b /= lcm && lcm `mod` b == 0)
-                 return $ replaceInContext (Nat(a * lcm `div` b) :/: Nat lcm) ctx
+                 lcmVal <- lookupClipboardG "lcm" ctx
+                 guard (b /= lcmVal && lcmVal `mod` b == 0)
+                 return $ replaceInContext (Nat(a * lcmVal `div` b) :/: Nat lcmVal) ctx
 
 addLikeFractions :: Rule (Context Expr)
 addLikeFractions = makeRule "addLikeFractions" $ \ctx -> do
src/Domain/Math/Fraction/Strategies.hs view
@@ -1,3 +1,16 @@+-----------------------------------------------------------------------------
+-- Copyright 2014, 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: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Fraction.Strategies
     (expandAndAdd) where
 
@@ -8,5 +21,5 @@ expandAndAdd :: LabeledStrategy (Context Expr)
 expandAndAdd = label "expandAndAdd" $
                try findLCM
-               <*> repeatS ( somewhere (expandToLCM ))
+               <*> repeatS ( somewhere expandToLCM )
                <*>  addLikeFractions
src/Domain/Math/Numeric/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Example exercises from ActiveMath
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Examples
    ( fractionExamples
    , fractionLiberalExamples
src/Domain/Math/Numeric/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Exercises
    ( naturalExercise, integerExercise
    , rationalExercise, fractionExercise
src/Domain/Math/Numeric/Generators.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Generators.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Generators
    ( integerGenerator, rationalGenerator, numGenerator
    , ratioGen, ratioExprGen, ratioExprGenNonZero, nonZero
src/Domain/Math/Numeric/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Rules where
 
 import Control.Monad
src/Domain/Math/Numeric/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Strategies
    ( naturalStrategy, integerStrategy
    , rationalStrategy, fractionStrategy
src/Domain/Math/Numeric/Tests.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,9 +9,10 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Tests.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Tests (main) where
 
-import Control.Monad
 import Data.Maybe
 import Data.Monoid
 import Domain.Math.Expr
@@ -25,51 +26,65 @@ import Test.QuickCheck
 
 main :: TestSuite
-main = suite "Numeric tests" $ do
+main = suite "Numeric tests"
 
-   suite "Correctness numeric views" $ do
-      let f s v = forM_ numGenerators $ \g -> do
-             addProperty ("idempotence " ++ s) $ propIdempotence g v
-             addProperty ("soundness " ++ s)   $ propSoundness semEqDouble g v
-      f "integer view"          integerView
-      f "rational view"         rationalView
-      f "integer normal form"   integerNF
-      f "rational normal form"  rationalNF
-      f "rational relaxed form" rationalRelaxedForm
+   [ let f s v = mconcat
+            [ useProperty ("idempotence " ++ s)
+                 (propIdempotence g v) <>
+              useProperty ("soundness " ++ s)
+                 (propSoundness semEqDouble g v)
+            | g <- numGenerators
+            ]
+     in suite "Correctness numeric views"
+           [ f "integer view"          integerView
+           , f "rational view"         rationalView
+           , f "integer normal form"   integerNF
+           , f "rational normal form"  rationalNF
+           , f "rational relaxed form" rationalRelaxedForm
+           ]
 
-   suite "Normal forms" $ do
-      let f s v = forM_ numGenerators $ \g ->
-             addProperty s $ propNormalForm g v
-      f "integer normal form" integerNF
-    -- f rationalNF -- no longer a normal form
+   , let f s v = [ useProperty s $ propNormalForm g v
+                 | g <- numGenerators
+                 ]
+     in suite "Normal forms" $
+           f "integer normal form" integerNF
+           -- f rationalNF -- no longer a normal form
 
-   suite "Correctness generators" $ do
-      let f s g v = addProperty s $ forAll (sized g) (`belongsTo` v)
-      f "integer" integerGenerator integerView
-      f "rational" rationalGenerator rationalView
-      f "ratio expr" ratioExprGen rationalNF
-      f "ratio expr nonzero" ratioExprGenNonZero rationalNF
+   , let f s g v = useProperty s $ forAll (sized g) (`belongsTo` v)
+     in suite "Correctness generators"
+           [ f "integer" integerGenerator integerView
+           , f "rational" rationalGenerator rationalView
+           , f "ratio expr" ratioExprGen rationalNF
+           , f "ratio expr nonzero" ratioExprGenNonZero rationalNF
+           ]
 
-   suite "View relations" $ do
-      let va .>. vb = forM_ numGenerators $ \g ->
-             addProperty "" $ forAll g $ \a ->
-                not (a `belongsTo` va) || a `belongsTo` vb
-      integerNF .>. integerView
-      rationalNF .>. rationalRelaxedForm
-      rationalRelaxedForm .>. rationalView
-      integerNF .>. rationalNF
-      integerView .>. rationalView
+   , let va .>. vb = mconcat
+            [ useProperty "" $ forAll g $ \a ->
+                 not (a `belongsTo` va) || a `belongsTo` vb
+            | g <- numGenerators
+            ]
+     in suite "View relations"
+           [ integerNF .>. integerView
+           , rationalNF .>. rationalRelaxedForm
+           , rationalRelaxedForm .>. rationalView
+           , integerNF .>. rationalNF
+           , integerView .>. rationalView
+           ]
 
-   suite "Pre/post conditions strategies" $ do
-      let f l s pre post = forM_ numGenerators $ \g ->
-             addProperty l $ forAll g $ \a ->
-                let run = fromMaybe a . fromContext . applyD s
-                        . newContext mempty . termNavigator
-                in not (a `belongsTo` pre) || run a `belongsTo` post
-      f "natural"  naturalStrategy  integerView  integerNF
-      f "integer"  integerStrategy  integerView  integerNF
-      f "rational" rationalStrategy rationalView rationalNF
-      f "fraction" fractionStrategy rationalView rationalNF
+   , let f l s pre post = mconcat
+            [ useProperty l $ forAll g $ \a ->
+                 let run = fromMaybe a . fromContext . applyD s
+                         . newContext . termNavigator
+                 in not (a `belongsTo` pre) || run a `belongsTo` post
+            | g <- numGenerators
+            ]
+     in suite "Pre/post conditions strategies"
+           [ f "natural"  naturalStrategy  integerView  integerNF
+           , f "integer"  integerStrategy  integerView  integerNF
+           , f "rational" rationalStrategy rationalView rationalNF
+           , f "fraction" fractionStrategy rationalView rationalNF
+           ]
+   ]
 
 numGenerators :: [Gen Expr]
 numGenerators = map sized
src/Domain/Math/Numeric/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Numeric.Views
    ( -- * Natural numbers
      naturalView, naturalNF
src/Domain/Math/Polynomial/Balance.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Balance.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Balance (balanceExercise) where
 
 import Control.Monad
@@ -49,7 +51,7 @@                      <||> predicateView (traverseView (equationSolvedWith doubleNF))
    , strategy      = balanceStrategy
    , extraRules    = map use buggyBalanceRules ++ map use buggyBalanceExprRules
-   , ruleOrdering  = ruleOrderingWithId (balanceOrder ++ buggyPriority)
+   , ruleOrdering  = ruleOrderingWith (balanceOrder ++ buggyPriority)
    , navigation    = termNavigator
    , testGenerator = Just $ liftM2 (\a b -> singleton (a :==: b)) (sized linearGen) (sized linearGen)
    , examples      = map (mapSecond singleton) linearExamples
@@ -81,20 +83,22 @@           <|> use removeDivision
           <|> somewhere (use divisionToFraction)
           <|> use negateBothSides
+          <|> use introTrue <|> use introFalse
            ))
    <*> label "Phase 2" (repeatS
            (  use varLeftMinus <|> use varLeftPlus
           <|> use conRightMinus <|> use conRightPlus
-          <|> (check p2 <*> (use varRightMinus <|> use varRightPlus))
-          <|> (check p1 <*> (use conLeftMinus <|> use conLeftPlus)
-           ))
+          <|> use introTrue <|> use introFalse
+          <|> atomic (check p2 <*> (use varRightMinus <|> use varRightPlus))
+          <|> atomic (check p1 <*> (use conLeftMinus <|> use conLeftPlus))
+           )
        <*> try (use scaleToOne)
        <*> try (use calculate))
        -- flip sides of an equation (at most once)
    <%> try (atomic (use (check conditionVarsRHS) <*> use flipEquation))
        -- divide by a common factor (but not as final "scale-to-one" step)
-   <%> many (notS (use scaleToOne) <*> use divideCommonFactor)
-   <%> many (use introTrue <|> use introFalse)
+   <%> many (atomic (notS (use scaleToOne) <*> use divideCommonFactor))
+   -- <%> many (use introTrue <|> use introFalse)
  where
    -- move constants to left only if there are no variables on the left
    p1 = maybe False (either (const False) (hasNoVar . leftHandSide) . fromWithBool) . fromContext
src/Domain/Math/Polynomial/BalanceUtils.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: BalanceUtils.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.BalanceUtils
    ( eqView, minusView, negView
    , matchLin, matchPlusCon
src/Domain/Math/Polynomial/BuggyBalance.hs view
@@ -1,6 +1,5 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: BuggyBalance.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.BuggyBalance
    ( buggyBalanceRules, buggyBalanceExprRules, buggyPriority
    ) where
@@ -454,8 +455,8 @@    buggyBalanceRecognizer "mulbal3" p
  where -- currently, symmetric
    p ~(a1 :==: a2) ~(b1 :==: b2) = do
-      ~dl <- diffTimes a1 b1
-      ~dr <- diffTimes a2 b2
+      dl <- diffTimes a1 b1
+      dr <- diffTimes a2 b2
       guard ((dl==1) /=  (dr==1)) -- xor; only one of dl/dr equals 1
       factorRef := if dr/=1 then dr else dl
src/Domain/Math/Polynomial/BuggyRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Some buggy rules catching common misconceptions (also on the abc-formula)
 --
 -----------------------------------------------------------------------------
+--  $Id: BuggyRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.BuggyRules
    ( buggyRulesExpr, buggyRulesEquation
    , abcBuggyRules, buggyQuadratic, buggySquareMultiplication
src/Domain/Math/Polynomial/Equivalence.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,6 +10,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Equivalence.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Equivalence
    ( linEq, quadrEqContext, highEqContext, simLogic, flipGT
    , eqAfterSubstitution, intervalRelations
@@ -28,7 +30,6 @@ import Domain.Math.Numeric.Views
 import Domain.Math.Polynomial.Views
 import Domain.Math.SquareRoot.Views
-import Ideas.Common.Algebra.Boolean
 import Ideas.Common.Context
 import Ideas.Common.Rewriting
 import Ideas.Common.Utils.Uniplate
src/Domain/Math/Polynomial/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,6 +11,8 @@ -- Example exercises from the Digital Mathematics Environment (DWO)
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Examples
    ( linearExamples, quadraticExamples, higherDegreeExamples
    , factorizeExamples, expandExamples
src/Domain/Math/Polynomial/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Exercises
    ( linearExercise, linearMixedExercise
    , quadraticExercise, quadraticNoABCExercise
@@ -55,7 +57,7 @@                     <||> predicateView (equationSolvedWith doubleNF)
    , extraRules   = map use buggyRulesEquation ++
                     map use buggyRulesExpr
-   , ruleOrdering = ruleOrderingWithId
+   , ruleOrdering = ruleOrderingWith
                        [ getId coverUpTimes, getId flipEquation
                        , getId removeDivision
                        ]
@@ -86,7 +88,7 @@    , ready        = predicateView relationsSolvedForm
    , extraRules   = map use abcBuggyRules ++ buggyQuadratic ++
                     map use buggyRulesEquation ++ map use buggyRulesExpr
-   , ruleOrdering = ruleOrderingWithId $
+   , ruleOrdering = ruleOrderingWith $
                        quadraticRuleOrder ++ [getId buggySquareMultiplication]
    , strategy     = quadraticStrategy
    , navigation   = termNavigator
@@ -106,7 +108,7 @@    , ready         = predicateView relationsSolvedForm
    , extraRules    = map use abcBuggyRules ++ buggyQuadratic ++
                      map use buggyRulesEquation ++ map use buggyRulesExpr
-   , ruleOrdering  = ruleOrderingWithId quadraticRuleOrder
+   , ruleOrdering  = ruleOrderingWith quadraticRuleOrder
    , strategy      = higherDegreeStrategy
    , navigation    = termNavigator
    , examples      = mapExamples (singleton . build equationView) higherDegreeExamples
@@ -151,7 +153,7 @@    , similarity   = withoutContext ((==) `on` cleanUpExpr)
    , equivalence  = withoutContext (viewEquivalent (polyViewWith rationalView))
    , ready        = predicateView linearFactorsView
-   , ruleOrdering = ruleOrderingWithId quadraticRuleOrder
+   , ruleOrdering = ruleOrderingWith quadraticRuleOrder
    , strategy     = findFactorsStrategy
    , navigation   = termNavigator
    , extraRules   = map liftToContext buggyRulesExpr
@@ -167,7 +169,7 @@    , similarity   = withoutContext ((==) `on` cleanUpExpr)
    , equivalence  = withoutContext (viewEquivalent (polyViewWith rationalView))
    , ready        = predicateView (polyNormalForm rationalView)
-   , ruleOrdering = ruleOrderingWithId (getId fractionProduct:quadraticRuleOrder)
+   , ruleOrdering = ruleOrderingWith (getId fractionProduct:quadraticRuleOrder)
    , strategy     = expandStrategy
    , navigation   = termNavigator
    , extraRules   = map liftToContext buggyRulesExpr
src/Domain/Math/Polynomial/Generators.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Generators.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Generators
    ( polynomialGen, polynomialDegreeGen
    , cubicGen, quadraticGen, linearGen
src/Domain/Math/Polynomial/IneqExercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: IneqExercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.IneqExercises
    ( ineqLinearExercise, ineqQuadraticExercise, ineqHigherDegreeExercise
    ) where
@@ -66,7 +68,7 @@    , similarity    = simIneqContext
    , strategy      = ineqQuadratic
    , navigation    = termNavigator
-   , ruleOrdering  = ruleOrderingWithId quadraticRuleOrder
+   , ruleOrdering  = ruleOrderingWith quadraticRuleOrder
    , examples      = level Medium $
                      map (Logic.Var . build inequalityView)
                          (concat $ ineqQuad1 ++ [ineqQuad2, extraIneqQuad])
@@ -84,7 +86,7 @@    , similarity    = simIneqContext
    , strategy      = ineqHigherDegree
    , navigation    = termNavigator
-   , ruleOrdering  = ruleOrderingWithId quadraticRuleOrder
+   , ruleOrdering  = ruleOrderingWith quadraticRuleOrder
    , examples      = level Medium $ map (Logic.Var . build inequalityView) ineqHigh
    }
src/Domain/Math/Polynomial/LeastCommonMultiple.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: LeastCommonMultiple.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.LeastCommonMultiple
    ( lcmExpr, divisionExpr, noCommonFactor, equalFactors, testLCM
    , powerProductView
@@ -93,19 +95,20 @@       in (e, n) : merge xs2
 
 testLCM :: TestSuite
-testLCM = suite "lcmExpr" $ do
-   addProperty "transitivity" $ f3 $ \a b c ->
-      lcmExpr a (lcmExpr b c) ~= lcmExpr (lcmExpr a b) c
-   addProperty "commutativity" $ f2 $ \a b ->
-      lcmExpr a b ~= lcmExpr b a
-   addProperty "idempotency" $ f1 $ \a ->
-      lcmExpr a a ~= absExpr a
-   addProperty "zero" $ f1 $ \a ->
-      lcmExpr a 0 ~= 0
-   addProperty "one" $ f1 $ \a ->
-      lcmExpr a 1 ~= absExpr a
-   addProperty "sign" $ f2 $ \a b ->
-      lcmExpr a b ~= lcmExpr (-a) b
+testLCM = suite "lcmExpr"
+   [ useProperty "transitivity" $ f3 $ \a b c ->
+        lcmExpr a (lcmExpr b c) ~= lcmExpr (lcmExpr a b) c
+   , useProperty "commutativity" $ f2 $ \a b ->
+        lcmExpr a b ~= lcmExpr b a
+   , useProperty "idempotency" $ f1 $ \a ->
+        lcmExpr a a ~= absExpr a
+   , useProperty "zero" $ f1 $ \a ->
+        lcmExpr a 0 ~= 0
+   , useProperty "one" $ f1 $ \a ->
+        lcmExpr a 1 ~= absExpr a
+   , useProperty "sign" $ f2 $ \a b ->
+        lcmExpr a b ~= lcmExpr (-a) b
+   ]
  where
    f1 g = liftM  g genExpr
    f2 g = liftM2 g genExpr genExpr
src/Domain/Math/Polynomial/RationalExamples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,6 +12,8 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html.
 --
 -----------------------------------------------------------------------------
+--  $Id: RationalExamples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.RationalExamples
    ( brokenEquations, normBroken, normBroken2, normBrokenCon, deelUit
    ) where
src/Domain/Math/Polynomial/RationalExercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: RationalExercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.RationalExercises
    ( rationalEquationExercise
    , simplifyRationalExercise, divisionRationalExercise
@@ -55,7 +57,7 @@    , equivalence   = eqRationalEquation
    , similarity    = withoutContext (viewEquivalent (traverseView (traverseView cleanUpView)))
    , strategy      = rationalEquationStrategy
-   , ruleOrdering  = ruleOrderingWithId quadraticRuleOrder
+   , ruleOrdering  = ruleOrderingWith quadraticRuleOrder
    , navigation    = termNavigator
    , examples      = level Medium $ map singleton (concat brokenEquations)
    }
@@ -70,7 +72,7 @@ --   , equivalence   = withoutContext eqSimplifyRational
    , similarity    = withoutContext (viewEquivalent cleanUpView)
    , strategy      = simplifyRationalStrategy
-   , ruleOrdering  = ruleOrderingWithId quadraticRuleOrder
+   , ruleOrdering  = ruleOrderingWith quadraticRuleOrder
    , navigation    = termNavigator
    , examples      = level Medium $ concat (normBroken ++ normBroken2)
    }
src/Domain/Math/Polynomial/RationalRules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: RationalRules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.RationalRules
    ( divisionIsZero, divisionIsOne, sameDivisor, sameDividend
    , crossMultiply, multiplyOneDiv, fractionPlus, cancelTermsDiv
src/Domain/Math/Polynomial/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Rules
    ( sameConFactor, abcFormula, allPowerFactors, bringAToOne, cancelTerms
    , commonFactorVar, commonFactorVarNew, defPowerNat
src/Domain/Math/Polynomial/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Strategies
    ( linearStrategy, linearMixedStrategy, linearStrategyG
    , quadraticStrategy, quadraticStrategyG
src/Domain/Math/Polynomial/Tests.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,9 +9,10 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Tests.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Tests (tests) where
 
-import Control.Monad
 import Domain.Math.Data.Polynomial
 import Ideas.Common.Algebra.Field
 import Ideas.Common.Algebra.FieldLaws
@@ -19,6 +20,7 @@ import Ideas.Common.Utils.TestSuite
 
 tests :: TestSuite
-tests = suite "Polynomial is a commutative ring" $
-   forM_ (commutativeRingLaws :: [Law (SafeNum (Polynomial Int))]) $ \p ->
-      addProperty (show p) p+tests = suite "Polynomial is a commutative ring"
+   [ useProperty (show p) p
+   | p <- commutativeRingLaws :: [Law (SafeNum (Polynomial Int))]
+   ]
src/Domain/Math/Polynomial/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Polynomial.Views
    ( polyView, polyViewWith
    , quadraticView, quadraticViewWith
src/Domain/Math/Power/Equation/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,6 +12,8 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html.
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Power.Equation.Examples
    ( powerEquations, expEquations, logEquations, higherPowerEquations
    , rootEquations, rootEquations2, rootSubstEquations, expEquations2
src/Domain/Math/Power/Equation/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Power.Equation.Exercises
    ( powerEqExercise
    , expEqExercise
@@ -64,7 +66,7 @@                            && rightHandSide rel `belongsTo` rationalView
   , suitable       = predicateView normExpEqView
   , equivalence    = withoutContext (viewEquivalent normExpEqView)
-  , ruleOrdering   = ruleOrderingWithId [getId root2power]
+  , ruleOrdering   = ruleOrderingWith [getId root2power]
   }
 
 logEqExercise :: Exercise (OrList (Relation Expr))
@@ -79,7 +81,7 @@   , ready          = predicateView relationsSolvedForm
   , suitable       = predicateView (traverseView equationView >>> normLogEqView)
   , equivalence    = withoutContext (viewEquivalent (traverseView equationView >>> normLogEqView))
-  , ruleOrdering   = ruleOrderingWithId [getId calcPower]
+  , ruleOrdering   = ruleOrderingWith [getId calcPower]
   }
 
 higherPowerEqExercise :: Exercise (OrList (Equation Expr))
@@ -95,7 +97,7 @@   , ready          = predicateView relationsSolvedForm
   , suitable       = predicateView (traverseView normPowerEqView)
   , equivalence    = withoutContext (viewEquivalent (normPowerEqView' hasSomeVar >>> higherDegreeEquationsView))
-  , ruleOrdering   = ruleOrderingWithId [getId calcPower]
+  , ruleOrdering   = ruleOrderingWith [getId calcPower]
   }
 
 rootEqExercise :: Exercise (OrList (Equation Expr))
@@ -110,5 +112,5 @@   , ready          = predicateView relationsSolvedForm
   , suitable       = predicateView (traverseView normPowerEqView)
   , equivalence    = withoutContext (on (==) (sortOrList . simplify (normPowerEqView' $ elem "x" . vars)))
-  , ruleOrdering   = ruleOrderingWithId [getId calcPower]
+  , ruleOrdering   = ruleOrderingWith [getId calcPower]
   }
src/Domain/Math/Power/Equation/NormViews.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,11 +9,14 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: NormViews.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Power.Equation.NormViews
    ( normPowerEqApproxView, normExpEqView, normLogEqView
    , normPowerEqView, normPowerEqView'
    ) where
 
+import Control.Applicative
 import Control.Monad
 import Data.List
 import Data.Maybe
@@ -41,8 +44,8 @@ normPowerEqApproxView d = makeView f (uncurry (.~=.))
    where
      f rel = case relationType rel of
-      EqualTo       -> fmap (second (simplifyWith (precision d) doubleView))
-                     $ match (equationView >>> normPowerEqView) rel
+      EqualTo       -> second (simplifyWith (precision d) doubleView) <$>
+                       match (equationView >>> normPowerEqView) rel
       Approximately -> return (leftHandSide rel, rightHandSide rel)
       _             -> Nothing
 
@@ -196,7 +199,7 @@            ry <- match rationalView y
            rx <- match rationalView x
            guard $ denominator rx == 1 && denominator ry /= 1
-           fmap fromInteger $
+           fromInteger <$>
               takeRoot (numerator rx Prelude.^ numerator ry) (denominator ry)
          `mplus` do
            -- (a/b)^y -> a^y/b^y
src/Domain/Math/Power/Equation/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.Equation.Rules
   -- ( -- * Power equation rules
src/Domain/Math/Power/Equation/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.Equation.Strategies
    -- ( powerEqStrategy
src/Domain/Math/Power/Examples.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -12,6 +12,8 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html.
 --
 -----------------------------------------------------------------------------
+--  $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Power.Examples where
 
 import Domain.Math.Expr
src/Domain/Math/Power/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,6 +10,7 @@ --
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.Exercises
    ( -- * Power exercises
@@ -61,7 +62,7 @@                            ++ powers1 ++ powers2
                            ++ negExp1 ++ negExp2
                            ++ normPower1 ++ normPower2 ++ normPower3
-   , ruleOrdering = ruleOrderingWithId $ map getId
+   , ruleOrdering = ruleOrderingWith $ map getId
                       [ root2power, subExponents, reciprocalVar, addExponents
                       , mulExponents, distributePower ]
    }
@@ -86,7 +87,7 @@    , examples     = level Medium $ concat $  powersOfA ++ powersOfX
                            ++ brokenExp1' ++ brokenExp2 ++ brokenExp3
                            ++ normPower5' ++ normPower6
-   , ruleOrdering = ruleOrderingWithId $ map getId
+   , ruleOrdering = ruleOrderingWith $ map getId
                       [ root2power, addExponents, subExponents, mulExponents
                       ,  distributePower, reciprocalVar ]
    }
@@ -110,11 +111,11 @@    , examples     = level Medium $ concat $  nonNegExp ++ nonNegExp2 ++ negExp4 ++ negExp5
                            ++ brokenExp1
                            ++ normPower4' ++ normPower5
-   , ruleOrdering = ruleOrderingWithId [ getId mulExponents
-                                       , getId reciprocalFrac
-                                       , getId reciprocalInv
-                                       , getId power2root
-                                       , getId distributePower ]
+   , ruleOrdering = ruleOrderingWith [ getId mulExponents
+                                     , getId reciprocalFrac
+                                     , getId reciprocalInv
+                                     , getId power2root
+                                     , getId distributePower ]
    }
 
 -- | Calculate the integer number for the given power expression. Supported
src/Domain/Math/Power/NormViews.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: NormViews.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.NormViews
    ( -- * Normalising views
src/Domain/Math/Power/OldViews.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: OldViews.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.OldViews
    ( powerFactorView, powerFactorViewForWith, powerFactorViewWith
src/Domain/Math/Power/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.Rules
   ( -- * Power rules
src/Domain/Math/Power/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.Strategies
    ( -- * Power strategies
src/Domain/Math/Power/Utils.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE FlexibleInstances #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -13,6 +13,8 @@ -- moved to other parts of the framework (eg. Common)
 --
 -----------------------------------------------------------------------------
+--  $Id: Utils.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Power.Utils where
 
 import Data.Foldable (toList)
src/Domain/Math/Power/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,7 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
 
 module Domain.Math.Power.Views
    ( -- * Power views
src/Domain/Math/Safe.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Safe.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Safe
    ( -- * Safe division
      SafeDiv(..), safeDivFractional
src/Domain/Math/Simplification.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-}
 -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -10,6 +10,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Simplification.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.Simplification
    ( Simplify(..), SimplifyConfig(..)
    , simplifyConfig
src/Domain/Math/SquareRoot/Tests.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Tests.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.SquareRoot.Tests (tests) where
 
 import Domain.Math.Data.SquareRoot
@@ -22,9 +24,10 @@ -- Testing
 
 tests :: TestSuite
-tests = mapM_ f $ commutativeRingLaws ++
-                  distributiveSubtractionLaws ++
-                  map fromAdditiveLaw appendInverseLaws
+tests = mconcat $ map f $
+   commutativeRingLaws ++
+   distributiveSubtractionLaws ++
+   map fromAdditiveLaw appendInverseLaws
  where
    f :: Law (SafeNum (SquareRoot Rational)) -> TestSuite
-   f p = addProperty (show p) p+   f p = useProperty (show p) p
src/Domain/Math/SquareRoot/Views.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.Math.SquareRoot.Views
    ( squareRootView, squareRootViewWith
    ) where
src/Domain/RelationAlgebra.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: RelationAlgebra.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra (module Export) where
 
 import Domain.RelationAlgebra.Exercises as Export
src/Domain/RelationAlgebra/Exercises.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra.Exercises (cnfExercise) where
 
 import Data.Maybe
@@ -35,13 +37,13 @@    , 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)
+                      in useGenerator (\_ -> templateGenerator 1 `suchThat` ok)
    , testGenerator  = Just arbitrary
    }
 
 stepsRemaining :: Int -> RelAlg -> Maybe Int
 stepsRemaining i =
-   lengthMax i . derivationTree False toCNF . inContext cnfExercise
+   lengthMax i . derivationTree toCNF . inContext cnfExercise
 
 {- cnfExerciseSimple :: Exercise RelAlg
 cnfExerciseSimple = cnfExercise
src/Domain/RelationAlgebra/Formula.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Formula.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra.Formula where
 
 import Control.Monad
src/Domain/RelationAlgebra/Generator.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Generator.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra.Generator (templateGenerator) where
 
 import Control.Monad
src/Domain/RelationAlgebra/Parser.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra.Parser (parseRelAlg, ppRelAlg) where
 
 import Domain.RelationAlgebra.Formula
src/Domain/RelationAlgebra/Rules.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra.Rules where
 
 import Domain.RelationAlgebra.Formula
@@ -40,7 +42,7 @@                    ]
 
 relalg :: IsId a => a -> Id
-relalg = ( # ) "relationalgebra"
+relalg = ( "relationalgebra" # )
 
 rule :: RuleBuilder f a => String -> f -> Rule a
 rule = C.rewriteRule . relalg
src/Domain/RelationAlgebra/Strategies.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -9,6 +9,8 @@ -- Portability :  portable (depends on ghc)
 --
 -----------------------------------------------------------------------------
+--  $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Domain.RelationAlgebra.Strategies (toCNF) where
 
 import Domain.RelationAlgebra.Formula
src/Main.hs view
@@ -1,5 +1,5 @@ -----------------------------------------------------------------------------
--- Copyright 2013, Open Universiteit Nederland. This file is distributed
+-- Copyright 2014, 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.
 -----------------------------------------------------------------------------
@@ -11,20 +11,19 @@ -- Main module for feedback services
 --
 -----------------------------------------------------------------------------
+--  $Id: Main.hs 6548 2014-05-16 10:34:18Z bastiaan $
+
 module Main (main) where
 
 import Control.Arrow
 import Ideas.Common.Exercise
 import Ideas.Common.Id
-import Ideas.Common.Utils (Some(..))
 import Ideas.Common.Utils.TestSuite
 import Ideas.Main.Default
-import Ideas.Service.DomainReasoner
-import Ideas.Service.ServiceList
-import Ideas.Service.Types (Service)
 import qualified Domain.LinearAlgebra as LA
 import qualified Domain.LinearAlgebra.Checks as LA
 import qualified Domain.Logic as Logic
+import qualified Domain.Logic.Consequence as Logic
 import qualified Domain.Logic.Proofs as Logic
 import qualified Domain.Math.ExerciseList as Math
 import qualified Domain.RelationAlgebra as RA
@@ -48,8 +47,10 @@    [ -- logic and relation-algebra
      Some Logic.dnfExercise
    , Some Logic.dnfUnicodeExercise
+   , Some Logic.cnfUnicodeExercise
    , Some Logic.proofExercise
    , Some Logic.proofUnicodeExercise
+   , Some Logic.consequenceExercise
    , Some RA.cnfExercise
      -- linear algebra
    , Some LA.gramSchmidtExercise
@@ -90,6 +91,7 @@    , ("linalg.systemwithmatrix",  "linearalgebra.systemwithmatrix")
    , ("logic.dnf",                "logic.propositional.dnf")
    , ("logic.dnf-unicode",        "logic.propositional.dnf.unicode")
+   , ("logic.proof",              "logic.propositional.proof")
    , ("relationalg.cnf",          "relationalgebra.cnf")
    -- MathDox compatibility
    , ("gaussianelimination"        , "linearalgebra.gaussianelim")
@@ -105,6 +107,5 @@    ] ++ Math.scriptList
 
 myTestSuite :: TestSuite
-myTestSuite = do
-   sequence_ Math.testSuiteList
-   LA.checks+myTestSuite =
+   mconcat Math.testSuiteList <> LA.checks