diff --git a/opentheory-prime.cabal b/opentheory-prime.cabal --- a/opentheory-prime.cabal +++ b/opentheory-prime.cabal @@ -1,43 +1,45 @@ name: opentheory-prime -version: 1.23 +version: 1.79 category: Number Theory -synopsis: Prime numbers +synopsis: Prime natural numbers license: MIT license-file: LICENSE -cabal-version: >= 1.8.0.6 +cabal-version: >= 1.8.0.2 build-type: Simple author: Joe Leslie-Hurd maintainer: Joe Leslie-Hurd description: - Prime numbers - automatically generated from the opentheory package - haskell-prime-1.23 + Prime natural numbers - this package was automatically generated from the + OpenTheory package natural-prime-1.79 library build-depends: base >= 4.0 && < 5.0, - random >= 1.0.1.1 && < 2.0, QuickCheck >= 2.4.0.1 && < 3.0, - opentheory-primitive >= 1.0 && < 2.0, - opentheory >= 1.73 && <= 1.76 + opentheory-primitive >= 1.3 && < 2.0, + opentheory >= 1.193 && < 1.196, + opentheory-divides >= 1.53 && < 1.56, + opentheory-stream >= 1.42 && < 1.43 hs-source-dirs: src ghc-options: -Wall exposed-modules: - OpenTheory.Number.Natural.Prime - OpenTheory.Number.Natural.Prime.Sieve + OpenTheory.Natural.Prime + OpenTheory.Natural.Prime.Sieve executable opentheory-prime-test build-depends: base >= 4.0 && < 5.0, - random >= 1.0.1.1 && < 2.0, QuickCheck >= 2.4.0.1 && < 3.0, - opentheory-primitive >= 1.0 && < 2.0, - opentheory >= 1.73 && <= 1.76 + opentheory-primitive >= 1.3 && < 2.0, + opentheory >= 1.193 && < 1.196, + opentheory-divides >= 1.53 && < 1.56, + opentheory-stream >= 1.42 && < 1.43 hs-source-dirs: src, testsrc ghc-options: -Wall - main-is: Test.hs + main-is: Main.hs diff --git a/src/OpenTheory/Natural/Prime.hs b/src/OpenTheory/Natural/Prime.hs new file mode 100644 --- /dev/null +++ b/src/OpenTheory/Natural/Prime.hs @@ -0,0 +1,19 @@ +{- | +module: $Header$ +description: Prime natural numbers +license: MIT + +maintainer: Joe Leslie-Hurd +stability: provisional +portability: portable +-} + +module OpenTheory.Natural.Prime +where + +import qualified OpenTheory.Natural.Prime.Sieve as Sieve +import qualified OpenTheory.Primitive.Natural as Natural +import qualified OpenTheory.Stream as Stream + +primes :: [Natural.Natural] +primes = Stream.unfold Sieve.next Sieve.initial diff --git a/src/OpenTheory/Natural/Prime/Sieve.hs b/src/OpenTheory/Natural/Prime/Sieve.hs new file mode 100644 --- /dev/null +++ b/src/OpenTheory/Natural/Prime/Sieve.hs @@ -0,0 +1,50 @@ +{- | +module: $Header$ +description: Prime natural numbers +license: MIT + +maintainer: Joe Leslie-Hurd +stability: provisional +portability: portable +-} + +module OpenTheory.Natural.Prime.Sieve +where + +import qualified OpenTheory.Primitive.Natural as Natural + +newtype Sieve = + Sieve { + unSieve :: + (Natural.Natural, + [(Natural.Natural, (Natural.Natural, Natural.Natural))]) + } + +initial :: Sieve +initial = Sieve (1, []) + +increment :: Sieve -> (Bool, Sieve) +increment = + \s -> + let (n, ps) = unSieve s in + let n' = n + 1 in + let (b, ps') = inc n' 1 ps in + (b, Sieve (n', ps')) + where + {-inc :: + Natural.Natural -> Natural.Natural -> + [(Natural.Natural, (Natural.Natural, Natural.Natural))] -> + (Bool, [(Natural.Natural, (Natural.Natural, Natural.Natural))])-} + inc n _ [] = (True, (n, (0, 0)) : []) + inc n i ((p, (k, j)) : ps) = + let k' = (k + i) `mod` p in + let j' = j + i in + if k' == 0 then (False, (p, (0, j')) : ps) + else let (b, ps') = inc n j' ps in (b, (p, (k', 0)) : ps') + +perimeter :: Sieve -> Natural.Natural +perimeter s = fst (unSieve s) + +next :: Sieve -> (Natural.Natural, Sieve) +next s = + let (b, s') = increment s in if b then (perimeter s', s') else next s' diff --git a/src/OpenTheory/Number/Natural/Prime.hs b/src/OpenTheory/Number/Natural/Prime.hs deleted file mode 100644 --- a/src/OpenTheory/Number/Natural/Prime.hs +++ /dev/null @@ -1,18 +0,0 @@ -{- | -module: $Header$ -description: Prime numbers -license: MIT - -maintainer: Joe Leslie-Hurd -stability: provisional -portability: portable --} -module OpenTheory.Number.Natural.Prime -where - -import qualified OpenTheory.Data.Stream as Data.Stream -import qualified OpenTheory.Number.Natural.Prime.Sieve as Sieve -import qualified OpenTheory.Primitive.Natural as Primitive.Natural - -all :: [Primitive.Natural.Natural] -all = Data.Stream.unfold Sieve.next Sieve.initial diff --git a/src/OpenTheory/Number/Natural/Prime/Sieve.hs b/src/OpenTheory/Number/Natural/Prime/Sieve.hs deleted file mode 100644 --- a/src/OpenTheory/Number/Natural/Prime/Sieve.hs +++ /dev/null @@ -1,53 +0,0 @@ -{- | -module: $Header$ -description: Prime numbers -license: MIT - -maintainer: Joe Leslie-Hurd -stability: provisional -portability: portable --} -module OpenTheory.Number.Natural.Prime.Sieve -where - -import qualified OpenTheory.Primitive.Natural as Primitive.Natural - -newtype Sieve = - Sieve { - unSieve :: - (Primitive.Natural.Natural, - [(Primitive.Natural.Natural, - (Primitive.Natural.Natural, Primitive.Natural.Natural))]) - } - -initial :: Sieve -initial = Sieve (1, []) - -increment :: Sieve -> (Bool, Sieve) -increment = - \s -> - let (n, ps) = unSieve s in - let n' = n + 1 in - let (b, ps') = inc n' 1 ps in - (b, Sieve (n', ps')) - where - {-inc :: - Primitive.Natural.Natural -> Primitive.Natural.Natural -> - [(Primitive.Natural.Natural, - (Primitive.Natural.Natural, Primitive.Natural.Natural))] -> - (Bool, - [(Primitive.Natural.Natural, - (Primitive.Natural.Natural, Primitive.Natural.Natural))])-} - inc n _ [] = (True, (n, (0, 0)) : []) - inc n i ((p, (k, j)) : ps) = - let k' = (k + i) `mod` p in - let j' = j + i in - if k' == 0 then (False, (p, (0, j')) : ps) - else let (b, ps') = inc n j' ps in (b, (p, (k', 0)) : ps') - -perimeter :: Sieve -> Primitive.Natural.Natural -perimeter s = fst (unSieve s) - -next :: Sieve -> (Primitive.Natural.Natural, Sieve) -next s = - let (b, s') = increment s in if b then (perimeter s', s') else next s' diff --git a/testsrc/Main.hs b/testsrc/Main.hs new file mode 100644 --- /dev/null +++ b/testsrc/Main.hs @@ -0,0 +1,45 @@ +{- | +module: Main +description: Prime natural numbers - testing +license: MIT + +maintainer: Joe Leslie-Hurd +stability: provisional +portability: portable +-} +module Main + ( main ) +where + +import qualified OpenTheory.Natural.Divides as Divides +import qualified OpenTheory.Natural.Prime as Prime +import qualified OpenTheory.Primitive.Natural as Natural +import qualified OpenTheory.Stream as Stream +import OpenTheory.Primitive.Test + +assertion0 :: Bool +assertion0 = not (Stream.nth Prime.primes 0 == 0) + +proposition0 :: Natural.Natural -> Natural.Natural -> Bool +proposition0 i j = + (Stream.nth Prime.primes i <= Stream.nth Prime.primes j) == (i <= j) + +proposition1 :: Natural.Natural -> Natural.Natural -> Bool +proposition1 i j = + not + (Divides.divides (Stream.nth Prime.primes i) + (Stream.nth Prime.primes (i + (j + 1)))) + +proposition2 :: Natural.Natural -> Natural.Natural -> Bool +proposition2 n i = + any (\p -> Divides.divides p (n + 2)) + (Stream.naturalTake Prime.primes i) || + Stream.nth Prime.primes i <= n + 2 + +main :: IO () +main = + do assert "Assertion 0:\n ~(nth Prime.all 0 = 0)\n " assertion0 + check "Proposition 0:\n !i j. nth Prime.all i <= nth Prime.all j <=> i <= j\n " proposition0 + check "Proposition 1:\n !i j. ~divides (nth Prime.all i) (nth Prime.all (i + (j + 1)))\n " proposition1 + check "Proposition 2:\n !n i.\n any (\\p. divides p (n + 2)) (take Prime.all i) \\/\n nth Prime.all i <= n + 2\n " proposition2 + return () diff --git a/testsrc/Test.hs b/testsrc/Test.hs deleted file mode 100644 --- a/testsrc/Test.hs +++ /dev/null @@ -1,54 +0,0 @@ -{- | -module: Main -description: Prime numbers - testing -license: MIT - -maintainer: Joe Leslie-Hurd -stability: provisional -portability: portable --} -module Main - ( main ) -where - -import qualified OpenTheory.Data.Stream as Data.Stream -import qualified OpenTheory.Number.Natural as Number.Natural -import qualified OpenTheory.Number.Natural.Geometric - as Number.Natural.Geometric -import qualified OpenTheory.Number.Natural.Prime as Number.Natural.Prime -import qualified OpenTheory.Primitive.Random as Primitive.Random -import qualified OpenTheory.Primitive.Test as Primitive.Test - -assertion0 :: Bool -assertion0 = not (Data.Stream.nth Number.Natural.Prime.all 0 == 0) - -proposition0 :: Primitive.Random.Random -> Bool -proposition0 r = - let (i, r') = Number.Natural.Geometric.fromRandom r in - let (j, _) = Number.Natural.Geometric.fromRandom r' in - (Data.Stream.nth Number.Natural.Prime.all i <= - Data.Stream.nth Number.Natural.Prime.all j) == (i <= j) - -proposition1 :: Primitive.Random.Random -> Bool -proposition1 r = - let (i, r') = Number.Natural.Geometric.fromRandom r in - let (j, _) = Number.Natural.Geometric.fromRandom r' in - not - (Number.Natural.divides (Data.Stream.nth Number.Natural.Prime.all i) - (Data.Stream.nth Number.Natural.Prime.all (i + j + 1))) - -proposition2 :: Primitive.Random.Random -> Bool -proposition2 r = - let (n, r') = Number.Natural.fromRandom r in - let (i, _) = Number.Natural.Geometric.fromRandom r' in - any (\p -> Number.Natural.divides p (n + 2)) - (Data.Stream.take' Number.Natural.Prime.all i) || - Data.Stream.nth Number.Natural.Prime.all i <= n + 2 - -main :: IO () -main = - do Primitive.Test.assert "Assertion 0:\n ~(H.nth H.Prime.all 0 = 0)\n " assertion0 - Primitive.Test.check "Proposition 0:\n !r.\n let (i, r') <- H.Geometric.fromRandom r in\n let (j, r'') <- H.Geometric.fromRandom r' in\n H.nth H.Prime.all i <= H.nth H.Prime.all j <=> i <= j\n " proposition0 - Primitive.Test.check "Proposition 1:\n !r.\n let (i, r') <- H.Geometric.fromRandom r in\n let (j, r'') <- H.Geometric.fromRandom r' in\n ~H.divides (H.nth H.Prime.all i) (H.nth H.Prime.all (i + j + 1))\n " proposition1 - Primitive.Test.check "Proposition 2:\n !r.\n let (n, r') <- H.fromRandom r in\n let (i, r'') <- H.Geometric.fromRandom r' in\n any (\\p. H.divides p (n + 2)) (H.take' H.Prime.all i) \\/\n H.nth H.Prime.all i <= n + 2\n " proposition2 - return ()