quox/lib/Quox/Typechecker.idr
2023-01-26 19:55:08 +01:00

284 lines
9.5 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Quox.Typechecker
import public Quox.Syntax
import public Quox.Typing
import public Quox.Equal
import public Control.Monad.Either
import Decidable.Decidable
import Data.SnocVect
%default total
public export
0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)
public export
0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
CanTC q = CanTC' q IsGlobal
private covering %inline
expectTYPE : CanTC' q _ m => Term q d n -> m Universe
expectTYPE s =
case whnf !ask s of
Element (TYPE l) _ => pure l
_ => throwError $ ExpectedTYPE s
private covering %inline
expectPi : CanTC' q _ m => Term q d n ->
m (q, Term q d n, ScopeTerm q d n)
expectPi ty =
case whnf !ask ty of
Element (Pi qty _ arg res) _ => pure (qty, arg, res)
_ => throwError $ ExpectedPi ty
private covering %inline
expectSig : CanTC' q _ m => Term q d n ->
m (Term q d n, ScopeTerm q d n)
expectSig ty =
case whnf !ask ty of
Element (Sig _ arg res) _ => pure (arg, res)
_ => throwError $ ExpectedSig ty
private covering %inline
expectEq : CanTC' q _ m => Term q d n ->
m (DScopeTerm q d n, Term q d n, Term q d n)
expectEq ty =
case whnf !ask ty of
Element (Eq _ ty l r) _ => pure (ty, l, r)
_ => throwError $ ExpectedEq ty
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
private %inline
popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
popQ pi = popQs [< pi]
private %inline
tail : TyContext q d (S n) -> TyContext q d n
tail = {tctx $= tail, qctx $= tail}
private %inline
weakI : IsQty q => InferResult q d n -> InferResult q d (S n)
weakI = {type $= weakT, qout $= (:< zero)}
private
lookupBound : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n
lookupBound pi VZ (MkTyContext {tctx = tctx :< ty, _}) =
InfRes {type = weakT ty, qout = (zero <$ tctx) :< pi}
lookupBound pi (VS i) ctx =
weakI $ lookupBound pi i (tail ctx)
private
lookupFree : IsQty q => CanTC q m => Name -> m (Definition q)
lookupFree x =
case lookup x !ask of
Just d => pure d
Nothing => throwError $ NotInScope x
private %inline
subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
subjMult sg qty = if isYes $ isZero qty 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
-- to either push them or parametrise the whole typechecker over ambient
-- substitutions. both of them seem like the same amount of work for the
-- computer but pushing is less work for the me
||| `check ctx sg subj ty` checks that in the context `ctx`, the term
||| `subj` has the type `ty`, with quantity `sg`. if so, returns the
||| quantities of all bound variables that it used.
export covering %inline
check : TyContext q d n -> SQty q -> Term q d n -> Term q d n ->
m (CheckResult q n)
check ctx sg subj ty =
let Element subj nc = pushSubsts subj in
check' ctx sg subj nc ty
||| `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
||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
||| and returns its type and the bound variables it used.
export covering %inline
infer : TyContext q d n -> SQty q -> Elim q d n -> m (InferResult q d n)
infer ctx sg subj =
let Element subj nc = pushSubsts subj in
infer' ctx sg subj nc
export covering
check' : TyContext q d n -> SQty q ->
(subj : Term q d n) -> (0 nc : NotClo subj) -> Term q d n ->
m (CheckResult q n)
check' ctx sg (TYPE l) _ ty = do
-- if < ' then Ψ | Γ ⊢ Type · 0 ⇐ Type ' ⊳ 𝟎
l' <- expectTYPE ty
expectEqualQ zero sg.fst
unless (l < l') $ throwError $ BadUniverse l l'
pure $ zeroFor ctx
check' ctx sg (Pi qty _ arg res) _ ty = do
l <- expectTYPE ty
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢ A · 0 ⇐ Type 𝟎
ignore $ check0 ctx arg (TYPE l)
-- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type 𝟎
case res of
TUsed res => ignore $ check0 (extendTy arg zero ctx) res (TYPE l)
TUnused res => ignore $ check0 ctx res (TYPE l)
-- then Ψ | Γ ⊢ (x : A) → B · 0 ⇐ Type 𝟎
pure $ zeroFor ctx
check' ctx sg (Lam _ body) _ ty = do
(qty, arg, res) <- expectPi ty
-- if Ψ | Γ, x · πσ : A ⊢ t · σ ⇐ B ⊳ Σ, x · σπ
qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
-- then Ψ | Γ ⊢ λx. t · σ ⇐ (x · π : A) → B ⊳ Σ
popQ (sg.fst * qty) qout
check' ctx sg (Sig _ fst snd) _ ty = do
l <- expectTYPE ty
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢ A · 0 ⇐ Type 𝟎
ignore $ check0 ctx fst (TYPE l)
-- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type 𝟎
case snd of
TUsed snd => ignore $ check0 (extendTy fst zero ctx) snd (TYPE l)
TUnused snd => ignore $ check0 ctx snd (TYPE l)
-- then Ψ | Γ ⊢ (x : A) × B · 0 ⇐ Type 𝟎
pure $ zeroFor ctx
check' ctx sg (Pair fst snd) _ ty = do
(tfst, tsnd) <- expectSig ty
-- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ₁
qfst <- check ctx sg fst tfst
let tsnd = sub1 tsnd (fst :# tfst)
-- if Ψ | Γ ⊢ t · σ ⇐ B[s] ⊳ Σ₂
qsnd <- check ctx sg snd tsnd
-- then Ψ | Γ ⊢ (s, t) · σ ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
pure $ qfst + qsnd
check' ctx sg (Eq i t l r) _ ty = do
u <- expectTYPE ty
expectEqualQ zero sg.fst
-- if Ψ, i | Γ ⊢ A · 0 ⇐ Type 𝟎
case t of
DUsed t => ignore $ check0 (extendDim ctx) t (TYPE u)
DUnused t => ignore $ check0 ctx t (TYPE u)
-- if Ψ | Γ ⊢ l · 0 ⇐ A0𝟎
ignore $ check0 ctx t.zero l
-- if Ψ | Γ ⊢ r · 0 ⇐ A1𝟎
ignore $ check0 ctx t.one r
-- then Ψ | Γ ⊢ Eq [i ⇒ A] l r ⇐ Type 𝟎
pure $ zeroFor ctx
check' ctx sg (DLam i body) _ ty = do
(ty, l, r) <- expectEq ty
-- if Ψ, i | Γ ⊢ t · σ ⇐ A ⊳ Σ
qout <- check (extendDim ctx) sg body.term ty.term
let eqs = makeDimEq ctx.dctx
-- if Ψ ⊢ t0 = l
equal !ask eqs body.zero l
-- if Ψ ⊢ t1 = r
equal !ask eqs body.one r
-- then Ψ | Γ ⊢ (λᴰi ⇒ t) · σ ⇐ Eq [i ⇒ A] l r ⊳ Σ
pure qout
check' ctx sg (E e) _ ty = do
-- if Ψ | Γ ⊢ e · σ ⇒ A' ⊳ Σ
infres <- infer ctx sg e
-- if Ψ ⊢ A' <: A
sub !ask (makeDimEq ctx.dctx) infres.type ty
-- then Ψ | Γ ⊢ e · σ ⇐ A ⊳ Σ
pure infres.qout
export covering
infer' : TyContext q d n -> SQty q ->
(subj : Elim q d n) -> (0 nc : NotClo subj) ->
m (InferResult q d n)
infer' ctx sg (F x) _ = do
-- if x · π : A {≔ s} in global context
g <- lookupFree x
-- if σ ≤ π
expectCompatQ sg.fst g.qty
-- then Ψ | Γ ⊢ x ⇒ A ⊳ 𝟎
pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
infer' ctx sg (B i) _ =
-- if x : A ∈ Γ
-- 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 funres.type
-- if Ψ | Γ ⊢ s · σ∧π ⇐ A ⊳ Σ₂
-- (0∧π = σ∧0 = 0; σ∧π = σ otherwise)
argout <- check ctx (subjMult sg qty) arg argty
-- then Ψ | Γ ⊢ f s · σ ⇒ B[s] ⊳ Σ₁ + Σ₂
pure $ InfRes {
type = sub1 res $ arg :# argty,
qout = funres.qout + argout
}
infer' ctx sg (CasePair pi pair _ ret _ _ body) _ = do
-- if 1 ≤ π
expectCompatQ one pi
-- if Ψ | Γ ⊢ pair · 1 ⇒ (x : A) × B ⊳ Σ₁
pairres <- infer ctx sone pair
ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
(tfst, tsnd) <- expectSig pairres.type
-- if Ψ | Γ, x · π : A, y · π : B ⊢ σ body ⇐ ret[(x, y)]
-- ⊳ Σ₂, x · π₁, y · π₂
-- if π₁, π₂ ≤ π
let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx
retarg = Pair (BVT 0) (BVT 1) :# (pairres.type // fromNat 2)
bodyty = ret.term // (retarg ::: shift 2)
bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
-- then Ψ | Γ ⊢ σ case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
pure $ InfRes {
type = sub1 ret pair,
qout = pi * pairres.qout + bodyout
}
infer' ctx sg (fun :% dim) _ = do
-- if Ψ | Γ ⊢ f · σ ⇒ Eq [i ⇒ A] l r ⊳ Σ
InfRes {type, qout} <- infer ctx sg fun
(ty, _, _) <- expectEq type
-- then Ψ | Γ ⊢ f p · σ ⇒ Ap ⊳ Σ
pure $ InfRes {type = dsub1 ty dim, qout}
infer' ctx sg (term :# type) _ = do
-- if Ψ | Γ ⊢ A · 0 ⇐ Type 𝟎
ignore $ check0 ctx type (TYPE UAny)
-- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ
qout <- check ctx sg term type
-- then Ψ | Γ ⊢ (s ∷ A) · σ ⇒ A ⊳ Σ
pure $ InfRes {type, qout}