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

untangle big mutual block in Equal

Browse source
This commit is contained in:
rhiannon morris 2023-08-28 22:07:33 +02:00
parent d5d30ee198
commit 1e8932690b
1 changed files with 486 additions and 470 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

410
lib/Quox/Equal.idr
View file

@ -103,6 +103,7 @@ isSubSing defs ctx ty0 = do
Box {} => pure False Box {} => pure False
||| the left argument if the current mode is `Super`; otherwise the right one.
private %inline private %inline
bigger : Has EqModeState fs => (left, right : Lazy a) -> Eff fs a bigger : Has EqModeState fs => (left, right : Lazy a) -> Eff fs a
bigger l r = gets $ \case Super => l; _ => r bigger l r = gets $ \case Super => l; _ => r
@ -127,23 +128,31 @@ computeElimTypeE defs ectx e =
let Val n = ectx.termLen in let Val n = ectx.termLen in
lift $ computeElimType defs (toWhnfContext ectx) e lift $ computeElimType defs (toWhnfContext ectx) e
parameters (defs : Definitions)
mutual
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
||| the current variance `mode`. ||| the current variance `mode`.
||| |||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠ ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
export covering %inline export covering %inline
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Eff EqualInner () compare0 : Definitions -> EqContext n -> (ty, s, t : Term 0 n) ->
compare0 ctx ty s t = Eff EqualInner ()
wrapErr (WhileComparingT ctx !mode ty s t) $ do
let Val n = ctx.termLen namespace Elim
Element ty' _ <- whnf defs ctx ty.loc ty ||| compare two eliminations according to the given variance `mode`.
Element s' _ <- whnf defs ctx s.loc s |||
Element t' _ <- whnf defs ctx t.loc t ||| ⚠ **assumes that they have both been typechecked, and have
tty <- ensureTyCon ty.loc ctx ty' ||| equal types.** ⚠
compare0' ctx ty' s' t' export covering %inline
compare0 : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
Eff EqualInner (Term 0 n)
||| 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 %inline
compareType : Definitions -> EqContext n -> (s, t : Term 0 n) ->
Eff EqualInner ()
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with ||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t". ||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
@ -151,21 +160,22 @@ parameters (defs : Definitions)
toLamBody : Elim d n -> Term d (S n) toLamBody : Elim d n -> Term d (S n)
toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
namespace Term
private covering private covering
compare0' : EqContext n -> compare0' : (defs : Definitions) -> EqContext n ->
(ty, s, t : Term 0 n) -> (ty, s, t : Term 0 n) ->
(0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) => (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
(0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) => (0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) =>
Eff EqualInner () Eff EqualInner ()
compare0' ctx (TYPE {}) s t = compareType ctx s t compare0' defs ctx (TYPE {}) s t = compareType defs ctx s t
compare0' ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $ compare0' defs ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $
case (s, t) of case (s, t) of
-- Γ, x : A ⊢ s = t : B -- Γ, x : A ⊢ s = t : B
-- ------------------------------------------- -- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B -- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
(Lam b1 {}, Lam b2 {}) => (Lam b1 {}, Lam b2 {}) =>
compare0 ctx' res.term b1.term b2.term compare0 defs ctx' res.term b1.term b2.term
-- Γ, x : A ⊢ s = e x : B -- Γ, x : A ⊢ s = e x : B
-- ----------------------------------- -- -----------------------------------
@ -173,7 +183,7 @@ parameters (defs : Definitions)
(E e, Lam b {}) => eta s.loc e b (E e, Lam b {}) => eta s.loc e b
(Lam b {}, E e) => eta s.loc e b (Lam b {}, E e) => eta s.loc e b
(E e, E f) => ignore $ Elim.compare0 ctx e f (E e, E f) => ignore $ Elim.compare0 defs ctx e f
(Lam {}, t) => wrongType t.loc ctx ty t (Lam {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t
@ -183,10 +193,10 @@ parameters (defs : Definitions)
ctx' = extendTy qty res.name arg ctx ctx' = extendTy qty res.name arg ctx
eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
eta _ e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b eta _ e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b
eta loc e (S _ (N _)) = clashT loc ctx ty s t eta loc e (S _ (N _)) = clashT loc ctx ty s t
compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $ compare0' defs ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
case (s, t) of case (s, t) of
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x} -- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
-- -------------------------------------------- -- --------------------------------------------
@ -194,10 +204,10 @@ parameters (defs : Definitions)
-- --
-- [todo] η for π ≥ 0 maybe -- [todo] η for π ≥ 0 maybe
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
compare0 ctx fst sFst tFst compare0 defs ctx fst sFst tFst
compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd compare0 defs ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
(E e, E f) => ignore $ Elim.compare0 ctx e f (E e, E f) => ignore $ Elim.compare0 defs ctx e f
(Pair {}, E _) => clashT s.loc ctx ty s t (Pair {}, E _) => clashT s.loc ctx ty s t
(E _, Pair {}) => clashT s.loc ctx ty s t (E _, Pair {}) => clashT s.loc ctx ty s t
@ -206,7 +216,7 @@ parameters (defs : Definitions)
(E _, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s (s, _) => wrongType s.loc ctx ty s
compare0' ctx ty@(Enum {}) s t = local_ Equal $ compare0' defs ctx ty@(Enum {}) s t = local_ Equal $
case (s, t) of case (s, t) of
-- -------------------- -- --------------------
-- Γ ⊢ `t = `t : {ts} -- Γ ⊢ `t = `t : {ts}
@ -214,7 +224,7 @@ parameters (defs : Definitions)
-- t ∈ ts is in the typechecker, not here, ofc -- t ∈ ts is in the typechecker, not here, ofc
(Tag t1 {}, Tag t2 {}) => (Tag t1 {}, Tag t2 {}) =>
unless (t1 == t2) $ clashT s.loc ctx ty s t unless (t1 == t2) $ clashT s.loc ctx ty s t
(E e, E f) => ignore $ Elim.compare0 ctx e f (E e, E f) => ignore $ Elim.compare0 defs ctx e f
(Tag {}, E _) => clashT s.loc ctx ty s t (Tag {}, E _) => clashT s.loc ctx ty s t
(E _, Tag {}) => clashT s.loc ctx ty s t (E _, Tag {}) => clashT s.loc ctx ty s t
@ -223,14 +233,14 @@ parameters (defs : Definitions)
(E _, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s (s, _) => wrongType s.loc ctx ty s
compare0' _ (Eq {}) _ _ = compare0' _ _ (Eq {}) _ _ =
-- ✨ uip ✨ -- ✨ uip ✨
-- --
-- ---------------------------- -- ----------------------------
-- Γ ⊢ e = f : Eq [i ⇒ A] s t -- Γ ⊢ e = f : Eq [i ⇒ A] s t
pure () pure ()
compare0' ctx nat@(Nat {}) s t = local_ Equal $ compare0' defs ctx nat@(Nat {}) s t = local_ Equal $
case (s, t) of case (s, t) of
-- --------------- -- ---------------
-- Γ ⊢ 0 = 0 : ℕ -- Γ ⊢ 0 = 0 : ℕ
@ -239,9 +249,9 @@ parameters (defs : Definitions)
-- Γ ⊢ s = t : ℕ -- Γ ⊢ s = t : ℕ
-- ------------------------- -- -------------------------
-- Γ ⊢ succ s = succ t : ℕ -- Γ ⊢ succ s = succ t : ℕ
(Succ s' {}, Succ t' {}) => compare0 ctx nat s' t' (Succ s' {}, Succ t' {}) => compare0 defs ctx nat s' t'
(E e, E f) => ignore $ Elim.compare0 ctx e f (E e, E f) => ignore $ Elim.compare0 defs ctx e f
(Zero {}, Succ {}) => clashT s.loc ctx nat s t (Zero {}, Succ {}) => clashT s.loc ctx nat s t
(Zero {}, E _) => clashT s.loc ctx nat s t (Zero {}, E _) => clashT s.loc ctx nat s t
@ -255,85 +265,72 @@ parameters (defs : Definitions)
(E _, t) => wrongType t.loc ctx nat t (E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s (s, _) => wrongType s.loc ctx nat s
compare0' ctx ty@(BOX q ty' {}) s t = local_ Equal $ compare0' defs ctx ty@(BOX q ty' {}) s t = local_ Equal $
case (s, t) of case (s, t) of
-- Γ ⊢ s = t : A -- Γ ⊢ s = t : A
-- ----------------------- -- -----------------------
-- Γ ⊢ [s] = [t] : [π.A] -- Γ ⊢ [s] = [t] : [π.A]
(Box s' {}, Box t' {}) => compare0 ctx ty' s' t' (Box s' {}, Box t' {}) => compare0 defs ctx ty' s' t'
(E e, E f) => ignore $ Elim.compare0 ctx e f (E e, E f) => ignore $ Elim.compare0 defs ctx e f
(Box {}, t) => wrongType t.loc ctx ty t (Box {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s (s, _) => wrongType s.loc ctx ty s
compare0' ctx ty@(E _) s t = do compare0' defs ctx ty@(E _) s t = do
-- a neutral type can only be inhabited by neutral values -- a neutral type can only be inhabited by neutral values
-- e.g. an abstract value in an abstract type, bound variables, … -- e.g. an abstract value in an abstract type, bound variables, …
let E e = s | _ => wrongType s.loc ctx ty s let E e = s | _ => wrongType s.loc ctx ty s
E f = t | _ => wrongType t.loc ctx ty t E f = t | _ => wrongType t.loc ctx ty t
ignore $ Elim.compare0 ctx e f ignore $ Elim.compare0 defs 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 %inline
compareType : EqContext n -> (s, t : Term 0 n) -> Eff EqualInner ()
compareType ctx s t = do
let Val n = ctx.termLen
Element s' _ <- whnf defs ctx s.loc s
Element t' _ <- whnf defs ctx t.loc t
ts <- ensureTyCon s.loc ctx s'
tt <- ensureTyCon t.loc ctx t'
st <- either pure (const $ clashTy s.loc ctx s' t') $
nchoose $ sameTyCon s' t'
compareType' ctx s' t'
private covering private covering
compareType' : EqContext n -> (s, t : Term 0 n) -> compareType' : (defs : Definitions) -> EqContext n -> (s, t : Term 0 n) ->
(0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) => (0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
(0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) => (0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
(0 _ : So (sameTyCon s t)) => (0 _ : So (sameTyCon s t)) =>
Eff EqualInner () Eff EqualInner ()
-- equality is the same as subtyping, except with the -- equality is the same as subtyping, except with the
-- "≤" in the TYPE rule being replaced with "=" -- "≤" in the TYPE rule being replaced with "="
compareType' ctx a@(TYPE k {}) (TYPE l {}) = compareType' defs ctx a@(TYPE k {}) (TYPE l {}) =
-- 𝓀 ≤ ℓ -- 𝓀 ≤ ℓ
-- ---------------------- -- ----------------------
-- Γ ⊢ Type 𝓀 <: Type ℓ -- Γ ⊢ Type 𝓀 <: Type ℓ
expectModeU a.loc !mode k l expectModeU a.loc !mode k l
compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _}) compareType' defs ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂ -- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- ---------------------------------------- -- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
expectEqualQ a.loc sQty tQty expectEqualQ loc sQty tQty
local flip $ compareType ctx sArg tArg -- contra local flip $ compareType defs ctx sArg tArg -- contra
compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term compareType defs (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
compareType' 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
-- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂ -- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- -------------------------------------- -- --------------------------------------
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂ -- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
compareType ctx sFst tFst compareType defs ctx sFst tFst
compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term compareType defs (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
compareType' 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
-- Γ ⊢ A₁‹ε/i› <: A₂‹ε/i› -- Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
-- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i› -- Γ ⊢ l₁ = l₂ : A₁‹𝟎/i› Γ ⊢ r₁ = r₂ : A₁‹𝟏/i›
-- ------------------------------------------------ -- ------------------------------------------------
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂ -- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero compareType defs (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
compareType (extendDim sTy.name One ctx) sTy.one tTy.one compareType defs (extendDim sTy.name One ctx) sTy.one tTy.one
ty <- bigger sTy tTy ty <- bigger sTy tTy
local_ Equal $ do local_ Equal $ do
Term.compare0 ctx ty.zero sl tl Term.compare0 defs ctx ty.zero sl tl
Term.compare0 ctx ty.one sr tr Term.compare0 defs ctx ty.one sr tr
compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do compareType' defs ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
-- ------------------ -- ------------------
-- Γ ⊢ {ts} <: {ts} -- Γ ⊢ {ts} <: {ts}
-- --
@ -341,84 +338,123 @@ parameters (defs : Definitions)
-- a runtime coercion -- a runtime coercion
unless (tags1 == tags2) $ clashTy s.loc ctx s t unless (tags1 == tags2) $ clashTy s.loc ctx s t
compareType' ctx (Nat {}) (Nat {}) = compareType' defs ctx (Nat {}) (Nat {}) =
-- ------------ -- ------------
-- Γ ⊢ ℕ <: ℕ -- Γ ⊢ ℕ <: ℕ
pure () pure ()
compareType' ctx (BOX pi a loc) (BOX rh b {}) = do compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
expectEqualQ loc pi rh expectEqualQ loc pi rh
compareType ctx a b compareType defs ctx a b
compareType' ctx (E e) (E f) = do compareType' defs ctx (E e) (E f) = do
-- no fanciness needed here cos anything other than a neutral -- no fanciness needed here cos anything other than a neutral
-- has been inlined by whnf -- has been inlined by whnf
ignore $ Elim.compare0 ctx e f ignore $ Elim.compare0 defs ctx e f
namespace Elim
||| compare two eliminations according to the given variance `mode`.
|||
||| ⚠ **assumes that they have both been typechecked, and have
||| equal types.** ⚠
export covering %inline
compare0 : EqContext n -> (e, f : Elim 0 n) -> Eff EqualInner (Term 0 n)
compare0 ctx e f = do
(err, ty) <- compare0Inner ctx e f
maybe (pure ty) throw err
private covering
compare0Inner : EqContext n -> (e, f : Elim 0 n) ->
Eff EqualInner (Maybe Error, Term 0 n)
compare0Inner 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) <- compare0' ctx e f ne nf
if !(isSubSing defs ctx ty)
then pure (Nothing, ty)
else pure (err, ty)
private private
try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error) try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error)
try_ act = lift $ catch (pure . Just) $ act $> Nothing try_ act = lift $ catch (pure . Just) $ act $> Nothing
private private
lookupFree : EqContext n -> Name -> Universe -> Loc -> lookupFree : Definitions -> EqContext n -> Name -> Universe -> Loc ->
Eff EqualInner (Term 0 n) Eff EqualInner (Term 0 n)
lookupFree 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) $
lookup x defs lookup x defs
namespace Elim
||| 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.
private covering private covering
compare0' : EqContext n -> compareArm : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
(def : Term 0 n) ->
Eff EqualInner ()
compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
compareArm defs ctx k ret u b1 b2 def =
let def = SN def in
compareArm_ defs ctx k ret u (fromMaybe def b1) (fromMaybe def b2)
where
compareArm_ : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : TypeCaseArmBody k 0 n) ->
Eff EqualInner ()
compareArm_ defs ctx KTYPE ret u b1 b2 =
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
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
compareArm_ defs ctx KEnum ret u b1 b2 =
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
compareArm_ defs ctx KNat ret u b1 b2 =
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
private covering
compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
Eff EqualInner (Maybe Error, Term 0 n)
private covering
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 EqualInner (Maybe Error, Term 0 n)
compare0' ctx e@(F x u loc) f@(F y v _) _ _ = do 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, pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f,
!(lookupFree ctx x u loc)) !(lookupFree defs ctx x u loc))
compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(F {}) f _ _ = clashE e.loc ctx e f
compare0' ctx e@(B i loc) f@(B j _) _ _ = compare0Inner' defs ctx e@(B i loc) f@(B j _) _ _ =
pure (guard (i /= j) $> ClashE loc ctx !mode e f, pure (guard (i /= j) $> ClashE loc ctx !mode e f,
ctx.tctx !! i) ctx.tctx !! i)
compare0' ctx e@(B {}) f _ _ = clashE e.loc 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]
compare0' ctx (App e s eloc) (App f t floc) ne nf = compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf =
local_ Equal $ do local_ Equal $ do
(err1, ety) <- compare0Inner ctx e f (err1, ety) <- compare0Inner defs ctx e f
(_, arg, res) <- expectPi defs ctx eloc ety (_, arg, res) <- expectPi defs ctx eloc ety
err2 <- try_ $ Term.compare0 ctx arg s t err2 <- try_ $ Term.compare0 defs ctx arg s t
pure (err1 <|> err2, sub1 res $ Ann s arg s.loc) pure (err1 <|> err2, sub1 res $ Ann s arg s.loc)
compare0' ctx e@(App {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(App {}) f _ _ = clashE e.loc 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
@ -426,20 +462,21 @@ parameters (defs : Definitions)
-- ----------------------------------------------------------- -- -----------------------------------------------------------
-- Ψ | Γ ⊢ 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]
compare0' 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 {}) ne nf =
local_ Equal $ do local_ Equal $ do
(err1, ety) <- compare0Inner ctx e f (err1, ety) <- compare0Inner defs ctx e f
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term 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_ $ err2 <- try_ $
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) Term.compare0 defs
(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 err3 <- try_ $ expectEqualQ e.loc epi fpi
pure (concat [err1, err2, err3], sub1 eret e) pure (concat [err1, err2, err3], sub1 eret e)
compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s} -- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R -- Ψ | Γ, x : {𝐚s} ⊢ Q = R
@ -447,18 +484,18 @@ parameters (defs : Definitions)
-- -------------------------------------------------- -- --------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ } -- Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
-- = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x] -- = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
compare0' 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 ctx e f (err1, ety) <- compare0Inner defs ctx e f
err2 <- try_ $ err2 <- try_ $
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term
cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety
exs <- for cases $ \t => do exs <- for cases $ \t => do
l <- lookupArm eloc t earms l <- lookupArm eloc t earms
r <- lookupArm floc t farms r <- lookupArm floc t farms
try_ $ try_ $
Term.compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r Term.compare0 defs ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
err3 <- try_ $ expectEqualQ eloc epi fpi err3 <- try_ $ expectEqualQ eloc epi fpi
pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e) pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e)
where where
@ -467,7 +504,7 @@ parameters (defs : Definitions)
lookupArm loc t arms = case lookup t arms of lookupArm loc t arms = case lookup t arms of
Just arm => pure arm Just arm => pure arm
Nothing => throw $ TagNotIn loc t (fromList $ keys arms) Nothing => throw $ TagNotIn loc t (fromList $ keys arms)
compare0' ctx e@(CaseEnum {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(CaseEnum {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ ℕ -- Ψ | Γ ⊢ e = f ⇒ ℕ
-- Ψ | Γ, x : ℕ ⊢ Q = R -- Ψ | Γ, x : ℕ ⊢ Q = R
@ -477,25 +514,25 @@ parameters (defs : Definitions)
-- Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ } -- Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ }
-- = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ } -- = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ }
-- ⇒ Q[e/x] -- ⇒ Q[e/x]
compare0' 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 ctx e f (err1, ety) <- compare0Inner defs ctx e f
err2 <- try_ $ err2 <- try_ $
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term compareType defs (extendTy Zero eret.name ety ctx) eret.term fret.term
err3 <- try_ $ err3 <- try_ $
Term.compare0 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 let [< p, ih] = esuc.names
err4 <- try_ $ err4 <- try_ $
Term.compare0 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 err5 <- try_ $ expectEqualQ e.loc epi fpi
err6 <- try_ $ expectEqualQ e.loc epi' fpi' err6 <- try_ $ expectEqualQ e.loc epi' fpi'
pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e) pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e)
compare0' ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ [ρ. A] -- Ψ | Γ ⊢ e = f ⇒ [ρ. A]
-- Ψ | Γ, x : [ρ. A] ⊢ Q = R -- Ψ | Γ, x : [ρ. A] ⊢ Q = R
@ -503,33 +540,33 @@ parameters (defs : Definitions)
-- -------------------------------------------------- -- --------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s } -- Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s }
-- = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x] -- = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
compare0' 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 ctx e f (err1, ety) <- compare0Inner defs ctx e f
err2 <- try_ $ err2 <- try_ $
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term 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_ $ err3 <- try_ $
Term.compare0 (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 err4 <- try_ $ expectEqualQ eloc epi fpi
pure (concat [err1, err2, err3, err4], sub1 eret e) pure (concat [err1, err2, err3, err4], sub1 eret e)
compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
-- all dim apps replaced with ends by whnf -- all dim apps replaced with ends by whnf
compare0' _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne compare0Inner' _ _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
compare0' _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
-- Ψ | Γ ⊢ s <: t : B -- Ψ | Γ ⊢ s <: t : B
-- -------------------------------- -- --------------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B -- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
-- --
-- and similar for :> and A -- and similar for :> and A
compare0' 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 ctx ty s t err <- try_ $ Term.compare0 defs ctx ty s t
pure (err, ty) pure (err, ty)
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
@ -538,108 +575,87 @@ parameters (defs : Definitions)
-- ----------------------------------------------------------- -- -----------------------------------------------------------
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖› -- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
compare0' ctx (Coe ty1 p1 q1 val1 _) compare0Inner' defs ctx (Coe ty1 p1 q1 val1 _)
(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 ctx ty1p ty2p err1 <- try_ $ compareType defs ctx ty1p ty2p
err2 <- try_ $ compareType ctx ty1q ty2q 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 ctx ty_p val1 val2 err3 <- try_ $ Term.compare0 defs ctx ty_p val1 val2
pure (concat [err1, err2, err3], ty_q) pure (concat [err1, err2, err3], ty_q)
compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
-- (no neutral compositions in a closed dctx) -- (no neutral compositions in a closed dctx)
compare0' _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne compare0Inner' _ _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne
compare0' _ (Comp {r = B i _, _}) _ _ _ = absurd i compare0Inner' _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
compare0' _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf compare0Inner' _ _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
-- (type case equality purely structural) -- (type case equality purely structural)
compare0' 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
-- try (err1, ety) <- compare0Inner defs ctx ty1 ty2
(err1, ety) <- compare0Inner ctx ty1 ty2
u <- expectTYPE defs ctx eloc ety u <- expectTYPE defs ctx eloc ety
err2 <- try_ $ compareType ctx ret1 ret2 err2 <- try_ $ compareType defs ctx ret1 ret2
err3 <- try_ $ compareType ctx def1 def2 err3 <- try_ $ compareType defs ctx def1 def2
exs <- for allKinds $ \k => exs <- for allKinds $ \k =>
try_ $ try_ $
compareArm 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 (concat $ [err1, err2, err3] ++ exs, ret1)
compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ s <: f ⇐ A -- Ψ | Γ ⊢ s <: f ⇐ A
-- -------------------------- -- --------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A -- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
-- --
-- and vice versa -- and vice versa
compare0' ctx (Ann s a _) f _ _ = do compare0Inner' defs ctx (Ann s a _) f _ _ = do
err <- try_ $ Term.compare0 ctx a s (E f) err <- try_ $ Term.compare0 defs ctx a s (E f)
pure (err, a) pure (err, a)
compare0' ctx e (Ann t b _) _ _ = do compare0Inner' defs ctx e (Ann t b _) _ _ = do
err <- try_ $ Term.compare0 ctx b (E e) t err <- try_ $ Term.compare0 defs ctx b (E e) t
pure (err, b) pure (err, b)
compare0' ctx e@(Ann {}) f _ _ = compare0Inner' defs ctx e@(Ann {}) f _ _ =
clashE e.loc ctx e f clashE e.loc ctx e f
||| compare two type-case branches, which came from the arms of the given compare0Inner defs ctx e f =
||| kind. `ret` is the return type of the case expression, and `u` is the wrapErr (WhileComparingE ctx !mode e f) $ do
||| universe the head is in. let Val n = ctx.termLen
private covering Element e ne <- whnf defs ctx e.loc e
compareArm : EqContext n -> (k : TyConKind) -> Element f nf <- whnf defs ctx f.loc f
(ret : Term 0 n) -> (u : Universe) -> (err, ty) <- compare0Inner' defs ctx e f ne nf
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) -> if !(isSubSing defs ctx ty)
(def : Term 0 n) -> then pure (Nothing, ty)
Eff EqualInner () else pure (err, ty)
compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
compareArm ctx k ret u b1 b2 def =
let def = SN def in
compareArm_ ctx k ret u (fromMaybe def b1) (fromMaybe def b2)
private covering
compareArm_ : EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : TypeCaseArmBody k 0 n) ->
Eff EqualInner ()
compareArm_ ctx KTYPE ret u b1 b2 =
compare0 ctx ret b1.term b2.term
compareArm_ ctx KPi ret u b1 b2 = do namespace Term
let [< a, b] = b1.names compare0 defs ctx ty s t =
ctx = extendTyN wrapErr (WhileComparingT ctx !mode ty s t) $ do
[< (Zero, a, TYPE u a.loc), let Val n = ctx.termLen
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx Element ty' _ <- whnf defs ctx ty.loc ty
compare0 ctx (weakT 2 ret) b1.term b2.term Element s' _ <- whnf defs ctx s.loc s
Element t' _ <- whnf defs ctx t.loc t
tty <- ensureTyCon ty.loc ctx ty'
compare0' defs ctx ty' s' t'
compareArm_ ctx KSig ret u b1 b2 = do namespace Elim
let [< a, b] = b1.names compare0 defs ctx e f = do
ctx = extendTyN (err, ty) <- compare0Inner defs ctx e f
[< (Zero, a, TYPE u a.loc), maybe (pure ty) throw err
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
compare0 ctx (weakT 2 ret) b1.term b2.term
compareArm_ ctx KEnum ret u b1 b2 = compareType defs ctx s t = do
compare0 ctx ret b1.term b2.term let Val n = ctx.termLen
Element s' _ <- whnf defs ctx s.loc s
Element t' _ <- whnf defs ctx t.loc t
ts <- ensureTyCon s.loc ctx s'
tt <- ensureTyCon t.loc ctx t'
st <- either pure (const $ clashTy s.loc ctx s' t') $
nchoose $ sameTyCon s' t'
compareType' defs ctx s' t'
compareArm_ 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 ctx (weakT 5 ret) b1.term b2.term
compareArm_ ctx KNat ret u b1 b2 =
compare0 ctx ret b1.term b2.term
compareArm_ ctx KBOX ret u b1 b2 = do
let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx
compare0 ctx (weakT 1 ret) b1.term b1.term
parameters (loc : Loc) (ctx : TyContext d n) parameters (loc : Loc) (ctx : TyContext d n)