quox/lib/Quox/Typechecker.idr

535 lines
19 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
2023-05-21 14:09:34 -04:00
import Quox.Displace
2022-04-23 18:21:30 -04:00
import Data.List
2023-03-26 10:09:47 -04:00
import Data.SnocVect
import Data.List1
2023-03-31 13:23:30 -04:00
import Quox.EffExtra
2022-04-23 18:21:30 -04:00
%default total
2023-01-20 20:34:28 -05:00
public export
2023-08-24 13:55:57 -04:00
0 TC : List (Type -> Type)
TC = [ErrorEff, DefsReader, NameGen]
2023-03-31 13:23:30 -04:00
2023-01-20 20:34:28 -05:00
2023-05-01 21:06:25 -04:00
parameters (loc : Loc)
export
2023-08-24 13:55:57 -04:00
popQs : Has ErrorEff fs => QContext s -> QOutput (s + n) ->
Eff fs (QOutput n)
2023-05-01 21:06:25 -04:00
popQs [<] qout = pure qout
popQs (pis :< pi) (qout :< rh) = do expectCompatQ loc rh pi; popQs pis qout
2022-04-23 18:21:30 -04:00
2023-05-01 21:06:25 -04:00
export %inline
popQ : Has ErrorEff fs => Qty -> QOutput (S n) -> Eff fs (QOutput n)
popQ pi = popQs [< pi]
2023-01-26 13:54:46 -05:00
export
2023-05-12 11:28:29 -04:00
lubs1 : List1 (QOutput n) -> QOutput n
lubs1 ([<] ::: _) = [<]
lubs1 ((qs :< p) ::: pqs) =
let (qss, ps) = unzip $ map unsnoc pqs in
2023-05-12 11:28:29 -04:00
lubs1 (qs ::: qss) :< foldl lub p ps
export
2023-05-12 11:28:29 -04:00
lubs : TyContext d n -> List (QOutput n) -> QOutput n
lubs ctx [] = zeroFor ctx
lubs ctx (x :: xs) = lubs1 $ x ::: xs
2022-04-23 18:21:30 -04:00
2023-04-01 13:16:43 -04:00
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-04-01 13:16:43 -04:00
check : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
2023-08-24 13:55:57 -04:00
Eff TC (CheckResult ctx.dctx 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
2023-08-24 13:55:57 -04:00
check0 : TyContext d n -> Term d n -> Term d n -> Eff TC ()
check0 ctx tm ty = ignore $ check ctx SZero tm ty
2023-02-14 15:14:47 -05:00
-- 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
2023-04-01 13:16:43 -04:00
checkC : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
2023-08-24 13:55:57 -04:00
Eff TC (CheckResult' n)
2023-02-19 11:51:44 -05:00
checkC ctx sg subj ty =
wrapErr (WhileChecking ctx sg subj ty) $
2023-05-21 14:09:34 -04:00
checkCNoWrap ctx sg subj ty
export covering %inline
checkCNoWrap : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
2023-08-24 13:55:57 -04:00
Eff TC (CheckResult' n)
2023-05-21 14:09:34 -04:00
checkCNoWrap ctx sg subj ty =
let Element subj nc = pushSubsts subj in
check' ctx sg subj ty
2023-02-19 11:51:44 -05:00
||| "Ψ | Γ ⊢₀ 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
2023-08-24 13:55:57 -04:00
checkType : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
export covering %inline
2023-08-24 13:55:57 -04:00
checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
checkTypeC ctx subj l =
wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l
export covering %inline
2023-08-24 13:55:57 -04:00
checkTypeNoWrap : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
checkTypeNoWrap ctx subj l =
let Element subj nc = pushSubsts subj in
checkType' ctx subj l
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
2023-04-01 13:16:43 -04:00
infer : (ctx : TyContext d n) -> SQty -> Elim d n ->
2023-08-24 13:55:57 -04:00
Eff TC (InferResult ctx.dctx 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-04-01 13:16:43 -04:00
inferC : (ctx : TyContext d n) -> SQty -> Elim d n ->
2023-08-24 13:55:57 -04:00
Eff TC (InferResult' d n)
2023-02-19 11:51:44 -05:00
inferC ctx sg subj =
wrapErr (WhileInferring ctx sg subj) $
2023-02-19 11:54:39 -05:00
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
private covering
2023-04-01 13:16:43 -04:00
toCheckType : TyContext d n -> SQty ->
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
2023-08-24 13:55:57 -04:00
Eff TC (CheckResult' n)
toCheckType ctx sg t ty = do
u <- expectTYPE !(askAt DEFS) ctx sg ty.loc ty
expectEqualQ t.loc Zero sg.qty
checkTypeNoWrap ctx t (Just u)
pure $ zeroFor ctx
2023-02-19 11:51:44 -05:00
private covering
2023-04-01 13:16:43 -04:00
check' : TyContext d n -> SQty ->
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
2023-08-24 13:55:57 -04:00
Eff TC (CheckResult' n)
2022-04-23 18:21:30 -04:00
2023-05-01 21:06:25 -04:00
check' ctx sg t@(TYPE {}) ty = toCheckType ctx sg t ty
2022-04-23 18:21:30 -04:00
check' ctx sg t@(IOState {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
2022-04-27 15:58:09 -04:00
2023-05-01 21:06:25 -04:00
check' ctx sg (Lam body loc) ty = do
(qty, arg, res) <- expectPi !(askAt DEFS) ctx SZero ty.loc ty
2023-02-14 15:14:47 -05:00
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ
let qty' = sg.qty * qty
2023-03-15 10:54:51 -04:00
qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
2023-05-01 21:06:25 -04:00
popQ loc qty' qout
2023-01-26 13:54:46 -05:00
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
2023-01-26 13:54:46 -05:00
2023-05-01 21:06:25 -04:00
check' ctx sg (Pair fst snd loc) ty = do
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx SZero ty.loc ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
2023-02-19 11:51:44 -05:00
qfst <- checkC ctx sg fst tfst
2023-05-01 21:06:25 -04:00
let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
-- 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
2023-05-01 21:06:25 -04:00
check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
2023-05-01 21:06:25 -04:00
check' ctx sg (Tag t loc) ty = do
tags <- expectEnum !(askAt DEFS) ctx SZero ty.loc ty
-- if t ∈ ts
2023-05-01 21:06:25 -04:00
unless (t `elem` tags) $ throw $ TagNotIn loc t tags
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
pure $ zeroFor ctx
check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
2023-01-20 20:34:28 -05:00
2023-05-01 21:06:25 -04:00
check' ctx sg (DLam body loc) ty = do
(ty, l, r) <- expectEq !(askAt DEFS) ctx SZero ty.loc 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
let ctx0 = eqDim (B VZ loc) (K Zero loc) ctx'
lift $ equal loc ctx0 sg ty body $ dweakT 1 l
-- if Ψ, i, i = 1 | Γ ⊢ t = r : A
let ctx1 = eqDim (B VZ loc) (K One loc) ctx'
lift $ equal loc ctx1 sg ty body $ dweakT 1 r
2023-02-25 13:14:11 -05:00
-- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
2023-01-20 20:34:28 -05:00
pure qout
2023-11-02 13:14:22 -04:00
check' ctx sg t@(NAT {}) ty = toCheckType ctx sg t ty
2023-03-26 08:40:54 -04:00
check' ctx sg (Nat {}) ty = do
2023-11-02 13:14:22 -04:00
expectNAT !(askAt DEFS) ctx SZero ty.loc ty
2023-03-26 08:40:54 -04:00
pure $ zeroFor ctx
2023-05-01 21:06:25 -04:00
check' ctx sg (Succ n {}) ty = do
2023-11-02 13:14:22 -04:00
expectNAT !(askAt DEFS) ctx SZero ty.loc ty
2023-05-01 21:06:25 -04:00
checkC ctx sg n ty
2023-03-26 08:40:54 -04:00
check' ctx sg t@(STRING {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(Str s {}) ty = do
expectSTRING !(askAt DEFS) ctx SZero ty.loc ty
pure $ zeroFor ctx
2023-03-31 13:11:35 -04:00
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
2023-05-01 21:06:25 -04:00
check' ctx sg (Box val loc) ty = do
(q, ty) <- expectBOX !(askAt DEFS) ctx SZero ty.loc ty
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ
valout <- checkC ctx (subjMult sg q) val ty
2023-03-31 13:11:35 -04:00
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
pure $ q * valout
2023-12-04 16:47:52 -05:00
check' ctx sg (Let qty rhs body loc) ty = do
eres <- inferC ctx (subjMult sg qty) rhs
let sqty = sg.qty * qty
qout <- checkC (extendTyLet sqty body.name eres.type (E rhs) ctx)
sg body.term (weakT 1 ty)
>>= popQ loc sqty
2023-12-04 16:47:52 -05:00
pure $ qty * eres.qout + 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
2023-05-01 21:06:25 -04:00
lift $ subtype e.loc 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
private covering
2023-04-01 13:16:43 -04:00
checkType' : TyContext d n ->
(subj : Term d n) -> (0 nc : NotClo subj) =>
2023-08-24 13:55:57 -04:00
Maybe Universe -> Eff TC ()
2023-05-01 21:06:25 -04:00
checkType' ctx (TYPE k loc) u = do
-- if 𝓀 < then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type
case u of
2023-05-01 21:06:25 -04:00
Just l => unless (k < l) $ throw $ BadUniverse loc k l
Nothing => pure ()
checkType' ctx (IOState loc) u = pure ()
-- Ψ | Γ ⊢₀ IOState ⇒ Type
2023-05-01 21:06:25 -04:00
checkType' ctx (Pi qty arg res _) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
checkTypeC ctx arg u
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
2023-04-03 11:46:23 -04:00
checkTypeScope ctx arg res u
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type
checkType' ctx t@(Lam {}) u =
2023-05-01 21:06:25 -04:00
throw $ NotType t.loc ctx t
2023-05-01 21:06:25 -04:00
checkType' ctx (Sig fst snd _) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
checkTypeC ctx fst u
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
2023-04-03 11:46:23 -04:00
checkTypeScope ctx fst snd u
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type
checkType' ctx t@(Pair {}) u =
2023-05-01 21:06:25 -04:00
throw $ NotType t.loc ctx t
2023-05-01 21:06:25 -04:00
checkType' ctx (Enum {}) u = pure ()
-- Ψ | Γ ⊢₀ {ts} ⇐ Type
checkType' ctx t@(Tag {}) u =
2023-05-01 21:06:25 -04:00
throw $ NotType t.loc ctx t
2023-05-01 21:06:25 -04:00
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
2023-04-01 10:02:02 -04:00
check0 ctx l t.zero
-- if Ψ | Γ ⊢₀ r ⇐ A1
2023-04-01 10:02:02 -04:00
check0 ctx r t.one
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type
checkType' ctx t@(DLam {}) u =
2023-05-01 21:06:25 -04:00
throw $ NotType t.loc ctx t
2023-11-02 13:14:22 -04:00
checkType' ctx (NAT {}) u = pure ()
checkType' ctx t@(Nat {}) u = throw $ NotType t.loc ctx t
2023-05-01 21:06:25 -04:00
checkType' ctx t@(Succ {}) u = throw $ NotType t.loc ctx t
2023-03-26 08:40:54 -04:00
checkType' ctx (STRING loc) u = pure ()
-- Ψ | Γ ⊢₀ STRING ⇒ Type
checkType' ctx t@(Str {}) u = throw $ NotType t.loc ctx t
2023-05-01 21:06:25 -04:00
checkType' ctx (BOX q ty _) u = checkType ctx ty u
checkType' ctx t@(Box {}) u = throw $ NotType t.loc ctx t
2023-03-31 13:11:35 -04:00
2023-12-04 16:47:52 -05:00
checkType' ctx (Let qty rhs body loc) u = do
expectEqualQ loc qty Zero
ety <- inferC ctx SZero rhs
checkType (extendTy Zero body.name ety.type ctx) body.term u
checkType' ctx (E e) u = do
2023-03-31 13:11:35 -04:00
-- if Ψ | Γ ⊢₀ E ⇒ Type
infres <- inferC ctx SZero e
2023-03-31 13:11:35 -04:00
-- if Ψ | Γ ⊢ Type <: Type 𝓀
case u of
2023-11-27 15:01:36 -05:00
Just u => lift $ subtype e.loc ctx infres.type (TYPE u e.loc)
Nothing => ignore $ expectTYPE !(askAt DEFS) ctx SZero e.loc infres.type
2023-03-31 13:11:35 -04:00
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
2023-04-03 11:46:23 -04:00
private covering
checkTypeScope : TyContext d n -> Term d n ->
2023-08-24 13:55:57 -04:00
ScopeTerm d n -> Maybe Universe -> Eff TC ()
2023-05-01 21:06:25 -04:00
checkTypeScope ctx s (S _ (N body)) u = checkType ctx body u
checkTypeScope ctx s (S [< x] (Y body)) u =
checkType (extendTy Zero x s ctx) body u
2023-04-03 11:46:23 -04:00
2023-02-19 11:51:44 -05:00
private covering
2023-04-01 13:16:43 -04:00
infer' : TyContext d n -> SQty ->
(subj : Elim d n) -> (0 nc : NotClo subj) =>
2023-08-24 13:55:57 -04:00
Eff TC (InferResult' d n)
2022-04-23 18:21:30 -04:00
2023-05-21 14:09:34 -04:00
infer' ctx sg (F x u loc) = do
2023-02-14 15:14:47 -05:00
-- if π·x : A {≔ s} in global context
2023-06-23 12:32:05 -04:00
g <- lookupFree x loc !(askAt DEFS)
2023-01-26 13:54:46 -05:00
-- if σ ≤ π
expectCompatQ loc sg.qty g.qty.qty
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
2023-10-15 10:23:38 -04:00
pure $ InfRes {
type = g.typeWithAt ctx.dimLen ctx.termLen u,
qout = zeroFor ctx
}
2022-04-23 18:21:30 -04:00
2023-05-01 21:06:25 -04: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, 𝟎)
pure $ lookupBound sg.qty i ctx.tctx
2023-05-01 21:06:25 -04:00
where
2023-04-01 13:16:43 -04:00
lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
lookupBound pi VZ (ctx :< var) =
InfRes {type = weakT 1 var.type, qout = zeroFor ctx :< pi}
2023-02-22 01:40:19 -05:00
lookupBound pi (VS i) (ctx :< _) =
let InfRes {type, qout} = lookupBound pi i ctx in
2023-04-15 09:13:01 -04:00
InfRes {type = weakT 1 type, qout = qout :< Zero}
2022-04-27 15:58:09 -04:00
2023-05-01 21:06:25 -04:00
infer' ctx sg (App fun arg loc) = do
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
2023-02-19 11:51:44 -05:00
funres <- inferC ctx sg fun
(qty, argty, res) <- expectPi !(askAt DEFS) ctx SZero fun.loc 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 {
2023-05-01 21:06:25 -04:00
type = sub1 res $ Ann arg argty arg.loc,
qout = funres.qout + qty * argout
2023-01-20 20:34:28 -05:00
}
2023-05-01 21:06:25 -04:00
infer' ctx sg (CasePair pi pair ret body loc) = 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
2023-04-01 13:16:43 -04:00
checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc 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 ρ₁, ρ₂ ≤ πσ
let [< x, y] = body.names
pisg = pi * sg.qty
2023-03-15 10:54:51 -04:00
bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
2023-05-01 21:06:25 -04:00
bodyty = substCasePairRet body.names pairres.type ret
bodyout <- checkC bodyctx sg body.term bodyty >>=
popQs loc [< pisg, pisg]
2023-04-15 09:13:01 -04:00
-- then Ψ | Γ ⊢ σ · caseπ ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
2023-01-26 13:54:46 -05:00
pure $ InfRes {
type = sub1 ret pair,
2023-03-31 13:11:35 -04:00
qout = pi * pairres.qout + bodyout
2023-01-26 13:54:46 -05:00
}
2023-09-18 15:52:51 -04:00
infer' ctx sg (Fst pair loc) = do
-- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
pairres <- inferC ctx sg pair
(tfst, _) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
-- then Ψ | Γ ⊢ σ · fst e ⇒ A ⊳ ωΣ
pure $ InfRes {
type = tfst,
qout = Any * pairres.qout
}
infer' ctx sg (Snd pair loc) = do
-- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
pairres <- inferC ctx sg pair
(_, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
-- then Ψ | Γ ⊢ σ · snd e ⇒ B[fst e/x] ⊳ ωΣ
pure $ InfRes {
type = sub1 tsnd (Fst pair loc),
qout = Any * pairres.qout
}
2023-05-01 21:06:25 -04:00
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t
ttags <- expectEnum !(askAt DEFS) ctx SZero t.loc tres.type
-- if 1 ≤ π, OR there is only zero or one option
2023-05-01 21:06:25 -04:00
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ loc One pi
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
2023-04-01 13:16:43 -04:00
checkTypeC (extendTy Zero ret.name tres.type ctx) ret.term Nothing
-- if for each "a ⇒ s" in arms,
2023-03-31 13:11:35 -04:00
-- Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σᵢ
-- with Σ₂ = lubs Σᵢ
let arms = SortedMap.toList arms
let armTags = SortedSet.fromList $ map fst arms
2023-05-01 21:06:25 -04:00
unless (ttags == armTags) $ throw $ BadCaseEnum loc ttags armTags
armres <- for arms $ \(a, s) =>
2023-05-01 21:06:25 -04:00
checkC ctx sg s $ sub1 ret $ Ann (Tag a s.loc) tres.type s.loc
pure $ InfRes {
type = sub1 ret t,
2023-05-12 11:28:29 -04:00
qout = pi * tres.qout + lubs ctx armres
}
2023-05-01 21:06:25 -04:00
infer' ctx sg (CaseNat pi pi' n ret zer suc loc) = do
2023-03-26 08:40:54 -04:00
-- if 1 ≤ π
2023-05-01 21:06:25 -04:00
expectCompatQ loc One pi
2023-03-26 08:40:54 -04:00
-- if Ψ | Γ ⊢ σ · n ⇒ ⊳ Σn
nres <- inferC ctx sg n
2023-05-01 21:06:25 -04:00
let nat = nres.type
2023-11-02 13:14:22 -04:00
expectNAT !(askAt DEFS) ctx SZero n.loc nat
2023-03-26 08:40:54 -04:00
-- if Ψ | Γ, n : ⊢₀ A ⇐ Type
2023-05-01 21:06:25 -04:00
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
2023-03-26 08:40:54 -04:00
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ /n] ⊳ Σz
2023-05-01 21:06:25 -04:00
zerout <- checkC ctx sg zer $ sub1 ret $ Ann (Zero zer.loc) nat zer.loc
-- if Ψ | Γ, n : , ih : A ⊢ σ · suc ⇐ A[succ p ∷ /n] ⊳ Σs, ρ.p, ς.ih
-- with ς ≤ π'σ, (ρ + ς) ≤ πσ
2023-03-26 08:40:54 -04:00
let [< p, ih] = suc.names
pisg = pi * sg.qty
2023-11-02 13:14:22 -04:00
sucCtx = extendTyN [< (pisg, p, NAT p.loc), (pi', ih, ret.term)] ctx
2023-05-01 21:06:25 -04:00
sucType = substCaseSuccRet suc.names ret
2023-03-26 08:40:54 -04:00
sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
expectCompatQ loc qih (pi' * sg.qty)
2023-03-26 08:40:54 -04:00
-- [fixme] better error here
2023-05-01 21:06:25 -04:00
expectCompatQ loc (qp + qih) pisg
-- if ς = 0, then Σb = lubs(Σz, Σs), otherwise Σb = Σz + ωςΣs
let bodyout = case qih of
Zero => lubs ctx [zerout, sucout]
_ => zerout + Any * sucout
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σb
2023-03-26 08:40:54 -04:00
pure $ InfRes {
type = sub1 ret n,
qout = pi * nres.qout + bodyout
2023-03-26 08:40:54 -04:00
}
2023-05-01 21:06:25 -04:00
infer' ctx sg (CaseBox pi box ret body loc) = do
2023-03-31 13:11:35 -04:00
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
boxres <- inferC ctx sg box
(rh, ty) <- expectBOX !(askAt DEFS) ctx SZero box.loc boxres.type
2023-03-31 13:11:35 -04:00
-- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
2023-04-01 13:16:43 -04:00
checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
2023-03-31 13:11:35 -04:00
-- with ς ≤ ρπσ
let rhpisg = rh * pi * sg.qty
bodyCtx = extendTy rhpisg body.name ty ctx
2023-05-01 21:06:25 -04:00
bodyType = substCaseBoxRet body.name ty ret
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc rhpisg
2023-04-15 09:13:01 -04:00
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
2023-03-31 13:11:35 -04:00
pure $ InfRes {
type = sub1 ret box,
qout = boxres.qout + bodyout
}
2023-05-01 21:06:25 -04:00
infer' ctx sg (DApp fun dim loc) = do
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
2023-02-19 11:51:44 -05:00
InfRes {type, qout} <- inferC ctx sg fun
ty <- fst <$> expectEq !(askAt DEFS) ctx SZero fun.loc type
-- then Ψ | Γ ⊢ σ · f p ⇒ Ap/𝑖 ⊳ Σ
2023-01-20 20:34:28 -05:00
pure $ InfRes {type = dsub1 ty dim, qout}
2023-05-01 21:06:25 -04:00
infer' ctx sg (Coe ty p q val loc) = do
2024-03-21 16:29:13 -04:00
-- if Ψ, 𝑖 | Γ ⊢₀ A ⇐ Type _
2023-05-01 21:06:25 -04:00
checkType (extendDim ty.name ctx) ty.term Nothing
2024-03-21 16:29:13 -04:00
-- if Ψ | Γ ⊢ σ · s ⇐ Ap/𝑖 ⊳ Σ
2023-05-01 21:06:25 -04:00
qout <- checkC ctx sg val $ dsub1 ty p
2024-03-21 16:29:13 -04:00
-- then Ψ | Γ ⊢ σ · coe (𝑖 ⇒ A) @p @q s ⇒ Aq/𝑖 ⊳ Σ
2023-05-01 21:06:25 -04:00
pure $ InfRes {type = dsub1 ty q, qout}
2023-04-15 09:13:01 -04:00
2023-05-01 21:06:25 -04:00
infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1) loc) = do
2024-03-21 16:29:13 -04:00
-- if Ψ | Γ ⊢₀ A ⇐ Type _
2023-04-15 09:13:01 -04:00
checkType ctx ty Nothing
2024-03-21 16:29:13 -04:00
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
2023-04-15 09:13:01 -04:00
qout <- checkC ctx sg val ty
2024-03-21 16:29:13 -04:00
-- if Ψ, 𝑗, 𝑖=0 | Γ ⊢ σ · t₀ ⇐ A ⊳ Σ₀
-- Ψ, 𝑗, 𝑖=0, 𝑗=p | Γ ⊢ t₀ = s ⇐ A
2023-04-15 09:13:01 -04:00
let ty' = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
2023-05-01 21:06:25 -04:00
ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
2023-09-17 07:54:26 -04:00
val0 = getTerm val0
2023-04-15 09:13:01 -04:00
qout0 <- check ctx0 sg val0 ty'
lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) sg ty' val0 val'
2024-03-21 16:29:13 -04:00
-- if Ψ, 𝑗, 𝑖=1 | Γ ⊢ σ · t₁ ⇐ A ⊳ Σ₁
-- Ψ, 𝑗, 𝑖=1, 𝑗=p | Γ ⊢ t₁ = s ⇐ A
2023-05-01 21:06:25 -04:00
let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
2023-09-17 07:54:26 -04:00
val1 = getTerm val1
2023-04-15 09:13:01 -04:00
qout1 <- check ctx1 sg val1 ty'
2024-03-21 16:29:13 -04:00
-- if Σ = Σ₀ = Σ₁
lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
2023-05-12 11:28:29 -04:00
let qouts = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
2024-03-21 16:29:13 -04:00
-- then Ψ | Γ ⊢ comp A @p @q s @r {0 𝑗 ⇒ t₀; 1 𝑗 ⇒ t₁} ⇒ A ⊳ Σ
2023-05-12 11:28:29 -04:00
pure $ InfRes {type = ty, qout = lubs ctx qouts}
2023-04-15 09:13:01 -04:00
2023-05-01 21:06:25 -04:00
infer' ctx sg (TypeCase ty ret arms def loc) = do
2023-04-03 11:46:23 -04:00
-- if σ = 0
expectEqualQ loc Zero sg.qty
2023-04-03 11:46:23 -04:00
-- if Ψ, Γ ⊢₀ e ⇒ Type u
u <- inferC ctx SZero ty >>=
expectTYPE !(askAt DEFS) ctx SZero ty.loc . type
2023-04-15 09:13:01 -04:00
-- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
2023-04-03 11:46:23 -04:00
checkTypeC ctx ret Nothing
2023-04-15 09:13:01 -04:00
-- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
for_ allKinds $ \k =>
for_ (lookupPrecise k arms) $ \(S names t) =>
2023-05-01 21:06:25 -04:00
check0 (extendTyN (typecaseTel k names u) ctx)
2023-09-17 07:54:26 -04:00
(getTerm t) (weakT (arity k) ret)
2023-04-03 11:46:23 -04:00
-- then Ψ, Γ ⊢₀ type-case ⋯ ⇒ C
pure $ InfRes {type = ret, qout = zeroFor ctx}
2023-05-01 21:06:25 -04:00
infer' ctx sg (Ann term type loc) = do
-- if Ψ | Γ ⊢₀ A ⇐ Type
checkTypeC ctx type Nothing
-- 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}