From c40e6a60ff19c176ba8de375f1a1aa17e47c2f8c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 14 Feb 2023 21:14:47 +0100
Subject: [PATCH] remove input qctx since it isn't used

---
 lib/Quox/Typechecker.idr    | 46 +++++++++++++++++++++----------------
 lib/Quox/Typing.idr         | 40 +++++++++++---------------------
 tests/Tests/Typechecker.idr | 25 ++++++++------------
 3 files changed, 48 insertions(+), 63 deletions(-)

diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index b76ba98..129381d 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -23,8 +23,8 @@ CanTC q = CanTC' q IsGlobal
 private
 popQs : HasErr q m => IsQty q =>
         SnocVect s q -> QOutput q (s + n) -> m (QOutput q n)
-popQs [<]         qctx         = pure qctx
-popQs (pis :< pi) (qctx :< rh) = do expectCompatQ rh pi; popQs pis qctx
+popQs [<]         qout         = pure qout
+popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
 private %inline
 popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
@@ -34,7 +34,7 @@ popQ pi = popQs [< pi]
 
 private %inline
 tail : TyContext q d (S n) -> TyContext q d n
-tail = {tctx $= tail, qctx $= tail}
+tail = {tctx $= tail}
 
 
 private %inline
@@ -48,13 +48,18 @@ lookupBound pi VZ (MkTyContext {tctx = tctx :< ty, _}) =
 lookupBound pi (VS i) ctx =
   weakI $ lookupBound pi i (tail ctx)
 
-private
+private %inline
 lookupFree : CanTC' q g m => Name -> m (Definition' q g)
 lookupFree x = lookupFree' !ask x
 
+||| ``sg `subjMult` pi`` is zero if either argument is, otherwise it
+||| is equal to `sg`. (written as "σ ⨴ π" to emphasise its left bias.)
+|||
+||| only certain quantities can occur for a typing judgement to avoid losing
+||| subject reduction [@qtt, §2.3], which is why this is not just `sg*pi`.
 private %inline
-subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
-subjMult sg qty = if isYes $ isZero qty then szero else sg
+subjMult : IsQty q => SQty q -> q -> SQty q
+subjMult sg pi = if isYes $ isZero pi then szero else sg
 
 
 export
@@ -84,7 +89,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   ||| `check0 ctx subj ty` checks a term in a zero context.
   export covering %inline
   check0 : TyContext q d n -> Term q d n -> Term q d n -> m ()
-  check0 ctx tm ty = ignore $ check (zeroed ctx) szero tm ty
+  check0 ctx tm ty = ignore $ check ctx szero tm ty
+    -- the output will always be 𝟎 because the subject quantity is 0
 
   ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
   ||| and returns its type and the bound variables it used.
@@ -114,16 +120,17 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     check0 ctx arg (TYPE l)
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case res of
-      TUsed   res => check0 (extendTy arg zero ctx) res (TYPE l)
+      TUsed   res => check0 (extendTy arg ctx) res (TYPE l)
       TUnused res => check0 ctx res (TYPE l)
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
     pure $ zeroFor ctx
 
   check' ctx sg (Lam _ body) _ ty = do
     (qty, arg, res) <- expectPi !ask ty
-    -- if Ψ | Γ, πσ·x : A ⊢ σ · t ⇐ B ⊳ Σ, σπ·x
+    -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
+    -- with ρ ≤ σπ
     let qty' = sg.fst * qty
-    qout <- check (extendTy arg qty' ctx) sg body.term res.term
+    qout <- check (extendTy arg ctx) sg body.term res.term
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ qty' qout
 
@@ -134,7 +141,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     check0 ctx fst (TYPE l)
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case snd of
-      TUsed   snd => check0 (extendTy fst zero ctx) snd (TYPE l)
+      TUsed   snd => check0 (extendTy fst ctx) snd (TYPE l)
       TUnused snd => check0 ctx snd (TYPE l)
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
     pure $ zeroFor ctx
@@ -189,7 +196,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
            m (InferResult q d n)
 
   infer' ctx sg (F x) _ = do
-    -- if x · π : A {≔ s} in global context
+    -- if π·x : A {≔ s} in global context
     g <- lookupFree x
     -- if σ ≤ π
     expectCompatQ sg.fst g.qty
@@ -198,15 +205,15 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   infer' ctx sg (B i) _ =
     -- if x : A ∈ Γ
-    -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ · x, 𝟎)
+    -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
     pure $ lookupBound sg.fst i ctx
 
   infer' ctx sg (fun :@ arg) _ = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- infer ctx sg fun
     (qty, argty, res) <- expectPi !ask funres.type
-    -- if Ψ | Γ ⊢ σ∧π · s ⇐ A ⊳ Σ₂
-    --   (0∧π = σ∧0 = 0; σ∧π = σ otherwise)
+    -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
+    --   (σ ⨴ 0 = 0; σ ⨴ π = σ otherwise)
     argout <- check ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
     pure $ InfRes {
@@ -219,12 +226,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     expectCompatQ one pi
     -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
     pairres <- infer ctx sone pair
-    check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
+    check0 (extendTy pairres.type ctx) ret.term (TYPE UAny)
     (tfst, tsnd) <- expectSig !ask pairres.type
-    -- if Ψ | Γ, π·x : A, π·y : B ⊢ σ body ⇐ ret[(x, y)]
-    --      ⊳ Σ₂, π₁·x, π₂·y
-    -- with π₁, π₂ ≤ π
-    let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx
+    -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ ret[(x, y)] ⊳ Σ₂, ρ₁·x, ρ₂·y
+    -- with ρ₁, ρ₂ ≤ π
+    let bodyctx = extendTyN [< tfst, tsnd.term] ctx
         bodyty  = substCasePairRet pairres.type ret
     bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index b955654..7896ed9 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -30,13 +30,9 @@ public export
 TContext : Type -> Nat -> Nat -> Type
 TContext q d = Context (Term q d)
 
-public export
-QContext : Type -> Nat -> Type
-QContext = Context'
-
 public export
 QOutput : Type -> Nat -> Type
-QOutput = QContext
+QOutput = Context'
 
 
 public export
@@ -44,55 +40,45 @@ record TyContext q d n where
   constructor MkTyContext
   dctx : DContext d
   tctx : TContext q d n
-  qctx : QContext q n
 
 %name TyContext ctx
 
 
 namespace TContext
-  export
+  export %inline
   pushD : TContext q d n -> TContext q (S d) n
   pushD tel = map (/// shift 1) tel
 
-  export
-  zeroed : IsQty q => TyContext q d n -> TyContext q d n
-  zeroed = {qctx $= map (const zero)}
-
-
 namespace TyContext
-  export
-  extendTyN : Telescope (\n => (Term q d n, q)) from to ->
+  export %inline
+  extendTyN : Telescope (Term q d) from to ->
               TyContext q d from -> TyContext q d to
-  extendTyN ss = {tctx $= (. map fst ss), qctx $= (. map snd ss)}
+  extendTyN ss = {tctx $= (. ss)}
 
-  export
-  extendTy : Term q d n -> q -> TyContext q d n -> TyContext q d (S n)
-  extendTy s rho = extendTyN [< (s, rho)]
+  export %inline
+  extendTy : Term q d n -> TyContext q d n -> TyContext q d (S n)
+  extendTy s = extendTyN [< s]
 
-  export
+  export %inline
   extendDim : TyContext q d n -> TyContext q (S d) n
   extendDim = {dctx $= DBind, tctx $= pushD}
 
-  export
+  export %inline
   eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
   eqDim p q = {dctx $= DEq p q}
 
 
 namespace QOutput
   parameters {auto _ : IsQty q}
-    export
+    export %inline
     (+) : QOutput q n -> QOutput q n -> QOutput q n
     (+) = zipWith (+)
 
-    export
+    export %inline
     (*) : q -> QOutput q n -> QOutput q n
     (*) pi = map (pi *)
 
-    export
-    zero : {n : Nat} -> QOutput q n
-    zero = pure zero
-
-    export
+    export %inline
     zeroFor : TyContext q _ n -> QOutput q n
     zeroFor ctx = zero <$ ctx.tctx
 
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 6aead68..35c6024 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -69,13 +69,8 @@ parameters (label : String) (act : Lazy (M ()))
   testTCFail = testThrows label (const True) $ runReaderT globals act
 
 
-ctxWith : DContext d -> Context (\i => (Term Three d i, Three)) n ->
-          TyContext Three d n
-ctxWith dctx tqctx =
-  let (tctx, qctx) = unzip tqctx in MkTyContext {dctx, tctx, qctx}
-
-ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n
-ctx = ctxWith DNil
+ctx : TContext Three 0 n -> TyContext Three 0 n
+ctx = MkTyContext DNil
 
 inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
 inferredTypeEq ctx exp got =
@@ -170,17 +165,15 @@ tests = "typechecker" :- [
   ],
 
   "bound vars" :- [
-    testTC "1·x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
-      inferAsQ {n = 1} (ctx [< (FT "A", one)]) sone
+    testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
+      inferAsQ {n = 1} (ctx [< FT "A"]) sone
         (BV 0) (FT "A") [< one],
-    testTC "1·x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
-      checkQ {n = 1} (ctx [< (FT "A", one)]) sone (BVT 0) (FT "A") [< one],
+    testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
+      checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one],
     note "f2 : A ⊸ A ⊸ A",
-    testTC "ω·x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
-      inferAsQ {n = 1} (ctx [< (FT "A", Any)]) sone
-        (F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any],
-    note #"("0·x : A ⊢ 1 · x ⇒ A" won't fail because"#,
-    note  " a var's quantity is only checked once it leaves scope)"
+    testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
+      inferAsQ {n = 1} (ctx [< FT "A"]) sone
+        (F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any]
   ],
 
   "lambda" :- [