quox/lib/Quox/Typechecker.idr

288 lines
9.7 KiB
Idris
Raw Normal View History

2022-04-23 18:21:30 -04:00
module Quox.Typechecker
import public Quox.Typing
import public Quox.Equal
2022-04-23 18:21:30 -04:00
%default total
2023-01-20 20:34:28 -05:00
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
2022-04-23 18:21:30 -04:00
2023-01-26 13:54:46 -05:00
private
popQs : HasErr q m => IsQty q =>
2023-02-19 11:51:44 -05:00
QOutput q s -> QOutput q (s + n) -> m (QOutput q n)
2023-02-14 15:14:47 -05:00
popQs [<] qout = pure qout
popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
2022-04-23 18:21:30 -04:00
private %inline
2023-01-26 13:54:46 -05:00
popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
popQ pi = popQs [< pi]
2022-04-23 18:21:30 -04:00
2023-01-08 14:44:25 -05:00
parameters {auto _ : IsQty q} {auto _ : CanTC q m}
mutual
2023-02-19 11:04:57 -05:00
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
|||
2023-01-20 20:34:28 -05:00
||| `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.
2023-02-19 11:51:44 -05:00
|||
||| if the dimension context is inconsistent, then return `Nothing`, without
||| doing any further work.
2022-04-23 18:21:30 -04:00
export covering %inline
2023-02-19 11:51:44 -05:00
check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
m (CheckResult ctx.dctx q n)
2023-02-20 15:38:47 -05:00
check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
2022-04-23 18:21:30 -04:00
2023-02-19 11:04:57 -05:00
||| "Ψ | Γ ⊢₀ s ⇐ A"
|||
||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
2023-01-26 13:54:46 -05:00
export covering %inline
check0 : TyContext q d n -> Term q d n -> Term q d n -> m ()
2023-02-14 15:14:47 -05:00
check0 ctx tm ty = ignore $ check ctx szero tm ty
-- the output will always be 𝟎 because the subject quantity is 0
2023-01-26 13:54:46 -05:00
2023-02-19 11:51:44 -05:00
||| `check`, assuming the dimension context is consistent
export covering %inline
checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
m (CheckResult' q n)
checkC ctx sg subj ty =
2023-02-19 11:54:39 -05:00
wrapErr (WhileChecking ctx sg.fst subj ty) $
let Element subj nc = pushSubsts subj in
2023-02-20 15:42:21 -05:00
check' ctx sg subj ty
2023-02-19 11:51:44 -05:00
2023-02-19 11:04:57 -05:00
||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ"
|||
2023-01-20 20:34:28 -05:00
||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
||| and returns its type and the bound variables it used.
2023-02-19 11:51:44 -05:00
|||
||| if the dimension context is inconsistent, then return `Nothing`, without
||| doing any further work.
export covering %inline
infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
m (InferResult ctx.dctx q d n)
2023-02-20 15:38:47 -05:00
infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
2023-02-19 11:51:44 -05:00
||| `infer`, assuming the dimension context is consistent
2022-04-23 18:21:30 -04:00
export covering %inline
2023-02-19 11:51:44 -05:00
inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
m (InferResult' q d n)
inferC ctx sg subj =
2023-02-19 11:54:39 -05:00
wrapErr (WhileInferring ctx sg.fst subj) $
let Element subj nc = pushSubsts subj in
2023-02-20 15:42:21 -05:00
infer' ctx sg subj
2022-04-23 18:21:30 -04:00
2023-02-19 11:51:44 -05:00
private covering
2023-01-20 20:34:28 -05:00
check' : TyContext q d n -> SQty q ->
2023-02-20 15:42:21 -05:00
(subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
2023-02-19 11:51:44 -05:00
m (CheckResult' q n)
2022-04-23 18:21:30 -04:00
2023-02-20 15:42:21 -05:00
check' ctx sg (TYPE k) ty = do
-- if 𝓀 < then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type
l <- expectTYPE !ask ty
2023-01-08 14:44:25 -05:00
expectEqualQ zero sg.fst
unless (k < l) $ throwError $ BadUniverse k l
pure $ zeroFor ctx
2022-04-23 18:21:30 -04:00
2023-02-22 01:40:19 -05:00
check' ctx sg (Pi qty arg res) ty = do
2023-02-11 12:15:50 -05:00
l <- expectTYPE !ask ty
2023-01-08 14:44:25 -05:00
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢₀ A ⇐ Type
check0 ctx arg (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
2023-02-22 01:40:19 -05:00
case res.body of
Y res => check0 (extendTy arg ctx) res (TYPE l)
N res => check0 ctx res (TYPE l)
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type
pure $ zeroFor ctx
2022-04-27 15:58:09 -04:00
2023-02-22 01:40:19 -05:00
check' ctx sg (Lam body) ty = do
2023-02-11 12:15:50 -05:00
(qty, arg, res) <- expectPi !ask ty
2023-02-14 15:14:47 -05:00
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ
let qty' = sg.fst * qty
2023-02-19 11:51:44 -05:00
qout <- checkC (extendTy arg ctx) sg body.term res.term
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
popQ qty' qout
2023-01-26 13:54:46 -05:00
2023-02-22 01:40:19 -05:00
check' ctx sg (Sig fst snd) ty = do
2023-02-11 12:15:50 -05:00
l <- expectTYPE !ask ty
2023-01-26 13:54:46 -05:00
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢₀ A ⇐ Type
check0 ctx fst (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
2023-02-22 01:40:19 -05:00
case snd.body of
Y snd => check0 (extendTy fst ctx) snd (TYPE l)
N snd => check0 ctx snd (TYPE l)
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type
2023-01-26 13:54:46 -05:00
pure $ zeroFor ctx
2023-02-20 15:42:21 -05:00
check' ctx sg (Pair fst snd) ty = do
2023-02-11 12:15:50 -05:00
(tfst, tsnd) <- expectSig !ask ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
2023-02-19 11:51:44 -05:00
qfst <- checkC ctx sg fst tfst
2023-01-26 13:54:46 -05:00
let tsnd = sub1 tsnd (fst :# tfst)
-- if Ψ | Γ ⊢ σ · t ⇐ B[s] ⊳ Σ₂
2023-02-19 11:51:44 -05:00
qsnd <- checkC ctx sg snd tsnd
-- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
2023-01-26 13:54:46 -05:00
pure $ qfst + qsnd
2022-04-27 15:58:09 -04:00
check' ctx sg (Enum _) ty = do
-- Ψ | Γ ⊢₀ {ts} ⇐ Type
ignore $ expectTYPE !ask ty
expectEqualQ zero sg.fst
pure $ zeroFor ctx
check' ctx sg (Tag t) ty = do
tags <- expectEnum !ask ty
-- if t ∈ ts
unless (t `elem` tags) $ throwError $ TagNotIn t tags
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
pure $ zeroFor ctx
2023-02-22 01:40:19 -05:00
check' ctx sg (Eq t l r) ty = do
2023-02-11 12:15:50 -05:00
u <- expectTYPE !ask ty
2023-01-20 20:34:28 -05:00
expectEqualQ zero sg.fst
-- if Ψ, i | Γ ⊢₀ A ⇐ Type
2023-02-22 01:40:19 -05:00
case t.body of
Y t => check0 (extendDim ctx) t (TYPE u)
N t => check0 ctx t (TYPE u)
-- if Ψ | Γ ⊢₀ l ⇐ A0
check0 ctx t.zero l
-- if Ψ | Γ ⊢₀ r ⇐ A1
check0 ctx t.one r
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type
2023-01-20 20:34:28 -05:00
pure $ zeroFor ctx
2023-02-22 01:40:19 -05:00
check' ctx sg (DLam body) ty = do
2023-02-11 12:15:50 -05:00
(ty, l, r) <- expectEq !ask ty
-- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
2023-02-19 11:51:44 -05:00
qout <- checkC (extendDim ctx) sg body.term ty.term
-- if Ψ | Γ ⊢ t0 = l : A0
equal ctx ty.zero body.zero l
-- if Ψ | Γ ⊢ t1 = r : A1
equal ctx ty.one body.one r
-- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
2023-01-20 20:34:28 -05:00
pure qout
2023-02-20 15:42:21 -05:00
check' ctx sg (E e) ty = do
-- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
2023-02-19 11:51:44 -05:00
infres <- inferC ctx sg e
-- if Ψ | Γ ⊢ A' <: A
subtype ctx infres.type ty
-- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
2022-04-27 15:58:09 -04:00
pure infres.qout
2022-04-23 18:21:30 -04:00
2023-02-19 11:51:44 -05:00
private covering
2023-01-20 20:34:28 -05:00
infer' : TyContext q d n -> SQty q ->
2023-02-20 15:42:21 -05:00
(subj : Elim q d n) -> (0 nc : NotClo subj) =>
2023-02-19 11:51:44 -05:00
m (InferResult' q d n)
2022-04-23 18:21:30 -04:00
2023-02-20 15:42:21 -05:00
infer' ctx sg (F x) = do
2023-02-14 15:14:47 -05:00
-- if π·x : A {≔ s} in global context
2023-01-20 20:34:28 -05:00
g <- lookupFree x
2023-01-26 13:54:46 -05:00
-- if σ ≤ π
expectCompatQ sg.fst g.qty
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
2023-02-22 01:40:19 -05:00
where
lookupFree : Name -> m (Definition q)
lookupFree x = lookupFree' !ask x
2022-04-23 18:21:30 -04:00
2023-02-20 15:42:21 -05:00
infer' ctx sg (B i) =
2023-01-26 13:54:46 -05:00
-- if x : A ∈ Γ
2023-02-14 15:14:47 -05:00
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
2023-02-19 11:51:44 -05:00
pure $ lookupBound sg.fst i ctx.tctx
2023-02-22 01:40:19 -05:00
where
lookupBound : q -> Var n -> TContext q d n -> InferResult' q d n
lookupBound pi VZ (ctx :< ty) =
InfRes {type = weakT ty, qout = zeroFor ctx :< pi}
lookupBound pi (VS i) (ctx :< _) =
let InfRes {type, qout} = lookupBound pi i ctx in
InfRes {type = weakT type, qout = qout :< zero}
2022-04-27 15:58:09 -04:00
2023-02-20 15:42:21 -05:00
infer' ctx sg (fun :@ arg) = do
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
2023-02-19 11:51:44 -05:00
funres <- inferC ctx sg fun
2023-02-11 12:15:50 -05:00
(qty, argty, res) <- expectPi !ask funres.type
2023-02-14 15:14:47 -05:00
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
2023-02-19 11:51:44 -05:00
argout <- checkC ctx (subjMult sg qty) arg argty
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
2023-01-20 20:34:28 -05:00
pure $ InfRes {
type = sub1 res $ arg :# argty,
qout = funres.qout + argout
}
2023-02-22 01:40:19 -05:00
infer' ctx sg (CasePair pi pair ret body) = do
2023-01-26 13:54:46 -05:00
-- if 1 ≤ π
expectCompatQ one pi
-- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
pairres <- inferC ctx sg pair
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
2023-02-14 15:14:47 -05:00
check0 (extendTy pairres.type ctx) ret.term (TYPE UAny)
2023-02-11 12:15:50 -05:00
(tfst, tsnd) <- expectSig !ask pairres.type
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
2023-02-23 04:04:00 -05:00
-- with ρ₁, ρ₂ ≤ πσ
2023-02-14 15:14:47 -05:00
let bodyctx = extendTyN [< tfst, tsnd.term] ctx
2023-02-10 15:40:44 -05:00
bodyty = substCasePairRet pairres.type ret
2023-02-23 04:04:00 -05:00
pisg = pi * sg.fst
bodyout <- popQs [< pisg, pisg] !(checkC bodyctx sg body.term bodyty)
-- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
2023-01-26 13:54:46 -05:00
pure $ InfRes {
type = sub1 ret pair,
qout = pi * pairres.qout + bodyout
}
infer' ctx sg (CaseEnum pi t ret arms) {n} = do
-- if 1 ≤ π
expectCompatQ one pi
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
check0 (extendTy tres.type ctx) ret.term (TYPE UAny)
-- if for each "a ⇒ s" in arms,
-- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂
-- for fixed Σ₂
armres <- for (SortedMap.toList arms) $ \(a, s) =>
checkC ctx sg s (sub1 ret (Tag a :# tres.type))
armout <- allEqual armres
-- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂
pure $ InfRes {
type = sub1 ret t,
qout = pi * tres.qout + armout
}
where
allEqual : List (QOutput q n) -> m (QOutput q n)
allEqual [] = pure $ zeroFor ctx
allEqual lst@(x :: xs) =
if all (== x) xs then pure x
else throwError $ BadCaseQtys lst
2023-02-20 15:42:21 -05:00
infer' ctx sg (fun :% dim) = do
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
2023-02-19 11:51:44 -05:00
InfRes {type, qout} <- inferC ctx sg fun
2023-02-20 15:42:21 -05:00
ty <- fst <$> expectEq !ask type
-- then Ψ | Γ ⊢ σ · f p ⇒ Ap ⊳ Σ
2023-01-20 20:34:28 -05:00
pure $ InfRes {type = dsub1 ty dim, qout}
2023-02-20 15:42:21 -05:00
infer' ctx sg (term :# type) = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
check0 ctx type (TYPE UAny)
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
2023-02-19 11:51:44 -05:00
qout <- checkC ctx sg term type
-- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ
2023-01-20 20:34:28 -05:00
pure $ InfRes {type, qout}