From 8d48abed0ef513765833846e1bead92160c8511d Mon Sep 17 00:00:00 2001
From: Nathan McCarty <nathan@mccarty.io>
Date: Fri, 23 Jun 2023 03:08:05 -0400
Subject: [PATCH] Add naive prime generation code

---
 PrimeSieve.ipkg            |  1 +
 src/PrimeSieve/Trivial.idr | 43 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+)
 create mode 100644 src/PrimeSieve/Trivial.idr

diff --git a/PrimeSieve.ipkg b/PrimeSieve.ipkg
index 7d9b4a9..f372568 100644
--- a/PrimeSieve.ipkg
+++ b/PrimeSieve.ipkg
@@ -17,6 +17,7 @@ license = "Parity Public License 7.0.0"
 -- modules to install
 modules = PrimeSieve
         , PrimeSieve.Util
+        , PrimeSieve.Trivial
 
 -- main file (i.e. file to load at REPL)
 main = PrimeSieve
diff --git a/src/PrimeSieve/Trivial.idr b/src/PrimeSieve/Trivial.idr
new file mode 100644
index 0000000..4ce6447
--- /dev/null
+++ b/src/PrimeSieve/Trivial.idr
@@ -0,0 +1,43 @@
+module PrimeSieve.Trivial
+
+import Data.Stream
+
+import PrimeSieve.Util
+
+%default total
+
+||| Test if a number is prime via trial division
+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
+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
+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