From 67c825ab396751b264a7f8613b2c37714edd917e Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 15 Apr 2024 22:40:20 +0200 Subject: [PATCH] add coercion regularity to the equality checker (not to whnf) --- lib/Quox/Equal.idr | 86 +++++++++++++++++++++++++++++----------------- 1 file changed, 54 insertions(+), 32 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 796b6ff..9506a72 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -8,6 +8,7 @@ import Quox.EffExtra import Data.List1 import Data.Maybe +import Data.Either %default total @@ -527,7 +528,7 @@ namespace Elim EqualElim : List (Type -> Type) EqualElim = InnerErrEff :: EqualInner - private covering + private covering %inline computeElimTypeE : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) -> (e : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) => @@ -535,14 +536,18 @@ namespace Elim computeElimTypeE defs ectx sg e = lift $ computeElimType defs (toWhnfContext ectx) sg e - private + private %inline putError : Has InnerErrEff fs => Error -> Eff fs () putError err = modifyAt InnerErr (<|> Just err) - private + private %inline try : Eff EqualInner () -> Eff EqualElim () try act = lift $ catch putError $ lift act {fs' = EqualElim} + private %inline + nested : Eff EqualInner a -> Eff EqualElim (Either Error a) + nested act = lift $ runExcept act + private covering %inline clashE : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) -> (e, f : Elim 0 n) -> (0 nf : NotRedexEq defs ctx sg f) => @@ -580,6 +585,52 @@ namespace Elim (0 nf : NotRedexEq defs ctx sg f) -> Eff EqualElim (Term 0 n) + -- (no neutral dim apps or comps in a closed dctx) + compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ = + void $ absurd $ noOr2 $ noOr2 ne + compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf = + void $ absurd $ noOr2 $ noOr2 nf + compare0Inner' _ _ _ (Comp {r = K {}, _}) _ ne _ = void $ absurd $ noOr2 ne + compare0Inner' _ _ _ (Comp {r = B i _, _}) _ _ _ = absurd i + compare0Inner' _ _ _ _ (Comp {r = K {}, _}) _ nf = void $ absurd $ noOr2 nf + + -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› + -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› + -- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖› + -- ----------------------------------------------------------- + -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s + -- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖› + compare0Inner' defs ctx sg (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 + (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q) + try $ do + compareType defs ctx ty1p ty2p + compareType defs ctx ty1q ty2q + Term.compare0 defs ctx sg ty_p val1 val2 + pure $ ty_q + + -- an adaptation of the rule + -- + -- Ψ | Γ ⊢ A‹0/𝑖› = A‹1/𝑖› ⇐ ★ + -- ----------------------------------------------------- + -- Ψ | Γ ⊢ coe (𝑖 ⇒ A) @p @q s ⇝ (s ∷ A‹1/𝑖›) ⇒ A‹1/𝑖› + -- + -- it's here so that whnf doesn't have to depend on the equality checker + compare0Inner' defs ctx sg (Coe ty p q val loc) f _ _ = do + tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one + if isRight tyEq + then compare0Inner defs ctx sg (Ann val (dsub1 ty q) loc) f + else clashE defs ctx sg (Coe ty p q val loc) f + + -- symmetric version of the above + compare0Inner' defs ctx sg e (Coe ty p q val loc) _ _ = do + tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one + if isRight tyEq + then compare0Inner defs ctx sg e (Ann val (dsub1 ty q) loc) + else clashE defs ctx sg e (Coe ty p q val loc) + compare0Inner' defs ctx sg e@(F {}) f _ _ = do if e == f then computeElimTypeE defs ctx sg f else clashE defs ctx sg e f @@ -711,12 +762,6 @@ namespace Elim pure $ sub1 eret e compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f - -- (no neutral dim apps in a closed dctx) - compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ = - void $ absurd $ noOr2 $ noOr2 ne - compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf = - void $ absurd $ noOr2 $ noOr2 nf - -- Ψ | Γ ⊢ s <: t : B -- -------------------------------- -- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B @@ -727,29 +772,6 @@ namespace Elim try $ Term.compare0 defs ctx sg ty s t pure ty - -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› - -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› - -- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖› - -- ----------------------------------------------------------- - -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s - -- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖› - compare0Inner' defs ctx sg (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 - (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q) - try $ do - compareType defs ctx ty1p ty2p - compareType defs ctx ty1q ty2q - Term.compare0 defs ctx sg ty_p val1 val2 - pure $ ty_q - compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f - - -- (no neutral compositions in a closed dctx) - compare0Inner' _ _ _ (Comp {r = K {}, _}) _ ne _ = void $ absurd $ noOr2 ne - compare0Inner' _ _ _ (Comp {r = B i _, _}) _ _ _ = absurd i - compare0Inner' _ _ _ _ (Comp {r = K {}, _}) _ nf = void $ absurd $ noOr2 nf - -- (type case equality purely structural) compare0Inner' defs ctx sg (TypeCase ty1 ret1 arms1 def1 eloc) (TypeCase ty2 ret2 arms2 def2 floc) ne _ =