comments etc
This commit is contained in:
parent
d71ac8c34d
commit
e375d008e5
|
|
@ -37,6 +37,11 @@ clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a
|
|||
clashE e f = throwError $ ClashE !mode e f
|
||||
|
||||
|
||||
||| true if a term is syntactically a type, or is neutral.
|
||||
|||
|
||||
||| this function *doesn't* push substitutions, because its main use is as a
|
||||
||| `So` argument to skip cases that are already known to be nonsense. and
|
||||
||| the substitutions have already been pushed.
|
||||
public export %inline
|
||||
isTyCon : (t : Term {}) -> Bool
|
||||
isTyCon (TYPE {}) = True
|
||||
|
|
@ -67,6 +72,14 @@ sameTyCon (E {}) _ = False
|
|||
|
||||
|
||||
parameters (defs : Definitions' q g)
|
||||
||| true if a type is known to be a subsingleton purely by its form.
|
||||
||| a subsingleton is a type with only zero or one possible values.
|
||||
||| equality/subtyping accepts immediately on values of subsingleton types.
|
||||
|||
|
||||
||| * a function type is a subsingleton if its codomain is.
|
||||
||| * a pair type is a subsingleton if both its elements are.
|
||||
||| * all equality types are subsingletons because uip is admissible by
|
||||
||| boundary separation.
|
||||
private
|
||||
isSubSing : Term q 0 n -> Bool
|
||||
isSubSing ty =
|
||||
|
|
@ -97,6 +110,10 @@ parameters {auto _ : HasErr q m}
|
|||
parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
||||
mutual
|
||||
namespace Term
|
||||
||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
|
||||
||| the current variance `mode`.
|
||||
|||
|
||||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
|
||||
export covering %inline
|
||||
compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
|
||||
compare0 ctx ty s t = do
|
||||
|
|
@ -106,6 +123,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
tty <- ensureTyCon ty
|
||||
compare0' ctx ty s t
|
||||
|
||||
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
|
||||
||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
|
||||
private %inline
|
||||
toLamBody : Elim q d n -> Term q d (S n)
|
||||
toLamBody e = E $ weakE e :@ BVT 0
|
||||
|
|
@ -119,29 +138,46 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
compare0' ctx (TYPE _) s t = compareType ctx s t
|
||||
|
||||
compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := Equal} $
|
||||
let ctx' = ctx :< arg
|
||||
eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
|
||||
eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b
|
||||
eta e (TUnused _) = clashT ty s t
|
||||
in
|
||||
case (s, t) of
|
||||
-- Γ, x : A ⊢ s = t : B
|
||||
-- -----------------------------------------
|
||||
-- Γ ⊢ (λx ⇒ s) = (λx ⇒ t) : (π·x : A) → B
|
||||
(Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
|
||||
(E e, Lam _ b) => eta e b
|
||||
(Lam _ b, E e) => eta e b
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
|
||||
-- Γ, x : A ⊢ s = e x : B
|
||||
-- ----------------------------------
|
||||
-- Γ ⊢ (λx ⇒ s) = e : (π·x : A) → B
|
||||
(E e, Lam _ b) => eta e b
|
||||
(Lam _ b, E e) => eta e b
|
||||
|
||||
(E e, E f) => Elim.compare0 ctx e f
|
||||
_ => throwError $ WrongType ty s t
|
||||
where
|
||||
ctx' : TContext q 0 (S n)
|
||||
ctx' = ctx :< arg
|
||||
|
||||
eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
|
||||
eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b
|
||||
eta e (TUnused _) = clashT ty s t
|
||||
|
||||
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
|
||||
-- no η (no fst/snd for π ≱ 0), so…
|
||||
-- [todo] η for π ≥ 0 maybe
|
||||
case (s, t) of
|
||||
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
|
||||
-- -------------------------------------------
|
||||
-- Γ ⊢ (s₁,t₁) = (s₂,t₂) : (x : A) × B
|
||||
--
|
||||
-- [todo] η for π ≥ 0 maybe
|
||||
(Pair sFst sSnd, Pair tFst tSnd) => do
|
||||
compare0 ctx fst sFst tFst
|
||||
compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
|
||||
|
||||
_ => throwError $ WrongType ty s t
|
||||
|
||||
-- ✨ uip ✨
|
||||
compare0' _ (Eq {}) _ _ = pure ()
|
||||
compare0' _ (Eq {}) _ _ =
|
||||
-- ✨ uip ✨
|
||||
--
|
||||
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
|
||||
pure ()
|
||||
|
||||
compare0' ctx ty@(E _) s t = do
|
||||
-- a neutral type can only be inhabited by neutral values
|
||||
|
|
@ -150,6 +186,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
E f <- pure t | _ => throwError $ WrongType ty s t
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
||| compares two types, using the current variance `mode` for universes.
|
||||
||| fails if they are not types, even if they would happen to be equal.
|
||||
export covering
|
||||
compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
|
||||
compareType ctx s t = do
|
||||
|
|
@ -167,22 +205,37 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
(0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
|
||||
(0 st : So (sameTyCon s t)) =>
|
||||
m ()
|
||||
-- equality is the same as subtyping, except with the
|
||||
-- "≤" in the TYPE rule being replaced with "="
|
||||
compareType' ctx (TYPE k) (TYPE l) =
|
||||
-- 𝓀 ≤ ℓ
|
||||
-- ----------------------
|
||||
-- Γ ⊢ Type 𝓀 <: Type ℓ
|
||||
expectModeU !mode k l
|
||||
|
||||
compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, _})
|
||||
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
|
||||
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
|
||||
-- ----------------------------------------
|
||||
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
|
||||
expectEqualQ sQty tQty
|
||||
local {mode $= flip} $ compareType ctx sArg tArg -- contra
|
||||
compareType (ctx :< sArg) sRes.term tRes.term
|
||||
|
||||
compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
|
||||
(Sig {fst = tFst, snd = tSnd, _}) = do
|
||||
-- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂
|
||||
-- --------------------------------------
|
||||
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
|
||||
compareType ctx sFst tFst
|
||||
compareType (ctx :< sFst) sSnd.term tSnd.term
|
||||
|
||||
compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
|
||||
(Eq {ty = tTy, l = tl, r = tr, _}) = do
|
||||
-- Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
|
||||
-- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i›
|
||||
-- ------------------------------------------------
|
||||
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
|
||||
compareType ctx sTy.zero tTy.zero
|
||||
compareType ctx sTy.one tTy.one
|
||||
local {mode := Equal} $ do
|
||||
|
|
@ -194,8 +247,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
-- has been inlined by whnfD
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
||| assumes the elim is already typechecked! only does the work necessary
|
||||
||| to calculate the overall type
|
||||
||| performs the minimum work required to recompute the type of an elim.
|
||||
|||
|
||||
||| ⚠ **assumes the elim is already typechecked.** ⚠
|
||||
private covering
|
||||
computeElimType : TContext q 0 n -> (e : Elim q 0 n) ->
|
||||
(0 ne : NotRedex defs e) ->
|
||||
|
|
@ -227,6 +281,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
namespace Elim
|
||||
-- [fixme] the following code ends up repeating a lot of work in the
|
||||
-- computeElimType calls. the results should be shared better
|
||||
|
||||
||| compare two eliminations according to the given variance `mode`.
|
||||
|||
|
||||
||| ⚠ **assumes that they have both been typechecked, and have
|
||||
||| equal types.** ⚠
|
||||
export covering %inline
|
||||
compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
|
||||
compare0 ctx e f =
|
||||
|
|
@ -244,6 +303,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
|
|||
m ()
|
||||
-- replace applied equalities with the appropriate end first
|
||||
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
|
||||
--
|
||||
-- [todo] maybe have typed whnf and do this (and η???) there instead
|
||||
compare0' ctx (e :% K p) f ne nf =
|
||||
compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
|
||||
compare0' ctx e (f :% K q) ne nf =
|
||||
|
|
|
|||
|
|
@ -45,8 +45,7 @@ interface Eq q => IsQty q where
|
|||
compat : Dec2 Compat
|
||||
|
||||
||| true if it is ok for this quantity to appear for the
|
||||
||| subject of a typing judgement. this is about the
|
||||
||| subject reduction stuff in atkey
|
||||
||| subject of a typing judgement [@qtt, §2.3].
|
||||
IsSubj : Pred q
|
||||
isSubj : Dec1 IsSubj
|
||||
zeroIsSubj : IsSubj zero
|
||||
|
|
|
|||
|
|
@ -69,6 +69,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
|
|||
-- substitutions. both of them seem like the same amount of work for the
|
||||
-- computer but pushing is less work for the me
|
||||
|
||||
||| "Ψ | Γ ⊢ σ · 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.
|
||||
|
|
@ -79,12 +81,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
|
|||
let Element subj nc = pushSubsts subj in
|
||||
check' ctx sg subj nc ty
|
||||
|
||||
||| `check0 ctx subj ty` checks a term in a zero context.
|
||||
||| "Ψ | Γ ⊢₀ s ⇐ A"
|
||||
|||
|
||||
||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
|
||||
export covering %inline
|
||||
check0 : TyContext q d n -> Term q d n -> Term q d n -> m ()
|
||||
check0 ctx tm ty = ignore $ check ctx szero tm ty
|
||||
-- the output will always be 𝟎 because the subject quantity is 0
|
||||
|
||||
||| "Ψ | Γ ⊢ σ · 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.
|
||||
export covering %inline
|
||||
|
|
@ -205,7 +211,6 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
|
|||
funres <- infer ctx sg fun
|
||||
(qty, argty, res) <- expectPi !ask funres.type
|
||||
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
|
||||
-- (σ ⨴ 0 = 0; σ ⨴ π = σ otherwise)
|
||||
argout <- check ctx (subjMult sg qty) arg argty
|
||||
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
|
||||
pure $ InfRes {
|
||||
|
|
|
|||
Loading…
Reference in New Issue