From 05f28724edc88d0f7b99833e4354aff883fa5da8 Mon Sep 17 00:00:00 2001
From: Tim Engler <engler@gmail.com>
Date: Mon, 28 Jun 2021 23:48:08 +0800
Subject: [PATCH] [ fix #1579 ] Nat hack for comparison operators (#1580)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
---
 libs/prelude/Prelude/EqOrd.idr  | 20 ++++++--------------
 libs/prelude/Prelude/Types.idr  | 24 +++++++++++++++++-------
 src/Compiler/CompileExpr.idr    |  4 ++++
 tests/idris2/reg042/NatOpts.idr |  6 ++++++
 tests/idris2/reg042/expected    | 26 ++++++++++++++++++++++++++
 tests/idris2/reg042/input       |  2 ++
 tests/idris2/reg044/Methods.idr | 17 +++++++++++++----
 tests/idris2/reg044/expected    | 13 +++++++------
 8 files changed, 81 insertions(+), 31 deletions(-)

diff --git a/libs/prelude/Prelude/EqOrd.idr b/libs/prelude/Prelude/EqOrd.idr
index 7820a0b76..6b0ee2e25 100644
--- a/libs/prelude/Prelude/EqOrd.idr
+++ b/libs/prelude/Prelude/EqOrd.idr
@@ -89,6 +89,7 @@ public export
 interface Eq ty => Ord ty where
   constructor MkOrd
   compare : ty -> ty -> Ordering
+  compare x y = if x < y then LT else if x == y then EQ else GT
 
   (<) : ty -> ty -> Bool
   (<) x y = compare x y == LT
@@ -129,8 +130,6 @@ Ord Bool where
 
 public export
 Ord Int where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Int x y)
   (<=) x y = intToBool (prim__lte_Int x y)
   (>) x y = intToBool (prim__gt_Int x y)
@@ -138,17 +137,18 @@ Ord Int where
 
 public export
 Ord Integer where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Integer x y)
   (<=) x y = intToBool (prim__lte_Integer x y)
   (>) x y = intToBool (prim__gt_Integer x y)
   (>=) x y = intToBool (prim__gte_Integer x y)
 
+-- Used for the nat hack
+public export
+compareInteger : (x, y : Integer) -> Ordering
+compareInteger = compare
+
 public export
 Ord Bits8 where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Bits8 x y)
   (<=) x y = intToBool (prim__lte_Bits8 x y)
   (>) x y = intToBool (prim__gt_Bits8 x y)
@@ -156,8 +156,6 @@ Ord Bits8 where
 
 public export
 Ord Bits16 where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Bits16 x y)
   (<=) x y = intToBool (prim__lte_Bits16 x y)
   (>) x y = intToBool (prim__gt_Bits16 x y)
@@ -165,8 +163,6 @@ Ord Bits16 where
 
 public export
 Ord Bits32 where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Bits32 x y)
   (<=) x y = intToBool (prim__lte_Bits32 x y)
   (>) x y = intToBool (prim__gt_Bits32 x y)
@@ -174,8 +170,6 @@ Ord Bits32 where
 
 public export
 Ord Bits64 where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Bits64 x y)
   (<=) x y = intToBool (prim__lte_Bits64 x y)
   (>) x y = intToBool (prim__gt_Bits64 x y)
@@ -183,8 +177,6 @@ Ord Bits64 where
 
 public export
 Ord Double where
-  compare x y = if x < y then LT else if x == y then EQ else GT
-
   (<) x y = intToBool (prim__lt_Double x y)
   (<=) x y = intToBool (prim__lte_Double x y)
   (>) x y = intToBool (prim__gt_Double x y)
diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
index 49064c8ed..5d94ff705 100644
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@@ -69,18 +69,28 @@ Num Nat where
 
   fromInteger x = integerToNat x
 
+-- used for nat hack
+public export
+equalNat : (m, n : Nat) -> Bool
+equalNat Z Z = True
+equalNat (S j) (S k) = equalNat j k
+equalNat _ _ = False
+
 public export
 Eq Nat where
-  Z == Z = True
-  S j == S k = j == k
-  _ == _ = False
+  (==) = equalNat
+
+-- used for nat hack
+public export
+compareNat : (m, n : Nat) -> Ordering
+compareNat Z Z = EQ
+compareNat Z (S k) = LT
+compareNat (S k) Z = GT
+compareNat (S j) (S k) = compareNat j k
 
 public export
 Ord Nat where
-  compare Z Z = EQ
-  compare Z (S k) = LT
-  compare (S k) Z = GT
-  compare (S j) (S k) = compare j k
+  compare = compareNat
 
 public export
 natToInteger : Nat -> Integer
diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr
index d486f9040..7332bf793 100644
--- a/src/Compiler/CompileExpr.idr
+++ b/src/Compiler/CompileExpr.idr
@@ -203,6 +203,10 @@ natHack =
     , MagicCRef (NS typesNS (UN "mult")) 2
          (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
     , MagicCRef (NS typesNS (UN "minus")) 2 magic__natMinus
+    , MagicCRef (NS typesNS (UN "equalNat")) 2
+         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__eq_Integer")) [m, n])
+    , MagicCRef (NS typesNS (UN "compareNat")) 2
+         (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN "compareInteger"))) [m, n])
     ]
 
 -- get all transformation from %builtin pragmas
diff --git a/tests/idris2/reg042/NatOpts.idr b/tests/idris2/reg042/NatOpts.idr
index 7e0a4dc89..c907ff47f 100644
--- a/tests/idris2/reg042/NatOpts.idr
+++ b/tests/idris2/reg042/NatOpts.idr
@@ -6,3 +6,9 @@ doMult x y = x `mult` y
 
 doMinus : Nat -> Nat -> Nat
 doMinus x y = x `minus` y
+
+doEqual : (m, n : Nat) -> Bool
+doEqual m n = m `equalNat` n
+
+doCompare : (m, n : Nat) -> Ordering
+doCompare m n = m `compareNat` n
diff --git a/tests/idris2/reg042/expected b/tests/idris2/reg042/expected
index 002ed74b9..7fd21a869 100644
--- a/tests/idris2/reg042/expected
+++ b/tests/idris2/reg042/expected
@@ -38,4 +38,30 @@ Refers to: [Prelude.Types.mult]
 Refers to (runtime): []
 Flags: [covering]
 Size change: Prelude.Types.mult: [Just (0, Same), Just (1, Same)]
+Main> Main.doCompare ==> [{arg:0}, {arg:1}];
+Compile time tree: [0] (Prelude.Types.compareNat {arg:0}[0] {arg:1}[1])
+Run time tree: Error: ""
+RigW
+Erasable args: []
+Detaggable arg types: []
+Specialise args: []
+Inferrable args: []
+Compiled: [{arg:0}, {arg:1}]: (Prelude.EqOrd.compareInteger [!{arg:0}, !{arg:1}])
+Refers to: [Prelude.Types.compareNat]
+Refers to (runtime): [Prelude.EqOrd.compareInteger]
+Flags: [covering]
+Size change: Prelude.Types.compareNat: [Just (0, Same), Just (1, Same)]
+Main> Main.doEqual ==> [{arg:0}, {arg:1}];
+Compile time tree: [0] (Prelude.Types.equalNat {arg:0}[0] {arg:1}[1])
+Run time tree: Error: ""
+RigW
+Erasable args: []
+Detaggable arg types: []
+Specialise args: []
+Inferrable args: []
+Compiled: [{arg:0}, {arg:1}]: (==Integer [!{arg:0}, !{arg:1}])
+Refers to: [Prelude.Types.equalNat]
+Refers to (runtime): []
+Flags: [covering]
+Size change: Prelude.Types.equalNat: [Just (0, Same), Just (1, Same)]
 Main> Bye for now!
diff --git a/tests/idris2/reg042/input b/tests/idris2/reg042/input
index 50fc88e59..65bb305df 100644
--- a/tests/idris2/reg042/input
+++ b/tests/idris2/reg042/input
@@ -1,4 +1,6 @@
 :di doPlus
 :di doMinus
 :di doMult
+:di doCompare
+:di doEqual
 :q
diff --git a/tests/idris2/reg044/Methods.idr b/tests/idris2/reg044/Methods.idr
index e35d1ee11..53c4ad31c 100644
--- a/tests/idris2/reg044/Methods.idr
+++ b/tests/idris2/reg044/Methods.idr
@@ -6,7 +6,16 @@ Eq Foo where
    C == C = True
    _ == _ = False
 
-Ord Foo where
-   A < B = True
-   B < C = True
-   _ < _ = False
+interface Read a where
+  readPrefix : String -> Maybe (a, String)
+
+  read : String -> Maybe a
+  read str = case readPrefix str of
+    Just (a, "") => pure a
+    Nothing => Nothing
+
+Read Foo where
+
+  read "A" = A
+  read "B" = B
+  read "C" = C
diff --git a/tests/idris2/reg044/expected b/tests/idris2/reg044/expected
index 6c654b065..a0e852167 100644
--- a/tests/idris2/reg044/expected
+++ b/tests/idris2/reg044/expected
@@ -1,9 +1,10 @@
 1/1: Building Methods (Methods.idr)
-Error: Missing methods in Ord: compare
+Error: Missing methods in Read: readPrefix
 
-Methods:9:1--12:17
- 09 | Ord Foo where
- 10 |    A < B = True
- 11 |    B < C = True
- 12 |    _ < _ = False
+Methods:17:1--21:15
+ 17 | Read Foo where
+ 18 | 
+ 19 |   read "A" = A
+ 20 |   read "B" = B
+ 21 |   read "C" = C