diff --git a/CHANGELOG.txt b/CHANGELOG.txt new file mode 100644 --- /dev/null +++ b/CHANGELOG.txt @@ -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. diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 --- /dev/null +++ b/LICENSE.txt @@ -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. diff --git a/NOTICE.txt b/NOTICE.txt new file mode 100644 --- /dev/null +++ b/NOTICE.txt @@ -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) diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ideas-math-types.cabal b/ideas-math-types.cabal new file mode 100644 --- /dev/null +++ b/ideas-math-types.cabal @@ -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 diff --git a/src/Domain/Algebra/Boolean.hs b/src/Domain/Algebra/Boolean.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/Boolean.hs @@ -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 diff --git a/src/Domain/Algebra/BooleanLaws.hs b/src/Domain/Algebra/BooleanLaws.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/BooleanLaws.hs @@ -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]) diff --git a/src/Domain/Algebra/Field.hs b/src/Domain/Algebra/Field.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/Field.hs @@ -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 diff --git a/src/Domain/Algebra/FieldLaws.hs b/src/Domain/Algebra/FieldLaws.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/FieldLaws.hs @@ -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)]) diff --git a/src/Domain/Algebra/Group.hs b/src/Domain/Algebra/Group.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/Group.hs @@ -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 diff --git a/src/Domain/Algebra/GroupLaws.hs b/src/Domain/Algebra/GroupLaws.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/GroupLaws.hs @@ -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) diff --git a/src/Domain/Algebra/Law.hs b/src/Domain/Algebra/Law.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/Law.hs @@ -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 diff --git a/src/Domain/Algebra/SmartGroup.hs b/src/Domain/Algebra/SmartGroup.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Algebra/SmartGroup.hs @@ -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 diff --git a/src/Domain/Logic/Formula.hs b/src/Domain/Logic/Formula.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Logic/Formula.hs @@ -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 diff --git a/src/Domain/Logic/Generator.hs b/src/Domain/Logic/Generator.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Logic/Generator.hs @@ -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 diff --git a/src/Domain/Logic/Views.hs b/src/Domain/Logic/Views.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Logic/Views.hs @@ -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 diff --git a/src/Domain/Math/Data/DecimalFraction.hs b/src/Domain/Math/Data/DecimalFraction.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/DecimalFraction.hs @@ -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 diff --git a/src/Domain/Math/Data/Interval.hs b/src/Domain/Math/Data/Interval.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/Interval.hs @@ -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) diff --git a/src/Domain/Math/Data/MixedFraction.hs b/src/Domain/Math/Data/MixedFraction.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/MixedFraction.hs @@ -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 diff --git a/src/Domain/Math/Data/OrList.hs b/src/Domain/Math/Data/OrList.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/OrList.hs @@ -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 diff --git a/src/Domain/Math/Data/Polynomial.hs b/src/Domain/Math/Data/Polynomial.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/Polynomial.hs @@ -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) + ] diff --git a/src/Domain/Math/Data/PrimeFactors.hs b/src/Domain/Math/Data/PrimeFactors.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/PrimeFactors.hs @@ -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 + ) diff --git a/src/Domain/Math/Data/Primes.hs b/src/Domain/Math/Data/Primes.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/Primes.hs @@ -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] + ] diff --git a/src/Domain/Math/Data/Relation.hs b/src/Domain/Math/Data/Relation.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/Relation.hs @@ -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, ((:>=:), (.>=.))) + ] diff --git a/src/Domain/Math/Data/SquareRoot.hs b/src/Domain/Math/Data/SquareRoot.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/SquareRoot.hs @@ -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 diff --git a/src/Domain/Math/Data/WithBool.hs b/src/Domain/Math/Data/WithBool.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Data/WithBool.hs @@ -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 diff --git a/src/Domain/Math/Expr.hs b/src/Domain/Math/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Expr.hs @@ -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 diff --git a/src/Domain/Math/Expr/Clipboard.hs b/src/Domain/Math/Expr/Clipboard.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Expr/Clipboard.hs @@ -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 diff --git a/src/Domain/Math/Expr/Data.hs b/src/Domain/Math/Expr/Data.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Expr/Data.hs @@ -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 diff --git a/src/Domain/Math/Expr/Parser.hs b/src/Domain/Math/Expr/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Expr/Parser.hs @@ -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 diff --git a/src/Domain/Math/Expr/Symbols.hs b/src/Domain/Math/Expr/Symbols.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Expr/Symbols.hs @@ -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" diff --git a/src/Domain/Math/Expr/Views.hs b/src/Domain/Math/Expr/Views.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Expr/Views.hs @@ -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 diff --git a/src/Domain/Math/Numeric/Views.hs b/src/Domain/Math/Numeric/Views.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Numeric/Views.hs @@ -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) diff --git a/src/Domain/Math/Safe.hs b/src/Domain/Math/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Domain/Math/Safe.hs @@ -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