rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 2 Releases Wiki Activity

return () from check0 

since it always returns 𝟎 anyway
This commit is contained in:
rhiannon morris 2023-02-13 22:06:03 +01:00
parent fe8c224299
commit 534e0d2270
1 changed files with 17 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
lib/Quox/Typechecker.idr
View File

@ -83,8 +83,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 (CheckResult q n)
check0 ctx = check (zeroed ctx) szero
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
||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
||| and returns its type and the bound variables it used.
@ -111,30 +111,31 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
l <- expectTYPE !ask ty
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
ignore $ check0 ctx arg (TYPE l)
check0 ctx arg (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
case res of
TUsed res => ignore $ check0 (extendTy arg zero ctx) res (TYPE l)
TUnused res => ignore $ check0 ctx res (TYPE l)
TUsed res => check0 (extendTy arg zero 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
qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
let qty' = sg.fst * qty
qout <- check (extendTy arg qty' ctx) sg body.term res.term
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
popQ (sg.fst * qty) qout
popQ qty' qout
check' ctx sg (Sig _ fst snd) _ ty = do
l <- expectTYPE !ask ty
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
ignore $ check0 ctx fst (TYPE l)
check0 ctx fst (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
case snd of
TUsed snd => ignore $ check0 (extendTy fst zero ctx) snd (TYPE l)
TUnused snd => ignore $ check0 ctx snd (TYPE l)
TUsed snd => check0 (extendTy fst zero ctx) snd (TYPE l)
TUnused snd => check0 ctx snd (TYPE l)
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
pure $ zeroFor ctx
@ -153,12 +154,12 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
expectEqualQ zero sg.fst
-- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
case t of
DUsed t => ignore $ check0 (extendDim ctx) t (TYPE u)
DUnused t => ignore $ check0 ctx t (TYPE u)
DUsed t => check0 (extendDim ctx) t (TYPE u)
DUnused t => check0 ctx t (TYPE u)
-- if Ψ | Γ ⊢₀ l ⇐ A‹0›
ignore $ check0 ctx t.zero l
check0 ctx t.zero l
-- if Ψ | Γ ⊢₀ r ⇐ A‹1›
ignore $ check0 ctx t.one r
check0 ctx t.one r
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
pure $ zeroFor ctx
@ -218,7 +219,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
expectCompatQ one pi
-- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
pairres <- infer ctx sone pair
ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
(tfst, tsnd) <- expectSig !ask pairres.type
-- if Ψ | Γ, π·x : A, π·y : B ⊢ σ body ⇐ ret[(x, y)]
-- ⊳ Σ₂, π₁·x, π₂·y
@ -241,7 +242,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
infer' ctx sg (term :# type) _ = do
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
ignore $ check0 ctx type (TYPE UAny)
check0 ctx type (TYPE UAny)
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
qout <- check ctx sg term type
-- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ