From 582666a254aa03a86ccdf644c55c799887892a8e Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 21 Mar 2024 21:29:13 +0100
Subject: [PATCH] comments in infer for coercions

---
 lib/Quox/Typechecker.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index a25e3cd..681aa7c 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -479,23 +479,34 @@ mutual
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (Coe ty p q val loc) = do
+    -- if Ψ, 𝑖 | Γ ⊢₀ A ⇐ Type _
     checkType (extendDim ty.name ctx) ty.term Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A‹p/𝑖› ⊳ Σ
     qout <- checkC ctx sg val $ dsub1 ty p
+    -- then Ψ | Γ ⊢ σ · coe (𝑖 ⇒ A) @p @q s ⇒ A‹q/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty q, qout}
 
   infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1) loc) = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type _
     checkType ctx ty Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     qout <- checkC ctx sg val ty
+    -- if Ψ, 𝑗, 𝑖=0      | Γ ⊢ σ · t₀ ⇐ A ⊳ Σ₀
+    --    Ψ, 𝑗, 𝑖=0, 𝑗=p | Γ ⊢ t₀ = s ⇐ A
     let ty'  = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
         ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
         val0 = getTerm val0
     qout0 <- check ctx0 sg val0 ty'
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) sg ty' val0 val'
+    -- if Ψ, 𝑗, 𝑖=1      | Γ ⊢ σ · t₁ ⇐ A ⊳ Σ₁
+    --    Ψ, 𝑗, 𝑖=1, 𝑗=p | Γ ⊢ t₁ = s ⇐ A
     let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
         val1  = getTerm val1
     qout1 <- check ctx1 sg val1 ty'
+    -- if Σ = Σ₀ = Σ₁
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
     let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
+    -- then Ψ | Γ ⊢ comp A @p @q s @r {0 𝑗 ⇒ t₀; 1 𝑗 ⇒ t₁} ⇒ A ⊳ Σ
     pure $ InfRes {type = ty, qout = lubs ctx qouts}
 
   infer' ctx sg (TypeCase ty ret arms def loc) = do