From ef8b8b0da39c3da94f159e366ce341351f87e4ab Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 10 Jan 2023 00:08:47 +0100
Subject: [PATCH] index Var.Compare by compare

i may go back on this if it's too annoying
---
 lib/Quox/Syntax/DimEq.idr | 13 ++++++++-----
 lib/Quox/Syntax/Var.idr   | 18 +++++++++---------
 2 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index e8b9bdf..b6c2686 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -104,10 +104,10 @@ mutual
 
   export %inline
   setVar : (i, j : Var d) -> DimEq' d -> DimEq d
-  setVar i j eqs = case compareP i j of
-    IsLT lt => setVar' i j lt eqs
-    IsEQ    => C eqs
-    IsGT gt => setVar' j i gt eqs
+  setVar i j eqs with (compareP i j) | (compare i.nat j.nat)
+    setVar i j eqs | IsLT lt | LT = setVar' i j lt eqs
+    setVar i i eqs | IsEQ    | EQ = C eqs
+    setVar i j eqs | IsGT gt | GT = setVar' j i gt eqs
 
 
 export %inline
@@ -166,7 +166,10 @@ export
 setSelf p ZeroIsOne = Refl
 setSelf (K Zero) (C eqs) = Refl
 setSelf (K One)  (C eqs) = Refl
-setSelf (B i)    (C eqs) = rewrite comparePSelf i in Refl
+setSelf (B i)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
+  _ | IsLT lt | LT = absurd lt
+  _ | IsEQ    | EQ = Refl
+  _ | IsGT gt | GT = absurd gt
 
 
 -- [todo] "well formed" dimeqs
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index 0d901e6..4a19a0a 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -172,34 +172,34 @@ isLT (VS i) (VS j) with (isLT i j)
 
 
 public export
-data Compare : (i, j : Var n) -> Type where
-  IsLT : (lt : i `LT` j) -> Compare i j
-  IsEQ :                    Compare i i
-  IsGT : (gt : i `GT` j) -> Compare i j
+data Compare : (i, j : Var n) -> Ordering -> Type where
+  IsLT : (lt : i `LT` j) -> Compare i j LT
+  IsEQ :                    Compare i i EQ
+  IsGT : (gt : i `GT` j) -> Compare i j GT
 %name Compare cmp
 
 export
-compareS : Compare i j -> Compare (VS i) (VS j)
+compareS : Compare i j o -> Compare (VS i) (VS j) o
 compareS (IsLT lt) = IsLT (LTS lt)
 compareS IsEQ      = IsEQ
 compareS (IsGT gt) = IsGT (LTS gt)
 
 export
-compareP : (i, j : Var n) -> Compare i j
+compareP : (i, j : Var n) -> Compare i j (compare i j)
 compareP VZ     VZ     = IsEQ
 compareP VZ     (VS j) = IsLT LTZ
 compareP (VS i) VZ     = IsGT LTZ
 compareP (VS i) (VS j) = compareS $ compareP i j
 
 export
-0 compareSelf : (c : Compare i i) -> c = IsEQ
+0 compareSelf : Compare i i o -> o = EQ
 compareSelf (IsLT lt) = absurd lt
 compareSelf IsEQ      = Refl
 compareSelf (IsGT gt) = absurd gt
 
 export
-0 comparePSelf : (i : Var n) -> compareP i i = IsEQ
-comparePSelf i = compareSelf {}
+0 comparePSelf : (i : Var n) -> Compare i i EQ
+comparePSelf i = rewrite sym $ compareNatDiag i.nat in compareP i i
 
 
 public export