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

refactor elim equality error stuff

Browse source
This commit is contained in:
rhiannon morris 2023-09-12 06:48:51 +02:00
parent 1e8932690b
commit 9973f8d07b
2 changed files with 148 additions and 141 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lib/Quox/Context.idr
View file

@ -6,6 +6,7 @@ import Quox.Name
import Data.DPair import Data.DPair
import Data.Nat import Data.Nat
import Data.Singleton
import Data.SnocList import Data.SnocList
import Data.SnocVect import Data.SnocVect
import Data.Vect import Data.Vect
@ -57,6 +58,7 @@ public export
tail : Context tm (S n) -> Context tm n tail : Context tm (S n) -> Context tm n
tail = fst . unsnoc tail = fst . unsnoc
parameters {0 tm : Nat -> Type} (f : forall n. tm n -> a) parameters {0 tm : Nat -> Type} (f : forall n. tm n -> a)
export export
toSnocListWith : Telescope tm _ _ -> SnocList a toSnocListWith : Telescope tm _ _ -> SnocList a

287
lib/Quox/Equal.idr
View file

@ -35,10 +35,6 @@ parameters (loc : Loc) (ctx : EqContext n)
clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a
clashTy s t = throw $ ClashTy loc ctx !mode s t 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 private %inline
wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a
wrongType ty s = throw $ WrongType loc ctx ty s wrongType ty s = throw $ WrongType loc ctx ty s
@ -83,10 +79,10 @@ isSubSing defs ctx ty0 = do
case ty0 of case ty0 of
TYPE {} => pure False TYPE {} => pure False
Pi {arg, res, _} => 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, _} => Sig {fst, snd, _} =>
isSubSing defs ctx fst `andM` 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, _} => Enum {cases, _} =>
pure $ length (SortedSet.toList cases) <= 1 pure $ length (SortedSet.toList cases) <= 1
Eq {} => pure True Eq {} => pure True
@ -117,17 +113,6 @@ ensureTyCon loc ctx t = case nchoose $ isTyConE t of
Left y => pure y Left y => pure y
Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen) 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 namespace Term
||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to ||| `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₂ -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
expectEqualQ loc sQty tQty expectEqualQ loc sQty tQty
local flip $ compareType defs ctx sArg tArg -- contra 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, _}) compareType' defs ctx (Sig {fst = sFst, snd = sSnd, _})
(Sig {fst = tFst, snd = tSnd, _}) = do (Sig {fst = tFst, snd = tSnd, _}) = do
@ -315,7 +300,7 @@ compareType' defs ctx (Sig {fst = sFst, snd = sSnd, _})
-- -------------------------------------- -- --------------------------------------
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂ -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
compareType defs ctx sFst tFst 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, _}) compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _})
(Eq {ty = tTy, l = tl, r = tr, _}) = do (Eq {ty = tTy, l = tl, r = tr, _}) = do
@ -354,12 +339,9 @@ compareType' defs ctx (E e) (E f) = do
private private
try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error) lookupFree : Has ErrorEff fs =>
try_ act = lift $ catch (pure . Just) $ act $> Nothing Definitions -> EqContext n -> Name -> Universe -> Loc ->
Eff fs (Term 0 n)
private
lookupFree : Definitions -> EqContext n -> Name -> Universe -> Loc ->
Eff EqualInner (Term 0 n)
lookupFree defs ctx x u loc = lookupFree defs ctx x u loc =
let Val n = ctx.termLen in let Val n = ctx.termLen in
maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $ maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $
@ -367,6 +349,41 @@ lookupFree defs ctx x u loc =
namespace Elim 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 ||| 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 ||| kind. `ret` is the return type of the case expression, and `u` is the
||| universe the head is in. ||| universe the head is in.
@ -375,7 +392,7 @@ namespace Elim
(ret : Term 0 n) -> (u : Universe) -> (ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) -> (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
(def : Term 0 n) -> (def : Term 0 n) ->
Eff EqualInner () Eff EqualElim ()
compareArm {b1 = Nothing, b2 = Nothing, _} = pure () compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
compareArm defs ctx k ret u b1 b2 def = compareArm defs ctx k ret u b1 b2 def =
let def = SN def in let def = SN def in
@ -384,77 +401,74 @@ namespace Elim
compareArm_ : Definitions -> EqContext n -> (k : TyConKind) -> compareArm_ : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) -> (ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : TypeCaseArmBody k 0 n) -> (b1, b2 : TypeCaseArmBody k 0 n) ->
Eff EqualInner () Eff EqualElim ()
compareArm_ defs ctx KTYPE ret u b1 b2 = 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 compareArm_ defs ctx KPi ret u b1 b2 = do
let [< a, b] = b1.names let [< a, b] = b1.names
ctx = extendTyN ctx = extendTyN0
[< (Zero, a, TYPE u a.loc), [< (a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx (b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
compare0 defs ctx (weakT 2 ret) b1.term b2.term try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term
compareArm_ defs ctx KSig ret u b1 b2 = do compareArm_ defs ctx KSig ret u b1 b2 = do
let [< a, b] = b1.names let [< a, b] = b1.names
ctx = extendTyN ctx = extendTyN0
[< (Zero, a, TYPE u a.loc), [< (a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx (b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
compare0 defs ctx (weakT 2 ret) b1.term b2.term try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term
compareArm_ defs ctx KEnum ret u b1 b2 = 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 compareArm_ defs ctx KEq ret u b1 b2 = do
let [< a0, a1, a, l, r] = b1.names let [< a0, a1, a, l, r] = b1.names
ctx = extendTyN ctx = extendTyN0
[< (Zero, a0, TYPE u a0.loc), [< (a0, TYPE u a0.loc),
(Zero, a1, TYPE u a1.loc), (a1, TYPE u a1.loc),
(Zero, a, Eq0 (TYPE u a.loc) (a, Eq0 (TYPE u a.loc) (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
(BVT 1 a0.loc) (BVT 0 a1.loc) a.loc), (l, BVT 2 a0.loc),
(Zero, l, BVT 2 a0.loc), (r, BVT 2 a1.loc)] ctx
(Zero, r, BVT 2 a1.loc)] ctx try $ Term.compare0 defs ctx (weakT 5 ret) b1.term b2.term
compare0 defs ctx (weakT 5 ret) b1.term b2.term
compareArm_ defs ctx KNat ret u b1 b2 = 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 compareArm_ defs ctx KBOX ret u b1 b2 = do
let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx let ctx = extendTy0 b1.name (TYPE u b1.name.loc) ctx
compare0 defs ctx (weakT 1 ret) b1.term b1.term try $ Term.compare0 defs ctx (weakT 1 ret) b1.term b1.term
private covering private covering
compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) -> compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
Eff EqualInner (Maybe Error, Term 0 n) Eff EqualElim (Term 0 n)
private covering private covering
compare0Inner' : (defs : Definitions) -> EqContext n -> compare0Inner' : (defs : Definitions) -> EqContext n ->
(e, f : Elim 0 n) -> (e, f : Elim 0 n) ->
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> (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 compare0Inner' defs ctx e@(F {}) f _ _ = do
pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f, if e == f then computeElimTypeE defs ctx f
!(lookupFree defs ctx x u loc)) else clashE defs ctx e f
compare0Inner' defs ctx e@(F {}) f _ _ = clashE e.loc ctx e f
compare0Inner' defs ctx e@(B i loc) f@(B j _) _ _ = compare0Inner' defs ctx e@(B {}) f _ _ = do
pure (guard (i /= j) $> ClashE loc ctx !mode e f, if e == f then computeElimTypeE defs ctx f
ctx.tctx !! i) else clashE defs ctx e f
compare0Inner' defs ctx e@(B {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B -- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
-- Ψ | Γ ⊢ s = t ⇐ A -- Ψ | Γ ⊢ s = t ⇐ A
-- ------------------------------- -- -------------------------------
-- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x] -- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = do
local_ Equal $ do ety <- compare0Inner defs ctx e f
(err1, ety) <- compare0Inner defs ctx e f (_, arg, res) <- expectPi defs ctx eloc ety
(_, arg, res) <- expectPi defs ctx eloc ety try $ Term.compare0 defs ctx arg s t
err2 <- try_ $ Term.compare0 defs ctx arg s t pure $ sub1 res $ Ann s arg s.loc
pure (err1 <|> err2, sub1 res $ Ann s arg s.loc) compare0Inner' defs ctx e'@(App {}) f' ne nf =
compare0Inner' defs ctx e@(App {}) f _ _ = clashE e.loc ctx e f clashE defs ctx e' f'
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B -- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
-- Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R -- Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R
@ -463,20 +477,21 @@ namespace Elim
-- Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s } -- Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s }
-- = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p] -- = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
compare0Inner' defs ctx (CasePair epi e eret ebody eloc) 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 local_ Equal $ do
(err1, ety) <- compare0Inner defs ctx e f ety <- compare0Inner defs ctx e f
compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term
(fst, snd) <- expectSig defs ctx eloc ety (fst, snd) <- expectSig defs ctx eloc ety
let [< x, y] = ebody.names let [< x, y] = ebody.names
err2 <- try_ $ try $ do
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
Term.compare0 defs Term.compare0 defs
(extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
(substCasePairRet ebody.names ety eret) (substCasePairRet ebody.names ety eret)
ebody.term fbody.term ebody.term fbody.term
err3 <- try_ $ expectEqualQ e.loc epi fpi expectEqualQ e.loc epi fpi
pure (concat [err1, err2, err3], sub1 eret e) pure $ sub1 eret e
compare0Inner' defs ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e'@(CasePair {}) f' ne nf =
clashE defs ctx e' f'
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s} -- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R -- Ψ | Γ, x : {𝐚s} ⊢ Q = R
@ -487,24 +502,17 @@ namespace Elim
compare0Inner' defs ctx (CaseEnum epi e eret earms eloc) compare0Inner' defs ctx (CaseEnum epi e eret earms eloc)
(CaseEnum fpi f fret farms floc) ne nf = (CaseEnum fpi f fret farms floc) ne nf =
local_ Equal $ do local_ Equal $ do
(err1, ety) <- compare0Inner defs ctx e f ety <- compare0Inner defs ctx e f
err2 <- try_ $ try $
compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety for_ (SortedMap.toList earms) $ \(t, l) => do
exs <- for cases $ \t => do let Just r = lookup t farms
l <- lookupArm eloc t earms | Nothing => putError $ TagNotIn floc t (fromList $ keys farms)
r <- lookupArm floc t farms let t' = Ann (Tag t l.loc) ety l.loc
try_ $ try $ Term.compare0 defs ctx (sub1 eret t') l r
Term.compare0 defs ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r try $ expectEqualQ eloc epi fpi
err3 <- try_ $ expectEqualQ eloc epi fpi pure $ sub1 eret e
pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e) compare0Inner' defs ctx e@(CaseEnum {}) f _ _ = clashE defs ctx e f
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
-- Ψ | Γ ⊢ e = f ⇒ ℕ -- Ψ | Γ ⊢ e = f ⇒ ℕ
-- Ψ | Γ, x : ℕ ⊢ Q = R -- Ψ | Γ, x : ℕ ⊢ Q = R
@ -517,22 +525,20 @@ namespace Elim
compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc) compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc)
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf = (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
local_ Equal $ do local_ Equal $ do
(err1, ety) <- compare0Inner defs ctx e f ety <- compare0Inner defs ctx e f
err2 <- try_ $ let [< p, ih] = esuc.names
compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term try $ do
err3 <- try_ $ compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
Term.compare0 defs ctx Term.compare0 defs ctx
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc)) (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
ezer fzer ezer fzer
let [< p, ih] = esuc.names
err4 <- try_ $
Term.compare0 defs Term.compare0 defs
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term (substCaseSuccRet esuc.names eret) esuc.term fsuc.term
err5 <- try_ $ expectEqualQ e.loc epi fpi expectEqualQ e.loc epi fpi
err6 <- try_ $ expectEqualQ e.loc epi' fpi' expectEqualQ e.loc epi' fpi'
pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e) pure $ sub1 eret e
compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE defs ctx e f
-- Ψ | Γ ⊢ e = f ⇒ [ρ. A] -- Ψ | Γ ⊢ e = f ⇒ [ρ. A]
-- Ψ | Γ, x : [ρ. A] ⊢ Q = R -- Ψ | Γ, x : [ρ. A] ⊢ Q = R
@ -543,19 +549,18 @@ namespace Elim
compare0Inner' defs ctx (CaseBox epi e eret ebody eloc) compare0Inner' defs ctx (CaseBox epi e eret ebody eloc)
(CaseBox fpi f fret fbody floc) ne nf = (CaseBox fpi f fret fbody floc) ne nf =
local_ Equal $ do local_ Equal $ do
(err1, ety) <- compare0Inner defs ctx e f ety <- compare0Inner defs ctx e f
err2 <- try_ $
compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term
(q, ty) <- expectBOX defs ctx eloc ety (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) Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx)
(substCaseBoxRet ebody.name ety eret) (substCaseBoxRet ebody.name ety eret)
ebody.term fbody.term ebody.term fbody.term
err4 <- try_ $ expectEqualQ eloc epi fpi expectEqualQ eloc epi fpi
pure (concat [err1, err2, err3, err4], sub1 eret e) pure $ sub1 eret e
compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f 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 {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
@ -566,8 +571,8 @@ namespace Elim
-- and similar for :> and A -- and similar for :> and A
compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do
ty <- bigger a b ty <- bigger a b
err <- try_ $ Term.compare0 defs ctx ty s t try $ Term.compare0 defs ctx ty s t
pure (err, ty) pure ty
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
-- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
@ -579,12 +584,13 @@ namespace Elim
(Coe ty2 p2 q2 val2 _) ne nf = do (Coe ty2 p2 q2 val2 _) ne nf = do
let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2 let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2 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) (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
err3 <- try_ $ Term.compare0 defs ctx ty_p val1 val2 try $ do
pure (concat [err1, err2, err3], ty_q) compareType defs ctx ty1p ty2p
compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f 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) -- (no neutral compositions in a closed dctx)
compare0Inner' _ _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne 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) compare0Inner' defs ctx (TypeCase ty1 ret1 arms1 def1 eloc)
(TypeCase ty2 ret2 arms2 def2 floc) ne _ = (TypeCase ty2 ret2 arms2 def2 floc) ne _ =
local_ Equal $ do local_ Equal $ do
(err1, ety) <- compare0Inner defs ctx ty1 ty2 ety <- compare0Inner defs ctx ty1 ty2
u <- expectTYPE defs ctx eloc ety u <- expectTYPE defs ctx eloc ety
err2 <- try_ $ compareType defs ctx ret1 ret2 try $ do
err3 <- try_ $ compareType defs ctx def1 def2 compareType defs ctx ret1 ret2
exs <- for allKinds $ \k => compareType defs ctx def1 def2
try_ $ for_ allKinds $ \k =>
compareArm defs ctx k ret1 u compareArm defs ctx k ret1 u
(lookupPrecise k arms1) (lookupPrecise k arms2) def1 (lookupPrecise k arms1) (lookupPrecise k arms2) def1
pure (concat $ [err1, err2, err3] ++ exs, ret1) pure ret1
compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE defs ctx e f
-- Ψ | Γ ⊢ s <: f ⇐ A -- Ψ | Γ ⊢ s <: f ⇐ A
-- -------------------------- -- --------------------------
@ -612,23 +618,23 @@ namespace Elim
-- --
-- and vice versa -- and vice versa
compare0Inner' defs ctx (Ann s a _) f _ _ = do compare0Inner' defs ctx (Ann s a _) f _ _ = do
err <- try_ $ Term.compare0 defs ctx a s (E f) try $ Term.compare0 defs ctx a s (E f)
pure (err, a) pure a
compare0Inner' defs ctx e (Ann t b _) _ _ = do compare0Inner' defs ctx e (Ann t b _) _ _ = do
err <- try_ $ Term.compare0 defs ctx b (E e) t try $ Term.compare0 defs ctx b (E e) t
pure (err, b) pure b
compare0Inner' defs ctx e@(Ann {}) f _ _ = compare0Inner' defs ctx e@(Ann {}) f _ _ =
clashE e.loc ctx e f clashE defs ctx e f
compare0Inner defs ctx e f = compare0Inner defs ctx e f = do
wrapErr (WhileComparingE ctx !mode e f) $ do let Val n = ctx.termLen
let Val n = ctx.termLen Element e ne <- whnf defs ctx e.loc e
Element e ne <- whnf defs ctx e.loc e Element f nf <- whnf defs ctx f.loc f
Element f nf <- whnf defs ctx f.loc f ty <- compare0Inner' defs ctx e f ne nf
(err, ty) <- compare0Inner' defs ctx e f ne nf if !(lift $ isSubSing defs ctx ty)
if !(isSubSing defs ctx ty) then putAt InnerErr Nothing
then pure (Nothing, ty) else modifyAt InnerErr $ map $ WhileComparingE ctx !mode e f
else pure (err, ty) pure ty
namespace Term namespace Term
@ -643,7 +649,7 @@ namespace Term
namespace Elim namespace Elim
compare0 defs ctx e f = do 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 maybe (pure ty) throw err
compareType defs ctx s t = do compareType defs ctx s t = do
@ -657,7 +663,6 @@ compareType defs ctx s t = do
compareType' defs ctx s' t' compareType' defs ctx s' t'
parameters (loc : Loc) (ctx : TyContext d n) parameters (loc : Loc) (ctx : TyContext d n)
-- [todo] only split on the dvars that are actually used anywhere in -- [todo] only split on the dvars that are actually used anywhere in
-- the calls to `splits` -- the calls to `splits`