Add naive prime generation code

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

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