Merge pull request #3007 from stefan-hoeck/constant_fin

[ performance ] make Eq and Ord for Fin run in constant time

CHANGELOG.md

@@ -169,6 +169,8 @@
 
 * Adds `leftmost` and `rightmost` to `Control.Order`, a generalisation of `min` and `max`.
 
+* `Eq` and `Ord` implementations for `Fin n` now run in constant time.
+
 * Adds `getTermCols` and `getTermLines` to the base library. They return the size of the
   terminal if either stdin or stdout is a tty.
 

libs/base/Data/Fin.idr

@@ -51,18 +51,16 @@ export
 Injective FS where
   injective Refl = Refl
 
-export
-Eq (Fin n) where
-    (==) FZ FZ = True
-    (==) (FS k) (FS k') = k == k'
-    (==) _ _ = False
-
 ||| Convert a Fin to a Nat
 public export
 finToNat : Fin n -> Nat
 finToNat FZ = Z
 finToNat (FS k) = S $ finToNat k
 
+export
+Eq (Fin n) where
+  x == y = finToNat x == finToNat y
+
 finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
 finToNatInjective FZ     FZ     _    = Refl
 finToNatInjective (FS _) FZ     Refl impossible
@@ -172,10 +170,7 @@ namespace List1
 
 export
 Ord (Fin n) where
-  compare  FZ     FZ    = EQ
-  compare  FZ    (FS _) = LT
-  compare (FS _)  FZ    = GT
-  compare (FS x) (FS y) = compare x y
+  compare x y = compare (finToNat x) (finToNat y)
 
 namespace Monoid
 

tests/base/data_fin/expected

@@ -7,3 +7,6 @@
 [0, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1]
 [3, 2, 1, 0, 11, 10, 9, 8, 7, 6, 5, 4]
 [9, 10, 11, 0, 1, 2, 3, 4, 5, 6, 7, 8]
+18446744073709551615
+True
+EQ

tests/base/data_fin/performance.idr

@@ -0,0 +1,16 @@
+import Data.Fin
+
+-- This tests that `Show`, `Eq`, and `Ord` for `Fin`
+-- run in constant time (Strictly speaking, it's O(log n) with
+-- a large base).
+--
+-- It also verifies that `last` and `finToNat` run in O(1)
+-- (both should be removed by the identity optimizer during
+-- compilation)
+main : IO ()
+main = do
+  let largeNat := the Nat 0xffff_ffff_ffff_ffff
+      fin      := last {n = largeNat}
+  printLn fin               -- `Show` for `Fin` runs in O(1)
+  printLn (fin == fin)      -- `Eq` for `Fin` runs in O(1)
+  printLn (compare fin fin) -- `Ord` for `Fin` runs in O(1)

tests/base/data_fin/run

@@ -2,3 +2,4 @@ rm -rf build
 
 $1 --no-banner --no-color --console-width 0 --check fromInteger.idr
 $1 --no-banner --no-color --console-width 0 Num.idr -x main
+$1 --no-banner --no-color --console-width 0 performance.idr -x main