From 9973f8d07b919f43c4671eeac4e1fc48bc4b257d Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 12 Sep 2023 06:48:51 +0200 Subject: [PATCH] refactor elim equality error stuff --- lib/Quox/Context.idr | 2 + lib/Quox/Equal.idr | 287 ++++++++++++++++++++++--------------------- 2 files changed, 148 insertions(+), 141 deletions(-) diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index b1a9376..0a923b3 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -6,6 +6,7 @@ import Quox.Name import Data.DPair import Data.Nat +import Data.Singleton import Data.SnocList import Data.SnocVect import Data.Vect @@ -57,6 +58,7 @@ public export tail : Context tm (S n) -> Context tm n tail = fst . unsnoc + parameters {0 tm : Nat -> Type} (f : forall n. tm n -> a) export toSnocListWith : Telescope tm _ _ -> SnocList a diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index adb0de3..ea54e4f 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -35,10 +35,6 @@ parameters (loc : Loc) (ctx : EqContext n) clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a clashTy s t = throw $ ClashTy loc ctx !mode s t - private %inline - clashE : Elim 0 n -> Elim 0 n -> Eff EqualInner a - clashE e f = throw $ ClashE loc ctx !mode e f - private %inline wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a wrongType ty s = throw $ WrongType loc ctx ty s @@ -83,10 +79,10 @@ isSubSing defs ctx ty0 = do case ty0 of TYPE {} => pure False Pi {arg, res, _} => - isSubSing defs (extendTy Zero res.name arg ctx) res.term + isSubSing defs (extendTy0 res.name arg ctx) res.term Sig {fst, snd, _} => isSubSing defs ctx fst `andM` - isSubSing defs (extendTy Zero snd.name fst ctx) snd.term + isSubSing defs (extendTy0 snd.name fst ctx) snd.term Enum {cases, _} => pure $ length (SortedSet.toList cases) <= 1 Eq {} => pure True @@ -117,17 +113,6 @@ ensureTyCon loc ctx t = case nchoose $ isTyConE t of Left y => pure y Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen) -||| performs the minimum work required to recompute the type of an elim. -||| -||| ⚠ **assumes the elim is already typechecked.** ⚠ -private covering -computeElimTypeE : (defs : Definitions) -> EqContext n -> - (e : Elim 0 n) -> (0 ne : NotRedex defs e) => - Eff EqualInner (Term 0 n) -computeElimTypeE defs ectx e = - let Val n = ectx.termLen in - lift $ computeElimType defs (toWhnfContext ectx) e - namespace Term ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to @@ -307,7 +292,7 @@ compareType' defs ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc}) -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ expectEqualQ loc sQty tQty local flip $ compareType defs ctx sArg tArg -- contra - compareType defs (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term + compareType defs (extendTy0 sRes.name sArg ctx) sRes.term tRes.term compareType' defs ctx (Sig {fst = sFst, snd = sSnd, _}) (Sig {fst = tFst, snd = tSnd, _}) = do @@ -315,7 +300,7 @@ compareType' defs ctx (Sig {fst = sFst, snd = sSnd, _}) -- -------------------------------------- -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂ compareType defs ctx sFst tFst - compareType defs (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term + compareType defs (extendTy0 sSnd.name sFst ctx) sSnd.term tSnd.term compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _}) (Eq {ty = tTy, l = tl, r = tr, _}) = do @@ -354,12 +339,9 @@ compareType' defs ctx (E e) (E f) = do private -try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error) -try_ act = lift $ catch (pure . Just) $ act $> Nothing - -private -lookupFree : Definitions -> EqContext n -> Name -> Universe -> Loc -> - Eff EqualInner (Term 0 n) +lookupFree : Has ErrorEff fs => + Definitions -> EqContext n -> Name -> Universe -> Loc -> + Eff fs (Term 0 n) lookupFree defs ctx x u loc = let Val n = ctx.termLen in maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $ @@ -367,6 +349,41 @@ lookupFree defs ctx x u loc = namespace Elim + private data InnerErr : Type where + + private + InnerErrEff : Type -> Type + InnerErrEff = StateL InnerErr (Maybe Error) + + private + EqualElim : List (Type -> Type) + EqualElim = InnerErrEff :: EqualInner + + private covering + computeElimTypeE : (defs : Definitions) -> EqContext n -> + (e : Elim 0 n) -> (0 ne : NotRedex defs e) => + Eff EqualElim (Term 0 n) + computeElimTypeE defs ectx e = + let Val n = ectx.termLen in + lift $ computeElimType defs (toWhnfContext ectx) e + + private + putError : Has InnerErrEff fs => Error -> Eff fs () + putError err = modifyAt InnerErr (<|> Just err) + + private + try : Eff EqualInner () -> Eff EqualElim () + try act = lift $ catch putError $ lift act {fs' = EqualElim} + + private covering %inline + clashE : (defs : Definitions) -> EqContext n -> + (e, f : Elim 0 n) -> (0 nf : NotRedex defs f) => + Eff EqualElim (Term 0 n) + clashE defs ctx e f = do + putError $ ClashE e.loc ctx !mode e f + computeElimTypeE defs ctx f + + ||| compare two type-case branches, which came from the arms of the given ||| kind. `ret` is the return type of the case expression, and `u` is the ||| universe the head is in. @@ -375,7 +392,7 @@ namespace Elim (ret : Term 0 n) -> (u : Universe) -> (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) -> (def : Term 0 n) -> - Eff EqualInner () + Eff EqualElim () compareArm {b1 = Nothing, b2 = Nothing, _} = pure () compareArm defs ctx k ret u b1 b2 def = let def = SN def in @@ -384,77 +401,74 @@ namespace Elim compareArm_ : Definitions -> EqContext n -> (k : TyConKind) -> (ret : Term 0 n) -> (u : Universe) -> (b1, b2 : TypeCaseArmBody k 0 n) -> - Eff EqualInner () + Eff EqualElim () compareArm_ defs ctx KTYPE ret u b1 b2 = - compare0 defs ctx ret b1.term b2.term + try $ Term.compare0 defs ctx ret b1.term b2.term compareArm_ defs ctx KPi ret u b1 b2 = do let [< a, b] = b1.names - ctx = extendTyN - [< (Zero, a, TYPE u a.loc), - (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx - compare0 defs ctx (weakT 2 ret) b1.term b2.term + ctx = extendTyN0 + [< (a, TYPE u a.loc), + (b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx + try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term compareArm_ defs ctx KSig ret u b1 b2 = do let [< a, b] = b1.names - ctx = extendTyN - [< (Zero, a, TYPE u a.loc), - (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx - compare0 defs ctx (weakT 2 ret) b1.term b2.term + ctx = extendTyN0 + [< (a, TYPE u a.loc), + (b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx + try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term compareArm_ defs ctx KEnum ret u b1 b2 = - compare0 defs ctx ret b1.term b2.term + try $ Term.compare0 defs ctx ret b1.term b2.term compareArm_ defs ctx KEq ret u b1 b2 = do let [< a0, a1, a, l, r] = b1.names - ctx = extendTyN - [< (Zero, a0, TYPE u a0.loc), - (Zero, a1, TYPE u a1.loc), - (Zero, a, Eq0 (TYPE u a.loc) - (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc), - (Zero, l, BVT 2 a0.loc), - (Zero, r, BVT 2 a1.loc)] ctx - compare0 defs ctx (weakT 5 ret) b1.term b2.term + ctx = extendTyN0 + [< (a0, TYPE u a0.loc), + (a1, TYPE u a1.loc), + (a, Eq0 (TYPE u a.loc) (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc), + (l, BVT 2 a0.loc), + (r, BVT 2 a1.loc)] ctx + try $ Term.compare0 defs ctx (weakT 5 ret) b1.term b2.term compareArm_ defs ctx KNat ret u b1 b2 = - compare0 defs ctx ret b1.term b2.term + try $ Term.compare0 defs ctx ret b1.term b2.term compareArm_ defs ctx KBOX ret u b1 b2 = do - let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx - compare0 defs ctx (weakT 1 ret) b1.term b1.term + let ctx = extendTy0 b1.name (TYPE u b1.name.loc) ctx + try $ Term.compare0 defs ctx (weakT 1 ret) b1.term b1.term private covering compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) -> - Eff EqualInner (Maybe Error, Term 0 n) + Eff EqualElim (Term 0 n) private covering compare0Inner' : (defs : Definitions) -> EqContext n -> (e, f : Elim 0 n) -> (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> - Eff EqualInner (Maybe Error, Term 0 n) + Eff EqualElim (Term 0 n) - compare0Inner' defs ctx e@(F x u loc) f@(F y v _) _ _ = do - pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f, - !(lookupFree defs ctx x u loc)) - compare0Inner' defs ctx e@(F {}) f _ _ = clashE e.loc ctx e f + compare0Inner' defs ctx e@(F {}) f _ _ = do + if e == f then computeElimTypeE defs ctx f + else clashE defs ctx e f - compare0Inner' defs ctx e@(B i loc) f@(B j _) _ _ = - pure (guard (i /= j) $> ClashE loc ctx !mode e f, - ctx.tctx !! i) - compare0Inner' defs ctx e@(B {}) f _ _ = clashE e.loc ctx e f + compare0Inner' defs ctx e@(B {}) f _ _ = do + if e == f then computeElimTypeE defs ctx f + else clashE defs ctx e f -- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B -- Ψ | Γ ⊢ s = t ⇐ A -- ------------------------------- -- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x] - compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = - local_ Equal $ do - (err1, ety) <- compare0Inner defs ctx e f - (_, arg, res) <- expectPi defs ctx eloc ety - err2 <- try_ $ Term.compare0 defs ctx arg s t - pure (err1 <|> err2, sub1 res $ Ann s arg s.loc) - compare0Inner' defs ctx e@(App {}) f _ _ = clashE e.loc ctx e f + compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = do + ety <- compare0Inner defs ctx e f + (_, arg, res) <- expectPi defs ctx eloc ety + try $ Term.compare0 defs ctx arg s t + pure $ sub1 res $ Ann s arg s.loc + compare0Inner' defs ctx e'@(App {}) f' ne nf = + clashE defs ctx e' f' -- Ψ | Γ ⊢ e = f ⇒ (x : A) × B -- Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R @@ -463,20 +477,21 @@ namespace Elim -- Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s } -- = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p] compare0Inner' defs ctx (CasePair epi e eret ebody eloc) - (CasePair fpi f fret fbody {}) ne nf = + (CasePair fpi f fret fbody floc) ne nf = local_ Equal $ do - (err1, ety) <- compare0Inner defs ctx e f - compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term + ety <- compare0Inner defs ctx e f (fst, snd) <- expectSig defs ctx eloc ety let [< x, y] = ebody.names - err2 <- try_ $ + try $ do + compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) (substCasePairRet ebody.names ety eret) ebody.term fbody.term - err3 <- try_ $ expectEqualQ e.loc epi fpi - pure (concat [err1, err2, err3], sub1 eret e) - compare0Inner' defs ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f + expectEqualQ e.loc epi fpi + pure $ sub1 eret e + compare0Inner' defs ctx e'@(CasePair {}) f' ne nf = + clashE defs ctx e' f' -- Ψ | Γ ⊢ e = f ⇒ {𝐚s} -- Ψ | Γ, x : {𝐚s} ⊢ Q = R @@ -487,24 +502,17 @@ namespace Elim compare0Inner' defs ctx (CaseEnum epi e eret earms eloc) (CaseEnum fpi f fret farms floc) ne nf = local_ Equal $ do - (err1, ety) <- compare0Inner defs ctx e f - err2 <- try_ $ - compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term - cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety - exs <- for cases $ \t => do - l <- lookupArm eloc t earms - r <- lookupArm floc t farms - try_ $ - Term.compare0 defs ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r - err3 <- try_ $ expectEqualQ eloc epi fpi - pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e) - where - lookupArm : Loc -> TagVal -> CaseEnumArms d n -> - Eff EqualInner (Term d n) - lookupArm loc t arms = case lookup t arms of - Just arm => pure arm - Nothing => throw $ TagNotIn loc t (fromList $ keys arms) - compare0Inner' defs ctx e@(CaseEnum {}) f _ _ = clashE e.loc ctx e f + ety <- compare0Inner defs ctx e f + try $ + compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term + for_ (SortedMap.toList earms) $ \(t, l) => do + let Just r = lookup t farms + | Nothing => putError $ TagNotIn floc t (fromList $ keys farms) + let t' = Ann (Tag t l.loc) ety l.loc + try $ Term.compare0 defs ctx (sub1 eret t') l r + try $ expectEqualQ eloc epi fpi + pure $ sub1 eret e + compare0Inner' defs ctx e@(CaseEnum {}) f _ _ = clashE defs ctx e f -- Ψ | Γ ⊢ e = f ⇒ ℕ -- Ψ | Γ, x : ℕ ⊢ Q = R @@ -517,22 +525,20 @@ namespace Elim compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc) (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf = local_ Equal $ do - (err1, ety) <- compare0Inner defs ctx e f - err2 <- try_ $ - compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term - err3 <- try_ $ + ety <- compare0Inner defs ctx e f + let [< p, ih] = esuc.names + try $ do + compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs ctx (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc)) ezer fzer - let [< p, ih] = esuc.names - err4 <- try_ $ Term.compare0 defs (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) (substCaseSuccRet esuc.names eret) esuc.term fsuc.term - err5 <- try_ $ expectEqualQ e.loc epi fpi - err6 <- try_ $ expectEqualQ e.loc epi' fpi' - pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e) - compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f + expectEqualQ e.loc epi fpi + expectEqualQ e.loc epi' fpi' + pure $ sub1 eret e + compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE defs ctx e f -- Ψ | Γ ⊢ e = f ⇒ [ρ. A] -- Ψ | Γ, x : [ρ. A] ⊢ Q = R @@ -543,19 +549,18 @@ namespace Elim compare0Inner' defs ctx (CaseBox epi e eret ebody eloc) (CaseBox fpi f fret fbody floc) ne nf = local_ Equal $ do - (err1, ety) <- compare0Inner defs ctx e f - err2 <- try_ $ - compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term + ety <- compare0Inner defs ctx e f (q, ty) <- expectBOX defs ctx eloc ety - err3 <- try_ $ + try $ do + compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) (substCaseBoxRet ebody.name ety eret) ebody.term fbody.term - err4 <- try_ $ expectEqualQ eloc epi fpi - pure (concat [err1, err2, err3, err4], sub1 eret e) - compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f + expectEqualQ eloc epi fpi + pure $ sub1 eret e + compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE defs ctx e f - -- all dim apps replaced with ends by whnf + -- (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 @@ -566,8 +571,8 @@ namespace Elim -- and similar for :> and A compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do ty <- bigger a b - err <- try_ $ Term.compare0 defs ctx ty s t - pure (err, ty) + try $ Term.compare0 defs ctx ty s t + pure ty -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› @@ -579,12 +584,13 @@ namespace Elim (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 - err1 <- try_ $ compareType defs ctx ty1p ty2p - err2 <- try_ $ compareType defs ctx ty1q ty2q (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q) - err3 <- try_ $ Term.compare0 defs ctx ty_p val1 val2 - pure (concat [err1, err2, err3], ty_q) - compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f + try $ do + compareType defs ctx ty1p ty2p + compareType defs ctx ty1q ty2q + Term.compare0 defs ctx ty_p val1 val2 + pure $ ty_q + compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE defs ctx e f -- (no neutral compositions in a closed dctx) compare0Inner' _ _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne @@ -595,16 +601,16 @@ namespace Elim compare0Inner' defs ctx (TypeCase ty1 ret1 arms1 def1 eloc) (TypeCase ty2 ret2 arms2 def2 floc) ne _ = local_ Equal $ do - (err1, ety) <- compare0Inner defs ctx ty1 ty2 - u <- expectTYPE defs ctx eloc ety - err2 <- try_ $ compareType defs ctx ret1 ret2 - err3 <- try_ $ compareType defs ctx def1 def2 - exs <- for allKinds $ \k => - try_ $ - compareArm defs ctx k ret1 u - (lookupPrecise k arms1) (lookupPrecise k arms2) def1 - pure (concat $ [err1, err2, err3] ++ exs, ret1) - compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f + ety <- compare0Inner defs ctx ty1 ty2 + u <- expectTYPE defs ctx eloc ety + try $ do + compareType defs ctx ret1 ret2 + compareType defs ctx def1 def2 + for_ allKinds $ \k => + compareArm defs ctx k ret1 u + (lookupPrecise k arms1) (lookupPrecise k arms2) def1 + pure ret1 + compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE defs ctx e f -- Ψ | Γ ⊢ s <: f ⇐ A -- -------------------------- @@ -612,23 +618,23 @@ namespace Elim -- -- and vice versa compare0Inner' defs ctx (Ann s a _) f _ _ = do - err <- try_ $ Term.compare0 defs ctx a s (E f) - pure (err, a) + try $ Term.compare0 defs ctx a s (E f) + pure a compare0Inner' defs ctx e (Ann t b _) _ _ = do - err <- try_ $ Term.compare0 defs ctx b (E e) t - pure (err, b) + try $ Term.compare0 defs ctx b (E e) t + pure b compare0Inner' defs ctx e@(Ann {}) f _ _ = - clashE e.loc ctx e f + clashE defs ctx e f - compare0Inner defs ctx e f = - wrapErr (WhileComparingE ctx !mode e f) $ do - let Val n = ctx.termLen - Element e ne <- whnf defs ctx e.loc e - Element f nf <- whnf defs ctx f.loc f - (err, ty) <- compare0Inner' defs ctx e f ne nf - if !(isSubSing defs ctx ty) - then pure (Nothing, ty) - else pure (err, ty) + compare0Inner defs ctx e f = do + let Val n = ctx.termLen + Element e ne <- whnf defs ctx e.loc e + Element f nf <- whnf defs ctx f.loc f + ty <- compare0Inner' defs ctx e f ne nf + if !(lift $ isSubSing defs ctx ty) + then putAt InnerErr Nothing + else modifyAt InnerErr $ map $ WhileComparingE ctx !mode e f + pure ty namespace Term @@ -643,7 +649,7 @@ namespace Term namespace Elim compare0 defs ctx e f = do - (err, ty) <- compare0Inner defs ctx e f + (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx e f maybe (pure ty) throw err compareType defs ctx s t = do @@ -657,7 +663,6 @@ compareType defs ctx s t = do compareType' defs ctx s' t' - parameters (loc : Loc) (ctx : TyContext d n) -- [todo] only split on the dvars that are actually used anywhere in -- the calls to `splits`