From 065ebedf2de24c578a437bce9428570129e373f0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 14 Feb 2023 21:29:04 +0100
Subject: [PATCH] use DimEq directly in typing context

---
 lib/Quox/Typechecker.idr    | 14 +++-----------
 lib/Quox/Typing.idr         | 12 +++---------
 tests/Tests/Typechecker.idr |  4 ++--
 3 files changed, 8 insertions(+), 22 deletions(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 129381d..02ce914 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -62,13 +62,6 @@ subjMult : IsQty q => SQty q -> q -> SQty q
 subjMult sg pi = if isYes $ isZero pi then szero else sg
 
 
-export
-makeDimEq : DContext d -> DimEq d
-makeDimEq DNil           = zeroEq
-makeDimEq (DBind dctx)   = makeDimEq dctx :<? Nothing
-makeDimEq (DEq p q dctx) = set p q $ makeDimEq dctx
-
-
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
   -- [todo] it seems like the options here for dealing with substitutions are
@@ -174,11 +167,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     (ty, l, r) <- expectEq !ask ty
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
     qout <- check (extendDim ctx) sg body.term ty.term
-    let eqs = makeDimEq ctx.dctx
     -- if Ψ | Γ ⊢ t‹0› = l : A‹0›
-    equal eqs ctx.tctx ty.zero body.zero l
+    equal ctx.dctx ctx.tctx ty.zero body.zero l
     -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
-    equal eqs ctx.tctx ty.one body.one  r
+    equal ctx.dctx ctx.tctx ty.one body.one  r
     -- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
@@ -186,7 +178,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- infer ctx sg e
     -- if Ψ | Γ ⊢ A' <: A
-    subtype (makeDimEq ctx.dctx) ctx.tctx infres.type ty
+    subtype ctx.dctx ctx.tctx infres.type ty
     -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
     pure infres.qout
 
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 7896ed9..428f29a 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -20,12 +20,6 @@ import Generics.Derive
 %default total
 
 
-public export
-data DContext : Nat -> Type where
-  DNil  : DContext 0
-  DBind : DContext d -> DContext (S d)
-  DEq   : Dim d -> Dim d -> DContext d -> DContext d
-
 public export
 TContext : Type -> Nat -> Nat -> Type
 TContext q d = Context (Term q d)
@@ -38,7 +32,7 @@ QOutput = Context'
 public export
 record TyContext q d n where
   constructor MkTyContext
-  dctx : DContext d
+  dctx : DimEq d
   tctx : TContext q d n
 
 %name TyContext ctx
@@ -61,11 +55,11 @@ namespace TyContext
 
   export %inline
   extendDim : TyContext q d n -> TyContext q (S d) n
-  extendDim = {dctx $= DBind, tctx $= pushD}
+  extendDim = {dctx $= (:<? Nothing), tctx $= pushD}
 
   export %inline
   eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
-  eqDim p q = {dctx $= DEq p q}
+  eqDim p q = {dctx $= set p q}
 
 
 namespace QOutput
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 35c6024..2126bf3 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -70,12 +70,12 @@ parameters (label : String) (act : Lazy (M ()))
 
 
 ctx : TContext Three 0 n -> TyContext Three 0 n
-ctx = MkTyContext DNil
+ctx = MkTyContext new
 
 inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
 inferredTypeEq ctx exp got =
   catchError
-    (inj $ equalType (makeDimEq ctx.dctx) ctx.tctx exp got)
+    (inj $ equalType ctx.dctx ctx.tctx exp got)
     (\_ : Error' => throwError $ WrongInfer exp got)
 
 qoutEq : (exp, got : QOutput Three n) -> M ()