rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

update compare0 for type-directed whnf

Browse source
This commit is contained in:
rhiannon morris 2023-08-26 21:32:15 +02:00
parent ba77c45c64
commit edfe30ff63
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
lib/Quox/Equal.idr
View file

@ -499,16 +499,18 @@ parameters (defs : Definitions)
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
-- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
-- Ψ | Γ ⊢ e <: f ⇒ _
-- (non-neutral forms have the coercion already pushed in)
-- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
-- -----------------------------------------------------------
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖›
compare0' ctx (Coe ty1 p1 q1 (E val1) _)
(Coe ty2 p2 q2 (E val2) _) ne nf = do
compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
compare0 ctx val1 val2
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
compare0' ctx (Coe ty1 p1 q1 val1 _)
(Coe ty2 p2 q2 val2 _) ne nf = do
let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
compareType ctx ty1p ty2p
compareType ctx ty1q ty2q
let ty_p = case !mode of Super => ty1p; _ => ty2p
Term.compare0 ctx ty_p val1 val2
compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
-- (no neutral compositions in a closed dctx)