diff --git a/ideas-math.cabal b/ideas-math.cabal --- a/ideas-math.cabal +++ b/ideas-math.cabal @@ -1,5 +1,5 @@ name: ideas-math -version: 1.1 +version: 1.2 synopsis: Interactive domain reasoner for logic and mathematics homepage: http://ideas.cs.uu.nl/www/ description: @@ -11,10 +11,10 @@ linear algebra (Gaussian elimination and linear systems), and relation algebra. The domain reasoner is used by learning environments such as the digital mathematical environment of the Freudenthal Institute, MathDox, - ActiveMath, and the GenExas logic tool. + ActiveMath, and the LogEx logic tool. category: Education -copyright: (c) 2014 +copyright: (c) 2015 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.6.3 +tested-with: GHC == 7.4.1, GHC == 7.6.3, GHC == 7.8.3 -- feedback scripts extra-source-files: @@ -40,14 +40,14 @@ Executable ideas-math Main-is: Main.hs - ghc-options: -Wall + ghc-options: -Wall -fno-warn-orphans hs-source-dirs: src Build-Depends: base >= 4.2 && < 5, QuickCheck >= 2.4.1 && < 2.7, containers, random, parsec, - ideas == 1.2 + ideas == 1.3 Other-modules: Domain.LinearAlgebra.Checks diff --git a/src/Domain/LinearAlgebra.hs b/src/Domain/LinearAlgebra.hs --- a/src/Domain/LinearAlgebra.hs +++ b/src/Domain/LinearAlgebra.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: LinearAlgebra.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: LinearAlgebra.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra (module Export) where diff --git a/src/Domain/LinearAlgebra/Checks.hs b/src/Domain/LinearAlgebra/Checks.hs --- a/src/Domain/LinearAlgebra/Checks.hs +++ b/src/Domain/LinearAlgebra/Checks.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Checks.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Checks.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.Checks (checks) where diff --git a/src/Domain/LinearAlgebra/EquationsRules.hs b/src/Domain/LinearAlgebra/EquationsRules.hs --- a/src/Domain/LinearAlgebra/EquationsRules.hs +++ b/src/Domain/LinearAlgebra/EquationsRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: EquationsRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: EquationsRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.EquationsRules ( ruleCoverAllEquations, ruleUncoverEquation, ruleScaleEquation diff --git a/src/Domain/LinearAlgebra/Exercises.hs b/src/Domain/LinearAlgebra/Exercises.hs --- a/src/Domain/LinearAlgebra/Exercises.hs +++ b/src/Domain/LinearAlgebra/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.Exercises ( gramSchmidtExercise, linearSystemExercise diff --git a/src/Domain/LinearAlgebra/GramSchmidtRules.hs b/src/Domain/LinearAlgebra/GramSchmidtRules.hs --- a/src/Domain/LinearAlgebra/GramSchmidtRules.hs +++ b/src/Domain/LinearAlgebra/GramSchmidtRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: GramSchmidtRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: GramSchmidtRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.GramSchmidtRules ( ruleNext, ruleNextOrthogonal diff --git a/src/Domain/LinearAlgebra/LinearSystem.hs b/src/Domain/LinearAlgebra/LinearSystem.hs --- a/src/Domain/LinearAlgebra/LinearSystem.hs +++ b/src/Domain/LinearAlgebra/LinearSystem.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: LinearSystem.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: LinearSystem.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.LinearSystem where diff --git a/src/Domain/LinearAlgebra/LinearView.hs b/src/Domain/LinearAlgebra/LinearView.hs --- a/src/Domain/LinearAlgebra/LinearView.hs +++ b/src/Domain/LinearAlgebra/LinearView.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: LinearView.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: LinearView.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.LinearView ( IsLinear(..), LinearMap, renameVariables diff --git a/src/Domain/LinearAlgebra/Matrix.hs b/src/Domain/LinearAlgebra/Matrix.hs --- a/src/Domain/LinearAlgebra/Matrix.hs +++ b/src/Domain/LinearAlgebra/Matrix.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Matrix.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Matrix.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.Matrix ( Matrix, Row, Column, isRectangular, makeMatrix, identity, mapWithPos diff --git a/src/Domain/LinearAlgebra/MatrixRules.hs b/src/Domain/LinearAlgebra/MatrixRules.hs --- a/src/Domain/LinearAlgebra/MatrixRules.hs +++ b/src/Domain/LinearAlgebra/MatrixRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: MatrixRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: MatrixRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.MatrixRules ( ruleFindColumnJ, ruleExchangeNonZero, ruleScaleToOne diff --git a/src/Domain/LinearAlgebra/Parser.hs b/src/Domain/LinearAlgebra/Parser.hs --- a/src/Domain/LinearAlgebra/Parser.hs +++ b/src/Domain/LinearAlgebra/Parser.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Parser.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.Parser ( parseMatrix, parseVectorSpace, parseSystem diff --git a/src/Domain/LinearAlgebra/Strategies.hs b/src/Domain/LinearAlgebra/Strategies.hs --- a/src/Domain/LinearAlgebra/Strategies.hs +++ b/src/Domain/LinearAlgebra/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.Strategies ( gaussianElimStrategy, linearSystemStrategy diff --git a/src/Domain/LinearAlgebra/Vector.hs b/src/Domain/LinearAlgebra/Vector.hs --- a/src/Domain/LinearAlgebra/Vector.hs +++ b/src/Domain/LinearAlgebra/Vector.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Vector.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Vector.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.LinearAlgebra.Vector ( Vector, VectorSpace diff --git a/src/Domain/Logic.hs b/src/Domain/Logic.hs --- a/src/Domain/Logic.hs +++ b/src/Domain/Logic.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Logic.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Logic.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic (module Export) where diff --git a/src/Domain/Logic/BuggyRules.hs b/src/Domain/Logic/BuggyRules.hs --- a/src/Domain/Logic/BuggyRules.hs +++ b/src/Domain/Logic/BuggyRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Buggy rules in the logic domain, expressing common misconceptions -- ----------------------------------------------------------------------------- --- $Id: BuggyRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: BuggyRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.BuggyRules (buggyRules) where diff --git a/src/Domain/Logic/Consequence.hs b/src/Domain/Logic/Consequence.hs --- a/src/Domain/Logic/Consequence.hs +++ b/src/Domain/Logic/Consequence.hs @@ -1,6 +1,6 @@ {-# LANGUAGE RankNTypes #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,20 +12,20 @@ -- Exercise for the logic domain: to prove two propositions equivalent -- ----------------------------------------------------------------------------- --- $Id: Consequence.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Consequence.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Consequence (consequenceExercise) where import Control.Monad +import Data.Function (on) 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.Strategies (cnfStrategy) import Domain.Logic.Utils import Domain.Math.Expr () import Ideas.Common.Library hiding (singleton) @@ -121,12 +121,12 @@ keepInitialAssumptions <*> try (use conjIntro) -- use cnf for the (singleton) assumption - <*> repeatS (somewhere (use topIsAnd)) -- topIsAndCom - <*> onAssumption (useC cnfStrategyDWA) + <*> repeatS (somewhere splitTop) + <*> onAssumption (useC cnfStrategy) -- use cnf for the consequence - <*> onConsequence (useC cnfStrategyDWA) + <*> onConsequence (useC cnfStrategy) -- strong normalization of assumption and consequence - <*> repeatS (somewhere (use absorptionSubset <|> use fakeAbsorption <|> use fakeAbsorptionNot)) + <*> repeatS (somewhere (use absorptionAndSubset <|> use fakeAbsorption <|> use fakeAbsorptionNot)) <*> repeatS (somewhere splitTop) <*> use checkCNF <*> normStrategy where @@ -144,19 +144,44 @@ use assumptionIsFalse |> use conjElim |> use comAndSubset - |> somewhere (use ruleFalseZeroAnd <|> use ruleTrueZeroOr) - |> somewhere (use ruleComplOr) + |> somewhere (use ruleFalseAnd <|> use ruleTrueOr) |> somewhere ( use ruleIdempOr <|> use ruleIdempAnd <|> - use ruleOrOverAnd <|> - use ruleTrueZeroAnd + use ruleComplOr <|> + use absorptionAndSubset <|> + use ruleDistrOr <|> + use ruleTrueAnd ) |> oncetd (use sortRuleOr) |> oncetd (use sortRuleAnd) -- |> oncetd eliminateVar |> somewhereConjunct introduceVar +sortRuleOr :: Rule SLogic +sortRuleOr = ruleTrans "CommOr.sort" $ + sortRuleBy compareVar $ disjunctions <-> ors + +sortRuleAnd :: Rule SLogic +sortRuleAnd = ruleTrans "CommAnd.sort" $ + sortRuleBy compareVar $ conjunctions <-> ands + +sortRuleBy :: (b -> b -> Ordering) -> View a [b] -> Transformation a +sortRuleBy cmp v = makeTrans $ \p -> do + xs <- match v p + guard (not (sortedBy cmp xs)) + let ys = sortBy cmp xs + return (build v ys) + +sortedBy :: (a -> a -> Ordering) -> [a] -> Bool +sortedBy cmp = rec + where + rec (x:y:zs) = cmp x y /= GT && rec (y:zs) + rec _ = True + +compareVar :: Ord a => Logic a -> Logic a -> Ordering +compareVar = compare `on` (\x -> (varsLogic x, x)) + keepInitialAssumptions :: Rule (Context Proof) keepInitialAssumptions = minorRule "initial" $ \ctx -> do (ps, _) <- fmap proofPair (fromContext ctx) @@ -251,9 +276,8 @@ fmap (p :||:) (introContradiction a q) introContradiction _ _ = Nothing --- let op: ook commutatieve variant nog toevoegen topIsAnd :: Rule Proof -topIsAnd = {- minor $ !!!!!!!!!!!!!!!!!!!!!-} +topIsAnd = minor $ ruleTrans "top-is-and" $ acTopRuleFor False (collect andView) topIsAndCom :: Rule Proof @@ -353,8 +377,8 @@ -- (p \/ q) /\ ... /\ (p \/ q \/ r) ~> (p \/ q) /\ ... -- (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes) -absorptionSubset :: Rule SLogic -absorptionSubset = ruleList "absorptionSubset" $ \p -> do +absorptionAndSubset :: Rule SLogic +absorptionAndSubset = ruleList "absorpand-subset" $ \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 diff --git a/src/Domain/Logic/Examples.hs b/src/Domain/Logic/Examples.hs --- a/src/Domain/Logic/Examples.hs +++ b/src/Domain/Logic/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,37 +11,71 @@ -- A set of example proofs -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Examples - ( exampleProofs + ( dnfExamples, cnfExamples, exampleProofs ) where import Domain.Logic.Formula import Ideas.Common.Exercise import Ideas.Common.Utils (ShowString(..)) -exampleProofs :: [(Difficulty, (SLogic, SLogic))] +dnfExamples :: Examples SLogic +dnfExamples = + [ (Easy, Not(q :->: r) :||: q :||: r) + , (Medium, (Not q :&&: Not (p :->: q)) :->: p) + , (Medium, ((q :||: Not r) :&&: (q :||: p) :&&: Not q)) + , (Medium, Not p :<->: (p :&&: q)) + , (Difficult, (p :||: q) :&&: (r :<->: p)) + ] + -- ((q :&&: r) :->: (q :->: r)) :->: (r :&&: (q :->: p)) + -- (q :&&: p) :<->: (q :&&: r) + -- Not ((p :&&: q) :<->: (Not r :||: q)) + where + p = Var (ShowString "p") + q = Var (ShowString "q") + r = Var (ShowString "r") + +cnfExamples :: Examples SLogic +cnfExamples = + [ (Easy, Not ((q :->: r) :->: Not q)) + , (Easy, (Not q :&&: Not (p :->: q)) :->: p) + , (Medium, ((q :||: p) :->: (q :->: p)) :->: (r :&&: q :&&: p)) + , (Medium, p :<->: (p :&&: q)) + , (Difficult, (p :&&: q) :||: (p :<->: r)) + ] + -- Not (q :->: r) :||: q :||: r + -- ((q :||: p) :&&: (p :||: r)) :||: Not (q :||: r) + -- (q :&&: p) :<->: (q :&&: r) + where + p = Var (ShowString "p") + q = Var (ShowString "q") + r = Var (ShowString "r") + +exampleProofs :: Examples (SLogic, SLogic) exampleProofs = - [ {- 1 -} medium (Not(p :||: (Not p :&&: q)), Not(p :||: q)) - , {- 2 -} medium ((p :->: q):||: Not p, (p :->: q) :||: q) + [ {- 16 -} easy (Not(p :&&: q) :||: (s :||: Not r), (p :&&: q) :->: (r :->: s)) + , {- 13 -} medium (Not((p :->:q) :->: (p:&&:q)), (p :->: q) :&&: (Not p :||: Not q)) + , {- 14 -} medium (Not((p :<->: q) :->: (p :||: (p :<->: q))), F) , {- 3 -} difficult ((p :&&: Not q):||:(q :&&: Not p), (p :||:q):&&:Not(p :&&: q)) - , {- 4 -} medium (Not(p :||: Not(p :||: Not q)), Not(p :||: q)) - , {- 5 -} difficult (p :<->: q, (p :->: q) :&&: (q :->: p)) + , {- 28 -} difficult ((p :&&: (q :&&: r)) :||: (Not p :&&: q), (Not p :&&: (q :&&: Not r)) :||: ( q :&&: r)) + + , {- 4 -} easy (Not(p :||: Not(p :||: Not q)), Not(p :||: q)) , {- 6 -} medium ((p :&&: q) :->: p, T) + , {- 12 -} medium ((p :->: q):->: (p :->: s), (Not q :->: Not p) :->: (Not s :->: Not p)) + , {- 19 -} easy (p :&&: q, Not(p :->: Not q)) + , {- 1 -} medium (Not(p :||: (Not p :&&: q)), Not(p :||: q)) + , {- 2 -} medium ((p :->: q):||: Not p, (p :->: q) :||: q) + , {- 5 -} difficult (p :<->: q, (p :->: q) :&&: (q :->: p)) , {- 7 -} medium ((p :->: q) :||: (q :->: p), T) , {- 8 -} difficult ((q :->: (Not p :->: q)) :->: p, Not p :->: (q :&&: ((p :&&: q) :&&: 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 -} 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 -} medium ((p :->: q) :->: Not p, p :->: (q :->: Not p)) , {- 22 -} medium ((Not q :&&: p) :->: p, (Not q :<->: q) :->: p) @@ -50,7 +84,6 @@ , {- 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)) diff --git a/src/Domain/Logic/Exercises.hs b/src/Domain/Logic/Exercises.hs --- a/src/Domain/Logic/Exercises.hs +++ b/src/Domain/Logic/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,15 +12,16 @@ -- "Discrete Wiskunde A (DWA)" -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Exercises - ( dnfExercise, dnfUnicodeExercise, cnfUnicodeExercise + ( dnfExercise, dnfUnicodeExercise, cnfExercise, cnfUnicodeExercise , extraLogicRules ) where import Data.Maybe import Domain.Logic.BuggyRules +import Domain.Logic.Examples import Domain.Logic.Formula import Domain.Logic.GeneralizedRules import Domain.Logic.Generator @@ -45,10 +46,11 @@ , ready = predicate isDNF , suitable = predicate notTooManyEquivs , extraRules = map liftToContext (extraLogicRules ++ buggyRules) - , strategy = dnfStrategyDWA + , strategy = dnfStrategy , navigation = navigator , testGenerator = Just (arbitrary `suchThat` notTooManyEquivs) , randomExercise = useGenerator dnfExerciseGenerator + , examples = dnfExamples } -- Direct support for unicode characters @@ -60,34 +62,41 @@ , prettyPrinter = ppLogicUnicodePars } -cnfUnicodeExercise :: Exercise SLogic -cnfUnicodeExercise = makeExercise - { exerciseId = describe "Proposition to CNF (unicode support)" $ - propositionalId # "cnf.unicode" +cnfExercise :: Exercise SLogic +cnfExercise = makeExercise + { exerciseId = describe "Proposition to CNF" $ + propositionalId # "cnf" , status = Stable - , parser = parseLogicUnicodePars - , prettyPrinter = ppLogicUnicodePars + , parser = parseLogicPars + , prettyPrinter = ppLogicPars , equivalence = withoutContext eqLogic , similarity = withoutContext equalLogicA , ready = predicate isCNF , suitable = predicate notTooManyEquivs , extraRules = map liftToContext (extraLogicRules ++ buggyRules) - , strategy = cnfStrategyDWA + , strategy = cnfStrategy , navigation = navigator , testGenerator = Just (arbitrary `suchThat` notTooManyEquivs) , randomExercise = useGenerator cnfExerciseGenerator + , examples = cnfExamples } +cnfUnicodeExercise :: Exercise SLogic +cnfUnicodeExercise = cnfExercise + { exerciseId = describe "Proposition to CNF (unicode support)" $ + propositionalId # "cnf.unicode" + , parser = parseLogicUnicodePars + , prettyPrinter = ppLogicUnicodePars + } + extraLogicRules :: [Rule SLogic] extraLogicRules = [ ruleCommOr, ruleCommAnd, ruleAssocOr, ruleAssocAnd - , generalRuleOrOverAnd, ruleOrOverAnd + , generalRuleDistrOr, ruleDistrOr + , generalRuleDistrAnd, ruleDistrAnd , inverseDeMorganOr, inverseDeMorganAnd , inverseAndOverOr, inverseOrOverAnd - -- Rules that are NOT allowed in DWA - -- , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl - -- , ruleCommEquiv, ruleDefEquivImpls, ruleEquivSame, ruleImplSame - ] + ] ++ inverseRules notTooManyEquivs :: SLogic -> Bool notTooManyEquivs = (<=2) . countEquivalences @@ -106,7 +115,15 @@ in gen `suchThat` ok where stepsRemaining i = - lengthMax i . derivationTree (strategy ex) . inContext ex + checkLength i ex + +checkLength :: Int -> Exercise a -> a -> Maybe Int +checkLength n ex a = defaultDerivation ex a >>= rec 0 . steps + where + rec i [] = Just i + rec i (_:xs) + | i >= n = Nothing + | otherwise = rec (i+1) xs -- QuickCheck property to monitor the number of steps needed -- to normalize a random proposition (30-40% is ok) diff --git a/src/Domain/Logic/Formula.hs b/src/Domain/Logic/Formula.hs --- a/src/Domain/Logic/Formula.hs +++ b/src/Domain/Logic/Formula.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Formula.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Formula.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Formula ( module Domain.Logic.Formula, module Ideas.Common.Algebra.Boolean diff --git a/src/Domain/Logic/GeneralizedRules.hs b/src/Domain/Logic/GeneralizedRules.hs --- a/src/Domain/Logic/GeneralizedRules.hs +++ b/src/Domain/Logic/GeneralizedRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,11 +11,11 @@ -- Generalized rules, and inverse rules, for De Morgan and distributivity -- ----------------------------------------------------------------------------- --- $Id: GeneralizedRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: GeneralizedRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.GeneralizedRules ( generalRuleDeMorganOr, generalRuleDeMorganAnd - , generalRuleAndOverOr, generalRuleOrOverAnd + , generalRuleDistrAnd, generalRuleDistrOr ) where -- Note: the generalized rules do not take AC-unification into account, @@ -30,46 +30,65 @@ generalRuleDeMorganOr :: Rule SLogic generalRuleDeMorganOr = - siblingOf groupDeMorgan $ makeSimpleRule "GenDeMorganOr" f + siblingOf groupDeMorgan $ makeListRule "GenDeMorganOr" f where f (Not e) = do - let xs = disjunctions e + xs <- subDisjunctions e guard (length xs > 2) return (ands (map Not xs)) - f _ = Nothing + f _ = [] generalRuleDeMorganAnd :: Rule SLogic generalRuleDeMorganAnd = - siblingOf groupDeMorgan $ makeSimpleRule "GenDeMorganAnd" f + siblingOf groupDeMorgan $ makeListRule "GenDeMorganAnd" f where f (Not e) = do - let xs = conjunctions e + xs <- subConjunctions e guard (length xs > 2) return (ors (map Not xs)) - f _ = Nothing + f _ = [] -generalRuleAndOverOr :: Rule SLogic -generalRuleAndOverOr = - siblingOf groupDistribution $ makeSimpleRule "GenAndOverOr" f +generalRuleDistrAnd :: Rule SLogic +generalRuleDistrAnd = + siblingOf groupDistribution $ makeListRule "GenAndOverOr" f where - f (x :&&: y) = - case (disjunctions x, disjunctions y) of - (xs, _) | length xs > 2 -> - return (ors (map (:&&: y) xs)) - (_, ys) | length ys > 2 -> - return (ors (map (x :&&:) ys)) - _ -> Nothing - f _ = Nothing + f (x :&&: y) = do -- left distributive + ys <- subDisjunctions y + guard (length ys > 2) + return (ors (map (x :&&:) ys)) + `mplus` do -- right distributive + xs <- subDisjunctions x + guard (length xs > 2) + return (ors (map (:&&: y) xs)) + f _ = [] -generalRuleOrOverAnd :: Rule SLogic -generalRuleOrOverAnd = - siblingOf groupDistribution $ makeSimpleRule "GenOrOverAnd" f +generalRuleDistrOr :: Rule SLogic +generalRuleDistrOr = + siblingOf groupDistribution $ makeListRule "GenOrOverAnd" f where - f (x :||: y) = - case (conjunctions x, conjunctions y) of - (xs, _) | length xs > 2 -> - return (ands (map (:||: y) xs)) - (_, ys) | length ys > 2 -> - return (ands (map (x :||:) ys)) - _ -> Nothing - f _ = Nothing + f (x :||: y) = do -- left distributive + ys <- subConjunctions y + guard (length ys > 2) + return (ands (map (x :||:) ys)) + `mplus` do -- right distributive + xs <- subConjunctions x + guard (length xs > 2) + return (ands (map (:||: y) xs)) + f _ = [] + +------------------------------------------------------------------------- +-- Helper functions + +-- All combinations where some disjunctions are grouped, and others are not +subDisjunctions :: SLogic -> [[SLogic]] +subDisjunctions = subformulas (:||:) . disjunctions + +subConjunctions :: SLogic -> [[SLogic]] +subConjunctions = subformulas (:&&:) . conjunctions + +subformulas :: (a -> a -> a) -> [a] -> [[a]] +subformulas _ [] = [] +subformulas _ [x] = [[x]] +subformulas op (x:xs) = map (x:) yss ++ [ op x y : ys| y:ys <- yss ] + where + yss = subformulas op xs diff --git a/src/Domain/Logic/Generator.hs b/src/Domain/Logic/Generator.hs --- a/src/Domain/Logic/Generator.hs +++ b/src/Domain/Logic/Generator.hs @@ -1,6 +1,6 @@ {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -10,7 +10,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Generator.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Generator.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Generator ( generateLogic, generateLevel, equalLogicA, equalLogicACI diff --git a/src/Domain/Logic/InverseRules.hs b/src/Domain/Logic/InverseRules.hs --- a/src/Domain/Logic/InverseRules.hs +++ b/src/Domain/Logic/InverseRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,18 +11,21 @@ -- Generalized rules, and inverse rules, for De Morgan and distributivity -- ----------------------------------------------------------------------------- --- $Id: InverseRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: InverseRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.InverseRules ( inverseDeMorganOr, inverseDeMorganAnd , inverseAndOverOr, inverseOrOverAnd + , inverseRules ) 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.Generator import Domain.Logic.Utils +-- import Domain.Logic.Rules import Ideas.Common.Library ----------------------------------------------------------------------------- @@ -91,4 +94,84 @@ allSame :: Eq a => [a] -> Bool allSame [] = True -allSame (x:xs) = all (==x) xs +allSame (x:xs) = all (==x) xs + +----------------------------------------------------------------------------- +-- More inverse rules + +inverseRules :: [Rule SLogic] +inverseRules = + [ invDefImpl, invDefEquiv, invDoubleNeg, invIdempOr, invIdempAnd + , invTrueAnd, invNotTrue, invFalseOr, invNotFalse + , invDistrAnd, invDistrOr + -- , invAbsorpOr, invAbsorpAnd, invTrueOr, invComplOr, invFalseAnd + -- , invComplAnd, invDistrAnd, invDistrOr + ] + +invDefImpl :: Rule SLogic +invDefImpl = siblingOf groupImplication $ rewriteRule "DefImpl.inv" $ + \x y -> Not x :||: y :~> x :->: y + +invDefEquiv :: Rule SLogic +invDefEquiv = siblingOf groupEquivalence $ rewriteRule "DefEquiv.inv" $ + \x y -> (x :&&: y) :||: (Not x :&&: Not y) :~> x :<->: y + +invDoubleNeg :: Rule SLogic +invDoubleNeg = siblingOf groupDoubleNegation $ rewriteRule "NotNot.inv" $ + \x -> x :~> Not (Not x) + +invIdempOr :: Rule SLogic +invIdempOr = siblingOf groupIdempotency $ rewriteRule "IdempOr.inv" $ + \x -> x :~> x :||: x + +invIdempAnd :: Rule SLogic +invIdempAnd = siblingOf groupIdempotency $ rewriteRule "IdempAnd.inv" $ + \x -> x :~> x :&&: x + +invTrueAnd :: Rule SLogic +invTrueAnd = siblingOf groupTrueConjunction $ rewriteRules "TrueZeroAnd.inv" + [ \x -> x :~> T :&&: x + , \x -> x :~> x :&&: T + ] + +invNotTrue :: Rule SLogic +invNotTrue = siblingOf groupNotTrue $ rewriteRule "NotTrue.inv" $ + F :~> Not T + +invFalseOr :: Rule SLogic +invFalseOr = siblingOf groupFalseDisjunction $ rewriteRules "FalseZeroOr.inv" + [ \x -> x :~> F :||: x + , \x -> x :~> x :||: F + ] + +invNotFalse :: Rule SLogic +invNotFalse = siblingOf groupNotFalse $ rewriteRule "NotFalse.inv" $ + T :~> Not F + +invDistrAnd :: Rule SLogic +invDistrAnd = siblingOf groupDistribution $ rewriteRules "AndOverOr.inv" + [ \x y z -> (x :&&: y) :||: (x :&&: z) :~> x :&&: (y :||: z) + , \x y z -> (x :&&: z) :||: (y :&&: z) :~> (x :||: y) :&&: z + ] + +invDistrOr :: Rule SLogic +invDistrOr = siblingOf groupDistribution $ rewriteRules "OrOverAnd.inv" + [ \x y z -> (x :||: y) :&&: (x :||: z) :~> x :||: (y :&&: z) + , \x y z -> (x :||: z) :&&: (y :||: z) :~> (x :&&: y) :||: z + ] + +{- TO DO: fix code below +proofInvRule :: String -> Rule SLogic -> Rule SLogic +proofInvRule = makeInvRule equalLogicA + +invAbsorpOr, invAbsorpAnd, invTrueOr, invComplOr, invFalseAnd, + invComplAnd, invDistrAnd, invDistrOr :: Rule SLogic +invAbsorpOr = proofInvRule "AbsorpOr.inv" ruleAbsorpOr +invAbsorpAnd = proofInvRule "AbsorpAnd.inv" ruleAbsorpAnd +invTrueOr = proofInvRule "TrueZeroOr.inv" ruleTrueOr +invComplOr = proofInvRule "ComplOr.inv" ruleComplOr +invFalseAnd = proofInvRule "FalseZeroAnd.inv" ruleFalseAnd +invComplAnd = proofInvRule "ComplAnd.inv" ruleComplAnd +invDistrAnd = proofInvRule "AndOverOr.inv" ruleDistrAnd -- see GeneralizedRules +invDistrOr = proofInvRule "OrOverAnd.inv" ruleDistrOr -- see GeneralizedRules +-} diff --git a/src/Domain/Logic/Parser.hs b/src/Domain/Logic/Parser.hs --- a/src/Domain/Logic/Parser.hs +++ b/src/Domain/Logic/Parser.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,16 +9,18 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Parser.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Parser ( parseLogic, parseLogicPars, parseLogicUnicodePars, parseLogicProof - , parseConsequence + , parseLogicProofs, parseConsequence , ppLogicPars, ppLogicUnicodePars + , associateToRight ) where import Domain.Logic.Formula import Ideas.Common.Utils (ShowString(..)) +import Ideas.Common.Utils.Uniplate import Ideas.Text.Parsing import qualified Text.ParserCombinators.Parsec.Token as P @@ -70,6 +72,14 @@ q <- parserSLogic unicode True return (p, q) +parseLogicProofs :: String -> Either String [(SLogic, SLogic)] +parseLogicProofs = parseSimple $ commaSep1 $ do + let unicode = False + 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) @@ -157,19 +167,36 @@ ppLogicUnicodePars = ppLogicParsGen unicodeTuple ppLogicParsGen :: SymbolTuple -> SLogic -> String -ppLogicParsGen (impl, equiv, conj, disj, neg, tr, fl) = - (\f -> f 0 "") . foldLogic alg +ppLogicParsGen (impl, equiv, conj, disj, neg, tr, fl) = rec1 where - alg = ( pp . fromShowString, binop 3 impl, binop 3 equiv, binop 1 conj - , binop 2 disj, nott, pp tr, pp fl - ) - binop :: Int -> String -> (Int -> String -> String) -> (Int -> String -> String) -> Int -> String -> String - binop prio op p q n = - parIf (n/=0 && (n==3 || prio/=n)) - (p prio . ((" "++op++" ")++) . q prio) - pp s = const (s++) - nott p _ = (neg++) . p 3 - parIf b f = if b then ("("++) . f . (")"++) else f + rec1 p@(_ :&&: _) = recAnd p + rec1 p@(_ :||: _) = recOr p + rec1 (p :->: q) = binop impl (rec2 p) (rec2 q) + rec1 (p :<->: q) = binop equiv (rec2 p) (rec2 q) + rec1 p = rec2 p + + recAnd (p :&&: q) = binop conj (recAnd p) (recAnd q) + recAnd p = rec2 p + + recOr (p :||: q) = binop disj (recOr p) (recOr q) + recOr p = rec2 p + + rec2 (Not p) = neg ++ rec2 p + rec2 p = rec3 p + + -- atoms + rec3 (Var x) = fromShowString x + rec3 T = tr + rec3 F = fl + rec3 p = pars (rec1 p) + + binop op x y = unwords [x, op, y] + pars s = "(" ++ s ++ ")" + +associateToRight :: Logic a -> Logic a +associateToRight p@(_ :&&: _) = ands (map associateToRight (conjunctions p)) +associateToRight p@(_ :||: _) = ors (map associateToRight (disjunctions p)) +associateToRight p = descend associateToRight p ----------------------------------------------------------- --- Ascii symbols diff --git a/src/Domain/Logic/Proofs.hs b/src/Domain/Logic/Proofs.hs --- a/src/Domain/Logic/Proofs.hs +++ b/src/Domain/Logic/Proofs.hs @@ -1,6 +1,6 @@ {-# LANGUAGE RankNTypes #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,58 +12,48 @@ -- Exercise for the logic domain: to prove two propositions equivalent -- ----------------------------------------------------------------------------- --- $Id: Proofs.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Proofs.hs 7529 2015-04-08 09:55:03Z bastiaan $ module Domain.Logic.Proofs - ( proofExercise, proofUnicodeExercise - , sortRuleOr, sortRuleAnd -- fix me + ( proofExercise, proofTopExercise, proofUnicodeExercise + , topIsAnd, topIsAndCom ) where import Control.Arrow import Control.Monad import Data.Foldable (toList) -import Data.Function (on) import Data.List 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.InverseRules hiding (inverseRules) import Domain.Logic.Parser import Domain.Logic.Rules -import Domain.Logic.Strategies (somewhereOr) +import Domain.Logic.Strategies import Domain.Logic.Utils import Domain.Math.Expr () import Ideas.Common.Library import Ideas.Common.Traversal.Navigator -import Ideas.Common.Traversal.Utils import Ideas.Common.Utils -{- -see :: Int -> IO () -see n = do - let a = snd (examples proofExercise !! n) - der = defaultDerivation proofExercise a - printDerivation proofExercise a - putStrLn $ ">> " ++ show (derivationLength der) ++ " steps\n" --} - -- Currently, we use the DWA strategy proofExercise :: Exercise Proof proofExercise = makeExercise { exerciseId = describe "Prove two propositions equivalent" $ propositionalId # "proof" , status = Experimental - , parser = mapSecond makeProof . parseLogicProof False - , prettyPrinter = showProof + , parser = -- maybe (Left "nee") Right . fromTerm . read + mapSecond makeProof . parseLogicProof False + , prettyPrinter = -- show . toTerm + showProof , equivalence = withoutContext equivalentProofs , similarity = withoutContext similarProofs , suitable = predicate $ all (uncurry eqLogic) . subProofs , ready = predicate $ all (uncurry equalLogicA) . subProofs - , strategy = proofStrategy + , strategy = {- cleanUpStrategyAfter (applyTop cleanUp) -}proofStrategy , extraRules = map use extraLogicRules ++ inverseRules ++ map use buggyRules , navigation = termNavigator , examples = map (second makeProof) exampleProofs @@ -77,13 +67,37 @@ , prettyPrinter = showProofUnicode } +proofTopExercise :: Exercise Proof +proofTopExercise = proofExercise + { exerciseId = describe "Prove two propositions equivalent (with top-level decomposition)" $ + propositionalId # "proof.top" + , parser = mapSecond (ands . map makeProof) . parseLogicProofs + , prettyPrinter = showSubProofs + , equivalence = withoutContext eqSubProofs + , similarity = withoutContext simSubProofs + } + type Proof = Logic (SLogic, SLogic) +{- +cleanUp :: Proof -> Proof +cleanUp proof = makeProof (associateToRight lhs, associateToRight rhs) + where + (lhs, rhs) = proofPair proof -} + subProofs :: Proof -> [(SLogic, SLogic)] subProofs = toList makeProof :: (SLogic, SLogic) -> Proof -makeProof = Var +makeProof pair = + let p = Var pair in + case apply (topIsOr <|> topIsAnd <|> topIsNot <|> topIsEquiv <|> topIsImpl) p of + Just (Var eq1 :||: Var eq2) -> makeProof eq1 :||: makeProof eq2 + Just (Var eq1 :&&: Var eq2) -> makeProof eq1 :&&: makeProof eq2 + Just (Var eq1 :->: Var eq2) -> makeProof eq1 :->: makeProof eq2 + Just (Var eq1 :<->: Var eq2) -> makeProof eq1 :<->: makeProof eq2 + Just (Not (Var eq)) -> Not (makeProof eq) + _ -> p proofPair :: Proof -> (SLogic, SLogic) proofPair x = (catLogic (fmap fst x), catLogic (fmap snd x)) @@ -98,6 +112,11 @@ where f p q = ppLogicUnicodePars p ++ " == " ++ ppLogicUnicodePars q +showSubProofs :: Proof -> String +showSubProofs = intercalate ", " . map (uncurry f) . subProofs + where + f p q = ppLogicPars p ++ " == " ++ ppLogicPars q + equivalentProofs :: Proof -> Proof -> Bool equivalentProofs proof1 proof2 = let (p1, q1) = proofPair proof1 @@ -110,6 +129,20 @@ (p2, q2) = proofPair proof2 in equalLogicA p1 p2 && equalLogicA q1 q2 +eqSubProofs :: Proof -> Proof -> Bool +eqSubProofs proof1 proof2 = + let ok = uncurry eqLogic + in all ok (subProofs proof1) == all ok (subProofs proof2) + +simSubProofs :: Proof -> Proof -> Bool +simSubProofs proof1 proof2 = + let (xs1, xs2) = unzip (subProofs proof1) + (ys1, ys2) = unzip (subProofs proof2) + ok = uncurry equalLogicA + in length xs1 == length ys1 + && all ok (zip xs1 ys1) + && all ok (zip xs2 ys2) + proofStrategy :: LabeledStrategy (Context Proof) proofStrategy = label "proof equivalent" $ repeatS ( @@ -117,29 +150,29 @@ -- disabled: first investigate how the common subexpressions should be -- communicated to the client -- |> somewhere commonExprAtom - |> useC dnfStrategyDWA + |> useC towardsDNF |> commonLiteralSpecial - |> useC orToTop + |> useC distrAnd |> (use checkDNF <*> commonLiteral) ) <*> use checkDNF <*> normStrategy - where - splitTop = use topIsNot <|> use topIsImpl + +splitTop :: Strategy (Context Proof) +splitTop = use topIsNot <|> use topIsEquiv <|> use topIsImpl -- only use commutativity if not already in desired order <|> (use topIsAnd |> use topIsAndCom) <|> (use topIsOr |> use topIsOrCom) - <|> use topIsEquiv commonLiteralSpecial :: Strategy (Context Proof) commonLiteralSpecial = - repeat1 (somewhere (use ruleCommonLiteralSpecialInFront)) + repeatS (somewhere (use ruleCommonLiteralSpecialInFront)) <*> repeat1 (somewhere (use ruleInvDistrCommonLiteral)) <*> repeatS (somewhere (use topIsAnd)) ruleCommonLiteralSpecialInFront :: Rule Proof -ruleCommonLiteralSpecialInFront = makeRule "command.common-literal-special" f +ruleCommonLiteralSpecialInFront = siblingOf groupCommutativity $ makeRule "command.common-literal-special" f where f (Var eq) = [ Var x | x <- maybeToList (findInFrontLeft eq) ] ++ @@ -158,92 +191,42 @@ guard $ and [ isDNF p && isDNF q | (p, q) <- subProofs proof ] Just proof +{- ------------------------------------------------------------------ +In the strong-normalization strategy we do not check for common literals: + |> somewhere (use checkDNF <*> commonLiteral) +Therefore, we also do not need simplification rules: + |> somewhere (use ruleFalseAnd <|> use ruleTrueOr + <|> use ruleFalseOr <|> use ruleTrueAnd) + |> somewhere (use ruleComplAnd) +------------------------------------------------------------------ -} normStrategy :: Strategy (Context Proof) normStrategy = repeatS $ - somewhere (use ruleFalseZeroAnd <|> use ruleTrueZeroOr) - |> somewhere (use ruleComplAnd) + somewhere splitTop |> somewhere ( use ruleIdempOr <|> use ruleIdempAnd <|> - use ruleAndOverOr <|> - use ruleFalseZeroOr + use absorptionOrSubset <|> + use ruleComplOr ) - |> oncetd (use sortRuleAnd) - |> oncetd (use sortRuleOr) |> somewhereDisjunct introduceVar -sortRuleBy :: (b -> b -> Ordering) -> View a [b] -> Transformation a -sortRuleBy cmp v = makeTrans $ \p -> do - xs <- match v p - guard (not (sortedBy cmp xs)) - let ys = sortBy cmp xs - return (build v ys) - -sortRuleOr :: Rule SLogic -sortRuleOr = ruleTrans "CommOr.sort" $ - sortRuleBy compareVar $ disjunctions <-> ors - -sortRuleAnd :: Rule SLogic -sortRuleAnd = ruleTrans "CommAnd.sort" $ - sortRuleBy compareVar $ conjunctions <-> ands - -compareVar :: Ord a => Logic a -> Logic a -> Ordering -compareVar = compare `on` (\x -> (varsLogic x, x)) - -sortedBy :: (a -> a -> Ordering) -> [a] -> Bool -sortedBy cmp = rec - where - rec (x:y:zs) = cmp x y /= GT && rec (y:zs) - rec _ = True +-- (p /\ q) \/ ... \/ (p /\ q /\ r) ~> (p /\ q) \/ ... +-- (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes) +absorptionOrSubset :: Rule SLogic +absorptionOrSubset = siblingOf groupAbsorption $ ruleList "absorpor-subset" $ \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) ----------------------------------------------------------------------------- --- To DNF, with priorities (the "DWA" approach) -dnfStrategyDWA :: Strategy (Context SLogic) -dnfStrategyDWA = - toplevel <|> somewhereOr - ( label "Simplify" simpler - |> label "Sort and simplify" (sortAndSimplify |> deMorganAndSimplify) - |> label "Eliminate implications/equivalences" eliminateImplEquiv - |> label "Eliminate nots" eliminateNots - ) - where - toplevel = useRules - [ ruleFalseZeroOr, ruleTrueZeroOr, ruleIdempOr - , ruleAbsorpOr, ruleComplOr - ] - simpler = somewhere $ useRules - [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd - , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse - , ruleNotNot, ruleIdempOr, ruleIdempAnd, ruleAbsorpOr, ruleAbsorpAnd - , ruleComplOr, ruleComplAnd - ] - sortAndSimplify = somewhere $ - use ruleAbsorpOrNot - <|> use sortForIdempOr - <|> use sortForIdempAnd - <|> use sortForComplOr - <|> use sortForComplAnd - deMorganAndSimplify = somewhere $ - deMorganOrNot <|> deMorganAndNot - eliminateImplEquiv = - somewhere (use ruleDefImpl) -- preference: top-down! - |> somewhere (use ruleDefEquiv) -- preference: bottom-up! - - eliminateNots = somewhere $ useRules - [ generalRuleDeMorganAnd, generalRuleDeMorganOr - , ruleDeMorganAnd, ruleDeMorganOr - ] - -orToTop :: LabeledStrategy (Context SLogic) -orToTop = label "Move ors to top" $ somewhere $ useRules - [ generalRuleAndOverOr, ruleAndOverOr ] - -useRules :: [Rule SLogic] -> Strategy (Context SLogic) -useRules = alternatives . map liftToContext - --- disabled for now +towardsDNF :: Strategy (Context SLogic) +towardsDNF = configureS (Reinsert `byName` specialGroupLiterals) $ + orRules <|> somewhereOr nnfStep +-- disabled for now: -- Find a common subexpression that can be treated as a box {- commonExprAtom :: Rule (Context Proof) @@ -280,38 +263,6 @@ -} -------------------------------------------------------------------- --- p \/ q \/ ~p ~> reorder p and ~p -sortForComplOr :: Rule SLogic -sortForComplOr = ruleMaybe "ComplOr.sort" $ \p -> do - let xs = disjunctions p - ys = sortBy compareVar xs - guard (xs /= ys && any (\x -> Not x `elem` xs) xs) - return (ors ys) - --- p /\ q /\ ~p ~> reorder p and ~p -sortForComplAnd :: Rule SLogic -sortForComplAnd = ruleMaybe "ComplAnd.sort" $ \p -> do - let xs = conjunctions p - ys = sortBy compareVar xs - guard (xs /= ys && any (\x -> Not x `elem` xs) xs) - return (ands ys) - --- p \/ q \/ p ~> reorder p's -sortForIdempOr :: Rule SLogic -sortForIdempOr = ruleMaybe "IdempOr.sort" $ \p -> do - let xs = disjunctions p - ys = sortBy compareVar xs - guard (xs /= ys && not (distinct xs)) - return (ors ys) - --- p /\ q /\ p ~> reorder p's -sortForIdempAnd :: Rule SLogic -sortForIdempAnd = ruleMaybe "IdempAnd.sort" $ \p -> do - let xs = conjunctions p - ys = sortBy compareVar xs - guard (xs /= ys && not (distinct xs)) - return (ands ys) - acTopRuleFor :: Bool -> (forall a . Isomorphism (Logic a) [Logic a]) -> Transformation Proof acTopRuleFor com iso = makeTrans $ \proof -> do @@ -322,10 +273,16 @@ (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) - ] + return $ + -- if both sides have changed ... + if as1++as2 /= as && bs1++bs2 /= bs + then -- ... only keep the reordering on the left-hand side + Var (to iso (as1++as2), rhs) + else -- ... otherwise, decompose proof with "top" rule + to iso + [ Var (to iso as1, to iso bs1) + , Var (to iso as2, to iso bs2) + ] splitTwoLists :: (forall t . [t] -> [([t], [t])]) -> [a] -> [b] -> [([a], [a], [b], [b])] @@ -354,17 +311,19 @@ topIsOr :: Rule Proof topIsOr = minor $ ruleTrans "top-is-or" $ acTopRuleFor False (collect orView) -topIsEquiv :: Rule Proof -topIsEquiv = minor $ ruleTrans "top-is-equiv" $ acTopRuleFor False (collect eqView) - topIsAndCom :: Rule Proof -topIsAndCom = ruleTrans "top-is-and.com" $ acTopRuleFor True (collect andView) +topIsAndCom = siblingOf groupCommutativity $ ruleTrans "top-is-and.com" $ acTopRuleFor True (collect andView) topIsOrCom :: Rule Proof -topIsOrCom = ruleTrans "top-is-or.com" $ acTopRuleFor True (collect orView) +topIsOrCom = siblingOf groupCommutativity $ ruleTrans "top-is-or.com" $ acTopRuleFor True (collect orView) ---topIsEquivCom :: Rule Proof ---topIsEquivCom = ruleTrans "top-is-equiv.com" $ acTopRuleFor True (collect eqView) +topIsEquiv :: Rule Proof +topIsEquiv = minorRule "top-is-equiv" f + where + f (Var (p :<->: q, r :<->: s)) = do + guard (eqLogic p r && eqLogic q s) + return (Var (p, r) :<->: Var (q, s)) + f _ = Nothing topIsImpl :: Rule Proof topIsImpl = minorRule "top-is-impl" f @@ -410,7 +369,8 @@ introduceVar :: Strategy (Context Proof) introduceVar = check missing <*> use introTrueLeft - <*> layer [] introCompl + <*> introCompl + <*> use ruleDistrAnd missing :: Context Proof -> Bool missing = isJust . missingVar @@ -428,37 +388,20 @@ Nothing -> Nothing introTrueLeft :: Rule SLogic -introTrueLeft = rewriteRule "IntroTrueLeft" $ +introTrueLeft = siblingOf groupTrueConjunction $ rewriteRule "IntroTrueLeft" $ \x -> x :~> T :&&: x introCompl :: Rule (Context Proof) -introCompl = makeRule "IntroCompl" $ \cp -> do - a <- missingVar (safe up cp) +introCompl = siblingOf groupTrueComplement $ makeRule "IntroCompl" $ \cp -> do + a <- missingVar cp let f = fromTerm >=> fmap toTerm . introTautology a changeTerm f cp where introTautology :: a -> Logic a -> Maybe (Logic a) introTautology a T = Just (Var a :||: Not (Var a)) + introTautology a (p :&&: q) = fmap (:&&: q) (introTautology a p) introTautology _ _ = Nothing - {- -go = applyAll (somewhereDisjunct introduceVar) $ inContext proofExercise $ - makeProof (p :||: (Not p :&&: q), p :||: q) - where - p = Var (ShowString "p") - q = Var (ShowString "q") - -somewhereEq :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof) -somewhereEq s = traverse [once, topdown] - (check isEq <*> layer [] s) - where - isEq :: Context Proof -> Bool - isEq cp = fromMaybe False $ do - t <- currentTerm cp - case fromTerm t :: Maybe (SLogic, SLogic) of - Just (p, q) -> return True - _ -> return False -} - somewhereDisjunct :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof) somewhereDisjunct s = oncetd (check isEq <*> layer [] (somewhereOrG s)) where @@ -474,134 +417,72 @@ in fix $ \this -> check (Prelude.not . curIsOr) <*> s <|> check curIsOr <*> layer [] this ----------------------- - -ruleAbsorpOrNot :: Rule SLogic -ruleAbsorpOrNot = rewriteRules "DistrOrNot" - [ -- not inside - \x y -> x :||: (Not x :&&: y) :~> (x :||: Not x) :&&: (x :||: y) - , \x y -> x :||: (y :&&: Not x) :~> (x :||: y) :&&: (x :||: Not x) - , \x y -> (Not x :&&: y) :||: x :~> (Not x :||: x) :&&: (y :||: x) - , \x y -> (y :&&: Not x) :||: x :~> (y :||: x) :&&: (Not x :||: x) - -- not outside - , \x y -> Not x :||: (x :&&: y) :~> (Not x :||: x) :&&: (Not x :||: y) - , \x y -> Not x :||: (y :&&: x) :~> (Not x :||: y) :&&: (Not x :||: x) - , \x y -> (x :&&: y) :||: Not x :~> (x :||: Not x) :&&: (y :||: Not x) - , \x y -> (y :&&: x) :||: Not x :~> (y :||: Not x) :&&: (x :||: Not x) - ] - --- specialization of De Morgan rules with a not inside (gives higher priority) -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 - -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 -ruleAbsorpAndNot = rewriteRules "AbsorpAndNot.distr" - [ -- not inside - \x y -> x :&&: (Not x :||: y) :~> (x :&&: Not x) :||: (x :&&: y) - , \x y -> x :&&: (y :||: Not x) :~> (x :&&: y) :||: (x :&&: Not x) - , \x y -> (Not x :||: y) :&&: x :~> (Not x :&&: x) :||: (y :&&: x) - , \x y -> (y :||: Not x) :&&: x :~> (y :&&: x) :||: (Not x :&&: x) - -- not outside - , \x y -> Not x :&&: (x :||: y) :~> (Not x :||: x) :&&: (Not x :||: y) - , \x y -> Not x :&&: (y :||: x) :~> (Not x :||: y) :&&: (Not x :||: x) - , \x y -> (x :||: y) :&&: Not x :~> (x :||: Not x) :&&: (y :||: Not x) - , \x y -> (y :||: x) :&&: Not x :~> (y :||: Not x) :&&: (x :||: Not x) - ] -} - ----------------------------------------------------------------------------- -- Inverse rules inverseRules :: [Rule (Context Proof)] -inverseRules = map use [invDefImpl, invDefEquiv, invNotNot, invIdempOr, invIdempAnd, - invTrueZeroAnd, invNotTrue, invFalseZeroOr, invNotFalse] ++ - [ invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd - , invComplAnd, invAndOverOr, invOrOverAnd] +inverseRules = map use [invDefImpl, invDefEquiv, invDoubleNeg, invIdempOr, invIdempAnd, + invTrueAnd, invNotTrue, invFalseOr, invNotFalse] ++ + [ invAbsorpOr, invAbsorpAnd, invTrueOr, invComplOr, invFalseAnd + , invComplAnd, invDistrAnd, invDistrOr] invDefImpl :: Rule SLogic -invDefImpl = rewriteRule "DefImpl.inv" $ +invDefImpl = siblingOf groupImplication $ rewriteRule "DefImpl.inv" $ \x y -> Not x :||: y :~> x :->: y invDefEquiv :: Rule SLogic -invDefEquiv = rewriteRule "DefEquiv.inv" $ +invDefEquiv = siblingOf groupEquivalence $ rewriteRule "DefEquiv.inv" $ \x y -> (x :&&: y) :||: (Not x :&&: Not y) :~> x :<->: y -invNotNot :: Rule SLogic -invNotNot = rewriteRule "NotNot.inv" $ +invDoubleNeg :: Rule SLogic +invDoubleNeg = siblingOf groupDoubleNegation $ rewriteRule "NotNot.inv" $ \x -> x :~> Not (Not x) invIdempOr :: Rule SLogic -invIdempOr = rewriteRule "IdempOr.inv" $ +invIdempOr = siblingOf groupIdempotency $ rewriteRule "IdempOr.inv" $ \x -> x :~> x :||: x invIdempAnd :: Rule SLogic -invIdempAnd = rewriteRule "IdempAnd.inv" $ +invIdempAnd = siblingOf groupIdempotency $ rewriteRule "IdempAnd.inv" $ \x -> x :~> x :&&: x -invTrueZeroAnd :: Rule SLogic -invTrueZeroAnd = rewriteRules "TrueZeroAnd.inv" +invTrueAnd :: Rule SLogic +invTrueAnd = siblingOf groupTrueConjunction $ rewriteRules "TrueZeroAnd.inv" [ \x -> x :~> T :&&: x , \x -> x :~> x :&&: T ] invNotTrue :: Rule SLogic -invNotTrue = rewriteRule "NotTrue.inv" $ +invNotTrue = siblingOf groupNotTrue $ rewriteRule "NotTrue.inv" $ F :~> Not T -invFalseZeroOr :: Rule SLogic -invFalseZeroOr = rewriteRules "FalseZeroOr.inv" +invFalseOr :: Rule SLogic +invFalseOr = siblingOf groupFalseDisjunction $ rewriteRules "FalseZeroOr.inv" [ \x -> x :~> F :||: x , \x -> x :~> x :||: F ] invNotFalse :: Rule SLogic -invNotFalse = rewriteRule "NotFalse.inv" $ +invNotFalse = siblingOf groupNotFalse $ rewriteRule "NotFalse.inv" $ T :~> Not F 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 +invAbsorpOr, invAbsorpAnd, invTrueOr, invComplOr, invFalseAnd, + invComplAnd, invDistrAnd, invDistrOr :: Rule (Context Proof) +invAbsorpOr = proofInvRule "AbsorpOr.inv" ruleAbsorpOr +invAbsorpAnd = proofInvRule "AbsorpAnd.inv" ruleAbsorpAnd +invTrueOr = proofInvRule "TrueZeroOr.inv" ruleTrueOr +invComplOr = proofInvRule "ComplOr.inv" ruleComplOr +invFalseAnd = proofInvRule "FalseZeroAnd.inv" ruleFalseAnd +invComplAnd = proofInvRule "ComplAnd.inv" ruleComplAnd +invDistrAnd = proofInvRule "AndOverOr.inv" ruleDistrAnd -- see GeneralizedRules +invDistrOr = proofInvRule "OrOverAnd.inv" ruleDistrOr -- 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 - (p, q, r) = (Var $ ShowString "p", Var $ ShowString "q", Var $ ShowString "r") --} - -- 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). @@ -618,7 +499,7 @@ intersectList (map conjunctions (disjunctions p ++ disjunctions q)) ruleCommonLiteralInFront :: Rule Proof -ruleCommonLiteralInFront = makeRule "command.common-literal" f +ruleCommonLiteralInFront = siblingOf groupCommutativity $ makeRule "command.common-literal" f where f (Var eq) = [ Var x | x <- maybeToList (findInFrontLeft eq) ] ++ @@ -638,7 +519,7 @@ Just (new, q) ruleInvDistrCommonLiteral :: Rule Proof -ruleInvDistrCommonLiteral = makeRule "andoveror.inv.common-literal" f +ruleInvDistrCommonLiteral = siblingOf groupDistribution $ makeRule "andoveror.inv.common-literal" f where f (Var eq) = [ Var x | x <- invDistr eq ] ++ [ Var (swap x) | x <- invDistr (swap eq) ] diff --git a/src/Domain/Logic/Rules.hs b/src/Domain/Logic/Rules.hs --- a/src/Domain/Logic/Rules.hs +++ b/src/Domain/Logic/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,15 +12,15 @@ -- DWA course) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Rules - ( ruleAbsorpAnd, ruleAbsorpOr, ruleAndOverOr, ruleOrOverAnd + ( ruleAbsorpAnd, ruleAbsorpOr, ruleDistrAnd, ruleDistrOr , ruleComplAnd, ruleComplOr, ruleDeMorganAnd, ruleDeMorganOr , ruleDefEquiv, ruleDefImpl - , ruleFalseZeroAnd, ruleFalseZeroOr, ruleIdempAnd, ruleIdempOr - , ruleNotFalse, ruleNotNot, ruleNotTrue - , ruleTrueZeroAnd, ruleTrueZeroOr + , ruleFalseAnd, ruleFalseOr, ruleIdempAnd, ruleIdempOr + , ruleNotFalse, ruleDoubleNeg, ruleNotTrue + , ruleTrueAnd, ruleTrueOr , ruleCommOr, ruleCommAnd, ruleAssocOr, ruleAssocAnd ) where @@ -66,15 +66,14 @@ ----------------------------------------------------------------------------- -- Distributivity -ruleAndOverOr :: Rule SLogic - -ruleAndOverOr = ruleListFor groupDistribution "AndOverOr" +ruleDistrAnd :: Rule SLogic +ruleDistrAnd = 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 = ruleListFor groupDistribution "OrOverAnd" +ruleDistrOr :: Rule SLogic +ruleDistrOr = ruleListFor groupDistribution "OrOverAnd" [ \x y z -> x :||: (y :&&: z) :~> (x :||: y) :&&: (x :||: z) , \x y z -> (x :&&: y) :||: z :~> (x :||: z) :&&: (y :||: z) ] @@ -82,19 +81,18 @@ ----------------------------------------------------------------------------- -- Idempotency -ruleIdempOr, ruleIdempAnd :: Rule SLogic - +ruleIdempOr :: Rule SLogic ruleIdempOr = ruleFor groupIdempotency "IdempOr" $ \x -> x :||: x :~> x +ruleIdempAnd :: Rule SLogic ruleIdempAnd = ruleFor groupIdempotency "IdempAnd" $ \x -> x :&&: x :~> x ----------------------------------------------------------------------------- -- Absorption -ruleAbsorpOr, ruleAbsorpAnd :: Rule SLogic - +ruleAbsorpOr :: Rule SLogic ruleAbsorpOr = ruleListFor groupAbsorption "AbsorpOr" [ \x y -> x :||: (x :&&: y) :~> x , \x y -> x :||: (y :&&: x) :~> x @@ -102,6 +100,7 @@ , \x y -> (y :&&: x) :||: x :~> x ] +ruleAbsorpAnd :: Rule SLogic ruleAbsorpAnd = ruleListFor groupAbsorption "AbsorpAnd" [ \x y -> x :&&: (x :||: y) :~> x , \x y -> x :&&: (y :||: x) :~> x @@ -112,54 +111,58 @@ ----------------------------------------------------------------------------- -- True-properties -ruleTrueZeroOr, ruleTrueZeroAnd, ruleComplOr, ruleNotTrue :: Rule SLogic - -ruleTrueZeroOr = ruleList "TrueZeroOr" +ruleTrueOr :: Rule SLogic +ruleTrueOr = ruleListFor groupTrueDisjunction "TrueZeroOr" [ \x -> T :||: x :~> T , \x -> x :||: T :~> T ] -ruleTrueZeroAnd = ruleList "TrueZeroAnd" +ruleTrueAnd :: Rule SLogic +ruleTrueAnd = ruleListFor groupTrueConjunction "TrueZeroAnd" [ \x -> T :&&: x :~> x , \x -> x :&&: T :~> x ] -ruleComplOr = ruleList "ComplOr" +ruleComplOr :: Rule SLogic +ruleComplOr = ruleListFor groupTrueComplement "ComplOr" [ \x -> x :||: Not x :~> T , \x -> Not x :||: x :~> T ] -ruleNotTrue = rule "NotTrue" $ +ruleNotTrue :: Rule SLogic +ruleNotTrue = ruleFor groupNotTrue "NotTrue" $ Not T :~> F ----------------------------------------------------------------------------- -- False-properties -ruleFalseZeroOr, ruleFalseZeroAnd, ruleComplAnd, ruleNotFalse :: Rule SLogic - -ruleFalseZeroOr = ruleList "FalseZeroOr" +ruleFalseOr :: Rule SLogic +ruleFalseOr = ruleListFor groupFalseDisjunction "FalseZeroOr" [ \x -> F :||: x :~> x , \x -> x :||: F :~> x ] -ruleFalseZeroAnd = ruleList "FalseZeroAnd" +ruleFalseAnd :: Rule SLogic +ruleFalseAnd = ruleListFor groupFalseConjunction "FalseZeroAnd" [ \x -> F :&&: x :~> F , \x -> x :&&: F :~> F ] -ruleComplAnd = ruleList "ComplAnd" +ruleComplAnd :: Rule SLogic +ruleComplAnd = ruleListFor groupFalseComplement "ComplAnd" [ \x -> x :&&: Not x :~> F , \x -> Not x :&&: x :~> F ] -ruleNotFalse = rule "NotFalse" $ +ruleNotFalse :: Rule SLogic +ruleNotFalse = ruleFor groupNotFalse "NotFalse" $ Not F :~> T ----------------------------------------------------------------------------- -- Double negation -ruleNotNot :: Rule SLogic -ruleNotNot = rule "NotNot" $ +ruleDoubleNeg :: Rule SLogic +ruleDoubleNeg = ruleFor groupDoubleNegation "NotNot" $ \x -> Not (Not x) :~> x ----------------------------------------------------------------------------- @@ -177,57 +180,12 @@ -- Implication elimination ruleDefImpl :: Rule SLogic -ruleDefImpl = rule "DefImpl" $ +ruleDefImpl = ruleFor groupImplication "DefImpl" $ \x y -> x :->: y :~> Not x :||: y ----------------------------------------------------------------------------- -- Equivalence elimination ruleDefEquiv :: Rule SLogic -ruleDefEquiv = rule "DefEquiv" $ - \x y -> x :<->: y :~> (x :&&: y) :||: (Not x :&&: Not y) - ------------------------------------------------------------------------------ --- Additional rules, not in the DWA course - -{- -ruleFalseInEquiv :: Rule SLogic -ruleFalseInEquiv = ruleList "FalseInEquiv" - [ \x -> F :<->: x :~> Not x - , \x -> x :<->: F :~> Not x - ] - -ruleTrueInEquiv :: Rule SLogic -ruleTrueInEquiv = ruleList "TrueInEquiv" - [ \x -> T :<->: x :~> x - , \x -> x :<->: T :~> x - ] - -ruleFalseInImpl :: Rule SLogic -ruleFalseInImpl = ruleList "FalseInImpl" - [ \x -> F :->: x :~> T - , \x -> x :->: F :~> Not x - ] - -ruleTrueInImpl :: Rule SLogic -ruleTrueInImpl = ruleList "TrueInImpl" - [ \x -> T :->: x :~> x - , \x -> x :->: T :~> T - ] - -ruleCommEquiv :: Rule SLogic -ruleCommEquiv = rule "CommEquiv" $ - \x y -> x :<->: y :~> y :<->: x - -ruleDefEquivImpls :: Rule SLogic -ruleDefEquivImpls = rule "DefEquivImpls" $ - \x y -> x :<->: y :~> (x :->: y) :&&: (y :->: x) - -ruleEquivSame :: Rule SLogic -ruleEquivSame = rule "EquivSame" $ - \x -> x :<->: x :~> T - -ruleImplSame :: Rule SLogic -ruleImplSame = rule "ImplSame" $ - \x -> x :->: (x::SLogic) :~> T --} +ruleDefEquiv = ruleFor groupEquivalence "DefEquiv" $ + \x y -> x :<->: y :~> (x :&&: y) :||: (Not x :&&: Not y) diff --git a/src/Domain/Logic/Strategies.hs b/src/Domain/Logic/Strategies.hs --- a/src/Domain/Logic/Strategies.hs +++ b/src/Domain/Logic/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,134 +9,146 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Strategies - ( dnfStrategyDWA, somewhereOr - , cnfStrategyDWA + ( dnfStrategy, cnfStrategy + , orRules, andRules, nnfStep, simplifyStep + , deMorgan, deMorganOr, deMorganAnd, distrAnd, distrOr + , eliminateImplEquiv + , specialDeMorganNot, specialDistrNot, specialGroupLiterals ) where +import Control.Monad +import Data.List import Domain.Logic.Formula import Domain.Logic.GeneralizedRules import Domain.Logic.Rules +import Domain.Logic.Utils import Ideas.Common.Library ----------------------------------------------------------------------------- --- To DNF, with priorities (the "DWA" approach) +-- Normal forms -dnfStrategyDWA :: LabeledStrategy (Context SLogic) -dnfStrategyDWA = label "Bring to dnf (DWA)" $ - repeatS $ toplevel <|> somewhereOr - ( label "Simplify" simpl - |> label "Eliminate implications/equivalences" eliminateImplEquiv - |> label "Eliminate nots" eliminateNots - |> label "Move ors to top" orToTop - ) - where - toplevel = useRules - [ ruleFalseZeroOr, ruleTrueZeroOr, ruleIdempOr - , ruleAbsorpOr, ruleComplOr - ] - 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 - ] - orToTop = somewhere $ useRules - [ generalRuleAndOverOr, ruleAndOverOr ] +dnfStrategy :: LabeledStrategy (Context SLogic) +dnfStrategy = label "DNF" $ repeatS $ + orRules <|> somewhereOr (nnfStep |> distrAnd) --- A specialized variant of the somewhere traversal combinator. Apply --- the strategy only at (top-level) disjuncts -somewhereOr :: IsStrategy g => g (Context SLogic) -> Strategy (Context SLogic) -somewhereOr s = - let curIsOr a = case currentInContext a of - Just (_ :||: _) -> True - _ -> False - in fix $ \this -> check (Prelude.not . curIsOr) <*> s - <|> check curIsOr <*> layer [] this +cnfStrategy :: LabeledStrategy (Context SLogic) +cnfStrategy = label "CNF" $ repeatS $ + andRules <|> somewhereAnd (nnfStep |> distrOr) ---check1, check2 :: (a -> Bool) -> Rule a ---check1 p = minorRule $ makeSimpleRule "check1" $ \a -> if p a then Just a else Nothing ---check2 p = minorRule $ makeSimpleRule "check2" $ \a -> if p a then Just a else Nothing +----------------------------------------------------------------- +-- Sub-strategies ------------------------------------------------------------------------------ --- To DNF, in four steps -{- -dnfStrategy :: LabeledStrategy (Context SLogic) -dnfStrategy = label "Bring to dnf" - $ label "Eliminate constants" eliminateConstants - <*> label "Eliminate implications/equivalences" eliminateImplEquiv - <*> label "Eliminate nots" eliminateNots - <*> label "Move ors to top" orToTop +orRules :: LabeledStrategy (Context SLogic) +orRules = label "OrRules" $ useRules + [ruleFalseOr, ruleTrueOr, ruleIdempOr, ruleAbsorpOr, ruleComplOr] + +andRules :: LabeledStrategy (Context SLogic) +andRules = label "AndRules" $ useRules + [ruleFalseAnd, ruleTrueAnd, ruleIdempAnd, ruleAbsorpAnd, ruleComplAnd] + +-- A step towards Negation Normal Form (NNF) +nnfStep :: Strategy (Context SLogic) +nnfStep = + simplifyStep + |> (remove specialGroupLiterals >|> specialDistrNot >|> specialDeMorganNot) + |> (eliminateImplEquiv >|> deMorgan) + +simplifyStep :: LabeledStrategy (Context SLogic) +simplifyStep = label "Simplify" $ oncetdPref $ + orRules <|> andRules <|> + useRules [ruleNotTrue, ruleNotFalse, ruleDoubleNeg] + +deMorganOr :: Strategy (Context SLogic) +deMorganOr = liftToContext generalRuleDeMorganOr >|> liftToContext ruleDeMorganOr + +deMorganAnd :: Strategy (Context SLogic) +deMorganAnd = liftToContext generalRuleDeMorganAnd >|> liftToContext ruleDeMorganAnd + +deMorgan :: LabeledStrategy (Context SLogic) +deMorgan = label "DeMorgan" $ somewhere $ + deMorganOr <|> deMorganAnd + +distrAnd :: LabeledStrategy (Context SLogic) +distrAnd = label "DistrAnd" $ oncebuPref $ + liftToContext generalRuleDistrAnd >|> liftToContext ruleDistrAnd + +distrOr :: LabeledStrategy (Context SLogic) +distrOr = label "DistrOr" $ oncebuPref $ + liftToContext generalRuleDistrOr >|> liftToContext ruleDistrOr + +eliminateImplEquiv :: LabeledStrategy (Context SLogic) +eliminateImplEquiv = label "EliminateImplEquiv" $ + somewhere (liftToContext ruleDefImpl) + >|> + oncebuPref (liftToContext ruleDefEquiv) + +-- specialization of De Morgan rules with a not inside (gives higher priority) +specialDeMorganNot :: LabeledStrategy (Context SLogic) +specialDeMorganNot = label "SpecialDeMorganNot" $ somewhere $ + (check (cond disjunctions) <*> deMorganOr) <|> + (check (cond conjunctions) <*> deMorganAnd) where - eliminateConstants = repeatS $ oncetd $ useRules - [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd - , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse - -- , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl - ] - eliminateImplEquiv = repeatS $ oncebu $ useRules - [ ruleDefImpl, ruleDefEquiv - ] - eliminateNots = repeatS $ oncetd $ - useRules - [ generalRuleDeMorganAnd, generalRuleDeMorganOr ] - |> useRules - [ ruleDeMorganAnd, ruleDeMorganOr - , ruleNotNot - ] - orToTop = repeatS $ somewhere $ - liftToContext generalRuleAndOverOr |> - liftToContext ruleAndOverOr -} + cond f ctx = case currentInContext ctx of + Just (Not x) -> + let ys = f x in length ys > 1 && any notComposed ys + _ -> False + notComposed (Not (Var _)) = False + notComposed (Not _) = True + notComposed _ = False --- local helper function -useRules :: [Rule SLogic] -> Strategy (Context SLogic) -useRules = alternatives . map liftToContext +specialDistrNot :: LabeledStrategy (Context SLogic) +specialDistrNot = label "SpecialDistrNot" $ somewhere $ liftToContext $ + (check condOr <*> ruleDistrOr) <|> + (check condAnd <*> ruleDistrAnd) + where + condOr (p :||: q) = cond conjunctions p q + condOr _ = False ------------------------------------------------------------------ --- Conjunctive normal form + condAnd (p :&&: q) = cond disjunctions p q + condAnd _ = False -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 - ) + cond f p q = (p `negatedIn` qs && length qs == 2) || + (q `negatedIn` ps && length ps == 2) + where + ps = f p + qs = f q + + negatedIn (Not x) xs = x `elem` xs || (Not (Not x) `elem` xs) + negatedIn x xs = Not x `elem` xs + +specialGroupLiterals :: LabeledStrategy (Context SLogic) +specialGroupLiterals = label "SpecialSort" $ somewhere $ + liftToContext groupLiteralsOr <|> liftToContext groupLiteralsAnd + +-- p \/ q \/ ~p ~> reorder p and ~p +-- p \/ q \/ p ~> reorder p's +groupLiteralsOr :: Rule SLogic +groupLiteralsOr = siblingOf groupCommutativity $ ruleMaybe "ComplOr.sort" $ \p -> do + let xs = disjunctions p + ys = sortLiterals xs + guard (xs /= ys) + return (ors ys) + +-- p /\ q /\ ~p ~> reorder p and ~p +-- p /\ q /\ p ~> reorder p's +groupLiteralsAnd :: Rule SLogic +groupLiteralsAnd = siblingOf groupCommutativity $ ruleMaybe "ComplAnd.sort" $ \p -> do + let xs = conjunctions p + ys = sortLiterals xs + guard (xs /= ys) + return (ands ys) + +sortLiterals :: [SLogic] -> [SLogic] +sortLiterals [] = [] +sortLiterals (p:ps) = p : ys ++ sortLiterals zs 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 ] + (ys, zs) = partition (\x -> x == p || x `isNegated` p) ps + isNegated (Not x) y = y `elem` [x, Not (Not x)] + isNegated x y = y == Not x --- 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 +-- local helper function +useRules :: [Rule SLogic] -> Strategy (Context SLogic) +useRules = alternatives . map liftToContext diff --git a/src/Domain/Logic/Utils.hs b/src/Domain/Logic/Utils.hs --- a/src/Domain/Logic/Utils.hs +++ b/src/Domain/Logic/Utils.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,16 +11,21 @@ -- Utilities for the logic domain -- ----------------------------------------------------------------------------- --- $Id: Utils.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Utils.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Utils - ( propositionalId, makeSimpleRule + ( propositionalId, makeSimpleRule, makeListRule -- groups of rules , groupAbsorption, groupAssociativity, groupCommutativity, groupDeMorgan , groupDistribution, groupIdempotency + , groupDoubleNegation, groupEquivalence, groupFalseComplement + , groupFalseConjunction, groupFalseDisjunction, groupNotTrue + , groupImplication, groupTrueComplement, groupTrueConjunction + , groupTrueDisjunction, groupNotFalse -- other utility functions , makeInvRule, makeInvRuleWithUse , collect, andView, orView, eqView + , somewhereOr, somewhereAnd , (===), (==>), (<=>) ) where @@ -30,6 +35,9 @@ propositionalId :: Id propositionalId = newId "logic.propositional" +makeListRule :: String -> (a -> [a]) -> Rule a +makeListRule s = makeRule (propositionalId # s) + makeSimpleRule :: String -> (a -> Maybe a) -> Rule a makeSimpleRule s = makeRule (propositionalId # s) @@ -45,6 +53,22 @@ groupDistribution = makeGroup "Distribution" groupIdempotency = makeGroup "Idempotency" +groupDoubleNegation, groupEquivalence, groupFalseComplement, + groupFalseConjunction, groupFalseDisjunction, groupNotTrue, + groupImplication, groupTrueComplement, groupTrueConjunction, + groupTrueDisjunction, groupNotFalse :: Id +groupDoubleNegation = makeGroup "doublenegation" +groupEquivalence = makeGroup "equivalence" +groupFalseComplement = makeGroup "falsecomplement" +groupFalseConjunction = makeGroup "falseconjunction" +groupFalseDisjunction = makeGroup "falsedisjunction" +groupNotTrue = makeGroup "group-nottrue" +groupImplication = makeGroup "implication" +groupTrueComplement = makeGroup "truecomplement" +groupTrueConjunction = makeGroup "trueconjunction" +groupTrueDisjunction = makeGroup "truedisjunction" +groupNotFalse = makeGroup "group-notfalse" + makeGroup :: String -> Id makeGroup s = describe "Group of logic rules" (propositionalId # s) @@ -53,16 +77,18 @@ makeInvRule :: IsId n => (a -> a -> Bool) -> n -> Rule a -> Rule a makeInvRule sim name r = - addRecognizerBool eq $ setBuggy (isBuggy r) $ makeRule name (const Nothing) + addRecognizerBool eq $ setSiblings $ setBuggy (isBuggy r) $ makeRule name (const Nothing) where eq a b = any (sim a) (applyAll r b) + setSiblings n = foldr siblingOf n (ruleSiblings r) 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) + addRecognizerBool eq $ setSiblings $ setBuggy (isBuggy r) $ makeRule name (const Nothing) where eq a b = any (sim a) (applyAll (somewhere (use r)) b) + setSiblings n = foldr siblingOf n (ruleSiblings r) collect :: View a (a, a) -> Isomorphism a [a] collect v = f <-> g @@ -77,6 +103,25 @@ where isEq (p :<->: q) = Just (p, q) isEq _ = Nothing + +-- A specialized variant of the somewhere traversal combinator. Apply +-- the strategy only at (top-level) disjuncts +somewhereOr :: IsStrategy g => g (Context SLogic) -> Strategy (Context SLogic) +somewhereOr s = + let curIsOr a = case currentInContext a of + Just (_ :||: _) -> True + _ -> False + in fix $ \this -> check (Prelude.not . curIsOr) <*> s + <|> check curIsOr <*> layer [] this + +-- 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 infix 6 ===, ==>, <=> diff --git a/src/Domain/Logic/Views.hs b/src/Domain/Logic/Views.hs --- a/src/Domain/Logic/Views.hs +++ b/src/Domain/Logic/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Logic.Views ( (.<->.), (.->.), (.&&.), (.||.) diff --git a/src/Domain/Math/Approximation.hs b/src/Domain/Math/Approximation.hs --- a/src/Domain/Math/Approximation.hs +++ b/src/Domain/Math/Approximation.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Selection of numerical algorithms for approximations -- ----------------------------------------------------------------------------- --- $Id: Approximation.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Approximation.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Approximation where diff --git a/src/Domain/Math/CleanUp.hs b/src/Domain/Math/CleanUp.hs --- a/src/Domain/Math/CleanUp.hs +++ b/src/Domain/Math/CleanUp.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: CleanUp.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: CleanUp.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.CleanUp ( cleanUpRelations, cleanUpRelation, cleanUpExpr diff --git a/src/Domain/Math/Data/DecimalFraction.hs b/src/Domain/Math/Data/DecimalFraction.hs --- a/src/Domain/Math/Data/DecimalFraction.hs +++ b/src/Domain/Math/Data/DecimalFraction.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -13,7 +13,7 @@ -- Division in the Fractional type class is not safe. -- ----------------------------------------------------------------------------- --- $Id: DecimalFraction.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: DecimalFraction.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.DecimalFraction ( DecimalFraction(..), fromDouble, validDivisor, digits diff --git a/src/Domain/Math/Data/Interval.hs b/src/Domain/Math/Data/Interval.hs --- a/src/Domain/Math/Data/Interval.hs +++ b/src/Domain/Math/Data/Interval.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -13,7 +13,7 @@ -- equality (provided that there is a valid ordering on the elements). -- ----------------------------------------------------------------------------- --- $Id: Interval.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Interval.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.Interval ( -- * Data types diff --git a/src/Domain/Math/Data/MixedFraction.hs b/src/Domain/Math/Data/MixedFraction.hs --- a/src/Domain/Math/Data/MixedFraction.hs +++ b/src/Domain/Math/Data/MixedFraction.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -13,7 +13,7 @@ -- for example, 5[1/4] or -3[2/5] -- ----------------------------------------------------------------------------- --- $Id: MixedFraction.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: MixedFraction.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.MixedFraction ( MixedFraction, wholeNumber, fractionPart, numerator, denominator diff --git a/src/Domain/Math/Data/OrList.hs b/src/Domain/Math/Data/OrList.hs --- a/src/Domain/Math/Data/OrList.hs +++ b/src/Domain/Math/Data/OrList.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -10,7 +10,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: OrList.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: OrList.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.OrList ( OrList, OrSet, true, false, (<>) diff --git a/src/Domain/Math/Data/Polynomial.hs b/src/Domain/Math/Data/Polynomial.hs --- a/src/Domain/Math/Data/Polynomial.hs +++ b/src/Domain/Math/Data/Polynomial.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Polynomial.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Polynomial.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.Polynomial ( Polynomial, toPolynomial, fromPolynomial, var, con, raise diff --git a/src/Domain/Math/Data/PrimeFactors.hs b/src/Domain/Math/Data/PrimeFactors.hs --- a/src/Domain/Math/Data/PrimeFactors.hs +++ b/src/Domain/Math/Data/PrimeFactors.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: PrimeFactors.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: PrimeFactors.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.PrimeFactors ( PrimeFactors diff --git a/src/Domain/Math/Data/Primes.hs b/src/Domain/Math/Data/Primes.hs --- a/src/Domain/Math/Data/Primes.hs +++ b/src/Domain/Math/Data/Primes.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Calculating prime numbers and prime factors -- ----------------------------------------------------------------------------- --- $Id: Primes.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Primes.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.Primes ( primes, isPrime, coprime, primeFactors, factors diff --git a/src/Domain/Math/Data/Relation.hs b/src/Domain/Math/Data/Relation.hs --- a/src/Domain/Math/Data/Relation.hs +++ b/src/Domain/Math/Data/Relation.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Mathematical relations -- ----------------------------------------------------------------------------- --- $Id: Relation.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Relation.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.Relation ( -- * Type class diff --git a/src/Domain/Math/Data/SquareRoot.hs b/src/Domain/Math/Data/SquareRoot.hs --- a/src/Domain/Math/Data/SquareRoot.hs +++ b/src/Domain/Math/Data/SquareRoot.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: SquareRoot.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: SquareRoot.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.SquareRoot ( SquareRoot diff --git a/src/Domain/Math/Data/TestingClassLaws.hs b/src/Domain/Math/Data/TestingClassLaws.hs --- a/src/Domain/Math/Data/TestingClassLaws.hs +++ b/src/Domain/Math/Data/TestingClassLaws.hs @@ -1,7 +1,7 @@ {-# LANGUAGE TypeFamilies #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: TestingClassLaws.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: TestingClassLaws.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.TestingClassLaws where diff --git a/src/Domain/Math/Data/WithBool.hs b/src/Domain/Math/Data/WithBool.hs --- a/src/Domain/Math/Data/WithBool.hs +++ b/src/Domain/Math/Data/WithBool.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,7 +12,7 @@ -- Values extended with boolean constants -- ----------------------------------------------------------------------------- --- $Id: WithBool.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: WithBool.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Data.WithBool ( WithBool, fromWithBool, join diff --git a/src/Domain/Math/Derivative/Examples.hs b/src/Domain/Math/Derivative/Examples.hs --- a/src/Domain/Math/Derivative/Examples.hs +++ b/src/Domain/Math/Derivative/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,11 +12,12 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html. -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Derivative.Examples ( diffSet1, diffSet2, diffSet3, diffSet4 , diffSet5, diffSet6, diffSet7, diffSet8 + , diffSet9 ) where import Data.Maybe @@ -166,5 +167,36 @@ ] , [ sqrt (2*x^2-1)/(x+3), sqrt (4*x^2+3)/(x+7) , sqrt (3*x^2+1)/(x-2), sqrt (5*x^2-4)/(x-7) + ] + ] + +-- Goniometrische functies differentieren (blz 95, G&R wi vwo B deel 3 +diffSet9 :: [[Expr]] +diffSet9 = differentiateLists $ + let x = Var "x" in + [ -- voorbeeld + [ 1 + 2*cos (3*x - 1/4*pi) + , x*sin x + -- , (tan x)^2 Not supported + ] + -- opgave 30 + , [ 3+4*sin (2*x-1/3*pi) + , 10+16*cos (1/2*(x-1)) + , x*cos x + , x*(cos (2*x)) + , x^2*sin(3*x) + , 2*x*sin(3*x-1) + ] + -- opgave 33 + , [ (cos x)^2 + , 2*(sin x)^2 + , 1+(2*cos x)^2 + , x+ 3*(sin x)^2 + ] + -- opgave 34 + , [ (sin x)^3 + , x*(sin x)^2 + , (cos (2*x))^2 + -- , (cos (x^2))^2 Not supported ] ] diff --git a/src/Domain/Math/Derivative/Exercises.hs b/src/Domain/Math/Derivative/Exercises.hs --- a/src/Domain/Math/Derivative/Exercises.hs +++ b/src/Domain/Math/Derivative/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,12 +9,12 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Derivative.Exercises ( derivativeExercise, derivativePolyExercise , derivativeProductExercise, derivativeQuotientExercise - , derivativePowerExercise + , derivativePowerExercise, derivativeGonioExercise ) where import Control.Monad @@ -104,11 +104,17 @@ , ready = predicate noDiff , strategy = derivativeStrategy , ruleOrdering = derivativeOrdering - , equivalence = withoutContext eqQuotientDiff + , equivalence = withoutContext eqQuotientDiff , navigation = navigator , examples = level Medium $ concat $ diffSet3++diffSet4++diffSet5++ diffSet6++diffSet7++diffSet8 {- diffSet6 -- ++diffSet7++diffSet8 -} + } + +derivativeGonioExercise :: Exercise Expr +derivativeGonioExercise = derivativeExercise + { exerciseId = diffId # "gonio" + , examples = level Medium $ concat diffSet9 } derivativeOrdering :: Rule a -> Rule a -> Ordering diff --git a/src/Domain/Math/Derivative/Rules.hs b/src/Domain/Math/Derivative/Rules.hs --- a/src/Domain/Math/Derivative/Rules.hs +++ b/src/Domain/Math/Derivative/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Derivative.Rules where @@ -20,7 +20,7 @@ import Domain.Math.Numeric.Views import Domain.Math.Polynomial.Views import Domain.Math.Power.Views -import Ideas.Common.Library hiding (root) +import Ideas.Common.Library import Prelude hiding ((^)) derivativeRules :: [Rule Expr] @@ -28,7 +28,8 @@ [ ruleDerivCon, ruleDerivPlus, ruleDerivMin, ruleDerivNegate , ruleDerivMultiple, ruleDerivPower, ruleDerivVar , ruleDerivProduct, ruleDerivQuotient, ruleDerivPowerChain - , ruleSine, ruleLog, ruleDerivSqrt, ruleDerivSqrtChain + , ruleSine, ruleCosine, ruleSineLinear, ruleCosineLinear + , ruleLog, ruleDerivSqrt, ruleDerivSqrtChain ] diff :: Expr -> Expr @@ -53,6 +54,28 @@ ruleSine :: Rule Expr ruleSine = rewriteRule (diffId, "sine") $ \x -> diff (lambda x (sin (Var x))) :~> cos (Var x) + +ruleCosine :: Rule Expr +ruleCosine = rewriteRule (diffId, "cosine") $ + \x -> diff (lambda x (cos (Var x))) :~> -sin (Var x) + +ruleSineLinear :: Rule Expr +ruleSineLinear = makeRule (diffId, "sine.linear") f + where + f (Sym d [Sym l [Var v, Sym s [expr]]]) | isDiffSymbol d && isLambdaSymbol l && s == sinSymbol = do + (x, a, _) <- match linearView expr + guard (v == x) + return (a*cos expr) + f _ = Nothing + +ruleCosineLinear :: Rule Expr +ruleCosineLinear = makeRule (diffId, "cosine.linear") f + where + f (Sym d [Sym l [Var v, Sym c [expr]]]) | isDiffSymbol d && isLambdaSymbol l && c == cosSymbol = do + (x, a, _) <- match linearView expr + guard (v == x) + return (-a*sin expr) + f _ = Nothing ruleLog :: Rule Expr ruleLog = rewriteRule (diffId, "logarithmic") $ diff --git a/src/Domain/Math/Derivative/Strategies.hs b/src/Domain/Math/Derivative/Strategies.hs --- a/src/Domain/Math/Derivative/Strategies.hs +++ b/src/Domain/Math/Derivative/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Derivative.Strategies ( derivativeStrategy, derivativePolyStrategy @@ -86,7 +86,7 @@ list = map liftToContext [ ruleDerivPlus, ruleDerivMin, ruleDerivNegate, ruleDerivPowerFactor , ruleDerivCon ] - mycfg = makeStrategyConfiguration [(byName myFractionTimes, Remove)] + mycfg = Remove `byName` myFractionTimes distr = cleanUpStrategyAfter (applyTop cleanUpExpr) $ label "distr" (somewhere (alternatives rulesPolyNF)) diff --git a/src/Domain/Math/Equation/BalanceRules.hs b/src/Domain/Math/Equation/BalanceRules.hs --- a/src/Domain/Math/Equation/BalanceRules.hs +++ b/src/Domain/Math/Equation/BalanceRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: BalanceRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: BalanceRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Equation.BalanceRules ( plusRule, minusRule, timesRule, divisionRule diff --git a/src/Domain/Math/Equation/CoverUpExercise.hs b/src/Domain/Math/Equation/CoverUpExercise.hs --- a/src/Domain/Math/Equation/CoverUpExercise.hs +++ b/src/Domain/Math/Equation/CoverUpExercise.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: CoverUpExercise.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: CoverUpExercise.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Equation.CoverUpExercise ( coverUpExercise, coverUpStrategy diff --git a/src/Domain/Math/Equation/CoverUpRules.hs b/src/Domain/Math/Equation/CoverUpRules.hs --- a/src/Domain/Math/Equation/CoverUpRules.hs +++ b/src/Domain/Math/Equation/CoverUpRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: CoverUpRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: CoverUpRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Equation.CoverUpRules ( coverUpRules, coverUpRulesOr @@ -34,7 +34,7 @@ import Domain.Math.Data.OrList import Domain.Math.Data.Relation import Domain.Math.Expr -import Ideas.Common.Library hiding (root) +import Ideas.Common.Library --------------------------------------------------------------------- -- Constructors for cover-up rules diff --git a/src/Domain/Math/Equation/Examples.hs b/src/Domain/Math/Equation/Examples.hs --- a/src/Domain/Math/Equation/Examples.hs +++ b/src/Domain/Math/Equation/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Example exercises from the Digital Mathematics Environment (DWO) -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Equation.Examples ( fillInResult, coverUpEquations diff --git a/src/Domain/Math/Equation/Views.hs b/src/Domain/Math/Equation/Views.hs --- a/src/Domain/Math/Equation/Views.hs +++ b/src/Domain/Math/Equation/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Equation.Views ( relationSolvedForm, relationsSolvedForm diff --git a/src/Domain/Math/ExerciseList.hs b/src/Domain/Math/ExerciseList.hs --- a/src/Domain/Math/ExerciseList.hs +++ b/src/Domain/Math/ExerciseList.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- All exported exercises in the mathematical domain -- ----------------------------------------------------------------------------- --- $Id: ExerciseList.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: ExerciseList.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.ExerciseList ( exerciseList, viewList, scriptList, testSuiteList @@ -69,6 +69,7 @@ , Some derivativePolyExercise , Some derivativeProductExercise , Some derivativeQuotientExercise + -- , Some derivativeGonioExercise -- , Some derivativePowerExercise , Some simplifyPowerExercise , Some powerOfExercise diff --git a/src/Domain/Math/Expr.hs b/src/Domain/Math/Expr.hs --- a/src/Domain/Math/Expr.hs +++ b/src/Domain/Math/Expr.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Expr.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Expr.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Expr (module Export) where diff --git a/src/Domain/Math/Expr/Clipboard.hs b/src/Domain/Math/Expr/Clipboard.hs --- a/src/Domain/Math/Expr/Clipboard.hs +++ b/src/Domain/Math/Expr/Clipboard.hs @@ -1,6 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -13,7 +13,7 @@ -- is part of the environment (terms that are placed in a context) -- ----------------------------------------------------------------------------- --- $Id: Clipboard.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Clipboard.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Expr.Clipboard ( -- * Data type diff --git a/src/Domain/Math/Expr/Data.hs b/src/Domain/Math/Expr/Data.hs --- a/src/Domain/Math/Expr/Data.hs +++ b/src/Domain/Math/Expr/Data.hs @@ -1,6 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -10,7 +10,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Data.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Data.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Expr.Data ( Expr(..), toExpr, fromExpr, fromDouble @@ -197,6 +197,9 @@ showSymbol s | isRootSymbol s = "root" | isLogSymbol s = "log" + | s == sinSymbol = "sin" + | s == cosSymbol = "cos" + | s == piSymbol = "pi" | otherwise = show s symbolTable = [ (s, (a, n, op)) | (n, (a, xs)) <- zip [1..] table, (s, op) <- xs ] diff --git a/src/Domain/Math/Expr/Parser.hs b/src/Domain/Math/Expr/Parser.hs --- a/src/Domain/Math/Expr/Parser.hs +++ b/src/Domain/Math/Expr/Parser.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Parser.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Expr.Parser ( parseExpr, parseExprM @@ -109,6 +109,8 @@ [ sqrt <$ reserved "sqrt" <*> atom , binary rootSymbol <$ reserved "root" <*> atom <*> atom , binary logSymbol <$ reserved "log" <*> atom <*> atom + , unary sinSymbol <$ reserved "sin" <*> atom + , unary cosSymbol <$ reserved "cos" <*> atom , do reserved "D" x <- identifier <|> parens identifier a <- atom @@ -134,6 +136,7 @@ , do notFollowedBy (char '-') either fromInteger fromDouble <$> naturalOrFloat , variable <$> identifier + , pi <$ reserved "pi" , parens expr ] @@ -160,7 +163,8 @@ lexer :: P.TokenParser a lexer = P.makeTokenParser $ emptyDef - { reservedNames = ["sqrt", "root", "log", "and", "or", "true", "false", "D"] + { reservedNames = [ "sqrt", "root", "log", "and", "or", "true", "false", "D" + , "sin", "cos", "pi" ] , reservedOpNames = ["==", "<=", ">=", "<", ">", "~=", "+", "-", "*", "^", "/"] , opStart = oneOf ":!#$%&*+./<=>?@\\^|-~" , opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~" diff --git a/src/Domain/Math/Expr/Symbols.hs b/src/Domain/Math/Expr/Symbols.hs --- a/src/Domain/Math/Expr/Symbols.hs +++ b/src/Domain/Math/Expr/Symbols.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Exports relevant OpenMath symbols -- ----------------------------------------------------------------------------- --- $Id: Symbols.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Symbols.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Expr.Symbols ( -- OpenMath dictionary symbols diff --git a/src/Domain/Math/Expr/Views.hs b/src/Domain/Math/Expr/Views.hs --- a/src/Domain/Math/Expr/Views.hs +++ b/src/Domain/Math/Expr/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Expr.Views ( module Domain.Math.Expr.Views diff --git a/src/Domain/Math/Fraction/Exercises.hs b/src/Domain/Math/Fraction/Exercises.hs --- a/src/Domain/Math/Fraction/Exercises.hs +++ b/src/Domain/Math/Fraction/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Fraction.Exercises ( simpleFractionAddition diff --git a/src/Domain/Math/Fraction/Rules.hs b/src/Domain/Math/Fraction/Rules.hs --- a/src/Domain/Math/Fraction/Rules.hs +++ b/src/Domain/Math/Fraction/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Fraction.Rules where diff --git a/src/Domain/Math/Fraction/Strategies.hs b/src/Domain/Math/Fraction/Strategies.hs --- a/src/Domain/Math/Fraction/Strategies.hs +++ b/src/Domain/Math/Fraction/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Fraction.Strategies (expandAndAdd) where diff --git a/src/Domain/Math/Numeric/Examples.hs b/src/Domain/Math/Numeric/Examples.hs --- a/src/Domain/Math/Numeric/Examples.hs +++ b/src/Domain/Math/Numeric/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Example exercises from ActiveMath -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Examples ( fractionExamples diff --git a/src/Domain/Math/Numeric/Exercises.hs b/src/Domain/Math/Numeric/Exercises.hs --- a/src/Domain/Math/Numeric/Exercises.hs +++ b/src/Domain/Math/Numeric/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Exercises ( naturalExercise, integerExercise diff --git a/src/Domain/Math/Numeric/Generators.hs b/src/Domain/Math/Numeric/Generators.hs --- a/src/Domain/Math/Numeric/Generators.hs +++ b/src/Domain/Math/Numeric/Generators.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Generators.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Generators.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Generators ( integerGenerator, rationalGenerator, numGenerator diff --git a/src/Domain/Math/Numeric/Rules.hs b/src/Domain/Math/Numeric/Rules.hs --- a/src/Domain/Math/Numeric/Rules.hs +++ b/src/Domain/Math/Numeric/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Rules where diff --git a/src/Domain/Math/Numeric/Strategies.hs b/src/Domain/Math/Numeric/Strategies.hs --- a/src/Domain/Math/Numeric/Strategies.hs +++ b/src/Domain/Math/Numeric/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Strategies ( naturalStrategy, integerStrategy diff --git a/src/Domain/Math/Numeric/Tests.hs b/src/Domain/Math/Numeric/Tests.hs --- a/src/Domain/Math/Numeric/Tests.hs +++ b/src/Domain/Math/Numeric/Tests.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Tests.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Tests.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Tests (main) where diff --git a/src/Domain/Math/Numeric/Views.hs b/src/Domain/Math/Numeric/Views.hs --- a/src/Domain/Math/Numeric/Views.hs +++ b/src/Domain/Math/Numeric/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Numeric.Views ( -- * Natural numbers diff --git a/src/Domain/Math/Polynomial/Balance.hs b/src/Domain/Math/Polynomial/Balance.hs --- a/src/Domain/Math/Polynomial/Balance.hs +++ b/src/Domain/Math/Polynomial/Balance.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Balance.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Balance.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Balance (balanceExercise) where diff --git a/src/Domain/Math/Polynomial/BalanceUtils.hs b/src/Domain/Math/Polynomial/BalanceUtils.hs --- a/src/Domain/Math/Polynomial/BalanceUtils.hs +++ b/src/Domain/Math/Polynomial/BalanceUtils.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: BalanceUtils.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: BalanceUtils.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.BalanceUtils ( eqView, minusView, negView diff --git a/src/Domain/Math/Polynomial/BuggyBalance.hs b/src/Domain/Math/Polynomial/BuggyBalance.hs --- a/src/Domain/Math/Polynomial/BuggyBalance.hs +++ b/src/Domain/Math/Polynomial/BuggyBalance.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: BuggyBalance.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: BuggyBalance.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.BuggyBalance ( buggyBalanceRules, buggyBalanceExprRules, buggyPriority diff --git a/src/Domain/Math/Polynomial/BuggyRules.hs b/src/Domain/Math/Polynomial/BuggyRules.hs --- a/src/Domain/Math/Polynomial/BuggyRules.hs +++ b/src/Domain/Math/Polynomial/BuggyRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Some buggy rules catching common misconceptions (also on the abc-formula) -- ----------------------------------------------------------------------------- --- $Id: BuggyRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: BuggyRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.BuggyRules ( buggyRulesExpr, buggyRulesEquation @@ -28,7 +28,7 @@ import Domain.Math.Numeric.Views import Domain.Math.Polynomial.Rules import Domain.Math.Polynomial.Views -import Ideas.Common.Library hiding (makeRule, root, ruleList) +import Ideas.Common.Library hiding (makeRule, ruleList) import Prelude hiding ((^)) import qualified Ideas.Common.Library as C diff --git a/src/Domain/Math/Polynomial/Equivalence.hs b/src/Domain/Math/Polynomial/Equivalence.hs --- a/src/Domain/Math/Polynomial/Equivalence.hs +++ b/src/Domain/Math/Polynomial/Equivalence.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -10,7 +10,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Equivalence.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Equivalence.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Equivalence ( linEq, quadrEqContext, highEqContext, simLogic, flipGT diff --git a/src/Domain/Math/Polynomial/Examples.hs b/src/Domain/Math/Polynomial/Examples.hs --- a/src/Domain/Math/Polynomial/Examples.hs +++ b/src/Domain/Math/Polynomial/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Example exercises from the Digital Mathematics Environment (DWO) -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Examples ( linearExamples, quadraticExamples, higherDegreeExamples diff --git a/src/Domain/Math/Polynomial/Exercises.hs b/src/Domain/Math/Polynomial/Exercises.hs --- a/src/Domain/Math/Polynomial/Exercises.hs +++ b/src/Domain/Math/Polynomial/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Exercises ( linearExercise, linearMixedExercise @@ -122,12 +122,10 @@ , strategy = configure cfg quadraticStrategy } where - cfg = makeStrategyConfiguration - [ (byName prepareSplitSquare, Reinsert) - , (byName bringAToOne, Reinsert) - , (byName (newId "abc form"), Remove) - , (byName simplerPolynomial, Remove) - ] + cfg = (Reinsert `byName` prepareSplitSquare) <> + (Reinsert `byName` bringAToOne) <> + (Remove `byName` newId "abc form") <> + (Remove `byName` simplerPolynomial) quadraticWithApproximationExercise :: Exercise (OrList (Relation Expr)) quadraticWithApproximationExercise = quadraticExercise @@ -139,10 +137,8 @@ , equivalence = withoutContext equivalentApprox } where - cfg = makeStrategyConfiguration - [ (byName (newId "approximate result"), Reinsert) - , (byName (newId "square root simplification"), Remove) - ] + cfg = (Reinsert `byName` newId "approximate result") <> + (Remove `byName` newId "square root simplification") findFactorsExercise :: Exercise Expr findFactorsExercise = makeExercise diff --git a/src/Domain/Math/Polynomial/Generators.hs b/src/Domain/Math/Polynomial/Generators.hs --- a/src/Domain/Math/Polynomial/Generators.hs +++ b/src/Domain/Math/Polynomial/Generators.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Generators.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Generators.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Generators ( polynomialGen, polynomialDegreeGen diff --git a/src/Domain/Math/Polynomial/IneqExercises.hs b/src/Domain/Math/Polynomial/IneqExercises.hs --- a/src/Domain/Math/Polynomial/IneqExercises.hs +++ b/src/Domain/Math/Polynomial/IneqExercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: IneqExercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: IneqExercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.IneqExercises ( ineqLinearExercise, ineqQuadraticExercise, ineqHigherDegreeExercise diff --git a/src/Domain/Math/Polynomial/LeastCommonMultiple.hs b/src/Domain/Math/Polynomial/LeastCommonMultiple.hs --- a/src/Domain/Math/Polynomial/LeastCommonMultiple.hs +++ b/src/Domain/Math/Polynomial/LeastCommonMultiple.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: LeastCommonMultiple.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: LeastCommonMultiple.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.LeastCommonMultiple ( lcmExpr, divisionExpr, noCommonFactor, equalFactors, testLCM diff --git a/src/Domain/Math/Polynomial/RationalExamples.hs b/src/Domain/Math/Polynomial/RationalExamples.hs --- a/src/Domain/Math/Polynomial/RationalExamples.hs +++ b/src/Domain/Math/Polynomial/RationalExamples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,7 +12,7 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html. -- ----------------------------------------------------------------------------- --- $Id: RationalExamples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: RationalExamples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.RationalExamples ( brokenEquations, normBroken, normBroken2, normBrokenCon, deelUit diff --git a/src/Domain/Math/Polynomial/RationalExercises.hs b/src/Domain/Math/Polynomial/RationalExercises.hs --- a/src/Domain/Math/Polynomial/RationalExercises.hs +++ b/src/Domain/Math/Polynomial/RationalExercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: RationalExercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: RationalExercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.RationalExercises ( rationalEquationExercise diff --git a/src/Domain/Math/Polynomial/RationalRules.hs b/src/Domain/Math/Polynomial/RationalRules.hs --- a/src/Domain/Math/Polynomial/RationalRules.hs +++ b/src/Domain/Math/Polynomial/RationalRules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: RationalRules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: RationalRules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.RationalRules ( divisionIsZero, divisionIsOne, sameDivisor, sameDividend diff --git a/src/Domain/Math/Polynomial/Rules.hs b/src/Domain/Math/Polynomial/Rules.hs --- a/src/Domain/Math/Polynomial/Rules.hs +++ b/src/Domain/Math/Polynomial/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Rules ( sameConFactor, abcFormula, allPowerFactors, bringAToOne, cancelTerms diff --git a/src/Domain/Math/Polynomial/Strategies.hs b/src/Domain/Math/Polynomial/Strategies.hs --- a/src/Domain/Math/Polynomial/Strategies.hs +++ b/src/Domain/Math/Polynomial/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Strategies ( linearStrategy, linearMixedStrategy, linearStrategyG @@ -39,11 +39,9 @@ linearMixedStrategy :: LabeledStrategy (Context (Equation Expr)) linearMixedStrategy = let f = applyTop (fmap (transform (simplify mixedFractionView) . cleanUpSimple)) - cfg = makeStrategyConfiguration - [ (byName ruleNormalizeMixedFraction, Reinsert) - , (byName ruleNormalizeRational, Remove) - ] - in cleanUpStrategyAfter f (configureNow (configure cfg linearStrategyG)) + cfg = (Reinsert `byName` ruleNormalizeMixedFraction) <> + (Remove `byName` ruleNormalizeRational) + in cleanUpStrategyAfter f $ configure cfg linearStrategyG linearStrategyG :: IsTerm a => LabeledStrategy (Context a) linearStrategyG = diff --git a/src/Domain/Math/Polynomial/Tests.hs b/src/Domain/Math/Polynomial/Tests.hs --- a/src/Domain/Math/Polynomial/Tests.hs +++ b/src/Domain/Math/Polynomial/Tests.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Tests.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Tests.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Tests (tests) where diff --git a/src/Domain/Math/Polynomial/Views.hs b/src/Domain/Math/Polynomial/Views.hs --- a/src/Domain/Math/Polynomial/Views.hs +++ b/src/Domain/Math/Polynomial/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Polynomial.Views ( polyView, polyViewWith diff --git a/src/Domain/Math/Power/Equation/Examples.hs b/src/Domain/Math/Power/Equation/Examples.hs --- a/src/Domain/Math/Power/Equation/Examples.hs +++ b/src/Domain/Math/Power/Equation/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,7 +12,7 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html. -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Equation.Examples ( powerEquations, expEquations, logEquations, higherPowerEquations diff --git a/src/Domain/Math/Power/Equation/Exercises.hs b/src/Domain/Math/Power/Equation/Exercises.hs --- a/src/Domain/Math/Power/Equation/Exercises.hs +++ b/src/Domain/Math/Power/Equation/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Equation.Exercises ( powerEqExercise diff --git a/src/Domain/Math/Power/Equation/NormViews.hs b/src/Domain/Math/Power/Equation/NormViews.hs --- a/src/Domain/Math/Power/Equation/NormViews.hs +++ b/src/Domain/Math/Power/Equation/NormViews.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: NormViews.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: NormViews.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Equation.NormViews ( normPowerEqApproxView, normExpEqView, normLogEqView diff --git a/src/Domain/Math/Power/Equation/Rules.hs b/src/Domain/Math/Power/Equation/Rules.hs --- a/src/Domain/Math/Power/Equation/Rules.hs +++ b/src/Domain/Math/Power/Equation/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Equation.Rules -- ( -- * Power equation rules diff --git a/src/Domain/Math/Power/Equation/Strategies.hs b/src/Domain/Math/Power/Equation/Strategies.hs --- a/src/Domain/Math/Power/Equation/Strategies.hs +++ b/src/Domain/Math/Power/Equation/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Equation.Strategies -- ( powerEqStrategy @@ -50,9 +50,9 @@ powerEqApproxStrategy :: LabeledStrategy (Context (Relation Expr)) powerEqApproxStrategy = label "Power equation with approximation" $ - configureNow (configure cfg powerEqStrategy) + configure cfg powerEqStrategy where - cfg = makeStrategyConfiguration [ (byName (newId "useApprox"), Reinsert) ] + cfg = Reinsert `byName` newId "useApprox" expEqStrategy :: LabeledStrategy (Context (Equation Expr)) expEqStrategy = cleanUpStrategy cleanup strat diff --git a/src/Domain/Math/Power/Examples.hs b/src/Domain/Math/Power/Examples.hs --- a/src/Domain/Math/Power/Examples.hs +++ b/src/Domain/Math/Power/Examples.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -12,7 +12,7 @@ -- see: http://www.fi.uu.nl/dwo/gr/frameset.html. -- ----------------------------------------------------------------------------- --- $Id: Examples.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Examples.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Examples where diff --git a/src/Domain/Math/Power/Exercises.hs b/src/Domain/Math/Power/Exercises.hs --- a/src/Domain/Math/Power/Exercises.hs +++ b/src/Domain/Math/Power/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -10,7 +10,7 @@ -- -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Exercises ( -- * Power exercises diff --git a/src/Domain/Math/Power/NormViews.hs b/src/Domain/Math/Power/NormViews.hs --- a/src/Domain/Math/Power/NormViews.hs +++ b/src/Domain/Math/Power/NormViews.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: NormViews.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: NormViews.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.NormViews ( -- * Normalising views diff --git a/src/Domain/Math/Power/OldViews.hs b/src/Domain/Math/Power/OldViews.hs --- a/src/Domain/Math/Power/OldViews.hs +++ b/src/Domain/Math/Power/OldViews.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: OldViews.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: OldViews.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.OldViews ( powerFactorView, powerFactorViewForWith, powerFactorViewWith diff --git a/src/Domain/Math/Power/Rules.hs b/src/Domain/Math/Power/Rules.hs --- a/src/Domain/Math/Power/Rules.hs +++ b/src/Domain/Math/Power/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Rules ( -- * Power rules @@ -34,7 +34,7 @@ import Domain.Math.Numeric.Views import Domain.Math.Power.Utils import Domain.Math.Power.Views -import Ideas.Common.Library hiding (root) +import Ideas.Common.Library import Prelude hiding ( (^) ) import qualified Domain.Math.Data.PrimeFactors as PF import qualified Prelude diff --git a/src/Domain/Math/Power/Strategies.hs b/src/Domain/Math/Power/Strategies.hs --- a/src/Domain/Math/Power/Strategies.hs +++ b/src/Domain/Math/Power/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Strategies ( -- * Power strategies diff --git a/src/Domain/Math/Power/Utils.hs b/src/Domain/Math/Power/Utils.hs --- a/src/Domain/Math/Power/Utils.hs +++ b/src/Domain/Math/Power/Utils.hs @@ -1,6 +1,6 @@ {-# LANGUAGE FlexibleInstances #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -13,7 +13,7 @@ -- moved to other parts of the framework (eg. Common) -- ----------------------------------------------------------------------------- --- $Id: Utils.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Utils.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Utils where diff --git a/src/Domain/Math/Power/Views.hs b/src/Domain/Math/Power/Views.hs --- a/src/Domain/Math/Power/Views.hs +++ b/src/Domain/Math/Power/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Power.Views ( -- * Power views @@ -30,7 +30,7 @@ import Control.Monad import Domain.Math.Expr import Domain.Math.Power.Utils -import Ideas.Common.Library hiding (root) +import Ideas.Common.Library -- Power views with constant factor ----------------------------------------- diff --git a/src/Domain/Math/Safe.hs b/src/Domain/Math/Safe.hs --- a/src/Domain/Math/Safe.hs +++ b/src/Domain/Math/Safe.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Safe.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Safe.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Safe ( -- * Safe division diff --git a/src/Domain/Math/Simplification.hs b/src/Domain/Math/Simplification.hs --- a/src/Domain/Math/Simplification.hs +++ b/src/Domain/Math/Simplification.hs @@ -1,6 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-} ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -10,7 +10,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Simplification.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Simplification.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.Simplification ( Simplify(..), SimplifyConfig(..) diff --git a/src/Domain/Math/SquareRoot/Tests.hs b/src/Domain/Math/SquareRoot/Tests.hs --- a/src/Domain/Math/SquareRoot/Tests.hs +++ b/src/Domain/Math/SquareRoot/Tests.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Tests.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Tests.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.SquareRoot.Tests (tests) where diff --git a/src/Domain/Math/SquareRoot/Views.hs b/src/Domain/Math/SquareRoot/Views.hs --- a/src/Domain/Math/SquareRoot/Views.hs +++ b/src/Domain/Math/SquareRoot/Views.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Views.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Views.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.Math.SquareRoot.Views ( squareRootView, squareRootViewWith diff --git a/src/Domain/RelationAlgebra.hs b/src/Domain/RelationAlgebra.hs --- a/src/Domain/RelationAlgebra.hs +++ b/src/Domain/RelationAlgebra.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: RelationAlgebra.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: RelationAlgebra.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra (module Export) where diff --git a/src/Domain/RelationAlgebra/Exercises.hs b/src/Domain/RelationAlgebra/Exercises.hs --- a/src/Domain/RelationAlgebra/Exercises.hs +++ b/src/Domain/RelationAlgebra/Exercises.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Exercises.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Exercises.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra.Exercises (cnfExercise) where @@ -42,8 +42,15 @@ } stepsRemaining :: Int -> RelAlg -> Maybe Int -stepsRemaining i = - lengthMax i . derivationTree toCNF . inContext cnfExercise +stepsRemaining i = checkLength i cnfExercise + +checkLength :: Int -> Exercise a -> a -> Maybe Int +checkLength n ex a = defaultDerivation ex a >>= rec 0 . steps + where + rec i [] = Just i + rec i (_:xs) + | i >= n = Nothing + | otherwise = rec (i+1) xs {- cnfExerciseSimple :: Exercise RelAlg cnfExerciseSimple = cnfExercise diff --git a/src/Domain/RelationAlgebra/Formula.hs b/src/Domain/RelationAlgebra/Formula.hs --- a/src/Domain/RelationAlgebra/Formula.hs +++ b/src/Domain/RelationAlgebra/Formula.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Formula.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Formula.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra.Formula where diff --git a/src/Domain/RelationAlgebra/Generator.hs b/src/Domain/RelationAlgebra/Generator.hs --- a/src/Domain/RelationAlgebra/Generator.hs +++ b/src/Domain/RelationAlgebra/Generator.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Generator.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Generator.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra.Generator (templateGenerator) where diff --git a/src/Domain/RelationAlgebra/Parser.hs b/src/Domain/RelationAlgebra/Parser.hs --- a/src/Domain/RelationAlgebra/Parser.hs +++ b/src/Domain/RelationAlgebra/Parser.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Parser.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Parser.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra.Parser (parseRelAlg, ppRelAlg) where diff --git a/src/Domain/RelationAlgebra/Rules.hs b/src/Domain/RelationAlgebra/Rules.hs --- a/src/Domain/RelationAlgebra/Rules.hs +++ b/src/Domain/RelationAlgebra/Rules.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Rules.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Rules.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra.Rules where diff --git a/src/Domain/RelationAlgebra/Strategies.hs b/src/Domain/RelationAlgebra/Strategies.hs --- a/src/Domain/RelationAlgebra/Strategies.hs +++ b/src/Domain/RelationAlgebra/Strategies.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -9,7 +9,7 @@ -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- --- $Id: Strategies.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Strategies.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Domain.RelationAlgebra.Strategies (toCNF) where diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -1,5 +1,5 @@ ----------------------------------------------------------------------------- --- Copyright 2014, Open Universiteit Nederland. This file is distributed +-- Copyright 2015, Open Universiteit Nederland. This file is distributed -- under the terms of the GNU General Public License. For more information, -- see the file "LICENSE.txt", which is included in the distribution. ----------------------------------------------------------------------------- @@ -11,7 +11,7 @@ -- Main module for feedback services -- ----------------------------------------------------------------------------- --- $Id: Main.hs 6548 2014-05-16 10:34:18Z bastiaan $ +-- $Id: Main.hs 7527 2015-04-08 07:58:06Z bastiaan $ module Main (main) where @@ -47,9 +47,11 @@ [ -- logic and relation-algebra Some Logic.dnfExercise , Some Logic.dnfUnicodeExercise + , Some Logic.cnfExercise , Some Logic.cnfUnicodeExercise , Some Logic.proofExercise , Some Logic.proofUnicodeExercise + , Some Logic.proofTopExercise , Some Logic.consequenceExercise , Some RA.cnfExercise -- linear algebra