opentheory-divides (empty) → 1.55

raw patch · 5 files changed

+146/−0 lines, 5 filesdep +QuickCheckdep +basedep +opentheorysetup-changed

Dependencies added: QuickCheck, base, opentheory, opentheory-primitive

Files

LICENSE +17/−0
Setup.hs +6/−0
opentheory-divides.cabal +40/−0
src/OpenTheory/Natural/Divides.hs +30/−0
testsrc/Main.hs +53/−0

+ LICENSE view

@@ -0,0 +1,17 @@+Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN+THE SOFTWARE.

+ Setup.hs view

@@ -0,0 +1,6 @@+module Main(main)++import Distribution.Simple++main :: IO ()+main = defaultMain

+ opentheory-divides.cabal view

@@ -0,0 +1,40 @@+name: opentheory-divides+version: 1.55+category: Number Theory+synopsis: The divides relation on natural numbers+license: MIT+license-file: LICENSE+cabal-version: >= 1.8.0.2+build-type: Simple+author: Joe Leslie-Hurd <joe@gilith.com>+maintainer: Joe Leslie-Hurd <joe@gilith.com>+description:+  The divides relation on natural numbers - this package was automatically+  generated from the OpenTheory package natural-divides-1.55++library+  build-depends:+    base >= 4.0 && < 5.0,+    QuickCheck >= 2.4.0.1 && < 3.0,+    opentheory-primitive >= 1.3 && < 2.0,+    opentheory >= 1.195 && < 1.196++  hs-source-dirs: src++  ghc-options: -Wall++  exposed-modules:+    OpenTheory.Natural.Divides++executable opentheory-divides-test+  build-depends:+    base >= 4.0 && < 5.0,+    QuickCheck >= 2.4.0.1 && < 3.0,+    opentheory-primitive >= 1.3 && < 2.0,+    opentheory >= 1.195 && < 1.196++  hs-source-dirs: src, testsrc++  ghc-options: -Wall++  main-is: Main.hs

+ src/OpenTheory/Natural/Divides.hs view

@@ -0,0 +1,30 @@+{- |+module: $Header$+description: The divides relation on natural numbers+license: MIT++maintainer: Joe Leslie-Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}++module OpenTheory.Natural.Divides+where++import qualified OpenTheory.Primitive.Natural as Natural++divides :: Natural.Natural -> Natural.Natural -> Bool+divides a b = if a == 0 then b == 0 else b `mod` a == 0++egcd ::+  Natural.Natural -> Natural.Natural ->+    (Natural.Natural, (Natural.Natural, Natural.Natural))+egcd a b =+  if b == 0 then (a, (1, 0))+  else+    let c = a `mod` b in+    if c == 0 then (b, (1, a `div` b - 1))+    else+      let (g, (s, t)) = egcd c (b `mod` c) in+      let u = s + b `div` c * t in+      (g, (u, t + a `div` b * u))

+ testsrc/Main.hs view

@@ -0,0 +1,53 @@+{- |+module: Main+description: The divides relation on natural numbers - testing+license: MIT++maintainer: Joe Leslie-Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module Main+  ( main )+where++import qualified OpenTheory.Natural as Natural+import qualified OpenTheory.Natural.Divides as Divides+import qualified OpenTheory.Primitive.Natural as Primitive.Natural+import OpenTheory.Primitive.Test++proposition0 :: Primitive.Natural.Natural -> Bool+proposition0 a = Divides.divides a 0++proposition1 :: Primitive.Natural.Natural -> Bool+proposition1 a = Divides.divides a a++proposition2 :: Primitive.Natural.Natural -> Bool+proposition2 a = Divides.divides 1 a++proposition3 ::+  Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool+proposition3 a b = Divides.divides (fst (Divides.egcd a b)) a++proposition4 ::+  Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool+proposition4 a b = Divides.divides (fst (Divides.egcd a b)) b++proposition5 :: Primitive.Natural.Natural -> Bool+proposition5 a = Divides.divides 2 a == Natural.naturalEven a++proposition6 ::+  Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool+proposition6 a b =+  let (g, (s, t)) = Divides.egcd (a + 1) b in t * b + g == s * (a + 1)++main :: IO ()+main =+    do check "Proposition 0:\n  !a. divides a 0\n  " proposition0+       check "Proposition 1:\n  !a. divides a a\n  " proposition1+       check "Proposition 2:\n  !a. divides 1 a\n  " proposition2+       check "Proposition 3:\n  !a b. divides (fst (egcd a b)) a\n  " proposition3+       check "Proposition 4:\n  !a b. divides (fst (egcd a b)) b\n  " proposition4+       check "Proposition 5:\n  !a. divides 2 a <=> even a\n  " proposition5+       check "Proposition 6:\n  !a b. let (g, s, t) <- egcd (a + 1) b in t * b + g = s * (a + 1)\n  " proposition6+       return ()