packages feed

ideas-math-types (empty) → 1.0

raw patch · 34 files changed

+5024/−0 lines, 34 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, ideas, parsec, semigroups

Files

+ CHANGELOG.txt view
@@ -0,0 +1,5 @@+ideas-math-types-1.0++Initial version of the library. Some modules have been released in 2015 as part +of the ideas mathematics tutors (http://hackage.haskell.org/package/ideas-math), +although these modules were not exposed as a library.
+ LICENSE.txt view
@@ -0,0 +1,202 @@+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+ NOTICE.txt view
@@ -0,0 +1,36 @@+Copyright 2019 Ideas project team++   Licensed under the Apache License, Version 2.0 (the "License");+   you may not use this file except in compliance with the License.+   You may obtain a copy of the License at++       http://www.apache.org/licenses/LICENSE-2.0++   Unless required by applicable law or agreed to in writing, software+   distributed under the License is distributed on an "AS IS" BASIS,+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+   See the License for the specific language governing permissions and+   limitations under the License.+   +PROJECT++   Ideas (Interactive Domain-specific Exercise Assistants) is a joint research+   project between the Open University of the Netherlands and Utrecht+   University. The project's goal is to use software and compiler technology to+   build state-of-the-art components of intelligent tutoring systems (ITS) and+   learning environments. The 'ideas' software package provides a generic+   framework for constructing the expert knowledge module (also known as a+   domain reasoner) for an ITS or learning environment. The 'ideas-math-types'+   software package provides helper datatypes for implementing domain reasoners+   for mathematics and logic. More information about the project can be found +   on the project's homepage:+   +       http://ideas.cs.uu.nl/+       +AUTHORS++   The authors and copyright holders of the 'ideas-math-types' software package are:+   - Bastiaan Heeren   (bastiaan.heeren@ou.nl, maintainer)+   - Alex Gerdes       (agerdes@me.com)+   - Johan Jeuring     (J.T.Jeuring@uu.nl)+   - Josje Lodder      (josje.lodder@ou.nl)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain
+ ideas-math-types.cabal view
@@ -0,0 +1,76 @@+name:                   ideas-math-types
+version:                1.0
+synopsis:               Common types for mathematical domain reasoners
+homepage:               http://ideas.cs.uu.nl/
+description:
+
+  This package provides common datatypes and utility functions for
+  mathematical domain reasoners that are based on the 'ideas' software
+  package. The package is currently used by our logic tutors (dnf/cnf 
+  normal forms, equational proofs, axiomatic proofs, inductive proofs),
+  the statistics tutor that provides feedback on the structure of 
+  hypothesis tests, and the analyzers of the Advise-Me project. Contact 
+  the package maintainers for further information about the package.
+
+category:               Education
+copyright:              (c) 2019
+license:                Apache-2.0
+license-file:           LICENSE.txt
+author:                 Bastiaan Heeren, Alex Gerdes, Johan Jeuring, Josje Lodder
+maintainer:             bastiaan.heeren@ou.nl
+stability:              provisional
+extra-source-files:     NOTICE.txt, CHANGELOG.txt
+build-type:             Simple
+cabal-version:          >= 1.10
+tested-with:            GHC == 7.10.3
+
+source-repository head
+  type:     svn
+  location: https://ideastest.science.uu.nl/svn/ideas/Tutors/math-types
+
+library
+  ghc-options:          -Wall
+  hs-source-dirs:       src
+  default-language:     Haskell2010
+
+  build-depends:       
+    base >=4.8 && <5, 
+    ideas >=1.6,
+    QuickCheck >=2.8,
+    containers,
+    parsec
+
+  if !impl(ghc >= 8.0)
+    Build-Depends: semigroups == 0.18.*
+
+  exposed-modules:     
+
+    Domain.Algebra.Boolean
+    Domain.Algebra.BooleanLaws
+    Domain.Algebra.Field
+    Domain.Algebra.FieldLaws
+    Domain.Algebra.Group
+    Domain.Algebra.GroupLaws
+    Domain.Algebra.Law
+    Domain.Algebra.SmartGroup
+    Domain.Logic.Formula
+    Domain.Logic.Generator
+    Domain.Logic.Views
+    Domain.Math.Data.WithBool
+    Domain.Math.Data.SquareRoot
+    Domain.Math.Data.Relation
+    Domain.Math.Data.Primes
+    Domain.Math.Data.PrimeFactors
+    Domain.Math.Data.Polynomial
+    Domain.Math.Data.OrList
+    Domain.Math.Data.MixedFraction
+    Domain.Math.Data.Interval
+    Domain.Math.Data.DecimalFraction
+    Domain.Math.Expr
+    Domain.Math.Expr.Clipboard
+    Domain.Math.Expr.Data
+    Domain.Math.Expr.Parser
+    Domain.Math.Expr.Symbols
+    Domain.Math.Expr.Views
+    Domain.Math.Numeric.Views
+    Domain.Math.Safe
+ src/Domain/Algebra/Boolean.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.Boolean
+   ( -- * Boolean algebra (re-exported)
+     BoolValue(..), Boolean(..)
+   , ands, ors, implies, equivalent
+     -- * CoBoolean (matching)
+   , CoBoolean(..), conjunctions, disjunctions
+     -- * Monoids monoid
+   , DualMonoid(..), And(..), Or(..)
+   ) where
+
+import Control.Applicative
+import Domain.Algebra.Group
+import Ideas.Common.Classes
+import Test.QuickCheck
+import qualified Data.Semigroup as Sem
+
+--------------------------------------------------------
+-- CoBoolean (matching)
+
+class BoolValue a => CoBoolean a where
+   isAnd        :: a -> Maybe (a, a)
+   isOr         :: a -> Maybe (a, a)
+   isComplement :: a -> Maybe a
+
+instance CoBoolean a => CoMonoid (And a) where
+   isEmpty  = isTrue . fromAnd
+   isAppend = fmap (mapBoth And) . isAnd . fromAnd
+
+instance CoBoolean a => CoMonoidZero (And a) where
+   isMonoidZero = isFalse . fromAnd
+
+instance CoBoolean a => CoMonoid (Or a) where
+   isEmpty  = isFalse . fromOr
+   isAppend = fmap (mapBoth Or) . isOr . fromOr
+
+instance CoBoolean a => CoMonoidZero (Or a) where
+   isMonoidZero = isTrue . fromOr
+
+conjunctions :: CoBoolean a => a -> [a]
+conjunctions = map fromAnd . associativeList . And
+
+disjunctions :: CoBoolean a => a -> [a]
+disjunctions = map fromOr . associativeList . Or
+
+--------------------------------------------------------
+-- Dual monoid for a monoid (and for or, and vice versa)
+
+class MonoidZero a => DualMonoid a where
+   (><)      :: a -> a -> a
+   dualCompl :: a -> a
+
+--------------------------------------------------------
+-- And monoid
+
+newtype And a = And {fromAnd :: a}
+   deriving (Show, Eq, Ord, Arbitrary, CoArbitrary)
+
+instance Functor And where -- could be derived
+   fmap f = And . f . fromAnd
+
+instance Applicative And where
+   pure            = And
+   And f <*> And a = And (f a)
+
+instance Boolean a => Sem.Semigroup (And a) where
+   (<>) = liftA2 (<&&>)
+
+instance Boolean a => Monoid (And a) where
+   mempty  = pure true
+   mappend = (Sem.<>)
+
+instance Boolean a => MonoidZero (And a) where
+   mzero = pure false
+
+instance Boolean a => DualMonoid (And a) where
+   (><)      = liftA2 (<||>)
+   dualCompl = liftA complement
+
+--------------------------------------------------------
+-- Or monoid
+
+newtype Or a  = Or {fromOr :: a}
+   deriving (Show, Eq, Ord, Arbitrary, CoArbitrary)
+
+instance Functor Or where -- could be derived
+   fmap f = Or . f . fromOr
+
+instance Applicative Or where
+   pure          = Or
+   Or f <*> Or a = Or (f a)
+
+instance Boolean a => Sem.Semigroup (Or a) where
+   (<>) = liftA2 (<||>)
+
+instance Boolean a => Monoid (Or a) where
+   mempty  = pure false
+   mappend = (Sem.<>)
+
+instance Boolean a => MonoidZero (Or a) where
+   mzero = pure true
+
+instance Boolean a => DualMonoid (Or a) where
+   (><)      = liftA2 (<&&>)
+   dualCompl = liftA complement
+ src/Domain/Algebra/BooleanLaws.hs view
@@ -0,0 +1,108 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.BooleanLaws
+   ( -- * Boolean laws
+     andOverOrLaws, orOverAndLaws
+   , complementAndLaws, complementOrLaws
+   , absorptionAndLaws, absorptionOrLaws
+   , deMorganAnd, deMorganOr
+   , doubleComplement, complementTrue, complementFalse
+   , booleanLaws
+     -- * Law transformer
+   , fromAndLaw, fromOrLaw
+     -- * Properties
+   , propsBoolean
+   ) where
+
+import Domain.Algebra.Boolean
+import Domain.Algebra.Group
+import Domain.Algebra.GroupLaws
+import Domain.Algebra.Law
+import Test.QuickCheck hiding ((><))
+
+--------------------------------------------------------
+-- Boolean laws
+
+andOverOrLaws, orOverAndLaws :: Boolean a => [Law a]
+andOverOrLaws = map fromAndLaw dualDistributive
+orOverAndLaws = map fromOrLaw  dualDistributive
+
+complementAndLaws, complementOrLaws :: Boolean a => [Law a]
+complementAndLaws = map fromAndLaw dualComplement
+complementOrLaws  = map fromOrLaw  dualComplement
+
+absorptionAndLaws, absorptionOrLaws :: Boolean a => [Law a]
+absorptionAndLaws = map fromAndLaw dualAbsorption
+absorptionOrLaws  = map fromOrLaw  dualAbsorption
+
+deMorganAnd, deMorganOr :: Boolean a => Law a
+deMorganAnd = fromAndLaw deMorgan
+deMorganOr  = fromOrLaw  deMorgan
+
+doubleComplement :: Boolean a => Law a
+doubleComplement = law "double-complement" $ \a ->
+   complement (complement a) :==: a
+
+complementTrue, complementFalse :: Boolean a => Law a
+complementTrue  = fromAndLaw dualTrueFalse
+complementFalse = fromOrLaw  dualTrueFalse
+
+booleanLaws :: Boolean a => [Law a]
+booleanLaws =
+   map fromAndLaw (idempotent : zeroLaws ++ commutativeMonoidLaws) ++
+   map fromOrLaw  (idempotent : zeroLaws ++ commutativeMonoidLaws) ++
+   andOverOrLaws ++ orOverAndLaws ++ complementAndLaws ++ complementOrLaws ++
+   absorptionAndLaws ++ absorptionOrLaws ++
+   [deMorganAnd, deMorganOr, doubleComplement, complementTrue, complementFalse]
+
+--------------------------------------------------------
+-- Dual laws
+
+dualDistributive :: DualMonoid a => [Law a]
+dualDistributive =
+   [leftDistributiveFor (<>) (><), rightDistributiveFor (<>) (><)]
+
+dualAbsorption :: DualMonoid a => [Law a]
+dualAbsorption =
+   [ law "absorption" $ \a b -> a `f` (a `g` b) :==: a
+   | f <- [(<>), flip (<>)]
+   , g <- [(><), flip (><)]
+   ]
+
+dualComplement :: DualMonoid a => [Law a]
+dualComplement =
+   [ law "complement" $ \a -> dualCompl a <> a :==: mzero
+   , law "complement" $ \a -> a <> dualCompl a :==: mzero
+   ]
+
+dualTrueFalse :: DualMonoid a => Law a
+dualTrueFalse = law "true-false" $ dualCompl mempty :==: mzero
+
+deMorgan :: DualMonoid a => Law a
+deMorgan = law "demorgan" $ \a b ->
+   dualCompl (a <> b) :==: dualCompl a >< dualCompl b
+
+--------------------------------------------------------
+-- And laws
+
+fromAndLaw :: Law (And a) -> Law a
+fromAndLaw = mapLaw And fromAnd
+
+fromOrLaw :: Law (Or a) -> Law a
+fromOrLaw = mapLaw Or fromOr
+
+--------------------------------------------------------
+-- Tests for Bool instance
+
+propsBoolean :: [Property]
+propsBoolean = map property (booleanLaws :: [Law Bool])
+ src/Domain/Algebra/Field.hs view
@@ -0,0 +1,244 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.Field
+   ( -- * Semi-ring
+     SemiRing(..)
+     -- * Ring
+   , Ring(..)
+     -- * Field
+   , Field(..)
+     -- * Additive monoid
+   , Additive(..)
+     -- * Multiplicative monoid
+   , Multiplicative(..)
+     -- * Datatype for safe numeric operators
+   , SafeNum, safeNum
+     -- * CoSemiRing, CoRing, and CoField (for matching)
+   , CoSemiRing(..), CoRing(..), CoField(..)
+   ) where
+
+import Control.Monad
+import Domain.Algebra.Group
+import Ideas.Common.Classes (mapBoth)
+import Test.QuickCheck
+import qualified Control.Applicative as A
+import qualified Control.Applicative as Applicative
+import qualified Data.Semigroup as Sem
+
+--------------------------------------------------------
+-- Semi-ring
+
+infixl 6 |+|
+infixl 7 |*|
+
+class SemiRing a where
+   -- additive
+   (|+|) :: a -> a -> a
+   zero  :: a
+   sum   :: [a] -> a
+   -- multiplicative
+   (|*|)   :: a -> a -> a
+   one     :: a
+   product :: [a] -> a
+   -- default implementation
+   sum     [] = zero
+   sum     xs = foldl1 (|+|) xs
+   product [] = one
+   product xs = foldl1 (|*|) xs
+
+--------------------------------------------------------
+-- Ring
+
+infixl 6 |-|
+
+-- Minimal complete definition: plusInverse or <->
+class SemiRing a => Ring a where
+   plusInverse :: a -> a
+   (|-|)       :: a -> a -> a
+   -- default definitions
+   plusInverse = (zero |-|)
+   a |-| b     = a |+| plusInverse b
+
+--------------------------------------------------------
+-- Field
+
+infixl 7 |/|
+
+-- Minimal complete definition: mulInverse or </>
+class Ring a => Field a where
+   timesInverse :: a -> a
+   (|/|)        :: a -> a -> a
+   -- default definitions
+   timesInverse = (one |/|)
+   a |/| b      = a |*| timesInverse b
+
+--------------------------------------------------------
+-- Additive monoid
+
+newtype Additive a = Additive {fromAdditive :: a}
+   deriving (Show, Eq, Ord, Arbitrary, CoArbitrary)
+
+instance Functor Additive where -- could be derived
+   fmap f = Additive . f . fromAdditive
+
+instance A.Applicative Additive where
+   pure = Additive
+   Additive f <*> Additive a = Additive (f a)
+
+instance SemiRing a => Sem.Semigroup (Additive a) where
+   (<>) = A.liftA2 (|+|)
+
+instance SemiRing a => Monoid (Additive a) where
+   mempty  = A.pure zero
+   mappend = (Sem.<>)
+
+instance Ring a => Group (Additive a) where
+   inverse   = A.liftA plusInverse
+   appendInv = A.liftA2 (|-|)
+
+--------------------------------------------------------
+-- Multiplicative monoid
+
+newtype Multiplicative a = Multiplicative {fromMultiplicative :: a}
+   deriving (Show, Eq, Ord, Arbitrary, CoArbitrary)
+
+instance Functor Multiplicative where -- could be derived
+   fmap f = Multiplicative . f . fromMultiplicative
+
+instance A.Applicative Multiplicative where
+   pure = Multiplicative
+   Multiplicative f <*> Multiplicative a = Multiplicative (f a)
+
+instance SemiRing a => Sem.Semigroup (Multiplicative a) where
+   (<>) = A.liftA2 (|*|)
+
+instance SemiRing a => Monoid (Multiplicative a) where
+   mempty  = A.pure one
+   mappend = (Sem.<>)
+
+instance Field a => Group (Multiplicative a) where
+   inverse   = A.liftA timesInverse
+   appendInv = A.liftA2 (|/|)
+
+instance SemiRing a => MonoidZero (Multiplicative a) where
+   mzero = Multiplicative zero
+
+--------------------------------------------------------
+-- Datatype for safe numeric operators
+
+data SafeNum a = Ok a | Exception String
+
+safeNum :: SafeNum a -> Either String a
+safeNum (Ok a)        = Right a
+safeNum (Exception s) = Left s
+
+instance Arbitrary a => Arbitrary (SafeNum a) where
+   arbitrary = liftM return arbitrary
+
+instance Eq a => Eq (SafeNum a) where
+   Ok a == Ok b = a == b
+   _    == _    = True
+
+instance Ord a => Ord (SafeNum a) where
+   Ok a `compare` Ok b = a `compare` b
+   _    `compare` _    = EQ
+
+instance Show a => Show (SafeNum a) where
+   show = either ("Exception: " ++) show . safeNum
+
+instance Functor SafeNum where
+   fmap f = either Exception (return . f) . safeNum
+
+instance Applicative.Applicative SafeNum where
+   pure  = return
+   (<*>) = ap
+
+instance Monad SafeNum where
+   return  = Ok
+   fail    = Exception
+   m >>= f = either Exception f (safeNum m)
+
+instance Num a => Num (SafeNum a) where
+   (+) = liftM2 (+)
+   (*) = liftM2 (*)
+   (-) = liftM2 (-)
+   negate = liftM negate
+   abs    = liftM abs
+   signum = liftM signum
+   fromInteger = return . fromInteger
+
+instance (Eq a, Fractional a) => Fractional (SafeNum a) where
+   a / b = liftM2 (/) a (safeDivisor b)
+   recip = liftM recip . safeDivisor
+   fromRational = return . fromRational
+
+instance Num a => SemiRing (SafeNum a) where
+   (|+|) = (+)
+   (|*|) = (*)
+   zero  = 0
+   one   = 1
+
+instance Num a => Ring (SafeNum a) where
+   plusInverse = negate
+   (|-|)       = (-)
+
+instance (Eq a, Fractional a) => Field (SafeNum a) where
+   timesInverse = recip
+   (|/|)        = (/)
+
+safeDivisor :: (Eq a, Num a) => SafeNum a -> SafeNum a
+safeDivisor m = m >>= \a ->
+   if a == 0 then fail "division by zero" else return a
+
+------------------------------------------------------------
+
+class CoSemiRing a where
+   -- additive
+   isPlus  :: a -> Maybe (a, a)
+   isZero  :: a -> Bool
+   -- multiplicative
+   isTimes :: a -> Maybe (a, a)
+   isOne   :: a -> Bool
+
+-- Minimal complete definition: plusInverse or <->
+class CoSemiRing a => CoRing a where
+   isNegate :: a -> Maybe a
+   isMinus  :: a -> Maybe (a, a)
+   -- default definition
+   isMinus _ = Nothing
+
+class CoRing a => CoField a where
+   isRecip    :: a -> Maybe a
+   isDivision :: a -> Maybe (a, a)
+   -- default definition
+   isDivision _ = Nothing
+
+instance CoSemiRing a => CoMonoid (Additive a) where
+   isEmpty  = isZero . fromAdditive
+   isAppend = fmap (mapBoth Additive) . isPlus . fromAdditive
+
+instance CoRing a => CoGroup (Additive a) where
+   isInverse   = fmap Additive . isNegate . fromAdditive
+   isAppendInv = fmap (mapBoth Additive) . isMinus . fromAdditive
+
+instance CoSemiRing a => CoMonoid (Multiplicative a) where
+   isEmpty  = isOne . fromMultiplicative
+   isAppend = fmap (mapBoth Multiplicative) . isTimes . fromMultiplicative
+
+instance CoField a => CoGroup (Multiplicative a) where
+   isInverse   = fmap Multiplicative . isRecip . fromMultiplicative
+   isAppendInv = fmap (mapBoth Multiplicative) . isDivision . fromMultiplicative
+
+instance CoSemiRing a => CoMonoidZero (Multiplicative a) where
+   isMonoidZero = isZero . fromMultiplicative
+ src/Domain/Algebra/FieldLaws.hs view
@@ -0,0 +1,111 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.FieldLaws
+   ( -- * Semi-ring laws
+     leftDistributive, rightDistributive
+   , distributiveLaws, semiRingLaws
+     -- * Ring laws
+   , leftNegateTimes, rightNegateTimes
+   , negateTimesLaws, ringLaws, commutativeRingLaws
+   , distributiveSubtractionLaws
+     -- * Field laws
+   , exchangeInverses, fieldLaws
+     -- * Laws for additive monoid
+   , fromAdditiveLaw
+     -- * Laws for multiplicative monoid
+   , fromMultiplicativeLaw
+     -- * Properties
+   , propsField
+   ) where
+
+import Domain.Algebra.Field
+import Domain.Algebra.GroupLaws
+import Domain.Algebra.Law
+import Test.QuickCheck
+
+--------------------------------------------------------
+-- Semi-ring laws
+
+leftDistributive :: SemiRing a => Law a
+leftDistributive = leftDistributiveFor (|*|) (|+|)
+
+rightDistributive :: SemiRing a => Law a
+rightDistributive = rightDistributiveFor (|*|) (|+|)
+
+distributiveLaws :: SemiRing a => [Law a]
+distributiveLaws = [leftDistributive, rightDistributive]
+
+semiRingLaws :: SemiRing a => [Law a]
+semiRingLaws =
+   map fromAdditiveLaw commutativeMonoidLaws ++
+   map fromMultiplicativeLaw monoidZeroLaws ++
+   distributiveLaws
+
+--------------------------------------------------------
+-- Ring laws
+
+leftNegateTimes :: Ring a => Law a
+leftNegateTimes = law "left-negate-times" $ \a b ->
+   plusInverse a |*| b :==: plusInverse (a |*| b)
+
+rightNegateTimes :: Ring a => Law a
+rightNegateTimes = law "right-negate-times" $ \a b ->
+   a |*| plusInverse b :==: plusInverse (a |*| b)
+
+negateTimesLaws :: Ring a => [Law a]
+negateTimesLaws = [leftNegateTimes, rightNegateTimes]
+
+ringLaws :: Ring a => [Law a]
+ringLaws =
+   map fromAdditiveLaw abelianGroupLaws ++
+   map fromMultiplicativeLaw monoidZeroLaws ++
+   distributiveLaws ++ negateTimesLaws
+
+commutativeRingLaws :: Ring a => [Law a]
+commutativeRingLaws =
+   fromMultiplicativeLaw commutative : ringLaws
+
+distributiveSubtractionLaws :: Ring a => [Law a]
+distributiveSubtractionLaws =
+   [leftDistributiveFor (|*|) (|-|), rightDistributiveFor (|*|) (|-|)]
+
+--------------------------------------------------------
+-- Field laws
+
+exchangeInverses :: Field a => Law a
+exchangeInverses = law "exchange-inverses" $ \a ->
+   timesInverse (plusInverse a) :==: plusInverse (timesInverse a)
+
+fieldLaws :: Field a => [Law a]
+fieldLaws =
+   map fromAdditiveLaw abelianGroupLaws ++
+   map fromMultiplicativeLaw abelianGroupLaws ++
+   distributiveLaws ++ negateTimesLaws ++ [exchangeInverses]
+
+--------------------------------------------------------
+-- Laws for additive monoid
+
+fromAdditiveLaw :: Law (Additive a) -> Law a
+fromAdditiveLaw = mapLaw Additive fromAdditive
+
+--------------------------------------------------------
+-- Laws for multiplicative monoid
+
+fromMultiplicativeLaw :: Law (Multiplicative a) -> Law a
+fromMultiplicativeLaw = mapLaw Multiplicative fromMultiplicative
+
+--------------------------------------------------------
+-- Properties
+
+propsField :: [Property]
+propsField = map property (fieldLaws :: [Law (SafeNum Rational)])
+ src/Domain/Algebra/Group.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.Group
+   ( -- * Monoids
+     Monoid(..), (<>)
+     -- * Groups
+   , Group(..), (<>-)
+     -- * Monoids with a zero element
+   , MonoidZero(..), WithZero, fromWithZero
+     -- * CoMonoid, CoGroup, and CoMonoidZero (for matching)
+   , CoMonoid(..), CoGroup(..), CoMonoidZero(..)
+   , associativeList
+   ) where
+
+import Control.Applicative
+import Control.Monad (liftM2)
+import Data.Maybe
+import Data.Monoid
+import Ideas.Common.Classes
+import qualified Data.Semigroup as Sem
+import qualified Data.Set as S
+
+--------------------------------------------------------
+-- Groups
+
+-- | Minimal complete definition: inverse or appendInverse
+class Monoid a => Group a where
+   inverse   :: a -> a
+   appendInv :: a -> a -> a
+   -- default definitions
+   inverse = (mempty <>-)
+   appendInv a b = a <> inverse b
+
+infixl 6 <>-
+
+(<>-) :: Group a => a -> a -> a
+(<>-) = appendInv
+
+--------------------------------------------------------
+-- Monoids with a zero element
+-- This element could be the additive identity from a (semi-)ring for
+-- the multiplicative monoid
+
+class Monoid a => MonoidZero a where
+   mzero :: a
+
+-- Type that adds a zero element
+newtype WithZero a = WZ { fromWithZero :: Maybe a }
+   deriving (Eq, Ord, Functor, Foldable, Applicative)
+
+instance Sem.Semigroup a => Sem.Semigroup (WithZero a) where
+   (<>) x y = WZ (liftM2 (Sem.<>) (fromWithZero x) (fromWithZero y))
+
+instance Monoid a => Monoid (WithZero a) where
+   mempty = WZ (Just mempty)
+   mappend x y = WZ (liftM2 mappend (fromWithZero x) (fromWithZero y))
+
+instance Monoid a => MonoidZero (WithZero a) where
+   mzero = WZ Nothing
+
+instance Traversable WithZero where
+   traverse f = liftA WZ . traverse f . fromWithZero
+
+--------------------------------------------------------
+-- Groups
+
+class CoMonoid a where
+   isEmpty  :: a -> Bool
+   isAppend :: a -> Maybe (a, a)
+
+class CoMonoid a => CoGroup a where
+   isInverse   :: a -> Maybe a
+   isAppendInv :: a -> Maybe (a, a)
+   -- default definition
+   isAppendInv = const Nothing
+
+class CoMonoid a => CoMonoidZero a where
+   isMonoidZero :: a -> Bool
+
+fromSemiGroup :: (CoMonoid a, Monoid b) => (a -> b) -> a -> b
+fromSemiGroup f = rec
+ where
+   rec a = maybe (f a) make (isAppend a)
+   make (x, y) = rec x <> rec y
+{-
+fromMonoid :: (CoMonoid a, Monoid b) => (a -> b) -> a -> b
+fromMonoid f = fromSemiGroup $ \a ->
+   if isEmpty a then mempty else f a
+
+fromGroup :: (CoGroup a, Group b) => (a -> b) -> a -> b
+fromGroup f = rec
+ where
+   rec = fromMonoid $ \a ->
+      case isInverse a of
+         Just x  -> inverse (rec x)
+         Nothing ->
+            case isAppendInverse a of
+               Just (x, y) -> rec x <>- rec y
+               Nothing     -> f a
+
+fromMonoidZero :: (CoMonoidZero a, MonoidZero b) => (a -> b) -> a -> b
+fromMonoidZero f = fromMonoid $ \a ->
+   if isZero a then zero else f a
+
+----------------------
+-}
+associativeList :: CoMonoid a => a -> [a]
+associativeList = fromSemiGroup singleton
+{-
+monoidList :: CoMonoid a => a -> [a]
+monoidList = fromMonoid singleton
+
+-- For commutative (and associative) monoids
+monoidMultiSet :: (CoMonoid a, Ord a) => a -> MultiSet a
+monoidMultiSet = fromMonoid singleton
+
+-- For associative, commutative, idempotent (ACI) monoids
+monoidSet :: (CoMonoid a, Ord a) => a -> S.Set a
+monoidSet = fromMonoid singleton
+
+groupSequence :: (CoGroup a, Eq a) => a -> GroupSequence a
+groupSequence = fromGroup singleton
+
+abelianMultiSet :: (CoGroup a, Ord a) => a -> MultiSet a
+abelianMultiSet = fromGroup singleton
+
+monoidZeroList :: CoMonoidZero a => a -> WithZero [a]
+monoidZeroList = fromMonoidZero (pure . singleton)
+
+----------------------
+
+newtype MultiSet a = MS (M.Map a Int)
+
+instance Collection MultiSet where
+   singleton a = MS (M.singleton a 1)
+
+instance Ord a => Monoid (MultiSet a) where
+   mempty  = MS mempty
+   mappend (MS m1) (MS m2) = MS (M.unionWith (+) m1 m2)
+
+instance Ord a => Group (MultiSet a) where
+   inverse (MS m) = MS (fmap negate m)
+
+----------------------
+
+newtype GroupSequence a = GS (Q.Seq (a, Bool))
+
+instance Collection GroupSequence where
+   singleton a = GS (Q.singleton (a, False))
+
+instance Eq a => Monoid (GroupSequence a) where
+   mempty = GS mempty
+   mappend (GS xs) (GS ys) =
+      case (Q.viewr xs, Q.viewl ys) of
+         (as Q.:> (a, ai), (b, bi) Q.:< bs) | a == b && ai /= bi ->
+            mappend (GS as) (GS bs)
+         _ -> GS (xs <> ys)
+
+instance Eq a => Group (GroupSequence a) where
+   inverse (GS xs) = GS (fmap (second not) xs) -- actually: reverse order!!
+-}
+----------------------
+
+instance CoMonoid [a] where
+   isEmpty = null
+   isAppend (x:xs@(_:_)) = Just ([x], xs)
+   isAppend _            = Nothing
+
+instance CoMonoid (S.Set a) where
+   isEmpty = S.null
+   isAppend s
+      | S.size s > 1 = Just (mapFirst S.singleton (S.deleteFindMin s))
+      | otherwise    = Nothing
+
+{-
+instance CoMonoid (Q.Seq a) where
+   isEmpty = Q.null
+   isAppend xs
+      | n > 1     = Just (Q.splitAt (n `div` 2) xs)
+      | otherwise = Nothing
+    where
+      n = Q.length xs
+-}
+instance CoMonoid a => CoMonoid (WithZero a) where
+   isEmpty    = maybe False isEmpty . fromWithZero
+   isAppend a = fromWithZero a >>= fmap (mapBoth pure) . isAppend
+
+instance CoMonoid a => CoMonoidZero (WithZero a) where
+   isMonoidZero = isNothing . fromWithZero
+ src/Domain/Algebra/GroupLaws.hs view
@@ -0,0 +1,150 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.GroupLaws
+   ( -- * Monoid laws
+     associative, leftIdentity
+   , rightIdentity, identityLaws, monoidLaws, commutativeMonoidLaws
+   , idempotent
+     -- * Group laws
+   , leftInverse, rightInverse, doubleInverse
+   , inverseIdentity, inverseDistrFlipped, inverseLaws, groupLaws
+   , appendInverseLaws
+     -- * Abelian group laws
+   , commutative, inverseDistr, abelianGroupLaws
+     -- * Laws for monoids with a zero element
+   , leftZero, rightZero, zeroLaws, monoidZeroLaws
+     -- * Generalized laws
+   , associativeFor, commutativeFor, idempotentFor
+   , leftDistributiveFor, rightDistributiveFor
+   ) where
+
+import Domain.Algebra.Group
+import Domain.Algebra.Law
+import Prelude hiding ((<*>))
+
+--------------------------------------------------------
+-- Monoids
+
+associative :: Monoid a => Law a
+associative = associativeFor (<>)
+
+leftIdentity :: Monoid a => Law a
+leftIdentity = law "left-identity" $ \a -> mempty <> a :==: a
+
+rightIdentity :: Monoid a => Law a
+rightIdentity = law "right-identity" $ \a -> a <> mempty :==: a
+
+identityLaws :: Monoid a => [Law a]
+identityLaws = [leftIdentity, rightIdentity]
+
+monoidLaws :: Monoid a => [Law a]
+monoidLaws = associative : identityLaws
+
+commutativeMonoidLaws :: Monoid a => [Law a]
+commutativeMonoidLaws = monoidLaws ++ [commutative]
+
+-- | Not all monoids are idempotent (see: idempotentFor)
+idempotent :: Monoid a => Law a
+idempotent = idempotentFor (<>)
+
+--------------------------------------------------------
+-- Groups
+
+leftInverse :: Group a => Law a
+leftInverse = law "left-inverse" $ \a -> inverse a <> a :==: mempty
+
+rightInverse :: Group a => Law a
+rightInverse = law "right-inverse" $ \a -> a <> inverse a :==: mempty
+
+doubleInverse :: Group a => Law a
+doubleInverse = law "double-inverse" $ \a -> inverse (inverse a) :==: a
+
+inverseIdentity :: Group a => Law a
+inverseIdentity = law "inverse-identity" $ inverse mempty :==: mempty
+
+inverseDistrFlipped :: Group a => Law a
+inverseDistrFlipped = law "inverse-distr-flipped" $ \a b ->
+   inverse (a <> b) :==: inverse b <> inverse a
+
+inverseLaws :: Group a => [Law a]
+inverseLaws = [leftInverse, rightInverse]
+
+groupLaws :: Group a => [Law a]
+groupLaws = monoidLaws ++ inverseLaws ++
+   [doubleInverse, inverseIdentity, inverseDistrFlipped]
+
+appendInverseLaws :: Group a => [Law a]
+appendInverseLaws =
+   [ make 1 $ \a b   ->           a <>- b :==: a <> inverse b
+   , make 2 $ \a     ->           a <>- a :==: mempty
+   , make 3 $ \a     ->      a <>- mempty :==: a
+   , make 4 $ \a     ->      mempty <>- a :==: inverse a
+   , make 5 $ \a b c ->    a <>- (b <> c) :==: (a <>- b) <>- c
+   , make 6 $ \a b c ->   a <>- (b <>- c) :==: (a <>- b) <> c
+   , make 7 $ \a b c ->    a <> (b <>- c) :==: (a <> b) <>- c
+   , make 8 $ \a b   ->   a <>- inverse b :==: a <> b
+   , make 9 $ \a b   -> inverse (a <>- b) :==: inverse a <> b
+   ]
+ where
+    make n = law ("append-inverse-law" ++ show (n :: Int))
+
+--------------------------------------------------------
+-- Abelian groups
+
+commutative :: Monoid a => Law a
+commutative = commutativeFor (<>)
+
+inverseDistr :: Group a => Law a
+inverseDistr = law "inverse-distr" $ \a b ->
+    inverse (a <> b) :==: (inverse a <> inverse b)
+
+abelianGroupLaws :: Group a => [Law a]
+abelianGroupLaws = groupLaws ++ [commutative, inverseDistr]
+
+--------------------------------------------------------
+-- Monoids with a zero element
+-- This element could be the additive identity from a (semi-)ring for
+-- the multiplicative monoid
+
+leftZero :: MonoidZero a => Law a
+leftZero = law "left-zero" $ \a -> mzero <> a :==: mzero
+
+rightZero:: MonoidZero a => Law a
+rightZero = law "right-zero" $ \a -> a <> mzero :==: mzero
+
+zeroLaws :: MonoidZero a => [Law a]
+zeroLaws = [leftZero, rightZero]
+
+monoidZeroLaws :: MonoidZero a => [Law a]
+monoidZeroLaws = monoidLaws ++ zeroLaws
+
+--------------------------------------------------------
+-- Generalized laws
+
+associativeFor :: (a -> a -> a) -> Law a
+associativeFor (?) = law "associative" $ \a b c ->
+   a ? (b ? c) :==: (a ? b) ? c
+
+commutativeFor :: (a -> a -> a) -> Law a
+commutativeFor (?) = law "commutative" $ \a b -> a ? b :==: b ? a
+
+idempotentFor :: (a -> a -> a) -> Law a
+idempotentFor (?) = law "idempotent" $ \a -> a ? a :==: a
+
+leftDistributiveFor :: (a -> a -> a) -> (a -> a -> a) -> Law a
+leftDistributiveFor (<*>) (<+>) = law "left-distributive" $ \a b c ->
+   a <*> (b <+> c) :==: (a <*> b) <+> (a <*> c)
+
+rightDistributiveFor :: (a -> a -> a) -> (a -> a -> a) -> Law a
+rightDistributiveFor (<*>) (<+>) = law "right-distributive" $ \a b c ->
+   (a <+> b) <*> c :==: (a <*> c) <+> (b <*> c)
+ src/Domain/Algebra/Law.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE FunctionalDependencies, FlexibleInstances, ExistentialQuantification #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.Law
+   ( Law, LawSpec((:==:)), law, lawAbs, mapLaw
+   , propertyLaw, rewriteLaw
+   ) where
+
+import Ideas.Common.Rewriting
+import Test.QuickCheck
+
+infix 1 :==:
+
+data Law a = Law String (LawSpec a)
+
+instance Show (Law a) where
+   show (Law s _) = s
+
+data LawSpec a
+   = AbsMono (a -> LawSpec a) -- simple abstraction (fewer classes needed)
+   | forall b . (Arbitrary b, Show b, Different b) => Abs (b -> LawSpec a) -- generalized abstraction
+   | a :==: a
+
+law :: LawBuilder l a => String -> l -> Law a
+law s l = Law s (lawSpec l)
+
+lawAbs :: (Different b, Arbitrary b, Show b) => (b -> LawSpec a) -> LawSpec a
+lawAbs = Abs
+
+class LawBuilder l a | l -> a where
+   lawSpec :: l -> LawSpec a
+
+instance LawBuilder (LawSpec a) a where
+   lawSpec = id
+
+instance LawBuilder (Law a) a where
+   lawSpec = getLawSpec
+
+instance LawBuilder b a => LawBuilder (a -> b) a where
+   lawSpec f = AbsMono (lawSpec . f)
+
+instance (Show a, Eq a, Arbitrary a) => Testable (Law a) where
+   property = propertyLaw (==)
+
+mapLaw :: (b -> a) -> (a -> b) -> Law a -> Law b
+mapLaw to from (Law s l) = Law s (rec l)
+ where
+   rec (AbsMono f) = AbsMono (rec . f . to)
+   rec (Abs f)     = Abs (rec . f)
+   rec (a :==: b)  = from a :==: from b
+
+propertyLaw :: (Arbitrary a, Show a, Testable b) => (a -> a -> b) -> Law a -> Property
+propertyLaw eq = rec . getLawSpec
+ where
+   rec (AbsMono f) = property (rec . f)
+   rec (Abs f)     = property (rec . f)
+   rec (a :==: b)  = property (eq a b)
+
+rewriteLaw :: (Different a, IsTerm a, Arbitrary a, Show a) => Law a -> RewriteRule a
+rewriteLaw (Law s l) = makeRewriteRule s l
+
+instance (Arbitrary a, IsTerm a, Show a, Different a) => RuleBuilder (LawSpec a) a where
+   buildRuleSpec i (a :==: b)  = buildRuleSpec i (a :~> b)
+   buildRuleSpec i (AbsMono f) = buildRuleSpec i f
+   buildRuleSpec i (Abs f)     = buildRuleSpec i f
+
+getLawSpec :: Law a -> LawSpec a
+getLawSpec (Law _ l) = l
+ src/Domain/Algebra/SmartGroup.hs view
@@ -0,0 +1,213 @@+{-# LANGUAGE GeneralizedNewtypeDeriving, PatternGuards #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Algebra.SmartGroup
+   ( -- * Smart datatypes
+     Smart(..), SmartZero(..), SmartGroup(..)
+     --- * Smart field
+   , SmartField(..), (.+.), (.-.), neg, (.*.), (./.)
+     -- * Smart booleans
+   , (.&&.), (.||.)
+   ) where
+
+import Control.Applicative
+import Control.Monad (mplus)
+import Data.Maybe
+import Domain.Algebra.Boolean
+import Domain.Algebra.Field
+import Domain.Algebra.Group
+import qualified Data.Semigroup as Sem
+
+newtype Smart a = Smart {fromSmart :: a}
+   deriving (Show, Eq, Ord, CoMonoid, MonoidZero, CoMonoidZero)
+
+instance Functor Smart where -- could be derived
+   fmap f = Smart . f . fromSmart
+
+instance Applicative Smart where
+   pure = Smart
+   Smart f <*> Smart a = Smart (f a)
+
+instance (CoMonoid a, Sem.Semigroup a) => Sem.Semigroup (Smart a) where
+   a <> b
+      | isEmpty a = b
+      | isEmpty b = a
+      | otherwise = liftA2 (Sem.<>) a b
+
+instance (CoMonoid a, Monoid a) => Monoid (Smart a) where
+   mempty = Smart mempty
+   mappend a b
+      | isEmpty a = b
+      | isEmpty b = a
+      | otherwise = liftA2 (<>) a b
+
+--------------------------------------------------------------
+
+newtype SmartZero a = SmartZero {fromSmartZero :: a}
+   deriving (Show, Eq, Ord, MonoidZero, CoMonoid, CoMonoidZero)
+
+instance Functor SmartZero where -- could be derived
+   fmap f = SmartZero . f . fromSmartZero
+
+instance Applicative SmartZero where
+   pure = SmartZero
+   SmartZero f <*> SmartZero a = SmartZero (f a)
+
+instance (CoMonoidZero a, MonoidZero a, Sem.Semigroup a) => Sem.Semigroup (SmartZero a) where
+   a <> b
+      | isMonoidZero a || isMonoidZero b = mzero
+      | otherwise = liftA2 (Sem.<>) a b
+
+instance (CoMonoidZero a, MonoidZero a) => Monoid (SmartZero a) where
+   mempty = SmartZero mempty
+   mappend a b
+      | isMonoidZero a || isMonoidZero b = mzero
+      | otherwise = liftA2 (<>) a b
+
+--------------------------------------------------------------
+
+newtype SmartGroup a = SmartGroup {fromSmartGroup :: a}
+   deriving (Show, Eq, Ord, CoMonoid, CoGroup, CoMonoidZero, MonoidZero)
+
+instance Functor SmartGroup where -- could be derived
+   fmap f = SmartGroup . f . fromSmartGroup
+
+instance Applicative SmartGroup where
+   pure = SmartGroup
+   SmartGroup f <*> SmartGroup a = SmartGroup (f a)
+
+instance (CoGroup a, Group a) => Sem.Semigroup (SmartGroup a) where
+   a <> b
+      | isEmpty a = b
+      | otherwise = fromMaybe (liftA2 (<>) a b) (matchGroup alg b)
+    where
+      alg = (a, \x y -> (a <> x) <> y, \x -> a <>- x, \x y -> (a <> x) <>- y)
+
+instance (CoGroup a, Group a) => Monoid (SmartGroup a) where
+   mempty  = SmartGroup mempty
+   mappend = (Sem.<>)
+
+instance (CoGroup a, Group a) => Group (SmartGroup a) where
+   inverse a = fromMaybe (liftA inverse a) (matchGroup alg a)
+    where
+      alg = (mempty, \x y -> inverse x <>- y, id, \x y -> inverse x <> y)
+   appendInv a b
+      | isEmpty a = inverse b
+      | otherwise = fromMaybe (liftA2 (<>-) a b) (matchGroup alg b)
+    where
+      alg = (a, \x y -> (a <>- x) <>- y, \x -> a <> x, \x y -> (a <>- x) <> y)
+
+--------------------------------------------------------------
+
+type GroupMatch a b = (b, a -> a -> b, a -> b, a -> a -> b)
+
+matchGroup :: CoGroup a => GroupMatch a b -> a -> Maybe b
+matchGroup (emp, app, inv, appinv) a =
+   (if isEmpty a then Just emp else Nothing) `mplus`
+   fmap (uncurry app) (isAppend a)  `mplus`
+   fmap inv (isInverse a) `mplus`
+   fmap (uncurry appinv) (isAppendInv a)
+
+--------------------------------------------------------------
+-- Smart Field
+
+newtype SmartField a = SmartField {fromSmartField :: a}
+   deriving (CoSemiRing, CoRing, CoField)
+
+instance Functor SmartField where -- could be derived
+   fmap f = SmartField . f . fromSmartField
+
+instance Applicative SmartField where
+   pure = SmartField
+   SmartField f <*> SmartField a = SmartField (f a)
+
+instance (CoField a, Field a) => SemiRing (SmartField a) where
+   zero = SmartField zero
+   one  = SmartField one
+   SmartField a |+| SmartField b = SmartField $ fromAdditive $ fromSmartGroup $
+      SmartGroup (Additive a) <> SmartGroup (Additive b)
+   a |*| b
+      | Just x <- isNegate a = plusInverse (x |*| b)
+      | Just x <- isNegate b = plusInverse (a |*| x)
+      | isZero a || isZero b = zero
+      | isOne a = b
+      | isOne b = a
+      | Just (x, y) <- isTimes b = (a |*| x) |*| y
+      | Just (x, y) <- isDivision b = (a |*| x) |/| y
+      | otherwise = liftA2 (|*|) a b
+
+instance (CoField a, Field a) => Ring (SmartField a) where
+   plusInverse = SmartField . fromAdditive . fromSmartGroup . inverse
+               . SmartGroup . Additive . fromSmartField
+   SmartField a |-| SmartField b = SmartField $ fromAdditive $ fromSmartGroup $
+      SmartGroup (Additive a) <>- SmartGroup (Additive b)
+
+instance (CoField a, Field a) => Field (SmartField a) where
+   timesInverse a
+      | Just x <- isNegate a = plusInverse (timesInverse x)
+      | Just (x, y) <- isDivision a, isOne y = x
+      | otherwise = liftA timesInverse a
+   a |/| b
+      | Just x <- isNegate a = plusInverse (x |/| b)
+      | Just x <- isNegate b = plusInverse (a |/| x)
+      | isOne b = a
+      | Just (x, y) <- isDivision a = x |/| (y |*| b)
+      | otherwise = liftA2 (|/|) a b
+
+------------------------------------------------------------------
+
+infixl 7 .*., ./.
+infixl 6 .-., .+.
+
+(.+.) :: (CoField a, Field a) => a -> a -> a
+a .+. b = fromSmartField $ SmartField a |+| SmartField b
+
+(.-.) :: (CoField a, Field a) => a -> a -> a
+a .-. b = fromSmartField $ SmartField a |-| SmartField b
+
+neg :: (CoField a, Field a) => a -> a
+neg = fromSmartField . plusInverse . SmartField
+
+(.*.) :: (CoField a, Field a) => a -> a -> a
+a .*. b = fromSmartField $ SmartField a |*| SmartField b
+
+(./.) :: (CoField a, Field a) => a -> a -> a
+a ./. b = fromSmartField $ SmartField a |/| SmartField b
+
+-- myrecip :: (CoField a, Field a) => a -> a
+-- myrecip = fromSmartField . timesInverse . SmartField
+
+--------------------------------------------------------------
+-- Smart booleans
+
+instance BoolValue a => BoolValue (Smart a) where
+   fromBool = Smart   . fromBool
+   isTrue   = isTrue  . fromSmart
+   isFalse  = isFalse . fromSmart
+
+instance (Boolean a, CoBoolean a) => Boolean (Smart a) where
+   a <&&> b = fmap fromAnd $ fromSmartZero $
+      SmartZero (fmap And a) <> SmartZero (fmap And b)
+   a <||> b = fmap fromOr $ fromSmartZero $
+      SmartZero (fmap Or a) <> SmartZero (fmap Or b)
+   complement (Smart a)
+      | isTrue  a = false
+      | isFalse a = true
+      | otherwise = Smart $ fromMaybe (complement a) (isComplement a)
+
+infixr 4 .||.
+infixr 5 .&&.
+
+(.&&.), (.||.) :: (Boolean a, CoBoolean a) => a -> a -> a
+a .&&. b = fromSmart $ Smart a <&&> Smart b
+a .||. b = fromSmart $ Smart a <||> Smart b
+ src/Domain/Logic/Formula.hs view
@@ -0,0 +1,230 @@+{-# LANGUAGE DeriveDataTypeable #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Logic.Formula
+   ( module Domain.Logic.Formula, module Domain.Algebra.Boolean
+   ) where
+
+import Control.Applicative
+import Control.Monad
+import Data.Foldable (toList)
+import Data.List
+import Data.Monoid
+import Data.Traversable (fmapDefault, foldMapDefault)
+import Data.Typeable
+import Domain.Algebra.Boolean
+import Ideas.Common.Classes
+import Ideas.Common.Rewriting hiding (trueSymbol, falseSymbol)
+import Ideas.Text.Latex
+import Ideas.Utils.Prelude (ShowString, subsets)
+import Ideas.Utils.Uniplate
+import qualified Ideas.Text.OpenMath.Dictionary.Logic1 as OM
+
+infixr 2 :<->:
+infixr 3 :->:
+infixr 4 :||:
+infixr 5 :&&:
+
+-- | The data type Logic is the abstract syntax for the domain
+-- | of logic expressions.
+data Logic a = Var a
+             | Logic a :->:  Logic a            -- implication
+             | Logic a :<->: Logic a            -- equivalence
+             | Logic a :&&:  Logic a            -- and (conjunction)
+             | Logic a :||:  Logic a            -- or (disjunction)
+             | Not (Logic a)                    -- not
+             | T                                -- true
+             | F                                -- false
+ deriving (Eq, Ord, Typeable)
+
+-- | For simple use, we assume the variables to be strings
+type SLogic = Logic ShowString
+
+instance Show a => Show (Logic a) where
+   show     = ppLogic
+   showList = (++) . intercalate ", " . map show
+
+instance Functor Logic where
+   fmap = fmapDefault
+
+instance Foldable Logic where
+   foldMap = foldMapDefault
+
+instance Traversable Logic where
+   traverse f = foldLogic
+      ( fmap Var . f, liftA2 (:->:), liftA2 (:<->:), liftA2 (:&&:)
+      , liftA2 (:||:), liftA Not, pure T, pure F
+      )
+
+instance BoolValue (Logic a) where
+   fromBool b = if b then T else F
+   isTrue T  = True
+   isTrue _  = False
+   isFalse F = True
+   isFalse _ = False
+
+instance Boolean (Logic a) where
+   (<&&>)     = (:&&:)
+   (<||>)     = (:||:)
+   complement = Not
+
+instance CoBoolean (Logic a) where
+   isAnd (p :&&: q)     = Just (p, q)
+   isAnd _              = Nothing
+   isOr  (p :||: q)     = Just (p, q)
+   isOr  _              = Nothing
+   isComplement (Not p) = Just p
+   isComplement _       = Nothing
+
+instance Container Logic where
+   singleton            = Var
+   getSingleton (Var a) = Just a
+   getSingleton _       = Nothing
+
+instance ToLatex a => ToLatex (Logic a) where
+   toLatexPrec = flip (foldLogic alg)
+    where
+      alg = ( pp, binopN 3 "rightarrow", binopN 0 "leftrightarrow", binopA 2 "wedge"
+            , binopA 1 "vee", nott, pp "T", pp "F")
+      binopA prio op p q n = parIf (n > prio) (p prio <> command op <> q prio)
+      binopN prio op p q n = parIf (n > prio) (p (prio+1) <> command op <> q (prio + 1))
+      pp s      = const (toLatex s)
+      nott p _  = command "neg" <> p 4
+      parIf b   = if b then parens else id
+
+-- | The type LogicAlg is the algebra for the data type Logic
+-- | Used in the fold for Logic.
+type LogicAlg b a = (b -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a, a)
+
+-- | foldLogic is the standard fold for Logic.
+foldLogic :: LogicAlg b a -> Logic b -> a
+foldLogic (var, impl, equiv, conj, disj, neg, tr, fl) = rec
+ where
+   rec logic =
+      case logic of
+         Var x     -> var x
+         p :->: q  -> rec p `impl`  rec q
+         p :<->: q -> rec p `equiv` rec q
+         p :&&: q  -> rec p `conj`  rec q
+         p :||: q  -> rec p `disj`  rec q
+         Not p     -> neg (rec p)
+         T         -> tr
+         F         -> fl
+
+-- | Pretty-printer for propositions
+ppLogic :: Show a => Logic a -> String
+ppLogic = ppLogicPrio 0
+
+ppLogicPrio :: Show a => Int -> Logic a -> String
+ppLogicPrio = (\f s -> f s "") . flip (foldLogic alg)
+ where
+   alg = ( pp . show, binop 3 "->", binop 0 "<->", binop 2 "/\\"
+         , binop 1 "||", nott, pp "T", pp "F")
+   binop prio op p q n = parIf (n > prio) (p (prio+1) . ((" "++op++" ")++) . q prio)
+   pp s      = const (s++)
+   nott p _  = ("~"++) . p 4
+   parIf b f = if b then ("("++) . f . (")"++) else f
+
+-- | The monadic join for logic
+catLogic :: Logic (Logic a) -> Logic a
+catLogic = foldLogic (id, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)
+
+-- | evalLogic takes a function that gives a logic value to a variable,
+-- | and a Logic expression, and evaluates the boolean expression.
+evalLogic :: (a -> Bool) -> Logic a -> Bool
+evalLogic env = foldLogic (env, impl, (==), (&&), (||), not, True, False)
+ where
+   impl p q = not p || q
+
+-- | eqLogic determines whether or not two Logic expression are logically
+-- | equal, by evaluating the logic expressions on all valuations.
+eqLogic :: Eq a => Logic a -> Logic a -> Bool
+eqLogic p q = all (\f -> evalLogic f p == evalLogic f q) fs
+ where
+   xs = varsLogic p `union` varsLogic q
+   fs = map (flip elem) (subsets xs)
+
+tautology :: Eq a => Logic a -> Bool
+tautology = eqLogic T
+
+isNot :: Logic a -> Bool
+isNot (Not _) = True
+isNot _       = False
+
+-- | A Logic expression is atomic if it is a variable or a constant True or False.
+isAtomic :: Logic a -> Bool
+isAtomic logic =
+   case logic of
+      Not (Var _) -> True
+      _           -> null (children logic)
+
+-- | Functions isDNF, and isCNF determine whether or not a Logix expression
+-- | is in disjunctive normal form, or conjunctive normal form, respectively.
+isDNF, isCNF :: Logic a -> Bool
+isDNF = all isAtomic . concatMap conjunctions . disjunctions
+isCNF = all isAtomic . concatMap disjunctions . conjunctions
+
+-- | Count the number of equivalences
+countEquivalences :: Logic a -> Int
+countEquivalences p = length [ () | _ :<->: _ <- universe p ]
+
+-- | Function varsLogic returns the variables that appear in a Logic expression.
+varsLogic :: Eq a => Logic a -> [a]
+varsLogic = nub . toList
+
+instance Uniplate (Logic a) where
+   uniplate this =
+      case this of
+         p :->: q  -> plate (:->:)  |* p |* q
+         p :<->: q -> plate (:<->:) |* p |* q
+         p :&&: q  -> plate (:&&:)  |* p |* q
+         p :||: q  -> plate (:||:)  |* p |* q
+         Not p     -> plate Not     |* p
+         _         -> plate this
+
+instance Different (Logic a) where
+   different = (T, F)
+
+instance IsTerm a => IsTerm (Logic a) where
+   toTerm = foldLogic
+      ( toTerm, binary impliesSymbol, binary equivalentSymbol
+      , binary andSymbol, binary orSymbol, unary notSymbol
+      , symbol trueSymbol, symbol falseSymbol
+      )
+
+   fromTerm a =
+      fromTermWith f a `mplus` liftM Var (fromTerm a)
+    where
+      f s []
+         | s == trueSymbol       = return T
+         | s == falseSymbol      = return F
+      f s [x]
+         | s == notSymbol        = return (Not x)
+      f s [x, y]
+         | s == impliesSymbol    = return (x :->: y)
+         | s == equivalentSymbol = return (x :<->: y)
+      f s xs
+         | s == andSymbol        = return (ands xs)
+         | s == orSymbol         = return (ors xs)
+      f _ _ = fail "fromTerm"
+
+trueSymbol, falseSymbol, notSymbol, impliesSymbol, equivalentSymbol,
+   andSymbol, orSymbol :: Symbol
+
+trueSymbol       = newSymbol OM.trueSymbol
+falseSymbol      = newSymbol OM.falseSymbol
+notSymbol        = newSymbol OM.notSymbol
+impliesSymbol    = newSymbol OM.impliesSymbol
+equivalentSymbol = newSymbol OM.equivalentSymbol
+andSymbol        = makeAssociative $ newSymbol OM.andSymbol
+orSymbol         = makeAssociative $ newSymbol OM.orSymbol
+ src/Domain/Logic/Generator.hs view
@@ -0,0 +1,150 @@+{-# LANGUAGE FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Logic.Generator
+   ( generateLogic, generateLevel, equalLogicA, equalLogicACI
+   , normalizeLogicA
+   ) where
+
+import Control.Monad
+import Data.Char
+import Data.Function
+import Data.List
+import Domain.Logic.Formula
+import Ideas.Common.Exercise
+import Ideas.Utils.Prelude (ShowString(..))
+import Ideas.Utils.Uniplate
+import Test.QuickCheck
+
+-------------------------------------------------------------
+-- Code that doesn't belong here
+
+-- | Equality modulo associativity of operators
+equalLogicA :: Eq a => Logic a -> Logic a -> Bool
+equalLogicA = (==) `on` normalizeLogicA
+
+normalizeLogicA :: Logic a -> Logic a
+normalizeLogicA a =
+   case a of
+      _ :&&: _ -> ands (map normalizeLogicA (conjunctions a))
+      _ :||: _ -> ors  (map normalizeLogicA (disjunctions a))
+      _        -> descend normalizeLogicA a
+
+-- | Equality modulo associativity/commutativity/idempotency of operators,
+--   and there units/absorbing elements
+equalLogicACI :: Ord a => Logic a -> Logic a -> Bool
+equalLogicACI p q = rec p == rec q
+ where
+   rec a@(_ :&&: _) =
+      let xs = filter (/=T) $ nub $ sort $ conjunctions a
+      in if F `elem` xs then F else ands (map rec xs)
+   rec a@(_ :||: _) =
+      let xs = filter (/=F) $ nub $ sort $ disjunctions a
+      in if T `elem` xs then T else ors (map rec xs)
+   rec a = descend rec a
+
+-----------------------------------------------------------
+-- Logic generator
+
+generateLogic :: Gen SLogic
+generateLogic = normalGenerator
+
+generateLevel :: Difficulty -> (Gen SLogic, (Int, Int))
+generateLevel dif
+   | dif <= Easy      = (easyGenerator,      (3, 6))
+   | dif >= Difficult = (difficultGenerator, (7, 18))
+   | otherwise        = (normalGenerator,    (4, 12))
+
+-- Use the propositions with 3-6 steps
+easyGenerator :: Gen SLogic
+easyGenerator = do
+   n  <- elements [2, 4] -- , return 8]
+   sizedGen True varGen n
+
+-- Use the propositions with 4-12 steps
+normalGenerator :: Gen SLogic
+normalGenerator = do
+   p0 <- sizedGen False varGen 4
+   p1 <- preventSameVar varList p0
+   return (removePartsInDNF p1)
+
+-- Use the propositions with 7-18 steps
+difficultGenerator :: Gen SLogic
+difficultGenerator = do
+   let vs = ShowString "s" : varList
+   p0 <- sizedGen False (elements vs) 4
+   p1 <- preventSameVar vs p0
+   return (removePartsInDNF p1)
+
+varList :: [ShowString]
+varList = map ShowString ["p", "q", "r"]
+
+varGen :: Gen ShowString
+varGen = elements varList
+
+sizedGen :: Bool -> Gen a -> Int -> Gen (Logic a)
+sizedGen constants gen = go
+ where
+   go n
+      | n > 0 =
+           let rec   = go (n `div` 2)
+               op2 f = liftM2 f rec rec
+           in frequency
+                 [ (2, go 0)
+                 , (2, op2 (:->:))
+                 , (1, op2 (:<->:))
+                 , (3, op2 (:&&:))
+                 , (3, op2 (:||:))
+                 , (3, liftM Not rec)
+                 ]
+      | constants = frequency
+           [(5, liftM Var gen), (1, return T), (1, return F)]
+      | otherwise = liftM Var gen
+
+-----------------------------------------------------------------
+-- Simple tricks for creating for "nice" logic propositions
+
+preventSameVar :: Eq a => [a] -> Logic a -> Gen (Logic a)
+preventSameVar xs = rec
+ where
+   rec p = case holes p of
+              [(Var a, _), (Var b, update)] | a==b -> do
+                 c <- elements $ filter (/=a) xs
+                 return $ update (Var c)
+              _ -> descendM rec p
+
+removePartsInDNF :: SLogic -> SLogic
+removePartsInDNF = buildOr . filter (not . simple) . disjunctions
+ where
+   buildOr [] = T
+   buildOr xs = foldl1 (:||:) xs
+
+   simple = all f . conjunctions
+    where
+      f (Not p) = null (children p)
+      f p       = null (children p)
+
+-----------------------------------------------------------
+--- QuickCheck generator
+
+instance Arbitrary SLogic where
+   arbitrary = sized (\i -> sizedGen True varGen (i `min` 4))
+
+instance CoArbitrary SLogic where
+   coarbitrary = foldLogic
+      (var, bin 1, bin 2, bin 3, bin 4, un 5, con 6, con 7)
+    where
+      con       = variant :: Int -> Gen a -> Gen a
+      var       = un 0 . coarbitrary . map ord . fromShowString
+      un  n a   = con n . a
+      bin n a b = con n . a . b
+ src/Domain/Logic/Views.hs view
@@ -0,0 +1,101 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Logic.Views
+   ( (.<->.), (.->.), (.&&.), (.||.)
+   , simplify, pushNot, pushNotWith
+   , orView, andView
+   ) where
+
+import Domain.Algebra.SmartGroup
+import Domain.Logic.Formula
+import Ideas.Common.Id
+import Ideas.Common.View hiding (simplify)
+
+------------------------------------------------------------
+-- Smart constructors
+
+infixr 2 .<->.
+infixr 3 .->.
+
+(.<->.) :: Logic a -> Logic a -> Logic a
+T .<->. q = q
+F .<->. q = nott q
+p .<->. T = p
+p .<->. F = nott p
+p .<->. q = p :<->: q
+
+(.->.) :: Logic a -> Logic a -> Logic a
+T .->. q = q
+F .->. _ = T
+_ .->. T = T
+p .->. F = nott p
+p .->. q = p :->: q
+
+{- (.||.) :: Logic a -> Logic a -> Logic a
+T .||. _ = T
+F .||. q = q
+_ .||. T = T
+p .||. F = p
+p .||. q = p :||: q
+
+(.&&.) :: Logic a -> Logic a -> Logic a
+T .&&. q = q
+F .&&. _ = F
+p .&&. T = p
+_ .&&. F = F
+p .&&. q = p :&&: q -}
+
+nott :: Logic a -> Logic a
+nott (Not p) = p
+nott p       = Not p
+
+-------------------------------------------------
+-- Views and transformations
+
+simplify :: Logic a -> Logic a
+simplify = foldLogic (Var, (.->.), (.<->.), (.&&.), (.||.), nott, T, F)
+
+pushNotWith :: (a -> Logic a) -> Logic a -> Logic a
+pushNotWith f = foldLogic (Var, (.->.), (.<->.), (.&&.), (.||.), rec, T, F)
+ where
+   rec logic =
+      case logic of
+         Not p :<->: q -> p     .<->. q
+         p :<->: Not q -> p     .<->. q
+         p :<->: q     -> rec p .<->. q
+         p :->:  q     -> p     .&&.  rec q
+         p :||:  q     -> rec p .&&.  rec q
+         p :&&:  q     -> rec p .||.  rec q
+         Not p         -> p
+         T             -> F
+         F             -> T
+         Var a         -> f a
+
+pushNot :: Logic a -> Logic a
+pushNot = pushNotWith (nott . Var)
+
+orView :: View (Logic a) [a]
+orView = "logic.orView" @> makeView (($ []) . f) (foldr ((.||.) . Var) F)
+ where
+   f (p :||: q) = (>>= f p) .  f q
+   f (Var a)    = return . (a:)
+   f F          = return
+   f _          = const Nothing
+
+andView :: View (Logic a) [a]
+andView = "logic.andView" @> makeView (($ []) . f) (foldr ((.&&.) . Var) T)
+ where
+   f (p :&&: q) = (>>= f p) .  f q
+   f (Var a)    = return . (a:)
+   f T          = return
+   f _          = const Nothing
+ src/Domain/Math/Data/DecimalFraction.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.DecimalFraction
+   ( DecimalFraction(..), fromDouble, validDivisor, digits
+   ) where
+
+import Control.Monad
+import Data.Maybe
+import Data.Ratio
+import Domain.Math.Safe
+
+import Test.QuickCheck
+
+-- |Data type for decimal fractions
+newtype DecimalFraction = DF Rational -- Invariant: denominator is valid
+   deriving (Eq, Ord, Num, Real, Arbitrary)
+
+instance Show DecimalFraction where
+   show d@(DF r) = show x ++ "." ++ replicate extra '0' ++ show y
+    where
+      digs   = digits d
+      base   = 10^digs
+      n      = numerator (r * fromInteger base)
+      (x, y) = n `divMod` base
+      extra  = digs - length (show y)
+
+instance Fractional DecimalFraction where
+   a/b = fromMaybe (error "invalid divisor") (safeDiv a b)
+   fromRational r = fromInteger (numerator r) / fromInteger (denominator r)
+
+instance SafeDiv DecimalFraction where
+   safeDiv (DF a) (DF b) = do
+      guard (validDivisor (DF b))
+      fmap DF (a `safeDiv` b)
+
+instance SafePower DecimalFraction where
+   safePower x (DF r)
+      | denominator r /= 1 = Nothing
+      | y >= 0             = Just a
+      | otherwise          = safeDiv 1 a
+    where
+      y = numerator r
+      a = x Prelude.^ abs y
+   safeRoot x y = safeRecip y >>= safePower x
+
+-- | Approximation of a double, with a precision of 8 digits
+fromDouble :: Double -> DecimalFraction
+fromDouble d = DF (fromInteger base / 10^digs)
+ where
+   digs = 8 :: Int -- maximum number of digits
+   base = round (d * 10^digs) :: Integer
+
+-- |Tests whether it is safe to divide by this fraction: it is safe to divide
+-- if its numerator(!) is a product of two's and five's.
+validDivisor :: DecimalFraction -> Bool
+validDivisor (DF a) = validDenominator (abs (numerator a))
+
+-- |number of decimal digits
+digits :: DecimalFraction -> Int
+digits (DF r) = head $ filter p [0..]
+ where
+   p i = 10^i `mod` denominator r == 0
+
+-- local helper
+validDenominator :: Integer -> Bool
+validDenominator n
+   | n == 0         = False
+   | even n         = validDenominator (n `div` 2)
+   | n `mod` 5 == 0 = validDenominator (n `div` 5)
+   | otherwise      = n == 1
+ src/Domain/Math/Data/Interval.hs view
@@ -0,0 +1,311 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.Interval
+   ( -- * Data types
+     Interval, Endpoint(..)
+     -- * Interval constructors
+   , empty, point, unbounded, open, closed
+   , leftOpen, rightOpen, greaterThan, greaterThanOrEqualTo
+   , lessThan, lessThanOrEqualTo, true, false
+     -- * Interval combinators
+   , except, union, intersect, complement
+     -- * Inspecing an interval
+   , segments, isIn
+     -- * QuickChecks
+   , testMe
+   ) where
+
+import Control.Monad
+import Data.List (intercalate)
+import Data.Maybe
+import Domain.Algebra.Boolean
+import Domain.Algebra.BooleanLaws
+import Domain.Algebra.Law
+import Ideas.Utils.TestSuite
+import Test.QuickCheck
+
+--------------------------------------------------------------------
+-- Data declarations
+
+newtype Interval a = I [Segment a]
+   deriving Eq
+
+data Segment a = S (Endpoint a) (Endpoint a)
+   deriving Eq
+
+data Endpoint a = Excluding a | Including a | Unbounded
+   deriving (Eq,Show)
+
+instance Ord a => BoolValue (Interval a) where
+   fromBool b = if b then unbounded else empty
+   isTrue   = (==true)
+   isFalse  = (==false)
+
+instance Ord a => Boolean (Interval a) where
+   (<&&>)     = intersect
+   (<||>)     = union
+   complement = complementIntervals
+
+instance Show a => Show (Interval a) where
+   show (I xs) = "{ " ++ intercalate ", " (map show xs) ++ " }"
+
+instance Show a => Show (Segment a) where
+   show (S a b) = showLeft a ++ "," ++ showRight b
+
+instance Functor Endpoint where
+   fmap f (Excluding a) = Excluding (f a)
+   fmap f (Including a) = Including (f a)
+   fmap _ Unbounded     = Unbounded
+
+showLeft, showRight :: Show a => Endpoint a -> String
+showLeft  (Excluding a) = '(' : show a
+showLeft  (Including a) = '[' : show a
+showLeft  Unbounded     = "(-inf"
+showRight (Excluding a) = show a ++ ")"
+showRight (Including a) = show a ++ "]"
+showRight Unbounded     = "inf)"
+
+--------------------------------------------------------------------
+-- Interval constructors
+
+empty :: Interval a
+empty = I []
+
+point :: a -> Interval a
+point a = I [S (Including a) (Including a)]
+
+unbounded :: Ord a => Interval a
+unbounded = makeInterval Unbounded Unbounded
+
+open :: Ord a => a -> a -> Interval a
+open a b = makeInterval (Excluding a) (Excluding b)
+
+closed :: Ord a => a -> a -> Interval a
+closed a b = makeInterval (Including a) (Including b)
+
+leftOpen :: Ord a => a -> a -> Interval a
+leftOpen a b = makeInterval (Excluding a) (Including b)
+
+rightOpen :: Ord a => a -> a -> Interval a
+rightOpen a b = makeInterval (Including a) (Excluding b)
+
+greaterThan :: Ord a => a -> Interval a
+greaterThan a = makeInterval (Excluding a) Unbounded
+
+greaterThanOrEqualTo :: Ord a => a -> Interval a
+greaterThanOrEqualTo a = makeInterval (Including a) Unbounded
+
+lessThan :: Ord a => a -> Interval a
+lessThan a = makeInterval Unbounded (Excluding a)
+
+lessThanOrEqualTo :: Ord a => a -> Interval a
+lessThanOrEqualTo a = makeInterval Unbounded (Including a)
+
+-- local constructor
+makeInterval :: Ord a => Endpoint a -> Endpoint a -> Interval a
+makeInterval pl pr = maybe empty (I . return) (makeSegment pl pr)
+
+makeSegment :: Ord a => Endpoint a -> Endpoint a -> Maybe (Segment a)
+makeSegment pl pr =
+   case compare <$> getPoint pl <*> getPoint pr of
+      Just EQ
+         | isExcluding pl -> Nothing
+         | isExcluding pr -> Nothing
+      Just GT             -> Nothing
+      _ -> Just (S pl pr)
+
+isIncluding :: Endpoint a -> Bool
+isIncluding (Including _) = True
+isIncluding _             = False
+
+isExcluding :: Endpoint a -> Bool
+isExcluding (Excluding _) = True
+isExcluding _             = False
+
+--------------------------------------------------------------------
+-- Inspecting an interval
+
+segments :: Interval a -> [(Endpoint a, Endpoint a)]
+segments (I xs) = [ (a, b) | S a b <- xs ]
+
+--------------------------------------------------------------------
+-- Combining multiple intervals
+
+except :: Ord a => a -> Interval a
+except a = lessThan a <||> greaterThan a
+
+insert :: Ord a => Segment a -> Interval a -> Interval a
+insert ia (I xs) = I (rec ia xs)
+ where
+   rec iv [] = [iv]
+   rec iv@(S a _) (hd@(S b _):rest) =
+      case merge iv hd of
+         Just new -> rec new rest
+         Nothing
+            | minPointLeft b a == b -> hd:rec iv rest
+            | otherwise             -> iv:hd:rest
+
+union :: Ord a => Interval a -> Interval a -> Interval a
+union xs (I ys) = foldr insert xs ys
+
+intersect :: Ord a => Interval a -> Interval a -> Interval a
+intersect (I xs) (I ys) = I (f xs ys)
+ where
+   f (a@(S _ ar):as) (b@(S _ br):bs) =
+      let cond = maxPointRight ar br == ar
+          rest | cond      = f (a:as) bs
+               | otherwise = f as (b:bs)
+      in maybe id (:) (inBoth a b) rest
+   f _ _ = []
+
+complementIntervals :: Ord a => Interval a -> Interval a
+complementIntervals (I xs)
+   | null xs   = unbounded
+   | otherwise = I $ catMaybes $
+        left (head xs) : zipWith f xs (drop 1 xs) ++ [right (last xs)]
+ where
+   f (S _ a) (S b _) = S <$> g a <*> g b
+
+   g (Including a) = Just (Excluding a)
+   g (Excluding a) = Just (Including a)
+   g Unbounded     = Nothing
+
+   left  (S al _) = fmap (S Unbounded) (g al)
+   right (S _ ar) = fmap (flip S Unbounded) (g ar)
+
+isIn :: Ord a => a -> Interval a -> Bool
+isIn a (I xs) = any p xs
+ where
+   p (S x y) = f GT x && f LT y
+   f value b =
+      let g c = (c==EQ && isIncluding b) || c==value
+      in maybe True (g . compare a) (getPoint b)
+
+---------------------------------------------------------------------
+-- Local helper functions
+
+getPoint :: Endpoint a -> Maybe a
+getPoint (Including a) = Just a
+getPoint (Excluding a) = Just a
+getPoint Unbounded     = Nothing
+
+merge :: Ord a => Segment a -> Segment a -> Maybe (Segment a)
+merge ia@(S al ar) ib@(S bl br)
+   | minPointLeft al bl /= al = merge ib ia
+   | otherwise =
+        case compare <$> getPoint ar <*> getPoint bl of
+           Just LT -> Nothing
+           Just EQ | isExcluding ar && isExcluding bl -> Nothing
+           _ -> Just (S al (maxPointRight ar br))
+
+inBoth :: Ord a => Segment a -> Segment a -> Maybe (Segment a)
+inBoth (S al ar) (S bl br) =
+   makeSegment (maxPointLeft al bl) (minPointRight ar br)
+
+minPointLeft, minPointRight, maxPointLeft, maxPointRight
+   :: Ord a => Endpoint a -> Endpoint a -> Endpoint a
+minPointLeft  = compareEndpoint True  True
+minPointRight = compareEndpoint True  False
+maxPointLeft  = compareEndpoint False False
+maxPointRight = compareEndpoint False True
+
+compareEndpoint :: Ord a => Bool -> Bool -> Endpoint a -> Endpoint a -> Endpoint a
+compareEndpoint b1 b2 a b =
+   case compare <$> getPoint a <*> getPoint b of
+      Just LT                -> x
+      Just EQ | p a          -> x
+              | otherwise    -> y
+      Just GT                -> y
+      Nothing | b2           -> Unbounded
+              | x==Unbounded -> y
+              | otherwise    -> x
+ where
+   p = if b1==b2 then isIncluding else isExcluding
+   (x, y) = if b1 then (a, b) else (b, a)
+
+---------------------------------------------------------------------
+-- QuickCheck
+
+instance (Arbitrary a, Ord a) => Arbitrary (Endpoint a) where
+   arbitrary = frequency
+      [ (2, Excluding <$> arbitrary)
+      , (2, Including <$> arbitrary)
+      , (1, return Unbounded)
+      ]
+instance (CoArbitrary a, Ord a) => CoArbitrary (Endpoint a) where
+   coarbitrary (Excluding a) = variant (0 :: Int) . coarbitrary a
+   coarbitrary (Including a) = variant (1 :: Int) . coarbitrary a
+   coarbitrary Unbounded     = variant (2 :: Int)
+
+instance (Arbitrary a, Ord a) => Arbitrary (Interval a) where
+   arbitrary = do
+      n  <- choose (0, 100)
+      xs <- replicateM n (makeInterval <$> arbitrary <*> arbitrary)
+      return (ors xs)
+
+instance (CoArbitrary a, Ord a) => CoArbitrary (Segment a) where
+   coarbitrary (S a b) = coarbitrary a . coarbitrary b
+
+instance (CoArbitrary a, Ord a) => CoArbitrary (Interval a) where
+   coarbitrary (I xs) = coarbitrary xs
+
+testMe :: TestSuite
+testMe = suite "Intervals"
+
+   [ suite "Constructor functions"
+        [ useProperty "empty"     $ op0 empty     (const False)
+        , useProperty "unbounded" $ op0 unbounded (const True)
+
+        , useProperty "greater than"             $ op1 greaterThan (>)
+        , useProperty "greater than or equal to" $ op1 greaterThanOrEqualTo (>=)
+        , useProperty "less than"                $ op1 lessThan (<)
+        , useProperty "less than or equal to"    $ op1 lessThanOrEqualTo (<=)
+        , useProperty "point    "                $ op1 point (==)
+
+        , useProperty "open"       $ op2 open      (<)  (<)
+        , useProperty "closed"     $ op2 closed    (<=) (<=)
+        , useProperty "left open"  $ op2 leftOpen  (<)  (<=)
+        , useProperty "right open" $ op2 rightOpen (<=) (<)
+        ]
+
+   , suite "Combinators"
+        [ useProperty "except"     defExcept
+        , useProperty "union"      defUnion
+        , useProperty "intersect"  defIntersect
+        , useProperty "complement" defComplement
+        ]
+
+   , suite "Boolean algebra"
+        [ useProperty (show p) p
+        | p <- booleanLaws :: [Law (Interval Int)]
+        ]
+   ]
+
+defExcept :: Int -> Int -> Bool
+defExcept a b = isIn a (except b) == (a/=b)
+
+defUnion, defIntersect :: Int -> Interval Int -> Interval Int -> Bool
+defUnion     a b c = isIn a (b `union` c) == (isIn a b || isIn a c)
+defIntersect a b c = isIn a (b `intersect` c) == (isIn a b && isIn a c)
+
+defComplement :: Int -> Interval Int -> Bool
+defComplement a b = isIn a (complement b) == not (isIn a b)
+
+op0 :: Interval Int -> (Int -> Bool) -> Int -> Bool
+op0 g p a = isIn a g == p a
+
+op1 :: (Int -> Interval Int) -> (Int -> Int -> Bool) -> Int -> Int -> Bool
+op1 g op a b = isIn a (g b) == (a `op` b)
+
+op2 :: (Int -> Int -> Interval Int) -> (Int -> Int -> Bool) -> (Int -> Int -> Bool) -> Int -> Int -> Int -> Bool
+op2 g opl opr a b c = isIn a (g b c) == (b `opl` a && a `opr` c)
+ src/Domain/Math/Data/MixedFraction.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.MixedFraction
+   ( MixedFraction, wholeNumber, fractionPart, numerator, denominator
+   ) where
+
+import qualified Data.Ratio as R
+
+newtype MixedFraction = MF { unMF :: Rational }
+   deriving (Eq, Ord, Num, Fractional, Real, RealFrac)
+
+instance Show MixedFraction where
+   show mf
+      | b == 0    = sign ++ show a
+      | a == 0    = sign ++ show b ++ "/" ++ show c
+      | otherwise = sign ++ show a ++ "[" ++ show b ++ "/" ++ show c ++ "]"
+    where
+      (a, b, c) = (wholeNumber mf, numerator mf, denominator mf)
+      sign = if mf < 0 then "-" else ""
+
+-- | Always positive
+wholeNumber :: MixedFraction -> Integer
+wholeNumber = fst . properMF
+
+-- | Always positive
+fractionPart :: MixedFraction -> Rational
+fractionPart = snd . properMF
+
+-- | Always positive
+numerator :: MixedFraction -> Integer
+numerator = R.numerator . fractionPart
+
+-- | Always positive
+denominator :: MixedFraction -> Integer
+denominator = R.denominator . fractionPart
+
+-- local helper
+properMF :: MixedFraction -> (Integer, Rational)
+properMF = properFraction . abs . unMF
+ src/Domain/Math/Data/OrList.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.OrList
+   ( OrList, OrSet, true, false, (<>)
+   , isTrue, isFalse, fromBool, toOrList
+   , noDuplicates, catOrList
+   , oneDisjunct, orListView, orSetView
+   ) where
+
+import Data.Foldable (toList)
+import Data.List
+import Data.Semigroup (Semigroup)
+import Domain.Algebra.Boolean
+import Domain.Algebra.Group
+import Domain.Logic.Formula (Logic((:||:)))
+import Ideas.Common.Classes
+import Ideas.Common.Rewriting
+import Ideas.Common.View
+import Test.QuickCheck
+import qualified Data.Set as S
+import qualified Domain.Logic.Formula as Logic
+
+instance Functor OrList where
+   fmap f (OrList a) = OrList (fmap (map f) a)
+
+instance Foldable OrList where
+   foldMap f (OrList a) = maybe mempty (foldMap f) (fromWithZero a)
+
+instance Traversable OrList where
+   traverse f (OrList a) =
+      maybe (pure mzero) (fmap toOrList . traverse f) (fromWithZero a)
+
+------------------------------------------------------------
+-- OrList data type
+
+newtype OrList a = OrList (WithZero [a]) deriving
+   (Eq, Ord, Semigroup, Monoid, MonoidZero, CoMonoid, CoMonoidZero)
+
+instance BoolValue (OrList a) where
+   fromBool b = if b then mzero else mempty
+   isTrue  = isMonoidZero
+   isFalse = isEmpty
+
+instance Container OrList where
+   singleton = OrList . pure . singleton
+   getSingleton (OrList a) = fromWithZero a >>= getSingleton
+
+instance IsTerm a => IsTerm (OrList a) where
+   toTerm = toTerm . build orListView
+   fromTerm expr = fromTerm expr >>= matchM orListView
+
+instance Arbitrary a => Arbitrary (OrList a) where
+   arbitrary = do
+      n  <- choose (1, 3)
+      xs <- vector n
+      return (toOrList xs)
+
+instance Show a => Show (OrList a) where
+   show xs | isTrue  xs = "true"
+           | isFalse xs = "false"
+           | otherwise  = f xs
+    where
+      f = unwords . intersperse "or" . map show . toList
+
+------------------------------------------------------------
+-- Functions
+
+-- | Remove duplicates
+noDuplicates :: Eq a => OrList a -> OrList a
+noDuplicates (OrList a) = OrList (fmap nub a)
+
+oneDisjunct :: Monad m => (a -> m (OrList a)) -> OrList a -> m (OrList a)
+oneDisjunct f (OrList a) =
+   case fromWithZero a of
+      Just [x] -> f x
+      _ -> fail "oneDisjunct"
+
+------------------------------------------------------------
+-- OrSet data type
+
+newtype OrSet a = OrSet (WithZero (S.Set a)) deriving
+   (Eq, Ord, Semigroup, Monoid, MonoidZero, CoMonoid, CoMonoidZero)
+
+instance (Show a, Ord a) => Show (OrSet a) where
+   show = show . build orSetView
+
+instance Ord a => BoolValue (OrSet a) where
+   fromBool b = if b then mzero else mempty
+   isTrue  = isMonoidZero
+   isFalse = isEmpty
+
+instance Container OrSet where
+   singleton = OrSet . pure . singleton
+   getSingleton (OrSet a) = fromWithZero a >>= getSingleton
+
+------------------------------------------------------------
+-- View to the logic data type
+
+toOrList :: [a] -> OrList a
+toOrList = mconcat . map singleton
+
+orListView :: View (Logic a) (OrList a)
+orListView = makeView f g
+ where
+   f p  = case p of
+             Logic.Var a -> return (singleton a)
+             Logic.T     -> return true
+             Logic.F     -> return false
+             a :||: b    -> mappend <$> f a <*> f b
+             _           -> Nothing
+   g = fromOr . foldOrListWith (Or . Logic.Var)
+
+orSetView :: Ord a => View (OrList a) (OrSet a)
+orSetView = makeView (Just . f) g
+ where
+   f (OrList xs) = OrSet  (fmap S.fromList xs)
+   g (OrSet  xs) = OrList (fmap S.toList xs)
+
+foldOrList :: MonoidZero a => OrList a -> a
+foldOrList xs
+   | isTrue xs  = mzero
+   | isFalse xs = mempty
+   | otherwise  = foldr1 (<>) (toList xs)
+
+foldOrListWith :: MonoidZero b => (a -> b) -> OrList a -> b
+foldOrListWith f = foldOrList . fmap f
+
+{-
+foldOrListF :: (MonoidZero (f a), Container f) => OrList a -> f a
+foldOrListF = foldOrListWith to -}
+
+catOrList :: OrList (OrList a) -> OrList a
+catOrList = foldOrList
+ src/Domain/Math/Data/Polynomial.hs view
@@ -0,0 +1,295 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.Polynomial
+   ( Polynomial, toPolynomial, fromPolynomial, var, con, raise
+   , degree, lowestDegree, coefficient
+   , isRoot, positiveRoots, negativeRoots
+   , derivative, eval, polynomialGCD, factorize
+   , testPolynomials
+   ) where
+
+import Control.Monad
+import Data.Char
+import Data.Ratio
+import Domain.Math.Data.Primes
+import Domain.Math.Safe
+import Ideas.Common.Classes
+import Ideas.Utils.TestSuite
+import Test.QuickCheck
+import qualified Data.IntMap as IM
+import qualified Data.IntSet as IS
+
+------------------------------------------------------------------
+-- Data type:
+--   Invariant: all keys are non-negative, all values are non-zero
+--   (note that the second part of the invariant (zero values)
+--    can be violated using the functor instance)
+
+newtype Polynomial a = P { unsafeP :: IM.IntMap a }
+
+invariant :: (Eq a,Num a) => IM.IntMap a -> IM.IntMap a
+invariant = IM.filterWithKey (\n a -> n >= 0 && a /= 0)
+
+makeP :: (Eq a,Num a) => IM.IntMap a -> Polynomial a
+makeP = P . invariant
+
+unP :: (Eq a,Num a) => Polynomial a -> IM.IntMap a
+unP = invariant . unsafeP
+
+toPolynomial :: (Eq a,Num a) => [a] -> Polynomial a
+toPolynomial = makeP . IM.fromAscList . zip [0..] . reverse
+
+fromPolynomial :: (Eq a,Num a) => Polynomial a -> [a]
+fromPolynomial p = map (`coefficient` p) [d, d-1 .. 0]
+ where d = degree p
+
+-------------------------------------------------------------------
+-- Instances
+
+instance (Eq a,Num a) => Eq (Polynomial a) where
+   p1 == p2 = unP p1 == unP p2
+
+instance (Eq a,Show a,Num a) => Show (Polynomial a) where
+   show p
+      | p ==0     = "f(x) = 0"
+      | otherwise = "f(x) = " ++ fixString (concatMap f (reverse (IM.toList (unP p))))
+    where
+      f (n, a) = sign (one (show a ++ g n))
+      g n = concat $ [ "x" | n > 0 ] ++ [ '^' : show n | n > 1 ]
+      one ('1':xs@('x':_))     = xs
+      one ('-':'1':xs@('x':_)) = xs
+      one xs                   = xs
+      sign ('-':xs) = " - " ++ xs
+      sign xs       = " + " ++ xs
+      fixString xs =
+         case dropWhile isSpace xs of
+            '+':ys -> dropWhile isSpace ys
+            '-':ys -> '-':dropWhile isSpace ys
+            ys     -> ys
+
+instance (Eq a,Fractional a) => SafeDiv (Polynomial a) where
+   -- polynomial division, no remainder
+   safeDiv p1 p2
+      | p2==0     = Nothing
+      | degree p1 < degree p2 = Nothing
+      | b==0      = return a
+      | otherwise = Nothing
+    where
+      (a, b) = divModPoly p1 p2
+
+-- the Functor instance does not maintain the invariant
+instance Functor Polynomial where
+   fmap f = P . IM.map f . unsafeP
+
+instance Foldable Polynomial where
+   foldMap f = foldMap f . unsafeP
+
+instance Traversable Polynomial where
+   sequenceA = fmap P . sequenceIntMap . unsafeP
+
+instance (Eq a,Num a) => Num (Polynomial a) where
+   p1 + p2 = makeP $ IM.unionWith (+) (unP p1) (unP p2)
+   p1 * p2 = sum [ raise i (fmap (*a) p1) | (i, a) <- IM.toList (unP p2) ]
+
+   {- makeP $ foldr (uncurry op) IM.empty list
+    where
+      op   = IM.insertWith (+)
+      list = [ (i+j, a*b) | (a, i) <- terms p1, (b, j) <- terms p2 ] -}
+   negate      = fmap negate
+   fromInteger = makeP . IM.singleton 0 . fromInteger
+   -- not defined for polynomials
+   abs    = error "abs not defined for polynomials"
+   signum = error "signum not defined for polynomials"
+
+instance (Eq a,Arbitrary a, Num a) => Arbitrary (Polynomial a) where
+   arbitrary = do
+      d <- choose (0, 5)
+      let f n x = con x * var ^ n
+      sum . zipWith f [0::Int ..] <$> vector (d+1)
+
+-------------------------------------------------------------------
+-- Functions on polynomials
+
+-- a single variable (such as "x")
+var :: (Eq a,Num a) => Polynomial a
+var = makeP (IM.singleton 1 1)
+
+con :: (Eq a,Num a) => a -> Polynomial a
+con = makeP . IM.singleton 0
+
+-- | Raise all powers by a constant (discarding negative exponents)
+raise :: (Eq a,Num a) => Int -> Polynomial a -> Polynomial a
+raise i = makeP . IM.fromAscList . map (mapFirst (+i)) . IM.toList . unP
+
+------------------------------------------------
+
+degree :: (Eq a,Num a) => Polynomial a -> Int
+degree p
+   | IS.null is = 0
+   | otherwise  = IS.findMax is
+ where is = IM.keysSet (unP p)
+
+lowestDegree :: (Eq a,Num a) => Polynomial a -> Int
+lowestDegree p
+   | IS.null is = 0
+   | otherwise  = IS.findMin is
+ where is = IM.keysSet (unP p)
+
+coefficient :: (Eq a,Num a) => Int -> Polynomial a -> a
+coefficient n = IM.findWithDefault 0 n . unP
+
+isRoot :: (Eq a,Num a) => Polynomial a -> a -> Bool
+isRoot p a = eval p a == 0
+
+-- Returns the maximal number of positive roots (Descartes theorem)
+-- Multiple roots are counted separately
+positiveRoots :: (Eq a,Num a) => Polynomial a -> Int
+positiveRoots = signChanges . IM.elems . unP
+
+-- Returns the maximal number of negative roots (Descartes theorem)
+-- Multiple roots are counted separately
+negativeRoots :: (Eq a,Num a) => Polynomial a -> Int
+negativeRoots = signChanges . flipOdd . IM.elems . unP
+ where
+   flipOdd (x:y:zs) = x:negate y:flipOdd zs
+   flipOdd xs = xs
+
+signChanges :: (Eq a,Num a) => [a] -> Int
+signChanges = f . map signum
+ where
+   f (x:xs@(hd:_)) = if x==hd then f xs else 1 + f xs
+   f _ = 0
+
+------------------------------------------------
+
+derivative :: (Eq a,Num a) => Polynomial a -> Polynomial a
+derivative p = makeP $ IM.fromAscList
+   [ (n-1, fromIntegral n*a) | (n, a) <- IM.toList (unP p) ]
+
+eval :: (Eq a,Num a) => Polynomial a -> a -> a
+eval p x = sum [ a * x^n | (n, a) <- IM.toList (unP p) ]
+
+-- polynomial long division
+divModPoly :: (Eq a,Fractional a) => Polynomial a -> Polynomial a -> (Polynomial a, Polynomial a)
+divModPoly p1 p2 = mapBoth toPolynomial $
+   longDivision (fromPolynomial p2) (fromPolynomial p1)
+
+-- use polynomial long division to compute the greatest common factor
+-- of the polynomials
+polynomialGCD :: (Eq a,Fractional a) => Polynomial a -> Polynomial a -> Polynomial a
+polynomialGCD x y
+   | degree y > degree x = rec y x
+   | otherwise           = rec x y
+ where
+   rec a b
+      | b == 0    = a
+      | otherwise = rec b (snd (divModPoly a b))
+
+------------------------
+
+factorize :: Polynomial Rational -> [Polynomial Rational]
+factorize = map toPolynomial . make . fromPolynomial
+ where
+   make ps
+      | null ps      = [[]]
+      | head ps == 0 = make (tail ps)
+      | last ps == 0 = [1, 0] : make (init ps)
+      | otherwise    = rec ps $ possibleRoots (last is) (head is)
+    where
+      is = toInts ps
+
+   rec ps [] = [ ps | ps /= [1] ]
+   rec ps list@(r:rs)
+      | b == 0     = [1, -r] : rec qs list
+      | otherwise  = rec ps rs
+    where
+      (qs, b) = syntheticDivision r ps
+
+toInts :: [Rational] -> [Int]
+toInts ps = map (`div` a) is
+ where
+   is  = map f ps
+   d   = foldr1 lcm (map denominator ps)
+   f x = fromIntegral $ (numerator x * d) `div` denominator x
+   a   = foldr1 gcd is
+
+possibleRoots :: Int -> Int -> [Rational]
+possibleRoots a b = reverse (map negate xs) ++ xs
+ where
+   xs  = map f (factors (abs a)) -- or: factors (abs (a*b))
+   f x = toRational x / toRational b
+
+-- TODO: replace me by sequenceA
+-- This definition is for backwards compatibility. In older versions of IntMap,
+-- the instance for Traversable is lacking.
+sequenceIntMap :: Applicative m => IM.IntMap (m a) -> m (IM.IntMap a)
+sequenceIntMap m = IM.fromDistinctAscList <$> zip ks <$> sequenceA as
+ where
+   (ks, as) = unzip (IM.toList m)
+
+---------------------------------------------------------------
+-- Algorithms for synthetic and long division
+
+{- syntheticDivision a p: divide polynomial p by (x-a)
+   Example:
+
+      -3|  1   7    11  -3
+              -3   -12   3
+      -------------------- +
+           1   4    -1   0   (last number is remainder)
+   -}
+syntheticDivision :: Num a => a -> [a] -> ([a], a)
+syntheticDivision a xs = (init zs, last zs)
+ where
+   ys = 0 : map (*a) zs
+   zs = zipWith (+) xs ys
+
+{- longDivision p q: divide polynomial q by p
+   Example:
+
+      x+3|   1   10   24
+             1    3          (1x)
+             ----------- -
+                  7   24     (7x)
+                  7   21
+                  ------ -
+                       3    (remainder)
+   -}
+longDivision :: (Eq a,Fractional a) => [a] -> [a] -> ([a], [a])
+longDivision []     = error "longDivision by zero"
+longDivision (0:xs) = longDivision xs
+longDivision (x:xs) = recN
+ where
+   recN ys = rec (length ys - length xs) ys
+
+   rec n (y:ys) | n > 0 =
+      let d  = y/x
+          zs = zipWith (-) ys (map (*d) xs ++ repeat 0)
+      in mapFirst (d:) (rec (n-1) zs)
+   rec _ ys = ([], ys)
+
+---------------------------------------------------------------
+-- Properties
+
+testPolynomials :: TestSuite
+testPolynomials = suite "polynomial"
+   [ useProperty "factorization" $ do
+        i  <- choose (0, 5)
+        as <- replicateM i $ choose (-20, 20)
+        b  <- choose (1, 30)
+        c  <- choose (-10*b, 10*b)
+        let qs = [ var - con (fromInteger a) | a <- as ]
+            p  = con (fromInteger c/fromInteger b) * product qs
+            ps = factorize p
+        return (all ((<= 1) . degree) ps && product ps == p)
+   ]
+ src/Domain/Math/Data/PrimeFactors.hs view
@@ -0,0 +1,140 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.PrimeFactors
+   ( PrimeFactors
+   , splitPower, greatestPower, allPowers
+   ) where
+
+import Data.Maybe
+import Domain.Math.Data.Primes
+import qualified Data.IntMap as IM
+
+-------------------------------------------------------------
+-- Representation
+
+-- Invariants:
+-- * Keys in map are prime numbers only (exception: representation of 0)
+-- * Elements in map are positive (non-zero)
+-- * Zero is represented by [(0,1)] (since 0^1 equals 0)
+-- * The number can be negative, in which case we use the factors of
+--   its absolute value
+data PrimeFactors = PF Integer Factors
+
+type Factors = IM.IntMap Int
+
+-------------------------------------------------------------
+-- Conversion to and from factors
+
+toFactors :: Integer -> Factors
+toFactors a
+   | a == 0    = IM.singleton 0 1
+   | otherwise = rec $ primeFactors $ abs $ fromInteger a
+ where
+   rec []     = IM.empty
+   rec (x:xs) = IM.insert x (length ys + 1) (rec zs)
+    where
+      (ys, zs) = break (/= x) xs
+
+fromFactors :: Factors -> Integer
+fromFactors = product . map f . IM.toList
+ where f (a, i) = toInteger a ^ toInteger i
+
+-------------------------------------------------------------
+-- Type class instances
+
+instance Show PrimeFactors where
+   show (PF a m) = show a ++ " (factors = " ++ show (IM.toList m) ++ ")"
+
+instance Eq PrimeFactors where
+    PF a _ == PF b _ = a==b
+
+instance Ord PrimeFactors where
+   PF a _ `compare` PF b _ = a `compare` b
+
+instance Num PrimeFactors where
+   PF a m1 + PF b m2
+      | a==0         = PF b m2 -- prevent recomputing prime factors
+      | b==0         = PF a m1
+      | otherwise    = fromInteger (a+b)
+   PF a m1 * PF b m2
+      | a==0 || b==0 = 0
+      | otherwise    = PF (a*b) (IM.unionWith (+) m1 m2)
+   negate (PF a m)   = PF (negate a) m
+   abs    (PF a m)   = PF (abs a) m
+   signum (PF a _)   = fromInteger (signum a)
+   fromInteger n     = PF n (toFactors n)
+
+instance Enum PrimeFactors where
+   toEnum   = fromIntegral
+   fromEnum = fromIntegral . toInteger
+
+instance Real PrimeFactors where
+   toRational = toRational . toInteger
+
+instance Integral PrimeFactors where
+   toInteger (PF a _) = a
+   quotRem = quotRemPF
+
+-------------------------------------------------------------
+-- Utility functions
+
+-- brute force, ugly
+greatestPower :: Integer -> Maybe (Integer, Integer)
+greatestPower n = f 2 1
+  where
+    f b e | n == b ^ e = Just (b, e)
+          | b > n      = Nothing
+          | b ^ e > n  = f (b + 1) 1
+          | otherwise  = f b (e + 1)
+
+-- -- n == a^x with (a,x) == greatestPower n
+-- prop_greatestPower n = traceShow n $
+--    maybe True (\(a,x) -> fromIntegral a ^ fromIntegral x == n) $ greatestPower n
+
+allPowers :: Integer -> [(Integer, Integer)]
+allPowers n = do
+  (b, e) <- maybeToList $ greatestPower n
+  let f i = let (a, r) = e `divMod` i
+            in if a > 1 && r == 0 then Just (b^i, a) else Nothing
+  mapMaybe f [1..e]
+
+-- prop_allPowers n = traceShow n $
+--   and (map (\(a,x) -> fromIntegral a ^ fromIntegral x == n) (allPowers n))
+
+-- splitPower i a = (b,c)
+--  => b^i * c = a
+splitPower :: Int -> PrimeFactors -> (PrimeFactors, PrimeFactors)
+splitPower i (PF a m) = (PF b p1, PF c p2)
+ where
+   pairs = IM.map (`quotRem` i) m
+   p1    = IM.filter (>0) (fmap fst pairs)
+   p2    = IM.filter (>0) (fmap snd pairs)
+   b     = fromFactors p1
+   c     = a `div` (b^i)
+
+quotRemPF :: PrimeFactors -> PrimeFactors -> (PrimeFactors, PrimeFactors)
+quotRemPF (PF a m1) (PF b m2)
+   | b==0 = error "PrimeFactors: division by zero"
+   | a==0 = (0,0)
+   | otherwise = sign $
+        case (IM.null up, IM.null dn) of
+           (True,  True)  -> (1, 0)
+           (False, True)  -> (PF (fromFactors up) up, 0)
+           (True,  False) -> (0, PF a m1)
+           _              -> (fromInteger qn, fromInteger rn)
+ where
+   (up, dn) = IM.partition (>0) $ IM.filter (/=0) $ IM.unionWith (+) m1 (IM.map negate m2)
+   (qn, rn) = fromFactors up `quotRem` fromFactors (IM.map negate dn)
+   sign (q, r) = ( fromInteger (signum a*signum b) * q
+                 , fromInteger (signum a) * r
+                 )
+ src/Domain/Math/Data/Primes.hs view
@@ -0,0 +1,175 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.Primes
+   ( primes, isPrime, coprime, primeFactors, factors
+   , testPrimes
+   ) where
+
+import Control.Monad
+import Data.Function
+import Data.List
+import Ideas.Utils.TestSuite
+import Test.QuickCheck
+import qualified Data.Sequence as S
+
+------------------------------------------------------------
+-- | All prime numbers smaller than 1000
+
+-- | An infinite list of prime numbers
+primes :: [Int]
+primes = 1 : 2 : 3 : 5 : sieve (candidates 7)
+
+-- | All prime factors of a number
+primeFactors :: Int -> [Int]
+primeFactors n
+   | n > 0     = rec (tail primes1000) n
+   | otherwise = error "primeFactors: non-positive argument"
+ where
+   rec [] a
+      | a < 1000000 = [a] -- primes up to 1000 have been checked
+      | otherwise   = sort (rhos a)
+   rec list@(p:ps) a
+      | a == 1    = []
+      | m == 0    = p : rec list d
+      | otherwise = rec ps a
+    where
+      (d, m) = a `divMod` p
+
+   rhos a =
+      case pollardsRho a of
+         Just d  -> rhos d ++ rhos (a `div` d)
+         Nothing -> [a] -- probably a prime
+
+primes1000 :: [Int]
+primes1000 =
+   [1,2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97
+   ,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193
+   ,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307
+   ,311,313,317,331,337,347,349,353,359,367,373,379,383,389,397,401,409,419,421
+   ,431,433,439,443,449,457,461,463,467,479,487,491,499,503,509,521,523,541,547
+   ,557,563,569,571,577,587,593,599,601,607,613,617,619,631,641,643,647,653,659
+   ,661,673,677,683,691,701,709,719,727,733,739,743,751,757,761,769,773,787,797
+   ,809,811,821,823,827,829,839,853,857,859,863,877,881,883,887,907,911,919,929
+   ,937,941,947,953,967,971,977,983,991,997]
+
+-- Pollard's rho algorithm
+--    see http://en.wikipedia.org/wiki/Pollard_rho
+pollardsRho :: Int -> Maybe Int
+pollardsRho n = msum (map try [1..10]) -- ten attempts
+ where
+   try :: Int -> Maybe Int
+   try c = rec 2 2 1
+    where
+      rec :: Int -> Int -> Int -> Maybe Int
+      rec x y d
+         | d == 1    = rec nx ny (abs (nx-ny) `gcd` n)
+         | d == n    = Nothing
+         | otherwise = Just d -- a non-trivial factor of n
+       where
+         nx = f x
+         ny = f (f y)
+
+      f :: Int -> Int
+      f x = (x*x+c) `mod` n
+
+-- | Testing for primality
+isPrime :: Int -> Bool
+isPrime a =
+   case primeFactors a of
+      b:_ -> a == b
+      _   -> True
+
+-- | Two numbers are coprime if they do not share a prime factor
+coprime :: Int -> Int -> Bool
+coprime = rec `on` primeFactors
+ where
+   rec xs@(x:xr) ys@(y:yr) =
+      case compare x y of
+         LT -> rec xr ys
+         EQ -> False
+         GT -> rec xs yr
+   rec _ _ = True
+
+-- | All factors of a (positive) number
+factors :: Int -> [Int]
+factors = sort . rec . primeFactors . abs
+ where
+   rec []     = [1]
+   rec (x:xs) = [ a*b | b <- take n (powers x), a <- rec zs ]
+    where
+      (ys, zs) = break (/= x) xs
+      n = 2 + length ys
+
+-- helper functions
+sieveSlow :: [Int] -> [Int]
+sieveSlow []     = []
+sieveSlow (x:xs) = x : sieveSlow (filter (noDivisorOf x) xs)
+
+sieve :: [Int] -> [Int]
+sieve = rec S.empty
+ where
+   rec _ [] = []
+   rec q (x:xs) =
+      case S.viewl q of
+         (y:ys) S.:< qr | x == y ->
+            rec qr (ys `removeFrom` xs)
+         _ -> x : rec (q S.|> map (*x) (candidates x)) xs
+
+   -- remove a sorted list from another list
+   removeFrom xs@(x:xr) ys@(y:yr) =
+      case compare x y of
+         LT -> removeFrom xr ys
+         EQ -> removeFrom xr yr
+         GT -> y:removeFrom xs yr
+   removeFrom _ _ = []
+
+-- infinite list starting from n, without factors of 2, 3, or 5
+candidates :: Int -> [Int]
+candidates n = dropWhile (< n)
+   [ 30*k+i | k <- [n `div` 30..], i <- [1,7,11,13,17,19,23,29] ]
+
+divisorOf :: Int -> Int -> Bool
+divisorOf x y = y `mod` x == 0
+
+noDivisorOf :: Int -> Int -> Bool
+noDivisorOf x y = y `mod` x /= 0
+
+powers :: Int -> [Int]
+powers a = iterate (*a) 1
+
+-- a trusted implementation
+primesSlow :: [Int]
+primesSlow = 1 : 2 : sieveSlow [3, 5 ..]
+
+testPrimes :: TestSuite
+testPrimes = suite "primes"
+   [ assertTrue "first 1000 primes" (take 1000 primesSlow == take 1000 primes)
+   , assertTrue "isPrime" (all isPrime primes1000)
+   , useProperty "product of prime factors" $
+        forAll (choose (1, 1000000)) $ \n ->
+        product (primeFactors n) == n
+   , useProperty "primality of prime factors" $
+        forAll (choose (1, 1000000)) $ \n ->
+        all isPrime (primeFactors n)
+   , useProperty "factoring product of two primes" $
+        forAll (elements $ tail primes1000) $ \a ->
+        forAll (elements $ tail primes1000) $ \b ->
+        primeFactors (a*b) == sort [a, b]
+   , useProperty "factors" $
+        forAll (choose (1, 10000)) $ \n ->
+        all (`divisorOf` n) (factors n)
+   , useProperty "factors of product" $
+        forAll (choose (1, 1000)) $ \a ->
+        forAll (choose (1, 1000)) $ \b ->
+        all (`elem` factors (a*b)) [a, b]
+   ]
+ src/Domain/Math/Data/Relation.hs view
@@ -0,0 +1,278 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.Relation
+   ( -- * Type class
+     Relational(..)
+     -- * Relation data type
+   , Relation, relationType, RelationType(..), relationSymbols
+   , notRelation, eval
+     -- * Constructor functions
+   , makeType, (.==.), (./=.), (.<.), (.>.), (.<=.), (.>=.), (.~=.)
+     -- * Equation (or equality)
+   , Equations, Equation(..), equationView
+     -- * Inequality
+   , Inequality(..), inequalityView
+   ) where
+
+import Control.Monad
+import Data.Foldable (toList)
+import Data.Maybe
+import Ideas.Common.Rewriting
+import Ideas.Common.View
+import Ideas.Text.OpenMath.Dictionary.Relation1
+import Test.QuickCheck
+
+-----------------------------------------------------------------------------
+-- Type class for relations
+
+class Functor f => Relational f where
+   leftHandSide  :: f a -> a
+   rightHandSide :: f a -> a
+   flipSides     :: f a -> f a -- possibly also flips operator
+   constructor   :: f a -> b -> b -> f b
+   isSymmetric   :: f a -> Bool
+   -- default definitions
+   isSymmetric _ = False
+
+-----------------------------------------------------------------------------
+-- Relation data type
+
+data Relation a = R { lhs :: a, relationType :: RelationType, rhs :: a }
+   deriving (Eq, Ord)
+
+-- Corresponds exactly to the symbols in the relation1 OpenMath dictionary
+data RelationType = EqualTo | NotEqualTo | LessThan | GreaterThan
+                  | LessThanOrEqualTo | GreaterThanOrEqualTo | Approximately
+   deriving (Show, Eq, Ord, Enum)
+
+instance Show a => Show (Relation a) where
+   show r = unwords [show (lhs r), showRelType (relationType r), show (rhs r)]
+
+instance Functor Relation where
+   fmap f (R x rt y) = R (f x) rt (f y)
+
+instance Foldable Relation where
+   foldMap = foldMapRelation
+
+instance Traversable Relation where
+   sequenceA = sequenceRelation
+
+instance Relational Relation where
+   leftHandSide  = lhs
+   rightHandSide = rhs
+   flipSides (R x rt y) = R y (flipRelType rt) x
+   constructor (R _ rt _) = flip R rt
+   isSymmetric = (`elem` [EqualTo, NotEqualTo, Approximately]) . relationType
+
+instance IsTerm a => IsTerm (Relation a) where
+   toTerm p =
+      let op  = relationType p
+          sym = maybe (newSymbol (show op)) snd (lookup op relationSymbols)
+      in binary sym (toTerm (leftHandSide p)) (toTerm (rightHandSide p))
+   fromTerm term =
+      case getFunction term of
+         Just (s, [a, b]) ->
+            case [ rt | (rt, (_, t)) <- relationSymbols, s==t ] of
+               [rt] -> liftM2 (makeType rt) (fromTerm a) (fromTerm b)
+               _    -> fail "fromTerm: relation"
+         _ -> fail "fromTerm: relation"
+
+relationSymbols :: [(RelationType, (String, Symbol))]
+relationSymbols =
+   [ (EqualTo,              ("==", newSymbol eqSymbol))
+   , (NotEqualTo,           ("/=", newSymbol neqSymbol))
+   , (LessThan,             ("<",  newSymbol ltSymbol))
+   , (GreaterThan,          (">",  newSymbol gtSymbol))
+   , (LessThanOrEqualTo,    ("<=", newSymbol leqSymbol))
+   , (GreaterThanOrEqualTo, (">=", newSymbol geqSymbol))
+   , (Approximately,        ("~=", newSymbol approxSymbol))
+   ]
+
+notRelation :: Relation a -> Relation a
+notRelation r = r { relationType = relationType r ? table }
+ where
+   table = xs ++ map swap xs ++ [(Approximately, Approximately)]
+   swap (x, y) = (y, x)
+   xs = [ (EqualTo, NotEqualTo)
+        , (LessThan, GreaterThanOrEqualTo)
+        , (LessThanOrEqualTo, GreaterThan)
+        ]
+
+eval :: (Ord a, Num a) => RelationType -> a -> a -> Bool
+eval relType =
+   case relType of
+      EqualTo              -> (==)
+      NotEqualTo           -> (/=)
+      LessThan             -> (<)
+      GreaterThan          -> (>)
+      LessThanOrEqualTo    -> (<=)
+      GreaterThanOrEqualTo -> (>=)
+      Approximately        -> \a b -> 1000 * abs (a-b) < 1
+
+-- helpers
+showRelType :: RelationType -> String
+showRelType = fst . (? relationSymbols)
+
+flipRelType :: RelationType -> RelationType
+flipRelType relType = fromMaybe relType (lookup relType table)
+ where
+   table = pairs ++ map (\(a,b) -> (b,a)) pairs
+   pairs = [(LessThan, GreaterThan), (LessThanOrEqualTo, GreaterThanOrEqualTo)]
+
+(?) :: Eq a => a -> [(a, b)] -> b
+a ? xs = fromMaybe (error "Relation: Error in lookup") (lookup a xs)
+
+foldMapRelation :: (Relational f, Monoid m) => (a -> m) -> f a -> m
+foldMapRelation f p = f (leftHandSide p) `mappend` f (rightHandSide p)
+
+sequenceRelation :: (Relational g, Applicative f) => g (f a) -> f (g a)
+sequenceRelation p = constructor p <$> leftHandSide p <*> rightHandSide p
+
+-----------------------------------------------------------------------------
+-- QuickCheck generators
+
+instance Arbitrary a => Arbitrary (Relation a) where
+   arbitrary = liftM3 R arbitrary arbitrary arbitrary
+
+instance CoArbitrary a => CoArbitrary (Relation a) where
+   coarbitrary p = coarbitrary (relationType p) . coarbitrary (toList p)
+
+instance Arbitrary RelationType where
+   arbitrary = elements [EqualTo .. Approximately]
+
+instance CoArbitrary RelationType where
+   coarbitrary op = variant (fromEnum op)
+
+-----------------------------------------------------------------------------
+-- Constructor functions
+
+infix 1 .==., ./=., .<., .>., .<=., .>=., .~=.
+
+(.==.), (./=.), (.<.), (.>.), (.<=.), (.>=.), (.~=.) :: a -> a -> Relation a
+(.==.) = makeType EqualTo
+(./=.) = makeType NotEqualTo
+(.<.)  = makeType LessThan
+(.>.)  = makeType GreaterThan
+(.<=.) = makeType LessThanOrEqualTo
+(.>=.) = makeType GreaterThanOrEqualTo
+(.~=.) = makeType Approximately
+
+makeType :: RelationType -> a -> a -> Relation a
+makeType = flip R
+
+-----------------------------------------------------------------------------
+-- Equation data type (view on Relation)
+
+infix 1 :==:
+
+type Equations a = [Equation a]
+
+data Equation  a = a :==: a
+   deriving (Eq, Ord)
+
+instance Show a => Show (Equation a) where
+   show = show . build equationView
+
+instance Functor Equation where
+   fmap f (x :==: y) = f x :==: f y
+
+instance Foldable Equation where
+   foldMap = foldMapRelation
+
+instance Traversable Equation where
+   sequenceA = sequenceRelation
+
+instance Relational Equation where
+   leftHandSide  = leftHandSide  . build equationView
+   rightHandSide = rightHandSide . build equationView
+   flipSides (x :==: y) = y :==: x
+   constructor   = const (:==:)
+   isSymmetric   = const True
+
+instance Arbitrary a => Arbitrary (Equation a) where
+   arbitrary   = liftM2 (:==:) arbitrary arbitrary
+
+instance CoArbitrary a => CoArbitrary (Equation a) where
+   coarbitrary = coarbitrary . build equationView
+
+instance IsTerm a => IsTerm (Equation a) where
+   toTerm = toTerm . build equationView
+   fromTerm a = fromTerm a >>= matchM equationView
+
+equationView :: View (Relation a) (Equation a)
+equationView = makeView f g
+ where
+   f (R x op y)
+      | op == EqualTo = return (x :==: y)
+      | otherwise     = Nothing
+   g (x :==: y) = x .==. y
+
+-----------------------------------------------------------------------------
+-- Inequality (view on Relation)
+
+infix 1 :<:, :>:, :<=:, :>=:
+
+data Inequality a = a :<: a | a :>: a | a :<=: a | a :>=: a
+
+instance Show a => Show (Inequality a) where
+   show = show . build inequalityView
+
+instance Functor Inequality where
+   fmap f ineq =
+      let a = leftHandSide ineq
+          b = rightHandSide ineq
+      in constructor ineq (f a) (f b)
+
+instance Foldable Inequality where
+   foldMap = foldMapRelation
+
+instance Traversable Inequality where
+   sequenceA = sequenceRelation
+
+instance Relational Inequality where
+   leftHandSide  = leftHandSide  . build inequalityView
+   rightHandSide = rightHandSide . build inequalityView
+   flipSides = fromMaybe (error "inequality: flipSides") . matchM inequalityView
+             . flipSides . build inequalityView
+   constructor ineq =
+      let relType = relationType (build inequalityView ineq)
+      in fst (relType ? inequalityTable)
+
+instance Arbitrary a => Arbitrary (Inequality a) where
+   arbitrary = do
+      op <- elements $ map (fst . snd) inequalityTable
+      liftM2 op arbitrary arbitrary
+
+instance CoArbitrary a => CoArbitrary (Inequality a) where
+   coarbitrary = coarbitrary . build inequalityView
+
+instance IsTerm a => IsTerm (Inequality a) where
+   toTerm = toTerm . build inequalityView
+   fromTerm a = fromTerm a >>= matchM inequalityView
+
+inequalityView :: View (Relation a) (Inequality a)
+inequalityView = makeView f g
+ where
+   f (R x op y) = fmap (\pair -> fst pair x y) (lookup op inequalityTable)
+   g ineq =
+      case ineq of
+         x :<:  y -> x .<.  y
+         x :>:  y -> x .>.  y
+         x :<=: y -> x .<=. y
+         x :>=: y -> x .>=. y
+
+inequalityTable :: [(RelationType, (a -> a -> Inequality a, a -> a -> Relation a))]
+inequalityTable =
+   [ (LessThan, ((:<:), (.<.))), (LessThanOrEqualTo, ((:<=:), (.<=.)))
+   , (GreaterThan, ((:>:), (.>.))), (GreaterThanOrEqualTo, ((:>=:), (.>=.)))
+   ]
+ src/Domain/Math/Data/SquareRoot.hs view
@@ -0,0 +1,200 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.SquareRoot
+   ( SquareRoot
+   , imaginary, imaginaryUnit
+   , con, toList, scale, fromSquareRoot
+   , sqrt, sqrtRational, isqrt, eval
+   ) where
+
+import Control.Monad
+import Data.Ratio
+import Domain.Math.Safe
+import Prelude hiding (sqrt)
+import Test.QuickCheck hiding (scale)
+import qualified Data.Map as M
+import qualified Domain.Math.Data.PrimeFactors as P
+import qualified Prelude
+
+-------------------------------------------------------------
+-- Representation
+
+-- Sum of square roots (possibly imaginary) that are normalized
+--
+-- Invariants:
+-- * all keys are normalized (sqrt 8 -> 2*(sqrt 2))
+-- * all values are non-zero
+-- * We maintain the "imaginary" property since sqrt(-1)*sqrt(-1) may or may not
+--   be equal to sqrt(1)
+--
+-- Note on the Ord instance: comparison does not follow the value (semantic
+-- interpretation); it can be used though for sorting and storing in maps
+
+data SquareRoot a = S
+   { imaginary     :: Bool
+   , squareRootMap :: SqMap a
+   } deriving (Eq, Ord)
+
+type SqMap a = M.Map P.PrimeFactors a
+
+-------------------------------------------------------------
+-- Primitive operations on maps
+
+-- re-establish invariants
+makeMap :: (Eq a,Num a) => SqMap a -> SqMap a
+makeMap = M.filter (/=0) . M.foldWithKey f M.empty
+ where
+   f k a m
+      | a == 0    = m
+      | otherwise = M.unionWith (+) (fmap (*a) (sqrtPF k)) m
+
+plusSqMap :: (Eq a,Num a) => SqMap a -> SqMap a -> SqMap a
+plusSqMap m1 m2 = M.filter (/=0) (M.unionWith (+) m1 m2)
+
+minusSqMap :: (Eq a,Num a) => SqMap a -> SqMap a -> SqMap a
+minusSqMap m1 m2 = m1 `plusSqMap` negateSqMap m2
+
+negateSqMap :: Num a => SqMap a -> SqMap a
+negateSqMap = fmap negate
+
+timesSqMap :: (Eq a,Num a) => SqMap a -> SqMap a -> SqMap a
+timesSqMap m1 m2 =
+   case (M.toList m1, M.toList m2) of
+      ([], _) -> M.empty
+      (_, []) -> M.empty
+      ([(n, a)], _) | n==1 -> if a==0 then M.empty else fmap (*a) m2
+      (_, [(n, a)]) | n==1 -> if a==0 then M.empty else fmap (*a) m1
+      _ ->
+         let op n a = M.unionWith (+) (f n (fmap (a *) m1))
+             f i    = M.mapKeys (*i)
+         in makeMap (M.foldWithKey op M.empty m2)
+
+recipSqMap :: (Eq a,Fractional a) => SqMap a -> SqMap a
+recipSqMap m =
+   case M.toList m of
+      []       -> error "SquareRoot: division by zero"
+      [(n, x)] -> M.singleton n (recip (x * fromIntegral n))
+      _        -> (a .-. b) .*. recipSqMap (makeMap ((a .*. a) .-. (b .*. b)))
+ where
+   (ys, zs) = splitAt (length xs `div` 2) xs
+   (a, b)   = (M.fromList ys, M.fromList zs)
+   xs  = M.toList m
+   (.*.) = timesSqMap
+   (.-.) = minusSqMap
+
+sqrtPF :: Num a => P.PrimeFactors -> SqMap a
+sqrtPF n
+   | n == 0    = M.empty
+   | otherwise = M.singleton b (fromIntegral a)
+ where
+   (a, b) = P.splitPower 2 n
+
+-------------------------------------------------------------
+-- Type class instances
+
+instance (Show a,Eq a,Num a) => Show (SquareRoot a) where
+   show (S isNeg m) = g (map f (M.toList m)) ++ imPart
+    where
+      f (n, a) = ( signum a == -1
+                 , times (guard (abs a /= 1) >> Just (show (abs a)))
+                         (guard (n /= 1)     >> Just ("sqrt(" ++ show (toInteger n) ++ ")"))
+                 )
+      imPart = if isNeg then " (imaginary number)" else ""
+      g []         = "0"
+      g ((b,x):xs) = (if b then "-" else "") ++ x ++ concatMap h xs
+      h (b, x)     = (if b then " - " else " + ") ++ x
+
+      times (Just a) (Just b) = a ++ "*" ++ b
+      times (Just a) Nothing  = a
+      times Nothing  (Just b) = b
+      times Nothing  Nothing  = "1"
+
+-- the Functor instance does not maintain the invariant (non-zero)
+instance Functor SquareRoot where
+   fmap f (S b m) = S b (M.map f m)
+
+instance (Eq a,Num a) => Num (SquareRoot a) where
+   S b1 m1 + S b2 m2 = S (b1 || b2) (plusSqMap  m1 m2)
+   S b1 m1 - S b2 m2 = S (b1 || b2) (minusSqMap m1 m2)
+   S b1 m1 * S b2 m2 = S (b1 || b2) (timesSqMap m1 m2)
+   negate (S b m)    = S b (negateSqMap m)
+   fromInteger       = con . fromInteger
+
+   -- not defined for square roots
+   abs    = error "abs not defined for square roots"
+   signum = error "signum not defined for square roots"
+
+instance (Eq a,Fractional a) => SafeDiv (SquareRoot a) where
+   safeDiv x y
+      | y == 0    = Nothing
+      | otherwise = Just (x/y)
+
+instance (Eq a,Fractional a) => Fractional (SquareRoot a) where
+   recip (S b m) = S b (recipSqMap m)
+   fromRational  = con . fromRational
+
+instance (Eq a,Fractional a) => Arbitrary (SquareRoot a) where
+   arbitrary = sized $ \n -> do
+      let make r1 r2 = fromRational r1 * sqrtRational r2
+      i <- choose (0, 10)
+      xs <- vectorOf i (liftM2 make (rationalGen n) (rationalGen n))
+      return (sum xs)
+
+rationalGen :: Int -> Gen Rational
+rationalGen n = do -- a+(b/c)
+   c <- choose (0, n)
+   b <- choose (0, c)
+   a <- choose (0, n)
+   return $ fromIntegral a + if c==0 then 0
+                                     else fromIntegral b / fromIntegral c
+
+-------------------------------------------------------------
+-- Utility functions
+
+imaginaryUnit :: Num a => SquareRoot a
+imaginaryUnit = S True (M.singleton (-1) 1)
+
+toList :: SquareRoot a -> [(a, Integer)]
+toList = map (\(k, r) -> (r, toInteger k)) . M.toList . squareRootMap
+
+fromSquareRoot :: Num a => SquareRoot a -> Maybe a
+fromSquareRoot a =
+   case toList a of
+      [(b, n)] | n==1 -> Just b
+      []              -> Just 0
+      _ -> Nothing
+
+con :: (Eq a,Num a) => a -> SquareRoot a
+con a = S False (if a==0 then M.empty else M.singleton 1 a)
+
+sqrt :: Num a => Integer -> SquareRoot a
+sqrt n
+   | n < 0     = S True (M.mapKeys negate m)
+   | otherwise = S False m
+ where
+   m = sqrtPF (fromIntegral (abs n))
+
+scale :: (Eq a,Num a) => a -> SquareRoot a -> SquareRoot a
+scale a sr = if a==0 then 0 else fmap (*a) sr
+
+isqrt :: Integer -> Integer
+isqrt = (floor :: Double -> Integer) . Prelude.sqrt . fromInteger
+
+sqrtRational :: (Eq a,Fractional a) => Rational -> SquareRoot a
+sqrtRational r = scale (1/fromIntegral b) (sqrt (a*b))
+ where
+   (a, b) = (numerator r, denominator r)
+
+eval :: Floating a => SquareRoot a -> a
+eval (S _ m) = M.foldWithKey f 0 m
+ where f n a b = a * Prelude.sqrt (fromIntegral n) + b
+ src/Domain/Math/Data/WithBool.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Data.WithBool
+   ( WithBool, fromWithBool, join
+   ) where
+
+import Control.Monad
+import Data.Char (toLower)
+import Data.Traversable (foldMapDefault)
+import Domain.Logic.Formula
+import Ideas.Common.Classes
+import Ideas.Common.Rewriting hiding (trueSymbol, falseSymbol)
+import Test.QuickCheck
+
+-------------------------------------------------------------------
+-- Abstract data type and instances
+
+newtype WithBool a = WB { fromWithBool :: Either Bool a }
+   deriving (Eq, Ord, Functor, Arbitrary)
+
+instance Show a => Show (WithBool a) where
+   show = either (map toLower . show) show . fromWithBool
+
+instance BoolValue (WithBool a) where
+   fromBool = WB . Left
+   isTrue   = either id  (const False) . fromWithBool
+   isFalse  = either not (const False) . fromWithBool
+
+instance Container WithBool where
+   singleton    = WB . Right
+   getSingleton = either (const Nothing) Just . fromWithBool
+
+instance Applicative WithBool where
+   pure  = singleton
+   (<*>) = ap
+
+instance Monad WithBool where
+   return  = singleton
+   m >>= f = either fromBool f (fromWithBool m)
+
+instance Foldable WithBool where
+   foldMap = foldMapDefault
+
+instance Traversable WithBool where
+   traverse _ (WB (Left b))  = pure (WB (Left b))
+   traverse f (WB (Right a)) = (WB . Right) <$> f a
+
+instance IsTerm a => IsTerm (WithBool a) where
+   toTerm = either f toTerm . fromWithBool
+    where
+      f True  = symbol trueSymbol
+      f False = symbol falseSymbol
+   fromTerm term
+      | isSymbol trueSymbol  term = return true
+      | isSymbol falseSymbol term = return false
+      | otherwise                 = singleton <$> fromTerm term
+ src/Domain/Math/Expr.hs view
@@ -0,0 +1,19 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Expr (module Export) where
+
+import Domain.Math.Expr.Clipboard as Export
+import Domain.Math.Expr.Data as Export
+import Domain.Math.Expr.Parser as Export
+import Domain.Math.Expr.Symbols as Export
+import Domain.Math.Expr.Views as Export
+ src/Domain/Math/Expr/Clipboard.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE DeriveDataTypeable #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-- Support for a clipboard, on which expressions can be placed. The clipboard
+-- is part of the environment (terms that are placed in a context)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Expr.Clipboard
+   ( -- * Data type
+     Clipboard
+     -- * Interface
+   , addToClipboard, removeClipboard, lookupClipboard
+     -- * Generalized interface
+   , addToClipboardG, lookupClipboardG
+   ) where
+
+import Data.Maybe
+import Data.Typeable
+import Domain.Math.Data.Relation
+import Domain.Math.Expr.Data
+import Domain.Math.Expr.Parser
+import Ideas.Common.Library
+import qualified Data.Map as M
+
+---------------------------------------------------------------------
+-- Clipboard variable
+
+newtype Clipboard = C {unC :: M.Map String Expr}
+   deriving Typeable
+
+instance Show Clipboard where
+   show = show . toExpr
+
+instance Read Clipboard where
+   readsPrec _ txt = do
+      expr <- parseExprM txt
+      clip <- fromExpr expr
+      return (clip, "")
+
+instance IsTerm Clipboard where
+   toTerm =
+      let f (s, a) = Var s :==: a
+      in toTerm . map f . M.toList . unC
+   fromTerm =
+      let f (x :==: a) = (\k -> (k, a)) <$> getVariable x
+      in fmap (C . M.fromList) . mapM f . fromTerm
+
+instance Reference Clipboard
+
+clipboard :: Ref Clipboard
+clipboard = makeRef "clipboard"
+
+getClipboard :: Context a -> Clipboard
+getClipboard = fromMaybe (C M.empty) . (clipboard ?)
+
+changeClipboard :: (Clipboard -> Clipboard) -> Context a -> Context a
+changeClipboard f c = insertRef clipboard (f (getClipboard c)) c
+
+---------------------------------------------------------------------
+-- Interface to work with clipboard
+
+addToClipboard :: String -> Expr -> Context a -> Context a
+addToClipboard = addToClipboardG
+
+lookupClipboard :: String -> Context b -> Maybe Expr
+lookupClipboard = lookupClipboardG
+
+removeClipboard :: String -> Context a -> Context a
+removeClipboard s = changeClipboard (C . M.delete s . unC)
+
+---------------------------------------------------------------------
+-- Generalized interface to work with clipboard
+
+addToClipboardG :: IsTerm a => String -> a -> Context b -> Context b
+addToClipboardG s a = changeClipboard (C . M.insert s (toExpr a) . unC)
+
+lookupClipboardG :: IsTerm a => String -> Context b -> Maybe a
+lookupClipboardG s c = clipboard ? c >>= M.lookup s . unC >>= fromExpr
+ src/Domain/Math/Expr/Data.hs view
@@ -0,0 +1,293 @@+{-# LANGUAGE DeriveDataTypeable #-}
+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Expr.Data
+   ( Expr(..), toExpr, fromExpr, fromDouble
+   ) where
+
+import Control.Monad
+import Data.Char (isAlphaNum)
+import Data.List
+import Data.Maybe
+import Data.Ratio
+import Data.Typeable
+import Domain.Logic.Formula hiding (Var)
+import Domain.Math.Data.Relation (relationSymbols)
+import Domain.Math.Expr.Symbols
+import Ideas.Common.Rewriting hiding (trueSymbol, falseSymbol)
+import Ideas.Utils.Uniplate
+import Test.QuickCheck hiding (function)
+import qualified Domain.Algebra.Field as F
+
+-----------------------------------------------------------------------
+-- Expression data type
+
+data Expr = -- Num
+            Expr :+: Expr
+          | Expr :*: Expr
+          | Expr :-: Expr
+          | Negate Expr
+          | Nat Integer
+            -- Fractional
+          | Expr :/: Expr
+            -- Floating-point
+          | Sqrt Expr
+          | Number Double -- positive only
+            -- Symbolic
+          | Var String
+          | Sym Symbol [Expr]
+   deriving (Eq, Ord, Typeable)
+
+-----------------------------------------------------------------------
+-- Numeric instances (and symbolic)
+
+instance Num Expr where
+   (+) = (:+:)
+   (*) = (:*:)
+   (-) = (:-:)
+   fromInteger n
+      | n < 0     = negate $ Nat $ abs n
+      | otherwise = Nat n
+   negate = Negate
+   abs    = unary absSymbol
+   signum = unary signumSymbol
+
+instance Fractional Expr where
+   (/) = (:/:)
+   fromRational r
+      | denominator r == 1 =
+           fromIntegral (numerator r)
+      | numerator r < 0 =
+           Negate (fromIntegral (abs (numerator r)) :/: fromIntegral (denominator r))
+      | otherwise =
+           fromIntegral (numerator r) :/: fromIntegral (denominator r)
+
+instance Floating Expr where
+   pi      = symbol piSymbol
+   sqrt    = Sqrt
+   (**)    = binary powerSymbol
+   logBase = binary logSymbol
+   exp     = unary expSymbol
+   log     = unary logSymbol
+   sin     = unary sinSymbol
+   tan     = unary tanSymbol
+   cos     = unary cosSymbol
+   asin    = unary asinSymbol
+   atan    = unary atanSymbol
+   acos    = unary acosSymbol
+   sinh    = unary sinhSymbol
+   tanh    = unary tanhSymbol
+   cosh    = unary coshSymbol
+   asinh   = unary asinhSymbol
+   atanh   = unary atanhSymbol
+   acosh   = unary acoshSymbol
+
+instance WithFunctions Expr where
+   function s (a:as) -- make binary
+      | s == plusSymbol   = foldl (:+:) a as
+      | s == timesSymbol  = foldl (:*:) a as
+   function s [a, b]
+      | s == minusSymbol    = a :-: b
+      | s == divideSymbol   = a :/: b
+      | s == rationalSymbol = a :/: b
+      | s == mixedFractionBinarySymbol = a :+: b
+      | isRootSymbol s && b == Nat 2 || b == Number 2.0 = Sqrt a
+   function s [a]
+      | s == negateSymbol = Negate a
+   function s as = Sym s as
+
+   getFunction expr =
+      case expr of
+         a :+: b  -> return (plusSymbol,   [a, b])
+         a :*: b  -> return (timesSymbol,  [a, b])
+         a :-: b  -> return (minusSymbol,  [a, b])
+         Negate a -> return (negateSymbol, [a])
+         a :/: b  -> return (divideSymbol, [a, b])
+         Sqrt a   -> return (rootSymbol,   [a, Nat 2])
+         Sym s as -> return (s, as)
+         _ -> fail "Expr.getFunction"
+
+-- Special symbol in Math-Bridge/ActiveMath
+mixedFractionBinarySymbol :: Symbol
+mixedFractionBinarySymbol = newSymbol "elementary.mixed_fraction"
+
+instance WithVars Expr where
+   variable = Var
+   getVariable (Var s) = return s
+   getVariable _       = fail "Expr.getVariable"
+
+fromDouble :: Double -> Expr
+fromDouble d
+   | d < 0     = negate (Number (abs d))
+   | otherwise = Number d
+
+-----------------------------------------------------------------------
+-- Uniplate instance
+
+instance Uniplate Expr where
+   uniplate expr =
+      case getFunction expr of
+         Just (s, as) -> plate function |- s ||* as
+         _            -> plate expr
+
+-----------------------------------------------------------------------
+-- Arbitrary instance
+
+instance Arbitrary Expr where
+   arbitrary = fromInteger <$> arbitrary
+      -- before changing this instance, check that the
+      -- Gaussian elimination exercise still works (with checkExercise)
+      {-
+      let syms = [plusSymbol, timesSymbol, minusSymbol, negateSymbol, divSymbol]
+      in sized (symbolGenerator (const [natGenerator]) syms) -}
+
+-----------------------------------------------------------------------
+-- Pretty printer
+
+instance Show Expr where
+   show = showExpr operatorTable
+
+showExpr :: OperatorTable -> Expr -> String
+showExpr table = rec 0
+ where
+   rec :: Int -> Expr -> String
+   rec _ (Nat n)    = if n>=0 then show n else "(ERROR)" ++ show n
+   rec _ (Number d) = if d>=0 then show d else "(ERROR)" ++ show d
+   rec _ (Var s)
+      | all isAlphaNum s = s
+      | otherwise        = "\"" ++ s ++ "\""
+   rec i expr =
+      case getFunction expr of
+         Just (s1, [Sym s2 [Var x, a]]) | s1 == diffSymbol && s2 == lambdaSymbol ->
+            parIf (i>10000) $ "D(" ++ x ++ ") " ++ rec 10001 a
+         Just (s, [Nat a, Nat b, Nat c]) | s == mixedFractionSymbol ->
+            let ok  = all (>= 0) [a, b, c]
+                err = if ok then "" else "(ERROR)"
+            in err ++ show a ++ "[" ++ show b ++ "/" ++ show c ++ "]"
+         -- To do: remove special case for sqrt
+         Just (s, [a, b]) | isRootSymbol s && b == Nat 2 ->
+            parIf (i>10000) $ unwords ["sqrt", rec 10001 a]
+         Just (s, xs) | s == listSymbol ->
+            "[" ++ intercalate ", " (map (rec 0) xs) ++ "]"
+         Just (s, []) | s == trueSymbol  -> "T"
+                      | s == falseSymbol -> "F"
+         Just (s, as) ->
+            case (lookup s symbolTable, as) of
+               (Just (InfixLeft, n, op), [x, y]) ->
+                  parIf (i>n) $ rec n x ++ op ++ rec (n+1) y
+               (Just (InfixRight, n, op), [x, y]) ->
+                  parIf (i>n) $ rec (n+1) x ++ op ++ rec n y
+               (Just (InfixNon, n, op), [x, y]) ->
+                  parIf (i>n) $ rec (n+1) x ++ op ++ rec (n+1) y
+               (Just (PrefixNon, n, op), [x]) ->
+                  parIf (i>=n) $ op ++ rec (n+1) x
+               _ ->
+                  parIf (not (null as) && i>10000) $ unwords (showSymbol s : map (rec 10001) as)
+         Nothing ->
+            error "showExpr"
+
+   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 ]
+
+   parIf b = if b then par else id
+   par s   = "(" ++ s ++ ")"
+
+type OperatorTable = [(Associativity, [(Symbol, String)])]
+
+data Associativity = InfixLeft | InfixRight | PrefixNon
+                   | InfixNon
+   deriving (Show, Eq)
+
+operatorTable :: OperatorTable
+operatorTable =
+   -- relation operators
+     (InfixNon, [ (s, space op) | (_, (op, s)) <- relationSymbols]) :
+   -- logic operators
+   [ (InfixNon,   [(impliesSymbol, "->"), (equivalentSymbol, "<->")]) -- 1
+   , (InfixRight, [(orSymbol, "||")])                         -- 2
+   , (InfixRight, [(andSymbol, "&&")])                        -- 3
+   , (PrefixNon,  [(notSymbol, "~")])                         -- 4
+   -- arithmetic operators
+   , (InfixLeft,  [(plusSymbol, "+"), (minusSymbol, "-")])    -- 6
+   , (PrefixNon,  [(negateSymbol, "-")])                      -- 6+
+   , (InfixLeft,  [(timesSymbol, "*"), (divideSymbol, "/")])  -- 7
+   , (InfixRight, [(powerSymbol, "^")])                       -- 8
+   ]
+ where
+   space a = " " ++ a ++ " " -- for consistency with Show Equation
+
+instance F.SemiRing Expr where
+   (|+|) = (+)
+   zero  = 0
+   (|*|) = (*)
+   one   = 1
+
+instance F.Ring Expr where
+   plusInverse = negate
+   (|-|)       = (-)
+
+instance F.Field Expr where
+   timesInverse = recip
+   (|/|)        = (/)
+
+instance F.CoSemiRing Expr where
+   isPlus  = isPlus
+   isZero  = (==0)
+   isTimes = isTimes
+   isOne   = (==1)
+
+instance F.CoRing Expr where
+   isNegate = isNegate
+   isMinus  = isMinus
+
+instance F.CoField Expr where
+   isRecip _  = Nothing
+   isDivision = isDivide
+
+instance Different Expr where
+   different = (Nat 0, Nat 1)
+
+instance IsTerm Expr where
+   toTerm (Nat n)    = TNum n
+   toTerm (Number d) = TFloat d
+   toTerm (Var v)    = TVar v
+   toTerm expr =
+      case getFunction expr of
+         Just (s, xs)
+            | s == listSymbol -> TList (map toTerm xs)
+            | otherwise       -> function s (map toTerm xs)
+         Nothing      -> error "IsTerm Expr"
+
+   fromTerm (TNum n)   = return (fromInteger n)
+   fromTerm (TFloat d) = return (fromDouble d)
+   fromTerm (TVar v)   = return (Var v)
+   fromTerm (TList xs) = function listSymbol <$> mapM fromTerm xs
+   fromTerm t =
+      case getFunction t of
+         Just (s, xs) -> do
+            ys <- mapM fromTerm xs
+            return (function s ys)
+         _ -> fail "fromTerm"
+
+toExpr :: IsTerm a => a -> Expr
+toExpr = fromJust . fromTerm . toTerm
+
+fromExpr :: (MonadPlus m, IsTerm a) => Expr -> m a
+fromExpr = fromTerm . toTerm
+ src/Domain/Math/Expr/Parser.hs view
@@ -0,0 +1,218 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE FlexibleContexts #-}
+
+module Domain.Math.Expr.Parser
+   ( parseExpr, parseExprM, pExpr, pRelExpr
+   , parseEqExpr, parseBoolEqExpr, parseRelExpr
+   , parseOrsEqExpr, parseOrsRelExpr
+   , parseLogicRelExpr
+   , parseExprTuple
+   ) where
+
+import Control.Monad
+import Data.Monoid
+import Domain.Logic.Formula (Logic, catLogic)
+import Domain.Math.Data.OrList
+import Domain.Math.Data.Relation
+import Domain.Math.Data.WithBool
+import Domain.Math.Expr.Data
+import Domain.Math.Expr.Symbols
+import Ideas.Common.Library hiding (many, many1, try, ors, choice)
+import Ideas.Utils.Parsing
+import Prelude hiding ((^))
+import qualified Text.ParserCombinators.Parsec.Token as P
+
+pExpr :: Parser Expr
+pExpr = expr
+
+pRelExpr :: Parser (Relation Expr)
+pRelExpr = relation expr
+
+parseExpr :: String -> Either String Expr
+parseExpr = parseSimple expr
+
+parseExprM :: Monad m => String -> m Expr
+parseExprM = either fail return . parseExpr
+
+parseEqExpr :: String -> Either String (Equation Expr)
+parseEqExpr = parseSimple (equation expr)
+
+parseBoolEqExpr :: String -> Either String (WithBool (Equation Expr))
+parseBoolEqExpr = parseSimple (boolAtom (equation expr))
+
+parseRelExpr :: String -> Either String (Relation Expr)
+parseRelExpr = parseSimple (relation expr)
+
+parseOrsEqExpr :: String -> Either String (OrList (Equation Expr))
+parseOrsEqExpr = parseSimple (ors (equation expr))
+
+parseOrsRelExpr :: String -> Either String (OrList (Relation Expr))
+parseOrsRelExpr = parseSimple (ors (relation expr))
+
+parseLogicRelExpr :: String -> Either String (Logic (Relation Expr))
+parseLogicRelExpr = parseSimple (catLogic <$> logic (relationChain expr))
+
+parseExprTuple :: String -> Either String [Expr]
+parseExprTuple = parseSimple (tuple expr)
+
+ors :: Parser a -> Parser (OrList a)
+ors p = mconcat <$> sepBy1 (boolAtom p) (reserved "or")
+
+logic :: Parser a -> Parser (Logic a)
+logic p = buildExpressionParser table (boolAtom p)
+ where
+   table =
+      [ [Infix ((<&&>) <$ reservedOp "and") AssocRight]
+      , [Infix ((<||>) <$ reservedOp "or" ) AssocRight]
+      ]
+
+boolAtom :: (Container f, BoolValue (f a)) => Parser a -> Parser (f a)
+boolAtom p = choice
+   [ true      <$  reserved "true"
+   , false     <$  reserved "false"
+   , singleton <$> p
+   ]
+
+equation :: Parser a -> Parser (Equation a)
+equation p = (:==:) <$> p <* reservedOp "==" <*> p
+
+relation :: Parser a -> Parser (Relation a)
+relation p = p <**> relType <*> p
+
+relationChain :: Parser a -> Parser (Logic (Relation a))
+relationChain p = (\x -> ands . make x) <$> p <*> many1 ((,) <$> relType <*> p)
+ where
+   make _ []             = []
+   make a ((f, b): rest) = singleton (f a b) : make b rest
+
+relType :: Parser (a -> a -> Relation a)
+relType = choice (map make table)
+ where
+   make (s, f) = f <$ reservedOp s
+   table =
+      [ ("==", (.==.)), ("/=", (./=.))
+      , ("<=", (.<=.)), (">=", (.>=.))
+      , ("<", (.<.)), (">", (.>.)), ("~=", (.~=.))
+      ]
+
+tuple :: Parser a -> Parser [a]
+tuple p = parens (sepBy p comma)
+
+expr :: Parser Expr
+expr = buildExpressionParser exprTable term
+
+term :: Parser Expr
+term = choice
+   [ 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
+        return $ unary diffSymbol (binary lambdaSymbol (Var x) a)
+   , do a  <- qualId
+        as <- many atom
+        return (function (newSymbol a) as)
+   , atom
+   ]
+
+pmixed :: Parser Expr
+pmixed = do
+   a      <- natural
+   P.brackets lexer $ do
+      b <- natural
+      reservedOp "/"
+      c <- natural
+      return $ mixed a b c
+
+atom :: Parser Expr
+atom = choice
+   [ try pmixed
+   , do notFollowedBy (char '-')
+        either fromInteger fromDouble <$> naturalOrFloat
+   , variable <$> identifier
+   , pi <$ reserved "pi"
+   , parens expr
+   ]
+
+exprTable :: [[Operator Char () Expr]]
+exprTable =
+   [ -- precedence level 7
+     [ Infix ((^) <$ reservedOp "^") AssocRight
+     ]
+     -- precedence level 7
+   , [ Infix ((*) <$ reservedOp "*") AssocLeft
+     , Infix ((/) <$ reservedOp "/") AssocLeft
+     ]
+     -- precedence level 6+
+   , [ Prefix (negate <$ reservedOp "-")
+     ]
+     -- precedence level 6
+   , [ Infix ((+) <$ reservedOp "+") AssocLeft
+     , Infix ((-) <$ reservedOp "-") AssocLeft
+     ]
+   ]
+
+--------------------------------------------------------------------------
+-- Lexing
+
+lexer :: P.TokenParser a
+lexer = P.makeTokenParser $ emptyDef
+   { reservedNames   = [ "sqrt", "root", "log", "and", "or", "true", "false", "D"
+                       , "sin", "cos", "pi" ]
+   , reservedOpNames = ["==", "/=", "<=", ">=", "<", ">", "~=", "+", "-", "*", "^", "/"]
+   , opStart         =  oneOf ":!#$%&*+./<=>?@\\^|-~"
+   , opLetter        =  oneOf ":!#$%&*+./<=>?@\\^|-~"
+   }
+
+identifier :: Parser String
+identifier = P.identifier lexer
+
+qualId :: CharParser st Id
+qualId = try (P.lexeme lexer (do
+   xs <- idPart `sepBy1` char '.'
+   guard (length xs > 1)
+   return (mconcat (map newId xs)))
+ <?> "qualified identifier")
+ where
+   idPart   = (:) <$> letter <*> many idLetter
+   idLetter = alphaNum <|> oneOf "-_"
+
+natural :: Parser Integer
+natural = P.natural lexer
+
+reserved :: String -> Parser ()
+reserved = P.reserved lexer
+
+reservedOp :: String -> Parser ()
+reservedOp = P.reservedOp lexer
+
+comma :: Parser String
+comma = P.comma lexer
+
+parens :: Parser a -> Parser a
+parens = P.parens lexer
+
+-----------------------------------------------------------------------
+-- Argument descriptor (for parameterized rules)
+
+instance Read Expr where
+   readsPrec _ input =
+      case parseExpr input of
+         Left _  -> []
+         Right a -> [(a, "")]
+
+instance Reference Expr
+ src/Domain/Math/Expr/Symbols.hs view
@@ -0,0 +1,149 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-- Exports relevant OpenMath symbols
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Expr.Symbols
+   ( -- OpenMath dictionary symbols
+     plusSymbol, timesSymbol, minusSymbol, divideSymbol, rationalSymbol
+   , rootSymbol, gcdSymbol, lcmSymbol
+   , powerSymbol, negateSymbol, sinSymbol, cosSymbol, lnSymbol
+   , diffSymbol, piSymbol, lambdaSymbol, listSymbol
+   , absSymbol, signumSymbol, logSymbol, expSymbol, tanSymbol, asinSymbol
+   , atanSymbol, acosSymbol, sinhSymbol, tanhSymbol, coshSymbol, asinhSymbol
+   , atanhSymbol, acoshSymbol, bottomSymbol, fcompSymbol, mixedFractionSymbol
+     -- Matching
+   , isPlus, isTimes, isMinus, isDivide, isPower, isNegate, isRoot
+   , isPowerSymbol, isRootSymbol, isLogSymbol, isDivideSymbol
+   , isMixedFractionSymbol
+   , (^), root, mixed
+   ) where
+
+import Control.Monad
+import Ideas.Common.Rewriting
+import Prelude hiding ((^))
+import qualified Ideas.Text.OpenMath.Dictionary.Arith1 as OM
+import qualified Ideas.Text.OpenMath.Dictionary.Calculus1 as OM
+import qualified Ideas.Text.OpenMath.Dictionary.Fns1 as OM
+import qualified Ideas.Text.OpenMath.Dictionary.List1 as OM
+import qualified Ideas.Text.OpenMath.Dictionary.Nums1 as OM
+import qualified Ideas.Text.OpenMath.Dictionary.Transc1 as OM
+
+-------------------------------------------------------------
+-- Arith1 dictionary
+
+plusSymbol, timesSymbol, minusSymbol, divideSymbol, rootSymbol,
+   powerSymbol, negateSymbol, absSymbol, gcdSymbol, lcmSymbol :: Symbol
+
+plusSymbol     = newSymbol OM.plusSymbol
+timesSymbol    = newSymbol OM.timesSymbol
+minusSymbol    = newSymbol OM.minusSymbol
+divideSymbol   = newSymbol OM.divideSymbol
+rootSymbol     = newSymbol OM.rootSymbol
+powerSymbol    = newSymbol OM.powerSymbol
+negateSymbol   = newSymbol OM.unaryMinusSymbol
+absSymbol      = newSymbol OM.absSymbol
+gcdSymbol      = newSymbol OM.gcdSymbol
+lcmSymbol      = newSymbol OM.lcmSymbol
+
+-------------------------------------------------------------
+-- Transc1 dictionary
+
+logSymbol, sinSymbol, cosSymbol, lnSymbol, expSymbol, tanSymbol,
+   sinhSymbol, tanhSymbol, coshSymbol :: Symbol
+
+logSymbol  = newSymbol OM.logSymbol
+sinSymbol  = newSymbol OM.sinSymbol
+cosSymbol  = newSymbol OM.cosSymbol
+lnSymbol   = newSymbol OM.lnSymbol
+expSymbol  = newSymbol OM.expSymbol
+tanSymbol  = newSymbol OM.tanSymbol
+sinhSymbol = newSymbol OM.sinhSymbol
+tanhSymbol = newSymbol OM.tanhSymbol
+coshSymbol = newSymbol OM.coshSymbol
+
+-------------------------------------------------------------
+-- Other dictionaries
+
+diffSymbol, lambdaSymbol, listSymbol, piSymbol, rationalSymbol :: Symbol
+
+diffSymbol     = newSymbol OM.diffSymbol
+lambdaSymbol   = newSymbol OM.lambdaSymbol
+listSymbol     = newSymbol OM.listSymbol
+piSymbol       = newSymbol OM.piSymbol
+rationalSymbol = newSymbol OM.rationalSymbol
+
+-------------------------------------------------------------
+-- Extra math symbols
+
+signumSymbol, asinSymbol, atanSymbol, acosSymbol, asinhSymbol, atanhSymbol,
+   acoshSymbol, bottomSymbol, fcompSymbol, mixedFractionSymbol :: Symbol
+
+signumSymbol = newSymbol "signum"
+asinSymbol   = newSymbol "asin"
+atanSymbol   = newSymbol "atan"
+acosSymbol   = newSymbol "acos"
+asinhSymbol  = newSymbol "asinh"
+atanhSymbol  = newSymbol "atanh"
+acoshSymbol  = newSymbol "acosh"
+bottomSymbol = newSymbol "error"
+fcompSymbol  = newSymbol "compose"
+
+-- support for mixed fractions
+mixedFractionSymbol = newSymbol ("extra", "mixedfraction")
+
+-------------------------------------------------------------
+-- Some match functions
+
+isPlus, isTimes, isMinus, isDivide, isPower, isRoot ::
+   (WithFunctions a, MonadPlus m) => a -> m (a, a)
+isNegate :: (WithFunctions a, MonadPlus m) => a -> m a
+
+isPlus   = isAssoBinary plusSymbol
+isTimes  = isAssoBinary timesSymbol
+isMinus  = isBinary     minusSymbol
+isDivide = isBinary     divideSymbol
+isNegate = isUnary      negateSymbol
+isPower  = isBinary     powerSymbol
+isRoot   = isBinary     rootSymbol
+
+isPowerSymbol, isRootSymbol, isLogSymbol, isDivideSymbol,
+   isMixedFractionSymbol :: Symbol -> Bool
+
+isPowerSymbol  = (== powerSymbol)
+isRootSymbol   = (== rootSymbol)
+isLogSymbol    = (== logSymbol)
+isDivideSymbol = (== divideSymbol)
+
+isMixedFractionSymbol = (== mixedFractionSymbol)
+
+infixr 8 ^
+
+(^) :: WithFunctions a => a -> a -> a
+(^) = binary powerSymbol
+
+root :: WithFunctions a => a -> a -> a
+root = binary rootSymbol
+
+mixed :: (Num a, WithFunctions a) => Integer -> Integer -> Integer -> a
+mixed a b c = function mixedFractionSymbol $ map fromInteger [a, b, c]
+
+-------------------------------------------------------------
+-- Helper
+
+-- left-associative
+isAssoBinary :: (WithFunctions a, Monad m) => Symbol -> a -> m (a, a)
+isAssoBinary s a =
+   case isFunction s a of
+      Just [x, y] -> return (x, y)
+      Just (x:xs) | length xs > 1 -> return (x, function s xs)
+      _ -> fail "isAssoBinary"
+ src/Domain/Math/Expr/Views.hs view
@@ -0,0 +1,153 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Expr.Views
+   ( module Domain.Math.Expr.Views
+   , (.+.), (.-.), neg, (.*.), (./.)
+   ) where
+
+import Domain.Algebra.Group
+import Domain.Algebra.SmartGroup
+import Domain.Math.Expr.Data
+import Domain.Math.Expr.Symbols
+import Ideas.Common.Library hiding ((.*.), (./.))
+import Ideas.Utils.Uniplate
+import Prelude hiding ((^))
+import qualified Data.Set as S
+
+------------------------------------------------------------
+-- Smart constructors
+
+infixr 8 .^.
+
+(.^.) :: Expr -> Expr -> Expr
+Nat 0 .^. _ = Nat 0
+Nat 1 .^. _ = Nat 1
+_ .^. Nat 0 = Nat 1
+a .^. Nat 1 = a
+a .^. b     = a ^ b
+
+------------------------------------------------------------
+-- Views of binary constructors
+
+plusView :: View Expr (Expr, Expr)
+plusView = makeView matchPlus (uncurry (.+.))
+ where
+   matchPlus (a :+: b)  = Just (a, b)
+   matchPlus (a :-: b)  = Just (a, neg b)
+   matchPlus (Negate a) = do (x, y) <- matchPlus a
+                             Just (neg x, neg y)
+   matchPlus _          = Nothing
+
+timesView :: View Expr (Expr, Expr)
+timesView = makeView matchTimes (uncurry (.*.))
+ where
+   matchTimes (a :*: b)  = Just (a, b)
+   matchTimes (Negate a) = do (x, y) <- matchTimes a
+                              Just (neg x, y)
+   matchTimes _          = Nothing
+
+divView :: View Expr (Expr, Expr)
+divView = makeView matchDiv (uncurry (./.))
+ where
+   matchDiv (a :/: b)  = Just (a, b)
+   matchDiv (Negate a) = do (x, y) <- matchDiv a
+                            Just (neg x, y)
+   matchDiv _          = Nothing
+
+-------------------------------------------------------------
+-- Sums and products
+
+sumView :: Isomorphism Expr [Expr]
+sumView = describe "View an expression as the sum of a list of elements, \
+   \taking into account associativity of plus, its unit element zero, and \
+   \inverse (both unary negation, and binary subtraction)." $
+   "math.sum" @> sumEP
+ where
+   sumEP = (($ []) . f False) <-> foldl (.+.) 0
+
+   f n (a :+: b)  = f n a . f n b
+   f n (a :-: b)  = f n a . f (not n) b
+   f n (Negate a) = f (not n) a
+   f _ (Nat 0)    = id
+   f n e          = if n then (neg e:) else (e:)
+
+-- no distribution
+simpleSumView :: Isomorphism Expr [Expr]
+simpleSumView = sumEP
+ where
+   sumEP = f <-> foldl (.+) 0
+
+   f (a :+: b)           = f a <> f b
+   f (a :-: b)           = f a <> f (-b)
+   f (Nat 0)             = mempty
+   f (Negate (Nat 0))    = mempty
+   f (Negate (Negate a)) = f a
+   f a                   = return a
+
+   Nat 0 .+ b = b
+   a .+ Nat 0 = a
+   a .+ Negate b  = a :-: b
+   a .+ b = a :+: b
+
+productView :: Isomorphism Expr (Bool, [Expr])
+productView = "math.product" @> productEP
+ where
+   productEP = (second ($ []) . f False) <-> g
+
+   f r (a :*: b)  = f r a .&. f r b
+   f r (a :/: b)  = case a of -- two special cases (for efficiency)
+                       Nat 1          -> f (not r) b
+                       Negate (Nat 1) -> first not (f (not r) b)
+                       _              -> f r a .&. f (not r) b
+   f r (Negate a) = first not (f r a)
+   f r e          = (False, if r then (recip e:) else (e:))
+
+   (n1, g1) .&. (n2, g2) = (n1 /= n2, g1 . g2)
+
+   g (b, xs) = (if b then neg else id) (foldl (.*.) 1 xs)
+
+simpleProductView :: Isomorphism Expr (Bool, [Expr])
+simpleProductView = "math.product.simple" @> simpleProductEP
+ where
+   simpleProductEP = (second ($ []) . f) <-> g
+
+   f (a :*: b)  = f a .&. f b
+   f (Nat 1)    = (False, id)
+   f (Negate a) = first not (f a)
+   f e          = (False, (e:))
+
+   (n1, g1) .&. (n2, g2) = (n1 /= n2, g1 . g2)
+
+   g (b, xs) = (if b then myNeg else id) (foldl (.*) 1 xs)
+
+   Nat 1 .* a = a
+   a .* Nat 1 = a
+   Nat 0 .* a | ok a = 0
+   a .* Nat 0 | ok a = 0
+   Negate a .* b = myNeg (a .* b)
+   a .* Negate b = myNeg (a .* b)
+   a .* b = a :*: b
+
+   myNeg (Negate a) = a
+   myNeg a = Negate a
+
+   ok (a :/: b) = b /= 0 && ok a && ok b -- to do: evaluate b before b/=0
+   ok a = all ok (children a)
+
+-- helper to determine the name of the variable (move to a different module?)
+selectVar :: Expr -> Maybe String
+selectVar = f  . S.toList . varSet
+ where
+   f []  = Just "x" -- exceptional case (e.g., for constants)
+   f [a] = Just a
+   f _   = Nothing
+ src/Domain/Math/Numeric/Views.hs view
@@ -0,0 +1,253 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Numeric.Views
+   ( -- * Natural numbers
+     naturalView, naturalNF
+     -- * Integers
+   , integerView, integerNF
+     -- * Decimal fractions
+   , decimalFractionView
+     -- * Rational numbers
+   , rationalView, rationalNF
+   , rationalRelaxedForm, fractionForm, rationalApproxView
+     -- * Mixed fractions
+   , mixedFractionView, mixedFractionNF
+     -- * Double
+   , doubleView, doubleNF
+   ) where
+
+import Control.Monad
+import Data.Ratio
+import Domain.Math.Expr hiding ((^))
+import Domain.Math.Safe
+import Ideas.Common.Id
+import Ideas.Common.Rewriting (function)
+import Ideas.Common.View
+import Ideas.Utils.Uniplate (descend)
+import qualified Domain.Math.Data.DecimalFraction as DF
+import qualified Domain.Math.Data.MixedFraction as MF
+
+-------------------------------------------------------------------
+-- Natural numbers
+
+-- |Non-negative numbers only, also for intermediate results
+naturalView :: View Expr Integer
+naturalView = "num.natural" @> makeView rec (fromInteger . abs)
+ where
+   rec :: Expr -> Maybe Integer
+   rec expr = do
+      x <- matchInteger rec expr
+      guard (x >= 0)
+      return x
+
+naturalNF :: View Expr Integer
+naturalNF = "num.natural.nf" @> makeView f (build naturalView)
+ where
+   f (Nat n) = Just n
+   f _       = Nothing
+
+-------------------------------------------------------------------
+-- Integers
+
+integerView :: View Expr Integer
+integerView = "num.integer" @> makeView (fix matchInteger) fromIntegral
+
+-- N or -N (where n is a natural number)
+integerNF :: View Expr Integer
+integerNF = "num.integer.nf" @> makeView (optionNegate f) fromInteger
+ where
+   f (Nat n) = Just n
+   f _       = Nothing
+
+matchInteger :: (Expr -> Maybe Integer) -> Expr -> Maybe Integer
+matchInteger f expr =
+   case expr of
+      a :/: b -> join (safeDiv <$> f a <*> f b)
+      Sqrt a  -> f a >>= safeSqrt
+      Sym s [a, b]
+         | isPowerSymbol s -> join (safePower <$> f a <*> f b)
+         | isRootSymbol  s -> join (safeRoot  <$> f a <*> f b)
+      _ -> matchNum f expr
+
+matchNum :: Num a => (Expr -> Maybe a) -> Expr -> Maybe a
+matchNum f expr =
+   case expr of
+      Nat n    -> return (fromInteger n)
+      a :+: b  -> (+) <$> f a <*> f b
+      a :-: b  -> (-) <$> f a <*> f b
+      Negate a -> negate <$> f a
+      a :*: b  -> (*) <$> f a <*> f b
+      _        -> Nothing
+
+-------------------------------------------------------------------
+-- Decimal fractions
+
+decimalFractionView :: View Expr DF.DecimalFraction
+decimalFractionView = "num.decimal" @> makeView (fix matchDecimal) f
+ where
+   f = fromDouble . fromRational . toRational
+
+matchDecimal :: (Expr -> Maybe DF.DecimalFraction) -> Expr -> Maybe DF.DecimalFraction
+matchDecimal f expr =
+   case expr of
+      Number d -> Just (DF.fromDouble d)
+      a :/: b  -> join (safeDiv <$> f a <*> f b)
+      Sym s [a, b]
+         | isPowerSymbol s -> join (safePower <$> f a <*> f b)
+      Sym s [a, b, c]
+         | isMixedFractionSymbol s -> f (a+b/c)
+      _ -> matchNum f expr
+
+-------------------------------------------------------------------
+-- Rational numbers
+
+-- |like  the original defintion, except that this view
+-- now also converts floating point numbers (using an exact approximation)
+rationalView :: View Expr Rational
+rationalView = describe "Interpret an expression as a (normalized) rational \
+   \number, performing computations such as addition and multiplication if \
+   \necessary." $
+   "number.rational" @> makeView f fromRational
+ where
+   f a = matchExact a >>= either (const Nothing) Just
+
+matchRational :: (Expr -> Maybe Rational) -> Expr -> Maybe Rational
+matchRational f expr =
+   case expr of
+      Number d -> return $ fromRational $ toRational $ DF.fromDouble d
+      a :/: b  -> join (safeDiv <$> f a <*> f b)
+      Sqrt a   -> f a >>= safeSqrt
+      Sym s [a, b]
+         | isPowerSymbol s -> join (safePower <$> f a <*> f b)
+         | isRootSymbol  s -> join (safeRoot  <$> f a <*> f b)
+      Sym s [a, b, c]
+         | isMixedFractionSymbol s -> f (a+b/c)
+      _ -> matchNum f expr
+
+matchExact :: Expr -> Maybe (Either Double Rational)
+matchExact expr =
+   fmap Left (match doubleNF expr) `mplus`
+   fmap Right (fix matchRational expr)
+
+-- first convert (approximate!) all numbers to their decimal representation
+rationalApproxView :: View Expr Rational
+rationalApproxView = makeView (match rationalView . f) fromRational
+ where
+   f (Number d) = fromRational $ toRational $ DF.fromDouble d
+   f expr       = descend f expr
+
+-- 5, -(2/5), (-2)/5, but not 2/(-5), 6/8, or -((-2)/5)
+rationalNF :: View Expr Rational
+rationalNF = "num.rational.nf" @> makeView f fromRational
+ where
+   f (Nat a :/: Nat b) = simpleRational a b
+   f (Negate (Nat a :/: Nat b)) = fmap negate (simpleRational a b)
+   f (Negate (Nat a) :/: Nat b) = fmap negate (simpleRational a b)
+   f a = fmap fromInteger (match integerNF a)
+
+simpleRational :: Integer -> Integer -> Maybe Rational
+simpleRational a b = do
+   guard (a > 0 && b > 1 && gcd a b == 1)
+   return (fromInteger a / fromInteger b)
+
+fractionForm :: View Expr (Integer, Integer)
+fractionForm = "num.fraction-form" @> makeView f g
+ where
+   f = match (divView >>> integerNF *** integerNF)
+   g (a, b) = fromInteger a ./. fromInteger b
+
+rationalRelaxedForm :: View Expr Rational
+rationalRelaxedForm = "num.rational-relaxed" @> makeView (optionNegate f) fromRational
+ where
+   f (e1 :/: e2) = do
+      a <- match integerNF e1
+      b <- match integerNF e2
+      safeDiv (fromInteger a) (fromInteger b)
+   f (Nat n) = Just (fromInteger n)
+   f _       = Nothing
+
+-------------------------------------------------------------------
+-- Mixed fractions
+
+mixedFractionView :: View Expr MF.MixedFraction
+mixedFractionView = "num.mixed-fraction" @> makeView f (sign g)
+ where
+   f = fmap fromRational . fix matchRational
+
+   sign k a | a < 0     = negate (k (abs a))
+            | otherwise = k a
+
+   g a
+      | frac  == 0 = fromInteger  whole
+      | whole == 0 = fromRational frac
+      | otherwise  = function mixedFractionSymbol $ map fromInteger parts
+    where
+      whole = MF.wholeNumber a
+      frac  = MF.fractionPart a
+      parts = [whole, numerator frac, denominator frac]
+
+mixedFractionNF :: View Expr MF.MixedFraction
+mixedFractionNF = describe "A normal form for mixed fractions. \
+   \Improper fractions (numerator greater or equal to denominator) are not \
+   \allowed." $
+   "number.mixed-fraction.nf" @> makeView f (build mixedFractionView)
+ where
+   f (Sym s [Nat a, Nat b, Nat c])
+      | isMixedFractionSymbol s = simple a b c
+   f (Negate (Sym s [Nat a, Nat b, Nat c]))
+      | isMixedFractionSymbol s = negate <$> simple a b c
+   f expr = do r <- match rationalNF expr
+               guard ((-1 < r && r < 1) || denominator r == 1)
+               return (fromRational r)
+
+   simple a b c = do
+      guard (a > 0 && b > 0 && b < c)
+      r <- simpleRational b c
+      return (fromInteger a + fromRational r)
+
+-------------------------------------------------------------------
+-- Double (imprecise floating-points)
+
+doubleView :: View Expr Double
+doubleView = "num.double" @> makeView (fix matchDouble) fromDouble
+
+doubleNF :: View Expr Double
+doubleNF = "num.double.nf" @> makeView (optionNegate f) fromDouble
+ where
+   f (Number d) = Just d
+   f _          = Nothing
+
+matchDouble :: (Expr -> Maybe Double) -> Expr -> Maybe Double
+matchDouble f expr =
+   case expr of
+      Number d -> Just d
+      a :/: b  -> join (safeDiv <$> f a <*> f b)
+      Sqrt a   -> f a >>= safeSqrt
+      Sym s [a]
+         | absSymbol == s  -> liftM abs (f a)
+      Sym s [a, b]
+         | isPowerSymbol s -> join (safePower <$> f a <*> f b)
+         | isRootSymbol s  -> join (safeRoot  <$> f a <*> f b)
+      Sym s [a, b, c]
+         | isMixedFractionSymbol s -> f (a+b/c)
+      _ -> matchNum f expr
+
+-------------------------------------------------------------------
+-- Helper functions
+
+optionNegate :: (Eq a,Num a) => (Expr -> Maybe a) -> Expr -> Maybe a
+optionNegate f (Negate a) = do b <- f a; guard (b /= 0); return (negate b)
+optionNegate f a          = f a
+
+fix :: (a -> a) -> a
+fix f = f (fix f)
+ src/Domain/Math/Safe.hs view
@@ -0,0 +1,88 @@+-----------------------------------------------------------------------------
+-- Copyright 2019, Ideas project team. This file is distributed under the
+-- terms of the Apache License 2.0. For more information, see the files
+-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+
+module Domain.Math.Safe
+   ( -- * Safe division
+     SafeDiv(..), safeDivFractional
+   , -- * Safe power and root
+     SafePower(..)
+   ) where
+
+import Control.Monad
+import Data.Ratio
+
+-------------------------------------------------------------------
+-- Safe division
+
+class Num a => SafeDiv a where
+   safeDiv   :: a -> a -> Maybe a
+   safeRecip :: a -> Maybe a
+   -- default definitions
+   safeRecip = safeDiv 1
+
+instance SafeDiv Integer where
+   safeDiv x y
+      | y /= 0 && m == 0 = Just d
+      | otherwise        = Nothing
+    where (d, m) = x `divMod` y
+
+instance SafeDiv Double where
+   safeDiv = safeDivFractional
+
+instance Integral a => SafeDiv (Ratio a) where
+   safeDiv = safeDivFractional
+
+safeDivFractional :: (Eq a,Fractional a) => a -> a -> Maybe a
+safeDivFractional x y
+   | y /= 0    = Just (x / y)
+   | otherwise = Nothing
+
+-------------------------------------------------------------------
+-- Safe power and root
+
+class Num a => SafePower a where
+   safePower :: a -> a -> Maybe a
+   safeSqrt  :: a -> Maybe a
+   safeRoot  :: a -> a -> Maybe a
+   -- default definitions
+   safeSqrt = (`safeRoot` 2)
+
+instance SafePower Integer where
+   safeRoot x y =
+      case fmap round (safeRoot (fromInteger x :: Double) (fromInteger y)) of
+         Just a | safePower a y == Just x -> Just a
+         _ -> Nothing
+   safePower x y
+      | y >= 0    = Just (x ^ y)
+      | otherwise = Nothing
+
+instance Integral a => SafePower (Ratio a) where
+   safeRoot x y = do
+      let n = toInteger (numerator y)
+      guard (denominator y == 1)
+      a <- safeRoot (toInteger (numerator x)) n
+      b <- safeRoot (toInteger (denominator x)) n
+      safeDiv (fromInteger a) (fromInteger b)
+   safePower x y
+      | denominator y /= 1 = Nothing
+      | numerator y >= 0   = Just a
+      | otherwise          = Just (1/a)
+    where
+      a = x ^ abs (numerator y)
+
+instance SafePower Double where
+   safePower x y
+      | x==0 && y<0 = Nothing
+      | otherwise   = Just (x**y)
+   safeRoot x y
+      | x >= 0 && y >= 1 = Just (x ** (1/y))
+      | otherwise        = Nothing