From c7abb148e8fd6e9146af7523eb54968fbdba7430 Mon Sep 17 00:00:00 2001
From: scarf <greenscarf005@gmail.com>
Date: Mon, 31 Jul 2023 16:36:40 +0900
Subject: [PATCH] feat: even and odd for Nat and Integral (#3021)

---
 CHANGELOG.md                          |  1 +
 libs/base/Data/Integral.idr           |  9 +++++
 tests/base/data_integral/Integral.idr | 52 +++++++++++++++++++++++++++
 tests/base/data_integral/expected     | 10 ++++++
 tests/base/data_integral/input        |  2 ++
 tests/base/data_integral/run          |  3 ++
 6 files changed, 77 insertions(+)
 create mode 100644 libs/base/Data/Integral.idr
 create mode 100644 tests/base/data_integral/Integral.idr
 create mode 100644 tests/base/data_integral/expected
 create mode 100644 tests/base/data_integral/input
 create mode 100644 tests/base/data_integral/run

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8d18f3096..ae2a37999 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -175,6 +175,7 @@
 
 * Adds `leftmost` and `rightmost` to `Control.Order`, a generalisation of `min` and `max`.
 
+* Adds `even` and `odd` to `Data.Integral`.
 * `Eq` and `Ord` implementations for `Fin n` now run in constant time.
 
 * Adds `getTermCols` and `getTermLines` to the base library. They return the
diff --git a/libs/base/Data/Integral.idr b/libs/base/Data/Integral.idr
new file mode 100644
index 000000000..876ac63a0
--- /dev/null
+++ b/libs/base/Data/Integral.idr
@@ -0,0 +1,9 @@
+module Data.Integral
+
+export
+even : Integral n => Eq n => n -> Bool
+even n = n `mod` 2 == 0
+
+export
+odd : Integral n => Eq n => n -> Bool
+odd = not . even
diff --git a/tests/base/data_integral/Integral.idr b/tests/base/data_integral/Integral.idr
new file mode 100644
index 000000000..f7c16efdf
--- /dev/null
+++ b/tests/base/data_integral/Integral.idr
@@ -0,0 +1,52 @@
+import Data.Integral
+
+Cases : Type
+Cases = List Bool
+
+natEvenCases : Cases
+natEvenCases = [
+    even 0,
+    even 2,
+    even 4,
+    even Z,
+    even (S (S Z))
+  ]
+
+natOddCases : Cases
+natOddCases = [
+    odd 1,
+    odd 3,
+    odd 5,
+    odd (S Z),
+    odd (S (S (S Z)))
+  ]
+
+integralEvenCases : Cases
+integralEvenCases = [
+    even (-4),
+    even (-2),
+    even 0,
+    even 2,
+    even 4
+]
+
+integralOddCases : Cases
+integralOddCases = [
+    odd (-5),
+    odd (-3),
+    odd (-1),
+    odd 1,
+    odd 3,
+    odd 5
+]
+
+main : IO ()
+main = do
+  printLn "Nat Even"
+  printLn natEvenCases
+  printLn "Nat Odd"
+  printLn natOddCases
+  printLn "Integral Even"
+  printLn integralEvenCases
+  printLn "Integral Odd"
+  printLn integralOddCases
diff --git a/tests/base/data_integral/expected b/tests/base/data_integral/expected
new file mode 100644
index 000000000..39ffccc9e
--- /dev/null
+++ b/tests/base/data_integral/expected
@@ -0,0 +1,10 @@
+1/1: Building Integral (Integral.idr)
+Main> "Nat Even"
+[True, True, True, True, True]
+"Nat Odd"
+[True, True, True, True, True]
+"Integral Even"
+[True, True, True, True, True]
+"Integral Odd"
+[True, True, True, True, True, True]
+Main> Bye for now!
diff --git a/tests/base/data_integral/input b/tests/base/data_integral/input
new file mode 100644
index 000000000..fc5992c29
--- /dev/null
+++ b/tests/base/data_integral/input
@@ -0,0 +1,2 @@
+:exec main
+:q
diff --git a/tests/base/data_integral/run b/tests/base/data_integral/run
new file mode 100644
index 000000000..1271d4512
--- /dev/null
+++ b/tests/base/data_integral/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner Integral.idr < input