PrimeSieve.ipkg

@@ -12,14 +12,10 @@ license = "Parity Public License 7.0.0"
 -- langversion
 
 -- packages to add to search path
-depends = contrib
-        , collie
+-- depends = 
 
 -- modules to install
 modules = PrimeSieve
-        , PrimeSieve.Util
-        , PrimeSieve.Trivial
-        , PrimeSieve.Simple
 
 -- main file (i.e. file to load at REPL)
 main = PrimeSieve

flake.lock

@@ -61,11 +61,11 @@
         "rust": "rust"
       },
       "locked": {
-        "lastModified": 1687504884,
-        "narHash": "sha256-M7eCdHpEV6WkVL2vPahM0X86eTS+zw72xeCC1LN2/I4=",
+        "lastModified": 1686465942,
+        "narHash": "sha256-+6ake+PQ9zVKrKaz3g8haA/t0woq1XLmbxYtoQwLgd8=",
         "ref": "trunk",
-        "rev": "b4d806c37bdd0dc91980e4e4eb0dee5383964cf5",
-        "revCount": 73,
+        "rev": "b306a4aff0f183268bd11d96ab3043638097f6f0",
+        "revCount": 72,
         "type": "git",
         "url": "https://git.sr.ht/~thatonelutenist/idr2nix"
       },
@@ -99,11 +99,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1687488839,
-        "narHash": "sha256-7JDjuyHwUvGJJge9jxfRJkuYyL5G5yipspc4J3HwjGA=",
+        "lastModified": 1686398752,
+        "narHash": "sha256-nGWNQVhSw4VSL+S0D0cbrNR9vs9Bq7rlYR+1K5f5j6w=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "f9e94676ce6c7531c44d38da61d2669ebec0f603",
+        "rev": "a30520bf8eabf8a5c37889d661e67a2dbcaa59e6",
         "type": "github"
       },
       "original": {

primesieve-sources.json

@@ -1,21 +1,9 @@
 {
-  "sources": {
-    "collie": {
-      "source": {
-        "url": "https://github.com/ohad/collie",
-        "rev": "46bff04a8d9a1598fec9b19f515541df16dc64ef",
-        "sha256": "sha256-0GziqzEUDs1tFd5yiu5NECV0nP1aMPe2QxS9oqhmW6I="
-      },
-      "ipkg": "collie.ipkg",
-      "name": "collie"
-    }
-  },
-  "sorted": [
-    "collie"
-  ],
+  "sources": {},
+  "sorted": [],
   "idris2": {
     "url": "https://github.com/idris-lang/Idris2",
-    "rev": "31c17ebec2e64c095076e8425637176db7658492",
-    "sha256": "sha256-DYwyjTdJjPDd/H5keb0tfmzR4AGwg/EaZMMQnLfksfY="
+    "rev": "5dcf62499df5cb861d153372ef3b4386dba25c98",
+    "sha256": "sha256-P9fVZNtgu08cvJmanL88W4F2l0PWKbSk8h8SS5JEN/M="
   }
 }

src/PrimeSieve.idr

@@ -1,230 +1,4 @@
 module PrimeSieve
 
-import System.Clock
-import Data.String
-
-import Collie
-
-import PrimeSieve.Trivial as Trivial
-import PrimeSieve.Simple as Simple
-
-primeSieve : Command "primesieve"
-primeSieve = MkCommand
-  { description = """
-    """
-   , subcommands =
-       [ "--help" ::= basic "Print this help text." none
-       , "bench-trivial" ::= basic "Benchmark the trivial generator" none
-       , "bench-simple" ::= basic "Benchmark the simple sieve" none
-       , "test-simple" ::= basic "test the simple sieve against trivial generation" none
-       , "test-trivial" ::= basic "test the trival generation against trivial generation" none
-       ]
-   , modifiers = []
-   , arguments = none }
-
-{nm : String} -> {cmd : Command nm} -> Show (ParseTreeT f g cmd) where
-  show (Here x) = "\{nm} <<args>>"
-  show (There pos parsedSub) = "\{nm} \{show parsedSub}"
-
-interface PrimeGen where
-  constructor MkPrimeGen
-  primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t
-  primes : (Integral t, Ord t, Num t, Range t) => Maybe (Stream t)
-
-
-%noinline
-call : (a -> b) -> a -> IO b
-call f x = fromPrim $ \w => MkIORes (f x) w
-
-displayTime : Clock t -> String
-displayTime x =
-  let (secs, ns) = (seconds x, nanoseconds x)
-      mins = secs `div` 60
-      secs = secs `mod` 60
-      nanos = ns `mod` 1_000
-      ns = ns `div` 1_000
-      micros = ns `mod` 1_000
-      millis = ns `div` 1_000
-  in """
-     \{padLeft 3 ' ' (show mins)}m \
-     \{padLeft 3 ' ' (show secs)}s \
-     \{padLeft 3 ' ' (show millis)}ms \
-     \{padLeft 3 ' ' (show micros)}μs \
-     \{padLeft 3 ' '(show nanos)}ns
-     """
-
-timeToDouble : Clock t -> Double
-timeToDouble x =
-  let (secs, ns) = (seconds x, nanoseconds x)
-      ns_double : Double = fromInteger ns
-      secs_double = (fromInteger secs)
-  in secs_double + (ns_double / 1000000000.0)
-
-record Timed a where
-  constructor MkTimed
-  result : a
-  desc : String
-  runCount : Nat
-  runsNonZero : NonZero runCount
-  runs : Vect runCount (Clock Duration)
-
-%name Timed timed, timed2, timed3
-
-(.min) : Timed a -> Clock Duration
-(.min) (MkTimed result desc runCount runsNonZero runs) = minVect' runs
-  where
-    minVect : (Ord b) => (xs : Vect n b) -> b -> b
-    minVect [] x = x
-    minVect (y :: xs) x =
-      if y < x
-        then minVect xs y
-        else minVect xs x
-    minVect' : (Ord b) => {n : Nat} -> (xs : Vect n b) -> {auto prf : NonZero n} -> b
-    minVect' {prf} [] impossible
-    minVect' (x :: xs) = minVect xs x
-
-(.max) : Timed a -> Clock Duration
-(.max) (MkTimed result desc runCount runsNonZero runs) = maxVect' runs
-  where
-    maxVect : (Ord b) => (xs : Vect n b) -> b -> b
-    maxVect [] x = x
-    maxVect (y :: xs) x =
-      if y > x
-        then maxVect xs y
-        else maxVect xs x
-    maxVect' : (Ord b) => {n : Nat} -> (xs : Vect n b) -> {auto prf : NonZero n} -> b
-    maxVect' {prf} [] impossible
-    maxVect' (x :: xs) = maxVect xs x
-
-(.avg) : Timed a -> Clock Duration
-(.avg) (MkTimed result desc runCount runsNonZero runs) = avgVect runCount runs
-  where
-    totalVect : (xs : Vect n (Clock Duration)) -> (acc : (Integer, Integer)) -> (Integer, Integer)
-    totalVect [] acc = acc
-    totalVect (x :: xs) (sec_total, ns_total) =
-      let (sec, ns) = (seconds x, nanoseconds x)
-      in totalVect xs (sec_total + sec, ns_total + ns)
-    avgVect : (count : Nat) -> (xs : Vect count (Clock Duration)) -> Clock Duration
-    avgVect 0 xs = makeDuration 0 0
-    avgVect count@(S count') xs =
-      let (sec, ns) = totalVect xs (0,0)
-          t = ((sec * 1_000_000_000) + ns) `div` (natToInteger count)
-      in makeDuration 0 t
-
-Show (Timed a) where
-  show t = """
-    \{t.desc}   \
-    min: \{displayTime t.min}   \
-    avg: \{displayTime t.avg}   \
-    max: \{displayTime t.max}
-    """
-
-mergeTimed : (x : Timed a) -> (y : Timed a) -> Timed a
-mergeTimed (MkTimed result desc 0 runsNonZero runs) (MkTimed x str k y xs) impossible
-mergeTimed (MkTimed result desc (S j) runsNonZero runs) (MkTimed x str k y xs) =
-  MkTimed x str ((S j) + k) SIsNonZero (runs ++ xs)
-
-timeIO : (prev : Maybe (Timed a))
-      -> (action : IO a)
-      -> (case prev of
-            Nothing => (desc : String) -> IO (Timed a)
-            (Just _) => IO (Timed a))
-timeIO Nothing action =
-  (\desc =>
-    do start <- clockTime Monotonic
-       result <- action
-       end <- clockTime Monotonic
-       let time = timeDifference end start
-       pure (MkTimed result desc 1 SIsNonZero [time]))
-timeIO (Just timed) action = do
-  single <- timeIO Nothing action timed.desc
-  pure (mergeTimed timed single)
-
-runTimes : (times : Nat) -> {auto prf : NonZero times} -> (desc : String) -> (action : IO a) -> IO (Timed a)
-runTimes 0 desc action impossible
-runTimes (S times') desc action = do
-  timed <- timeIO Nothing action desc
-  runTimes' times' timed action
-  where
-    runTimes' : Nat -> (acc : Timed a) -> IO a -> IO (Timed a)
-    runTimes' 0 acc x = pure acc
-    runTimes' (S k) acc x = do
-      timed <- timeIO (Just acc) x
-      runTimes' k timed x
-
-||| Benchmark a PrimeGen
-benchmark : PrimeGen -> IO ()
-benchmark x = do
-  putStrLn "Benching primesUntil method\n"
-  benchUntil 100
-  benchUntil 1_000
-  benchUntil 10_000
-  benchUntil 100_000
-  where
-    benchUntil : (limit : Bits64) -> IO ()
-    benchUntil limit =
-      do putStrLn "  Benchmarking primes up to \{show limit} (100 times):"
-         time <- runTimes
-                  100
-                  "Primes <= \{padLeft 6 ' ' (show limit)}"
-                  ((call PrimeSieve.primesUntil) limit)
-         putStrLn "    \{show time}"
-         let primesPerSec = 1.0 / (timeToDouble time.avg)
-         putStrLn
-           "    Avg \{show primesPerSec} primes/s (\{show (length time.result)} primes)\n"
-
-||| Test a PrimeGen against the default
-test : PrimeGen ->  IO ()
-test item = do
-  putStrLn "Testing primesUntil method\n"
-  tryUntil 10
-  tryUntil 100
-  tryUntil 1_000
-  tryUntil 10_000
-  tryUntil 100_000
-  putStrLn ""
-  let stream : Maybe (Stream Bits64) = PrimeSieve.primes
-  case stream of
-    Nothing => exitSuccess
-    (Just x) => do
-      tryStream 10 x
-      tryStream 100 x
-      tryStream 1_000 x
-      tryStream 10_000 x
-  where
-    fail : Show t => List t -> List t -> IO ()
-    fail expected got = do
-      putStrLn "fail\n"
-      putStrLn "Expected: \{show expected}"
-      putStrLn "Got: \{show got}"
-      exitFailure
-    tryCompare : (Show t, Eq t) => List t -> List t -> IO ()
-    tryCompare xs ys =
-      if xs == ys
-        then putStrLn "pass"
-        else fail xs ys
-    tryUntil : Bits64 -> IO ()
-    tryUntil k = do
-      putStr "  Testing up to \{show k}: "
-      let trivial : List Bits64 = Trivial.primesUntil k
-      let sample : List Bits64 = PrimeSieve.primesUntil k
-      tryCompare trivial sample
-    tryStream : Nat -> Stream Bits64 -> IO ()
-    tryStream k stream = do
-      putStr "  Testing up to \{show k}: "
-      let trivial = take k Trivial.primes
-      let sample = take k stream
-      tryCompare trivial sample
-
-
 main : IO ()
-main = do
-  Right cmdParse <- primeSieve.parseArgs
-  | Left err => putStrLn "Error: \{err}"
-  case fst (lookup cmdParse) of
-    "bench-trivial" => benchmark (MkPrimeGen Trivial.primesUntil (Just Trivial.primes))
-    "bench-simple" => benchmark (MkPrimeGen Simple.primesUntil Nothing)
-    "test-trivial" => test (MkPrimeGen Trivial.primesUntil (Just Trivial.primes))
-    "test-simple" => test (MkPrimeGen Simple.primesUntil Nothing)
-    "--help" => putStrLn "Usage: \n\{primeSieve.usage}"
-    _ => putStrLn "Parse as \{show cmdParse}"
+main = putStrLn "Hello!"

src/PrimeSieve/Simple.idr

@@ -1,9 +0,0 @@
-module PrimeSieve.Simple
-
-||| Use a basic, unoptimized sieve to generate the primes up to a specific number
-export
-primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t
-
-||| A stream of primes, Generated by a lazily extending sieve
-export
-primes : (Integral t, Ord t, Num t, Range t) => Stream t

src/PrimeSieve/Trivial.idr

@@ -1,46 +0,0 @@
-module PrimeSieve.Trivial
-
-import Data.Stream
-
-import PrimeSieve.Util
-
-%default total
-
-||| Test if a number is prime via trial division
-export
-isPrime : (Integral t, Ord t, Num t, Range t) => t -> Bool
-isPrime x =
-  let trial_divisors = [2..((isqrt x) + 1)]
-  in if x <= 2
-       then x == 2
-       else isPrime' trial_divisors x
-  where
-    isPrime' : List t -> t -> Bool
-    isPrime' [] x = True
-    isPrime' (y :: xs) x =
-      if x `mod` y == 0
-        then False
-        else isPrime' xs x
-
-||| A stream of primes, generated by testing via trial division
-export
-primes : (Integral t, Ord t, Num t, Range t) => Stream t
-primes =
-  let naturals : Stream t = iterate (+1) 1
-  in unfoldr next_prime naturals
-  where
-    next_prime : Stream t -> (t, Stream t)
-    next_prime orig@(y :: ys) =
-      if isPrime y
-      then (y, ys)
-      -- We assert_smaller here as there are an infinite number of primes, so we can never
-      -- run out of primes, and taking one off the head of the stream will always get us
-      -- closer to the next prime
-      else next_prime (assert_smaller orig ys)
-
-||| All the primes up until the given limit
-export
-primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t
--- We assert_total here as the list of primes is infinite and strictly increasing, so this
--- Will always terminate in finite time
-primesUntil limit = assert_total $ takeBefore (> limit) primes

src/PrimeSieve/Util.idr

@@ -1,18 +0,0 @@
-module PrimeSieve.Util
-
-%default total
-
-||| Integer square root
-export
-isqrt : (Integral t, Ord t) => t -> t
-isqrt n = sqrt' n
-  where
-    sqrt' : t -> t
-    sqrt' a =
-      let b = (a + (n `div` a)) `div` 2
-      in if a > b then sqrt' (assert_smaller a b) else a
-
-||| Nat square root
-export
-sqrtNat : Nat -> Nat
-sqrtNat = integerToNat . isqrt . natToInteger