From e4a20cc632d745ecee879daf69ac45d86c198e48 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 20 May 2023 21:38:23 +0200
Subject: [PATCH] remove redundancy in equality check

---
 lib/Quox/Equal.idr | 21 ++++-----------------
 1 file changed, 4 insertions(+), 17 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 50d2d01..abd4d66 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -373,17 +373,6 @@ parameters (defs : Definitions)
       -- has been inlined by whnf
       Elim.compare0 ctx e f
 
-    --  Ψ | Γ ⊢₀ e ⇒ Eq [𝑖 ⇒ A] s t
-    -- -----------------------------
-    --  Ψ | Γ ⊢ e @0 = s ⇒ A[0/𝑖]
-    --  Ψ | Γ ⊢ e @1 = s ⇒ A[1/𝑖]
-    private covering
-    replaceEnd : EqContext n ->
-                 (e : Elim 0 n) -> Loc -> DimConst -> Loc ->
-                 (0 ne : NotRedex defs e) -> Equal_ (Elim 0 n)
-    replaceEnd ctx e eloc p ploc ne = do
-      (ty, l, r) <- expectEq defs ctx eloc !(computeElimTypeE defs ctx e)
-      pure $ Ann (ends l r p) (dsub1 ty (K p ploc)) eloc
 
     namespace Elim
       -- [fixme] the following code ends up repeating a lot of work in the
@@ -408,12 +397,6 @@ parameters (defs : Definitions)
                   (e, f : Elim 0 n) ->
                   (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
                   Equal_ ()
-      -- replace applied equalities with the appropriate end first
-      -- (see `replaceEnd`)
-      compare0' ctx (DApp e (K p ploc) loc) f ne nf =
-        compare0 ctx !(replaceEnd ctx e loc p ploc $ noOr1 ne) f
-      compare0' ctx e (DApp f (K q qloc) loc) ne nf =
-        compare0 ctx e !(replaceEnd ctx f loc q qloc $ noOr1 nf)
 
       compare0' ctx e@(F x {}) f@(F y {}) _ _ =
         unless (x == y) $ clashE e.loc ctx e f
@@ -523,6 +506,10 @@ parameters (defs : Definitions)
           expectEqualQ eloc epi fpi
       compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
 
+      -- all dim apps replaced with ends by whnf
+      compare0' _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
+      compare0' _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
+
       --  Ψ | Γ ⊢ s <: t : B
       -- --------------------------------
       --  Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B