From 2c1ca7e19b42336390d125d760bcd7840b41676f Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 6 Apr 2022 20:31:38 +0200
Subject: [PATCH] improve equality somewhat

---
 src/Quox/Equal.idr | 105 ++++++++++++++++++++-------------------------
 1 file changed, 47 insertions(+), 58 deletions(-)

diff --git a/src/Quox/Equal.idr b/src/Quox/Equal.idr
index c2bdb9f..2853ca6 100644
--- a/src/Quox/Equal.idr
+++ b/src/Quox/Equal.idr
@@ -7,8 +7,8 @@ import Quox.Error
 
 
 public export
-data Error =
-  Clash  SomeTerm SomeTerm
+data Error
+= Clash  SomeTerm SomeTerm
 | ClashU Universe Universe
 | ClashQ Qty      Qty
 
@@ -35,92 +35,81 @@ parameters {auto _ : MonadThrow Error m}
 
   mutual
     private covering
-    equalTN' : DSubst d 0 -> (s, t : Term d n) ->
+    equalTN' : (s, t : Term 0 n) ->
                (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
 
-    equalTN' _ (TYPE k) (TYPE l) _ _ =
+    equalTN' (TYPE k) (TYPE l) _ _ =
       eq ClashU k l
-    equalTN' _ s@(TYPE _) t _ _ = clashT s t
+    equalTN' s@(TYPE _) t _ _ = clashT s t
 
-    equalTN' th (Pi qtm1 qty1 _ arg1 res1) (Pi qtm2 qty2 _ arg2 res2) _ _ = do
+    equalTN' (Pi qtm1 qty1 _ arg1 res1) (Pi qtm2 qty2 _ arg2 res2) _ _ = do
       eq ClashQ qtm1 qtm2
       eq ClashQ qty1 qty2
-      equalTS th arg1 arg2
-      equalTS th res1 res2
-    equalTN' _ s@(Pi {}) t _ _ = clashT s t
+      equalT0 arg1 arg2
+      equalT0 res1 res2
+    equalTN' s@(Pi {}) t _ _ = clashT s t
 
     -- [todo] eta
-    equalTN' th (Lam _ body1) (Lam _ body2) _ _ =
-      equalTS th body1 body2
-    equalTN' _ s@(Lam {}) t _ _ = clashT s t
+    equalTN' (Lam _ body1) (Lam _ body2) _ _ =
+      equalT0 body1 body2
+    equalTN' s@(Lam {}) t _ _ = clashT s t
 
-    equalTN' th (E e) (E f) ps pt = equalES th e f
-    equalTN' _ s@(E _) t _ _ = clashT s t
+    equalTN' (E e) (E f) ps pt = equalE0 e f
+    equalTN' s@(E _) t _ _ = clashT s t
 
-    equalTN' _ (CloT  {}) _ ps _ = void $ ps IsCloT
-    equalTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
+    equalTN' (CloT  {}) _ ps _ = void $ ps IsCloT
+    equalTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
 
     private covering
-    equalEN' : DSubst d 0 -> (e, f : Elim d n) ->
+    equalEN' : (e, f : Elim 0 n) ->
                (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
 
-    equalEN' _ (F x) (F y) _ _ = do
+    equalEN' (F x) (F y) _ _ = do
       eq (clashE' `on` F {d = 0, n = 0}) x y
-    equalEN' _ e@(F _) f _ _ = clashE e f
+    equalEN' e@(F _) f _ _ = clashE e f
 
-    equalEN' _ (B i) (B j) _ _ = do
+    equalEN' (B i) (B j) _ _ = do
       eq (clashE' `on` B {d = 0}) i j
-    equalEN' _ e@(B _) f _ _ = clashE e f
+    equalEN' e@(B _) f _ _ = clashE e f
 
-    equalEN' th (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
-      equalES th fun1 fun2
-      equalTS th arg1 arg2
-    equalEN' _ e@(_ :@ _) f _ _ = clashE e f
+    equalEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
+      equalE0 fun1 fun2
+      equalT0 arg1 arg2
+    equalEN' e@(_ :@ _) f _ _ = clashE e f
 
-    equalEN' th (tm1 :# ty1) (tm2 :# ty2) _ _ = do
-      equalTS th tm1 tm2
-      equalTS th ty1 ty2
-    equalEN' _ e@(_ :# _) f _ _ = clashE e f
+    equalEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
+      equalT0 tm1 tm2
+      equalT0 ty1 ty2
+    equalEN' e@(_ :# _) f _ _ = clashE e f
 
-    equalEN' _ (CloE  {}) _ pe _ = void $ pe IsCloE
-    equalEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
+    equalEN' (CloE  {}) _ pe _ = void $ pe IsCloE
+    equalEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
 
 
     private covering %inline
-    equalTN : DSubst d 0 -> NonRedexTerm d n -> NonRedexTerm d n -> m ()
-    equalTN th s t = equalTN' th s.fst t.fst s.snd t.snd
+    equalTN : NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
+    equalTN s t = equalTN' s.fst t.fst s.snd t.snd
 
     private covering %inline
-    equalEN : DSubst d 0 -> NonRedexElim d n -> NonRedexElim d n -> m ()
-    equalEN th e f = equalEN' th e.fst f.fst e.snd f.snd
+    equalEN : NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
+    equalEN e f = equalEN' e.fst f.fst e.snd f.snd
 
 
     export covering %inline
-    equalTS : DSubst d 0 -> Term d n -> Term d n -> m ()
-    equalTS th s t = equalTN th (whnfT s) (whnfT t)
+    equalT : DimEq d -> Term d n -> Term d n -> m ()
+    equalT eqs s t =
+      for_ (splits eqs) $ \th => (s /// th) `equalT0` (t /// th)
 
     export covering %inline
-    equalES : DSubst d 0 -> Elim d n -> Elim d n -> m ()
-    equalES th e f = equalEN th (whnfE e) (whnfE f)
+    equalE : DimEq d -> Elim d n -> Elim d n -> m ()
+    equalE eqs e f =
+      for_ (splits eqs) $ \th => (e /// th) `equalE0` (f /// th)
 
 
-  export covering %inline
-  equalT : DimEq d -> Term d n -> Term d n -> m ()
-  equalT eqs s t =
-    let s' = whnfT s; t' = whnfT t in
-    for_ (splits eqs) $ \th => equalTN th s' t'
+    export covering %inline
+    equalT0 : Term 0 n -> Term 0 n -> m ()
+    equalT0 s t = whnfT s `equalTN` whnfT t
 
-  export covering %inline
-  equalE : DimEq d -> Elim d n -> Elim d n -> m ()
-  equalE eqs e f =
-    let e' = whnfE e; f' = whnfE f in
-    for_ (splits eqs) $ \th => equalEN th e' f'
-
-
-  export covering %inline
-  equalT0 : Term 0 n -> Term 0 n -> m ()
-  equalT0 = equalT zeroEq
-
-  export covering %inline
-  equalE0 : Elim 0 n -> Elim 0 n -> m ()
-  equalE0 = equalE zeroEq
+    export covering %inline
+    equalE0 : Elim 0 n -> Elim 0 n -> m ()
+    equalE0 e f = whnfE e `equalEN` whnfE f