From a3d54c59df898d47a96890aafb4c9b5ad67804da Mon Sep 17 00:00:00 2001
From: Nathan McCarty <nathan@mccarty.io>
Date: Fri, 23 Jun 2023 02:24:58 -0400
Subject: [PATCH] Add integer square root

---
 PrimeSieve.ipkg         |  1 +
 src/PrimeSieve/Util.idr | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 src/PrimeSieve/Util.idr

diff --git a/PrimeSieve.ipkg b/PrimeSieve.ipkg
index 60cb213..7d9b4a9 100644
--- a/PrimeSieve.ipkg
+++ b/PrimeSieve.ipkg
@@ -16,6 +16,7 @@ license = "Parity Public License 7.0.0"
 
 -- modules to install
 modules = PrimeSieve
+        , PrimeSieve.Util
 
 -- main file (i.e. file to load at REPL)
 main = PrimeSieve
diff --git a/src/PrimeSieve/Util.idr b/src/PrimeSieve/Util.idr
new file mode 100644
index 0000000..93d40f4
--- /dev/null
+++ b/src/PrimeSieve/Util.idr
@@ -0,0 +1,18 @@
+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