quox/lib/Quox/Typechecker.idr

516 lines
18 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.Typing
import public Quox.Equal
import Data.List
import Data.SnocVect
import Data.List1
import Quox.EffExtra
%default total
public export
0 TCEff : List (Type -> Type)
TCEff = [ErrorEff, DefsReader, CurNSReader]
public export
0 TC : Type -> Type
TC = Eff TCEff
export
runTC : Mods -> Definitions -> TC a -> Either Error a
runTC ns defs =
extract . runExcept . runReaderAt DEFS defs . runReaderAt NS ns
export
popQs : Has ErrorEff fs => QOutput s -> QOutput (s + n) -> Eff fs (QOutput n)
popQs [<] qout = pure qout
popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
export %inline
popQ : Has ErrorEff fs => Qty -> QOutput (S n) -> Eff fs (QOutput n)
popQ pi = popQs [< pi]
export
lubs1 : List1 (QOutput n) -> Maybe (QOutput n)
lubs1 ([<] ::: _) = Just [<]
lubs1 ((qs :< p) ::: pqs) =
let (qss, ps) = unzip $ map unsnoc pqs in
[|lubs1 (qs ::: qss) :< foldlM lub p ps|]
export
lubs : TyContext d n -> List (QOutput n) -> Maybe (QOutput n)
lubs ctx [] = Just $ zeroFor ctx
lubs ctx (x :: xs) = lubs1 $ x ::: xs
||| context extension with no names or quantities
private
CtxExtension0' : Nat -> Nat -> Nat -> Type
CtxExtension0' s d n = Context (Term d . (+ n)) s
private
addNames0 : Context (Term d . (+ n)) s -> NContext s -> CtxExtension d n (s + n)
addNames0 [<] [<] = [<]
addNames0 (ts :< t) (xs :< x) = addNames0 ts xs :< (Zero, x, t)
export
typecaseTel : (k : TyConKind) -> Universe -> CtxExtension0' (arity k) d n
typecaseTel k u = case k of
KTYPE => [<]
-- A : ★ᵤ, B : 0.A → ★ᵤ
KPi => [< TYPE u, Arr Zero (BVT 0) (TYPE u)]
KSig => [< TYPE u, Arr Zero (BVT 0) (TYPE u)]
KEnum => [<]
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
KEq => [< TYPE u, TYPE u, Eq0 (TYPE u) (BVT 1) (BVT 0), BVT 2, BVT 2]
KNat => [<]
-- A : ★ᵤ
KBOX => [< TYPE u]
mutual
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
|||
||| `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.
|||
||| if the dimension context is inconsistent, then return `Nothing`, without
||| doing any further work.
export covering %inline
check : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
TC (CheckResult ctx.dctx n)
check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
||| "Ψ | Γ ⊢₀ s ⇐ A"
|||
||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
export covering %inline
check0 : TyContext d n -> Term d n -> Term d n -> TC ()
check0 ctx tm ty = ignore $ check ctx szero tm ty
-- the output will always be 𝟎 because the subject quantity is 0
||| `check`, assuming the dimension context is consistent
export covering %inline
checkC : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
TC (CheckResult' n)
checkC ctx sg subj ty =
wrapErr (WhileChecking ctx sg.fst subj ty) $
let Element subj nc = pushSubsts subj in
check' ctx sg subj ty
||| "Ψ | Γ ⊢₀ s ⇐ ★ᵢ"
|||
||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the
||| universe doesn't matter, only that a term is _a_ type, so it is optional.
export covering %inline
checkType : TyContext d n -> Term d n -> Maybe Universe -> TC ()
checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
export covering %inline
checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> TC ()
checkTypeC ctx subj l =
wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l
export covering %inline
checkTypeNoWrap : TyContext d n -> Term d n -> Maybe Universe -> TC ()
checkTypeNoWrap ctx subj l =
let Element subj nc = pushSubsts subj in
checkType' ctx subj l
||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ"
|||
||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
||| and returns its type and the bound variables it used.
|||
||| if the dimension context is inconsistent, then return `Nothing`, without
||| doing any further work.
export covering %inline
infer : (ctx : TyContext d n) -> SQty -> Elim d n ->
TC (InferResult ctx.dctx d n)
infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
||| `infer`, assuming the dimension context is consistent
export covering %inline
inferC : (ctx : TyContext d n) -> SQty -> Elim d n ->
TC (InferResult' d n)
inferC ctx sg subj =
wrapErr (WhileInferring ctx sg.fst subj) $
let Element subj nc = pushSubsts subj in
infer' ctx sg subj
private covering
toCheckType : TyContext d n -> SQty ->
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
TC (CheckResult' n)
toCheckType ctx sg t ty = do
u <- expectTYPE !ns !defs ctx ty
expectEqualQ Zero sg.fst
checkTypeNoWrap ctx t (Just u)
pure $ zeroFor ctx
private covering
check' : TyContext d n -> SQty ->
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
TC (CheckResult' n)
check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
check' ctx sg (Lam body) ty = do
(qty, arg, res) <- expectPi !ns !defs ctx ty
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ
let qty' = sg.fst * qty
qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
popQ qty' qout
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
check' ctx sg (Pair fst snd) ty = do
(tfst, tsnd) <- expectSig !ns !defs ctx ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
qfst <- checkC ctx sg fst tfst
let tsnd = sub1 tsnd (fst :# tfst)
-- if Ψ | Γ ⊢ σ · t ⇐ B[s] ⊳ Σ₂
qsnd <- checkC ctx sg snd tsnd
-- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
pure $ qfst + qsnd
check' ctx sg t@(Enum _) ty = toCheckType ctx sg t ty
check' ctx sg (Tag t) ty = do
tags <- expectEnum !ns !defs ctx ty
-- if t ∈ ts
unless (t `elem` tags) $ throw $ TagNotIn t tags
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
pure $ zeroFor ctx
check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
check' ctx sg (DLam body) ty = do
(ty, l, r) <- expectEq !ns !defs ctx ty
let ctx' = extendDim body.name ctx
ty = ty.term
body = body.term
-- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
qout <- checkC ctx' sg body ty
-- if Ψ, i, i = 0 | Γ ⊢ t = l : A
equal (eqDim (BV 0) (K Zero) ctx') ty body (dweakT 1 l)
-- if Ψ, i, i = 1 | Γ ⊢ t = r : A
equal (eqDim (BV 0) (K One) ctx') ty body (dweakT 1 r)
-- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
pure qout
check' ctx sg Nat ty = toCheckType ctx sg Nat ty
check' ctx sg Zero ty = do
expectNat !ns !defs ctx ty
pure $ zeroFor ctx
check' ctx sg (Succ n) ty = do
expectNat !ns !defs ctx ty
checkC ctx sg n Nat
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
check' ctx sg (Box val) ty = do
(q, ty) <- expectBOX !ns !defs ctx ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
valout <- checkC ctx sg val ty
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
pure $ q * valout
check' ctx sg (E e) ty = do
-- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
infres <- inferC ctx sg e
-- if Ψ | Γ ⊢ A' <: A
subtype ctx infres.type ty
-- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
pure infres.qout
private covering
checkType' : TyContext d n ->
(subj : Term d n) -> (0 nc : NotClo subj) =>
Maybe Universe -> TC ()
checkType' ctx (TYPE k) u = do
-- if 𝓀 < then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type
case u of
Just l => unless (k < l) $ throw $ BadUniverse k l
Nothing => pure ()
checkType' ctx (Pi qty arg res) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
checkTypeC ctx arg u
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
checkTypeScope ctx arg res u
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type
checkType' ctx t@(Lam {}) u =
throw $ NotType ctx t
checkType' ctx (Sig fst snd) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
checkTypeC ctx fst u
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
checkTypeScope ctx fst snd u
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type
checkType' ctx t@(Pair {}) u =
throw $ NotType ctx t
checkType' ctx (Enum _) u = pure ()
-- Ψ | Γ ⊢₀ {ts} ⇐ Type
checkType' ctx t@(Tag {}) u =
throw $ NotType ctx t
checkType' ctx (Eq t l r) u = do
-- if Ψ, i | Γ ⊢₀ A ⇐ Type
case t.body of
Y t' => checkTypeC (extendDim t.name ctx) t' u
N t' => checkTypeC ctx t' u
-- if Ψ | Γ ⊢₀ l ⇐ A0
check0 ctx l t.zero
-- if Ψ | Γ ⊢₀ r ⇐ A1
check0 ctx r t.one
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type
checkType' ctx t@(DLam {}) u =
throw $ NotType ctx t
checkType' ctx Nat u = pure ()
checkType' ctx Zero u = throw $ NotType ctx Zero
checkType' ctx t@(Succ _) u = throw $ NotType ctx t
checkType' ctx (BOX q ty) u = checkType ctx ty u
checkType' ctx t@(Box _) u = throw $ NotType ctx t
checkType' ctx (E e) u = do
-- if Ψ | Γ ⊢₀ E ⇒ Type
infres <- inferC ctx szero e
-- if Ψ | Γ ⊢ Type <: Type 𝓀
case u of
Just u => subtype ctx infres.type (TYPE u)
Nothing => ignore $
expectTYPE !ns !defs ctx infres.type
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
private covering
check0ScopeN : {s : Nat} ->
TyContext d n -> CtxExtension0' s d n ->
ScopeTermN s d n -> Term d n -> TC ()
check0ScopeN ctx ext (S _ (N body)) ty = check0 ctx body ty
check0ScopeN ctx ext (S names (Y body)) ty =
check0 (extendTyN (addNames0 ext names) ctx) body (weakT s ty)
private covering
check0Scope : TyContext d n -> Term d n ->
ScopeTerm d n -> Term d n -> TC ()
check0Scope ctx t = check0ScopeN ctx [< t]
private covering
checkTypeScopeN : TyContext d n -> CtxExtension0' s d n ->
ScopeTermN s d n -> Maybe Universe -> TC ()
checkTypeScopeN ctx ext (S _ (N body)) u = checkType ctx body u
checkTypeScopeN ctx ext (S names (Y body)) u =
checkType (extendTyN (addNames0 ext names) ctx) body u
private covering
checkTypeScope : TyContext d n -> Term d n ->
ScopeTerm d n -> Maybe Universe -> TC ()
checkTypeScope ctx s = checkTypeScopeN ctx [< s]
private covering
infer' : TyContext d n -> SQty ->
(subj : Elim d n) -> (0 nc : NotClo subj) =>
TC (InferResult' d n)
infer' ctx sg (F x) = do
-- if π·x : A {≔ s} in global context
g <- lookupFree !ns x !defs
-- if σ ≤ π
expectCompatQ sg.fst g.qty.fst
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
let Val d = ctx.dimLen; Val n = ctx.termLen
pure $ InfRes {type = g.type, qout = zeroFor ctx}
infer' ctx sg (B i) =
-- if x : A ∈ Γ
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
pure $ lookupBound sg.fst i ctx.tctx
where
lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
lookupBound pi VZ (ctx :< type) =
InfRes {type = weakT 1 type, qout = zeroFor ctx :< pi}
lookupBound pi (VS i) (ctx :< _) =
let InfRes {type, qout} = lookupBound pi i ctx in
InfRes {type = weakT 1 type, qout = qout :< Zero}
infer' ctx sg (fun :@ arg) = do
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
funres <- inferC ctx sg fun
(qty, argty, res) <- expectPi !ns !defs ctx funres.type
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
argout <- checkC 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
-- no check for 1 ≤ π, since pairs have a single constructor.
-- e.g. at 0 the components are also 0 in the body
--
-- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
pairres <- inferC ctx sg pair
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
(tfst, tsnd) <- expectSig !ns !defs ctx pairres.type
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-- with ρ₁, ρ₂ ≤ πσ
let [< x, y] = body.names
pisg = pi * sg.fst
bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
bodyty = substCasePairRet pairres.type ret
bodyout <- checkC bodyctx sg body.term bodyty >>= popQs [< pisg, pisg]
-- then Ψ | Γ ⊢ σ · caseπ ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
pure $ InfRes {
type = sub1 ret pair,
qout = pi * pairres.qout + bodyout
}
infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t
ttags <- expectEnum !ns !defs ctx tres.type
-- if 1 ≤ π, OR there is only zero or one option
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ One pi
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
checkTypeC (extendTy Zero ret.name tres.type ctx) ret.term Nothing
-- if for each "a ⇒ s" in arms,
-- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σᵢ
-- with Σ₂ = lubs Σᵢ
let arms = SortedMap.toList arms
let armTags = SortedSet.fromList $ map fst arms
unless (ttags == armTags) $ throw $ BadCaseEnum ttags armTags
armres <- for arms $ \(a, s) =>
checkC ctx sg s (sub1 ret (Tag a :# tres.type))
let Just armout = lubs ctx armres
| _ => throw $ BadQtys "case arms" ctx $
zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
pure $ InfRes {
type = sub1 ret t,
qout = pi * tres.qout + armout
}
infer' ctx sg (CaseNat pi pi' n ret zer suc) = do
-- if 1 ≤ π
expectCompatQ One pi
-- if Ψ | Γ ⊢ σ · n ⇒ ⊳ Σn
nres <- inferC ctx sg n
expectNat !ns !defs ctx nres.type
-- if Ψ | Γ, n : ⊢₀ A ⇐ Type
checkTypeC (extendTy Zero ret.name Nat ctx) ret.term Nothing
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ /n] ⊳ Σz
zerout <- checkC ctx sg zer (sub1 ret (Zero :# Nat))
-- if Ψ | Γ, n : , ih : A ⊢ σ · suc ⇐ A[succ p ∷ /n] ⊳ Σs, ρ₁.p, ρ₂.ih
-- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
let [< p, ih] = suc.names
pisg = pi * sg.fst
sucCtx = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
sucType = substCaseSuccRet ret
sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
expectCompatQ qih (pi' * sg.fst)
-- [fixme] better error here
expectCompatQ (qp + qih) pisg
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
pure $ InfRes {
type = sub1 ret n,
qout = pi * nres.qout + zerout + Any * sucout
}
infer' ctx sg (CaseBox pi box ret body) = do
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
boxres <- inferC ctx sg box
(q, ty) <- expectBOX !ns !defs ctx boxres.type
-- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
-- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
-- with ς ≤ ρπσ
let qpisg = q * pi * sg.fst
bodyCtx = extendTy qpisg body.name ty ctx
bodyType = substCaseBoxRet ty ret
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
pure $ InfRes {
type = sub1 ret box,
qout = boxres.qout + bodyout
}
infer' ctx sg (fun :% dim) = do
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
InfRes {type, qout} <- inferC ctx sg fun
ty <- fst <$> expectEq !ns !defs ctx type
-- then Ψ | Γ ⊢ σ · f p ⇒ Ap/𝑖 ⊳ Σ
pure $ InfRes {type = dsub1 ty dim, qout}
infer' ctx sg (Coe (S [< i] ty) p q val) = do
let ty = ty.term
checkType (extendDim i ctx) ty Nothing
qout <- checkC ctx sg val (ty // one p)
pure $ InfRes {type = ty // one q, qout}
infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1)) = do
checkType ctx ty Nothing
qout <- checkC ctx sg val ty
let ty' = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
ctx0 = extendDim j0 $ eqDim r (K Zero) ctx
val0 = val0.term
qout0 <- check ctx0 sg val0 ty'
equal (eqDim (BV 0) p' ctx0) ty' val0 val'
let ctx1 = extendDim j0 $ eqDim r (K One) ctx
val1 = val1.term
qout1 <- check ctx1 sg val1 ty'
equal (eqDim (BV 0) p' ctx1) ty' val1 val'
let qout0' = toMaybe $ map (, val0 // one p) qout0
qout1' = toMaybe $ map (, val1 // one p) qout1
qouts = (qout, val) :: catMaybes [qout0', qout1']
let Just qout = lubs ctx $ map fst qouts
| Nothing => throw $ BadQtys "composition" ctx qouts
pure $ InfRes {type = ty, qout}
infer' ctx sg (TypeCase ty ret arms def) = do
-- if σ = 0
expectEqualQ Zero sg.fst
-- if Ψ, Γ ⊢₀ e ⇒ Type u
u <- expectTYPE !ns !defs ctx . type =<< inferC ctx szero ty
-- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
checkTypeC ctx ret Nothing
-- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
for_ allKinds $ \k =>
for_ (lookupPrecise k arms) $ \(S names t) =>
check0 (extendTyN (addNames0 (typecaseTel k u) names) ctx)
t.term (weakT (arity k) ret)
-- then Ψ, Γ ⊢₀ type-case ⋯ ⇒ C
pure $ InfRes {type = ret, qout = zeroFor ctx}
infer' ctx sg (term :# type) = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
checkTypeC ctx type Nothing
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
qout <- checkC ctx sg term type
-- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ
pure $ InfRes {type, qout}