remove input qctx since it isn't used

This commit is contained in:
rhiannon morris 2023-02-14 21:14:47 +01:00
parent 846bbc9ca3
commit c40e6a60ff
3 changed files with 48 additions and 63 deletions

View file

@ -23,8 +23,8 @@ CanTC q = CanTC' q IsGlobal
private private
popQs : HasErr q m => IsQty q => popQs : HasErr q m => IsQty q =>
SnocVect s q -> QOutput q (s + n) -> m (QOutput q n) SnocVect s q -> QOutput q (s + n) -> m (QOutput q n)
popQs [<] qctx = pure qctx popQs [<] qout = pure qout
popQs (pis :< pi) (qctx :< rh) = do expectCompatQ rh pi; popQs pis qctx popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
private %inline private %inline
popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n) popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
@ -34,7 +34,7 @@ popQ pi = popQs [< pi]
private %inline private %inline
tail : TyContext q d (S n) -> TyContext q d n tail : TyContext q d (S n) -> TyContext q d n
tail = {tctx $= tail, qctx $= tail} tail = {tctx $= tail}
private %inline private %inline
@ -48,13 +48,18 @@ lookupBound pi VZ (MkTyContext {tctx = tctx :< ty, _}) =
lookupBound pi (VS i) ctx = lookupBound pi (VS i) ctx =
weakI $ lookupBound pi i (tail ctx) weakI $ lookupBound pi i (tail ctx)
private private %inline
lookupFree : CanTC' q g m => Name -> m (Definition' q g) lookupFree : CanTC' q g m => Name -> m (Definition' q g)
lookupFree x = lookupFree' !ask x lookupFree x = lookupFree' !ask x
||| ``sg `subjMult` pi`` is zero if either argument is, otherwise it
||| is equal to `sg`. (written as "σ ⨴ π" to emphasise its left bias.)
|||
||| only certain quantities can occur for a typing judgement to avoid losing
||| subject reduction [@qtt, §2.3], which is why this is not just `sg*pi`.
private %inline private %inline
subjMult : IsQty q => (sg : SQty q) -> q -> SQty q subjMult : IsQty q => SQty q -> q -> SQty q
subjMult sg qty = if isYes $ isZero qty then szero else sg subjMult sg pi = if isYes $ isZero pi then szero else sg
export export
@ -84,7 +89,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
||| `check0 ctx subj ty` checks a term in a zero context. ||| `check0 ctx subj ty` checks a term in a zero context.
export covering %inline export covering %inline
check0 : TyContext q d n -> Term q d n -> Term q d n -> m () 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 check0 ctx tm ty = ignore $ check ctx szero tm ty
-- the output will always be 𝟎 because the subject quantity is 0
||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`, ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
||| and returns its type and the bound variables it used. ||| and returns its type and the bound variables it used.
@ -114,16 +120,17 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
check0 ctx arg (TYPE l) check0 ctx arg (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
case res of case res of
TUsed res => check0 (extendTy arg zero ctx) res (TYPE l) TUsed res => check0 (extendTy arg ctx) res (TYPE l)
TUnused res => check0 ctx res (TYPE l) TUnused res => check0 ctx res (TYPE l)
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type
pure $ zeroFor ctx pure $ zeroFor ctx
check' ctx sg (Lam _ body) _ ty = do check' ctx sg (Lam _ body) _ ty = do
(qty, arg, res) <- expectPi !ask ty (qty, arg, res) <- expectPi !ask ty
-- if Ψ | Γ, πσ·x : A ⊢ σ · t ⇐ B ⊳ Σ, σπ·x -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ
let qty' = sg.fst * qty let qty' = sg.fst * qty
qout <- check (extendTy arg qty' ctx) sg body.term res.term qout <- check (extendTy arg ctx) sg body.term res.term
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
popQ qty' qout popQ qty' qout
@ -134,7 +141,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
check0 ctx fst (TYPE l) check0 ctx fst (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type
case snd of case snd of
TUsed snd => check0 (extendTy fst zero ctx) snd (TYPE l) TUsed snd => check0 (extendTy fst ctx) snd (TYPE l)
TUnused snd => check0 ctx snd (TYPE l) TUnused snd => check0 ctx snd (TYPE l)
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type
pure $ zeroFor ctx pure $ zeroFor ctx
@ -189,7 +196,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
m (InferResult q d n) m (InferResult q d n)
infer' ctx sg (F x) _ = do infer' ctx sg (F x) _ = do
-- if x · π : A {≔ s} in global context -- if π·x : A {≔ s} in global context
g <- lookupFree x g <- lookupFree x
-- if σ ≤ π -- if σ ≤ π
expectCompatQ sg.fst g.qty expectCompatQ sg.fst g.qty
@ -205,8 +212,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁ -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
funres <- infer ctx sg fun funres <- infer ctx sg fun
(qty, argty, res) <- expectPi !ask funres.type (qty, argty, res) <- expectPi !ask funres.type
-- if Ψ | Γ ⊢ σπ · s ⇐ A ⊳ Σ₂ -- if Ψ | Γ ⊢ σπ · s ⇐ A ⊳ Σ₂
-- (0∧π = σ∧0 = 0; σ∧π = σ otherwise) -- (σ ⨴ 0 = 0; σπ = σ otherwise)
argout <- check ctx (subjMult sg qty) arg argty argout <- check ctx (subjMult sg qty) arg argty
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂ -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
pure $ InfRes { pure $ InfRes {
@ -219,12 +226,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
expectCompatQ one pi expectCompatQ one pi
-- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁ -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
pairres <- infer ctx sone pair pairres <- infer ctx sone pair
check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny) check0 (extendTy pairres.type ctx) ret.term (TYPE UAny)
(tfst, tsnd) <- expectSig !ask pairres.type (tfst, tsnd) <- expectSig !ask pairres.type
-- if Ψ | Γ, π·x : A, π·y : B ⊢ σ body ⇐ ret[(x, y)] -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ ret[(x, y)] ⊳ Σ₂, ρ₁·x, ρ₂·y
-- ⊳ Σ₂, π₁·x, π₂·y -- with ρ₁, ρ₂ ≤ π
-- with π₁, π₂ ≤ π let bodyctx = extendTyN [< tfst, tsnd.term] ctx
let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx
bodyty = substCasePairRet pairres.type ret bodyty = substCasePairRet pairres.type ret
bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi] bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
-- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂ -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂

View file

@ -30,13 +30,9 @@ public export
TContext : Type -> Nat -> Nat -> Type TContext : Type -> Nat -> Nat -> Type
TContext q d = Context (Term q d) TContext q d = Context (Term q d)
public export
QContext : Type -> Nat -> Type
QContext = Context'
public export public export
QOutput : Type -> Nat -> Type QOutput : Type -> Nat -> Type
QOutput = QContext QOutput = Context'
public export public export
@ -44,55 +40,45 @@ record TyContext q d n where
constructor MkTyContext constructor MkTyContext
dctx : DContext d dctx : DContext d
tctx : TContext q d n tctx : TContext q d n
qctx : QContext q n
%name TyContext ctx %name TyContext ctx
namespace TContext namespace TContext
export export %inline
pushD : TContext q d n -> TContext q (S d) n pushD : TContext q d n -> TContext q (S d) n
pushD tel = map (/// shift 1) tel pushD tel = map (/// shift 1) tel
export
zeroed : IsQty q => TyContext q d n -> TyContext q d n
zeroed = {qctx $= map (const zero)}
namespace TyContext namespace TyContext
export export %inline
extendTyN : Telescope (\n => (Term q d n, q)) from to -> extendTyN : Telescope (Term q d) from to ->
TyContext q d from -> TyContext q d to TyContext q d from -> TyContext q d to
extendTyN ss = {tctx $= (. map fst ss), qctx $= (. map snd ss)} extendTyN ss = {tctx $= (. ss)}
export export %inline
extendTy : Term q d n -> q -> TyContext q d n -> TyContext q d (S n) extendTy : Term q d n -> TyContext q d n -> TyContext q d (S n)
extendTy s rho = extendTyN [< (s, rho)] extendTy s = extendTyN [< s]
export export %inline
extendDim : TyContext q d n -> TyContext q (S d) n extendDim : TyContext q d n -> TyContext q (S d) n
extendDim = {dctx $= DBind, tctx $= pushD} extendDim = {dctx $= DBind, tctx $= pushD}
export export %inline
eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
eqDim p q = {dctx $= DEq p q} eqDim p q = {dctx $= DEq p q}
namespace QOutput namespace QOutput
parameters {auto _ : IsQty q} parameters {auto _ : IsQty q}
export export %inline
(+) : QOutput q n -> QOutput q n -> QOutput q n (+) : QOutput q n -> QOutput q n -> QOutput q n
(+) = zipWith (+) (+) = zipWith (+)
export export %inline
(*) : q -> QOutput q n -> QOutput q n (*) : q -> QOutput q n -> QOutput q n
(*) pi = map (pi *) (*) pi = map (pi *)
export export %inline
zero : {n : Nat} -> QOutput q n
zero = pure zero
export
zeroFor : TyContext q _ n -> QOutput q n zeroFor : TyContext q _ n -> QOutput q n
zeroFor ctx = zero <$ ctx.tctx zeroFor ctx = zero <$ ctx.tctx

View file

@ -69,13 +69,8 @@ parameters (label : String) (act : Lazy (M ()))
testTCFail = testThrows label (const True) $ runReaderT globals act testTCFail = testThrows label (const True) $ runReaderT globals act
ctxWith : DContext d -> Context (\i => (Term Three d i, Three)) n -> ctx : TContext Three 0 n -> TyContext Three 0 n
TyContext Three d n ctx = MkTyContext DNil
ctxWith dctx tqctx =
let (tctx, qctx) = unzip tqctx in MkTyContext {dctx, tctx, qctx}
ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n
ctx = ctxWith DNil
inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M () inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
inferredTypeEq ctx exp got = inferredTypeEq ctx exp got =
@ -170,17 +165,15 @@ tests = "typechecker" :- [
], ],
"bound vars" :- [ "bound vars" :- [
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $ testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
inferAsQ {n = 1} (ctx [< (FT "A", one)]) sone inferAsQ {n = 1} (ctx [< FT "A"]) sone
(BV 0) (FT "A") [< one], (BV 0) (FT "A") [< one],
testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $ testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
checkQ {n = 1} (ctx [< (FT "A", one)]) sone (BVT 0) (FT "A") [< one], checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one],
note "f2 : A ⊸ A ⊸ A", note "f2 : A ⊸ A ⊸ A",
testTC "ω·x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $ testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
inferAsQ {n = 1} (ctx [< (FT "A", Any)]) sone inferAsQ {n = 1} (ctx [< FT "A"]) sone
(F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any], (F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any]
note #"("0·x : A1 · x ⇒ A" won't fail because"#,
note " a var's quantity is only checked once it leaves scope)"
], ],
"lambda" :- [ "lambda" :- [