refactor Ord to be based on compare

TODO.md

@@ -9,7 +9,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [x] for parse error, seek to col 0 token and process next decl
 - [ ] record update sugar, syntax TBD
   - I think I'm going to hold off on this for now as it requires the type to elaborate. This ends up at the head of an app, which typically is inferred. We'd need a special case somewhere that infers its argument instead.
-- [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality)
+- [x] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality)
 - [ ] Keep a `compare` function on `SortedMap` (like lean)
 - [x] keymap for monaco
 - [x] SortedMap.newt issue in `where`

aoc2024/Day13.newt

@@ -51,7 +51,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 calcCost : BigInt → Machine → Maybe BigInt
 calcCost extra (MkMachine (ax, ay) (bx, by) (px, py)) =

aoc2024/Day16.newt

@@ -72,7 +72,7 @@ dirVal East = 2
 dirVal West = 3
 
 instance Ord Dir where
-  a < b = dirVal a < dirVal b
+  compare a b = compare (dirVal a) (dirVal b)
 
 instance Eq Dir where
   a == b = dirVal a == dirVal b

aoc2024/Day17.newt

@@ -21,7 +21,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 data Machine : U where
   M : BigInt → BigInt → BigInt → List Int → Int → SnocList Int → Machine

aoc2024/Day22.newt

@@ -23,7 +23,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 infixl 7 _%_
 pfunc _%_ : BigInt → BigInt → BigInt := `(x,y) => x % y`

aoc2024/Day22b.newt

@@ -26,7 +26,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 -- base: 30s
 -- switching from tuple to int: 8 s

aoc2024/Day24.newt

@@ -18,7 +18,7 @@ instance Eq Op where
   _ == _ = False
 
 record Gate where
-  constructor GT
+  constructor MkG
   in1 : String
   in2 : String
   op : Op
@@ -49,7 +49,7 @@ parseFile text = do
     parseGate s = do
       let (in1 :: op :: in2 :: _ :: out :: Nil) = split s " " | _ => Left $ "bad gate: " ++ s
       op <- getOp op
-      Right $ GT in1 in2 op out
+      Right $ MkG in1 in2 op out
 
 
 State : U
@@ -114,10 +114,10 @@ range : Int → Int → List Int
 range a b = if a < b then a :: range (a + 1) b else Nil
 
 swapPins : String → String → Gate → Gate
-swapPins a g (GT i1 i2 op out) =
-  if out == a then GT i1 i2 op g
-  else if out == g then GT i1 i2 op a
-  else GT i1 i2 op out
+swapPins a g (MkG i1 i2 op out) =
+  if out == a then MkG i1 i2 op g
+  else if out == g then MkG i1 i2 op a
+  else MkG i1 i2 op out
 
 fail : ∀ a. String -> a
 fail msg = let x = trace "FAIL" msg in ?

aoc2024/Day6.newt

@@ -28,7 +28,7 @@ instance Eq Dir where
   a == b = show a == show b
 
 instance Ord Dir where
-  a < b = show a < show b
+  compare a b = compare (show a) (show b)
 
 Done : U
 Done = SortedMap (Point × Dir) Unit

newt/Prelude.newt

@@ -233,6 +233,7 @@ instance Concat String where
 
 pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False`
 pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? True : False`
+
 pfunc jsShow : ∀ a . a → String := `(_,a) => ''+a`
 instance Eq Int where
   a == b = jsEq a b
@@ -662,39 +663,45 @@ tail : ∀ a. List a → List a
 tail Nil = Nil
 tail (x :: xs) = xs
 
---
+data Ordering = LT | EQ | GT
+instance Eq Ordering where
+  LT == LT = True
+  EQ == EQ = True
+  GT == GT = True
+  _ == _ = False
+
+-- FIXME There is a subtle issue here with shadowing if the file defines a GT in its own namespace
+-- We end up chosing that an assigning to GT, which cause a lot of trouble.
+-- Prelude.GT is not in scope, because we've depended on the other one.
+pfunc jsCompare uses (LT EQ GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? EQ : a < b ? LT : GT`
 
 infixl 6 _<_ _<=_ _>_
 class Ord a where
-  -- isEq : Eq a
-  _<_ : a → a → Bool
+  compare : a → a → Ordering
+
+_<_ : ∀ a. {{Ord a}} -> a → a → Bool
+a < b = compare a b == LT
 
-_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
-a <= b = a == b || a < b
+_<=_ : ∀ a. {{Ord a}} → a → a → Bool
+a <= b = compare a b /= GT
 
 _>_ : ∀ a. {{Ord a}} → a → a → Bool
-a > b = b < a
+a > b = compare a b == GT
 
 search : ∀ cl. {{cl}} -> cl
 search {{x}} = x
 
 instance Ord Nat where
-  -- isEq = search
-  _ < Z = False
-  Z < S _ = True
-  S n < S m = n < m
-
+  compare Z Z = EQ
+  compare _ Z = GT
+  compare Z (S _) = LT
+  compare (S n) (S m) = compare n m
 
 instance Ord Int where
-  -- isEq = ?
-  x < y = ltInt x y
+  compare a b = jsCompare a b
 
 instance Ord Char where
-  x < y = jsLT x y
-
--- foo : ∀ a. {{Ord a}} -> a -> Bool
--- foo a = a == a
-
+  compare a b = jsCompare a b
 
 flip : ∀ a b c. (a → b → c) → (b → a → c)
 flip f b a = f a b
@@ -724,7 +731,7 @@ ite : ∀ a. Bool → a → a → a
 ite c t e = if c then t else e
 
 instance Ord String where
-  a < b = jsLT a b
+  compare a b = jsCompare a b
 
 instance Cast Int Nat where
   cast n = intToNat n
@@ -738,8 +745,10 @@ swap (a,b) = (b,a)
 instance ∀ a b. {{Eq a}} {{Eq b}} → Eq (a × b) where
   (a,b) == (c,d) = a == c && b == d
 
-instance ∀ a b. {{Eq a}} {{Ord a}} {{Ord b}} → Ord (a × b) where
-  (a,b) < (c,d) = if a == c then b < d else a < c
+instance ∀ a b. {{Ord a}} {{Ord b}} → Ord (a × b) where
+  compare (a,b) (c,d) = case compare a c of
+    EQ => compare b d
+    res => res
 
 instance ∀ a. {{Eq a}} → Eq (List a) where
   Nil == Nil = True

src/Lib/Eval.idr

@@ -1,8 +1,5 @@
 module Lib.Eval
 
--- For FC
-import Lib.Parser.Impl
-import Lib.Prettier
 import Lib.Types
 import Lib.TopContext
 
@@ -13,10 +10,6 @@ import Data.SnocList
 import Data.Vect
 import Data.SortedMap
 
--- Need to wire in the metas...
--- if it's top / ctx / IORef, I also need IO...
--- if I want errors, I need m anyway.  I've already got an error down there.
-
 export
 eval : Env -> Mode -> Tm -> M Val
 

src/Lib/Parser.idr

@@ -1,19 +1,11 @@
 module Lib.Parser
-import Lib.Types
-import Debug.Trace
-import Data.String
-
--- app: foo {a} a b
--- lam: λ {A} {b : A} (c : Blah) d e f => something
--- lam: \ {A} {b : A} (c : Blah) d e f => something
--- pi: (A : Set) -> {b : A} -> (c : Foo b) -> c -> bar d
--- pi: (A B : Set) {b : A} -> (c : Foo b) -> c -> bar d
 
-import Lib.Token
+import Data.Maybe
+import Data.String
 import Lib.Parser.Impl
 import Lib.Syntax
-import Data.List
-import Data.Maybe
+import Lib.Token
+import Lib.Types
 
 ident = token Ident <|> token MixFix
 
@@ -104,10 +96,6 @@ pArg = do
 
 AppSpine = List (Icit,FC,Raw)
 
--- helper for debugging
-traceM : Monad m => String -> m ()
-traceM msg = trace msg $ pure ()
-
 pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
 pratt ops prec stop left spine = do
   (left, spine) <- runPrefix stop left spine