quox/lib/Quox/Equal.idr
2023-06-23 18:32:05 +02:00

679 lines
26 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Quox.Equal
import Quox.BoolExtra
import public Quox.Typing
import Data.Maybe
import Quox.EffExtra
%default total
public export
EqModeState : Type -> Type
EqModeState = State EqMode
public export
Equal : Type -> Type
Equal = Eff [ErrorEff, DefsReader, NameGen]
public export
Equal_ : Type -> Type
Equal_ = Eff [ErrorEff, NameGen, EqModeState]
export
runEqualWith_ : EqMode -> NameSuf -> Equal_ a -> (Either Error a, NameSuf)
runEqualWith_ mode suf act =
extract $
runNameGenWith suf $
runExcept $
evalState mode act
export
runEqual_ : EqMode -> Equal_ a -> Either Error a
runEqual_ mode act = fst $ runEqualWith_ mode 0 act
export
runEqualWith : NameSuf -> Definitions -> Equal a -> (Either Error a, NameSuf)
runEqualWith suf defs act =
extract $
runStateAt GEN suf $
runReaderAt DEFS defs $
runExcept act
export
runEqual : Definitions -> Equal a -> Either Error a
runEqual defs act = fst $ runEqualWith 0 defs act
export %inline
mode : Has EqModeState fs => Eff fs EqMode
mode = get
parameters (loc : Loc) (ctx : EqContext n)
private %inline
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal_ a
clashT ty s t = throw $ ClashT loc ctx !mode ty s t
private %inline
clashTy : Term 0 n -> Term 0 n -> Equal_ a
clashTy s t = throw $ ClashTy loc ctx !mode s t
private %inline
clashE : Elim 0 n -> Elim 0 n -> Equal_ a
clashE e f = throw $ ClashE loc ctx !mode e f
private %inline
wrongType : Term 0 n -> Term 0 n -> Equal_ a
wrongType ty s = throw $ WrongType loc ctx ty s
public export %inline
sameTyCon : (s, t : Term d n) ->
(0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) =>
Bool
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _ = False
sameTyCon (Pi {}) (Pi {}) = True
sameTyCon (Pi {}) _ = False
sameTyCon (Sig {}) (Sig {}) = True
sameTyCon (Sig {}) _ = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _ = False
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
sameTyCon (Nat {}) (Nat {}) = True
sameTyCon (Nat {}) _ = False
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
||| true if a type is known to be a subsingleton purely by its form.
||| a subsingleton is a type with only zero or one possible values.
||| equality/subtyping accepts immediately on values of subsingleton types.
|||
||| * a function type is a subsingleton if its codomain is.
||| * a pair type is a subsingleton if both its elements are.
||| * equality types are subsingletons because of uip.
||| * an enum type is a subsingleton if it has zero or one tags.
||| * a box type is a subsingleton if its content is
public export covering
isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n -> Equal_ Bool
isSubSing defs ctx ty0 = do
Element ty0 nc <- whnf defs ctx ty0.loc ty0
case ty0 of
TYPE {} => pure False
Pi {arg, res, _} =>
isSubSing defs (extendTy Zero res.name arg ctx) res.term
Sig {fst, snd, _} =>
isSubSing defs ctx fst `andM`
isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
Enum {cases, _} =>
pure $ length (SortedSet.toList cases) <= 1
Eq {} => pure True
Nat {} => pure False
BOX {ty, _} => isSubSing defs ctx ty
E (Ann {tm, _}) => isSubSing defs ctx tm
E _ => pure False
Lam {} => pure False
Pair {} => pure False
Tag {} => pure False
DLam {} => pure False
Zero {} => pure False
Succ {} => pure False
Box {} => pure False
export
ensureTyCon : Has ErrorEff fs =>
(loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
Eff fs (So (isTyConE t))
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) =>
Equal_ (Term 0 n)
computeElimTypeE defs ectx e =
let Val n = ectx.termLen in
lift $ computeElimType defs (toWhnfContext ectx) e
parameters (defs : Definitions)
mutual
namespace Term
||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
||| the current variance `mode`.
|||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
export covering %inline
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal_ ()
compare0 ctx ty s t =
wrapErr (WhileComparingT ctx !mode ty s t) $ do
let Val n = ctx.termLen
Element ty' _ <- whnf defs ctx ty.loc ty
Element s' _ <- whnf defs ctx s.loc s
Element t' _ <- whnf defs ctx t.loc t
tty <- ensureTyCon ty.loc ctx ty'
compare0' ctx ty' s' t'
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
private %inline
toLamBody : Elim d n -> Term d (S n)
toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
private covering
compare0' : EqContext n ->
(ty, s, t : Term 0 n) ->
(0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
(0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) =>
Equal_ ()
compare0' ctx (TYPE {}) s t = compareType ctx s t
compare0' ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $
case (s, t) of
-- Γ, x : A ⊢ s = t : B
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
(Lam b1 {}, Lam b2 {}) =>
compare0 ctx' res.term b1.term b2.term
-- Γ, x : A ⊢ s = e x : B
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
(E e, Lam b {}) => eta s.loc e b
(Lam b {}, E e) => eta s.loc e b
(E e, E f) => Elim.compare0 ctx e f
(Lam {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
where
ctx' : EqContext (S n)
ctx' = extendTy qty res.name arg ctx
eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Equal_ ()
eta _ e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
eta loc e (S _ (N _)) = clashT loc ctx ty s t
compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
-- --------------------------------------------
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
--
-- [todo] η for π ≥ 0 maybe
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
compare0 ctx fst sFst tFst
compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
(E e, E f) => Elim.compare0 ctx e f
(Pair {}, E _) => clashT s.loc ctx ty s t
(E _, Pair {}) => clashT s.loc ctx ty s t
(Pair {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
compare0' ctx ty@(Enum {}) s t = local_ Equal $
case (s, t) of
-- --------------------
-- Γ ⊢ `t = `t : {ts}
--
-- t ∈ ts is in the typechecker, not here, ofc
(Tag t1 {}, Tag t2 {}) =>
unless (t1 == t2) $ clashT s.loc ctx ty s t
(E e, E f) => Elim.compare0 ctx e f
(Tag {}, E _) => clashT s.loc ctx ty s t
(E _, Tag {}) => clashT s.loc ctx ty s t
(Tag {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
compare0' _ (Eq {}) _ _ =
-- ✨ uip ✨
--
-- ----------------------------
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
pure ()
compare0' ctx nat@(Nat {}) s t = local_ Equal $
case (s, t) of
-- ---------------
-- Γ ⊢ 0 = 0 :
(Zero {}, Zero {}) => pure ()
-- Γ ⊢ s = t :
-- -------------------------
-- Γ ⊢ succ s = succ t :
(Succ s' {}, Succ t' {}) => compare0 ctx nat s' t'
(E e, E f) => Elim.compare0 ctx e f
(Zero {}, Succ {}) => clashT s.loc ctx nat s t
(Zero {}, E _) => clashT s.loc ctx nat s t
(Succ {}, Zero {}) => clashT s.loc ctx nat s t
(Succ {}, E _) => clashT s.loc ctx nat s t
(E _, Zero {}) => clashT s.loc ctx nat s t
(E _, Succ {}) => clashT s.loc ctx nat s t
(Zero {}, t) => wrongType t.loc ctx nat t
(Succ {}, t) => wrongType t.loc ctx nat t
(E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s
compare0' ctx ty@(BOX q ty' {}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s = t : A
-- -----------------------
-- Γ ⊢ [s] = [t] : [π.A]
(Box s' {}, Box t' {}) => compare0 ctx ty' s' t'
(E e, E f) => Elim.compare0 ctx e f
(Box {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
compare0' ctx ty@(E _) s t = do
-- a neutral type can only be inhabited by neutral values
-- e.g. an abstract value in an abstract type, bound variables, …
let E e = s | _ => wrongType s.loc ctx ty s
E f = t | _ => wrongType t.loc ctx ty t
Elim.compare0 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) -> Equal_ ()
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
compareType' : EqContext n -> (s, t : Term 0 n) ->
(0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
(0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
(0 _ : So (sameTyCon s t)) =>
Equal_ ()
-- equality is the same as subtyping, except with the
-- "≤" in the TYPE rule being replaced with "="
compareType' ctx a@(TYPE k {}) (TYPE l {}) =
-- 𝓀
-- ----------------------
-- Γ ⊢ Type 𝓀 <: Type
expectModeU a.loc !mode k l
compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
expectEqualQ a.loc sQty tQty
local flip $ compareType ctx sArg tArg -- contra
compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
(Sig {fst = tFst, snd = tSnd, _}) = do
-- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- --------------------------------------
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
compareType ctx sFst tFst
compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
(Eq {ty = tTy, l = tl, r = tr, _}) = do
-- Γ ⊢ A₁ε/i <: A₂ε/i
-- Γ ⊢ l₁ = l₂ : A₁𝟎/i Γ ⊢ r₁ = r₂ : A₁𝟏/i
-- ------------------------------------------------
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
compareType (extendDim sTy.name One ctx) sTy.one tTy.one
let ty = case !mode of Super => sTy; _ => tTy
local_ Equal $ do
Term.compare0 ctx ty.zero sl tl
Term.compare0 ctx ty.one sr tr
compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
-- ------------------
-- Γ ⊢ {ts} <: {ts}
--
-- no subtyping based on tag subsets, since that would need
-- a runtime coercion
unless (tags1 == tags2) $ clashTy s.loc ctx s t
compareType' ctx (Nat {}) (Nat {}) =
-- ------------
-- Γ ⊢ <:
pure ()
compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
expectEqualQ loc pi rh
compareType ctx a b
compareType' ctx (E e) (E f) = do
-- no fanciness needed here cos anything other than a neutral
-- has been inlined by whnf
Elim.compare0 ctx e f
namespace Elim
-- [fixme] the following code ends up repeating a lot of work in the
-- computeElimType calls. the results should be shared better
||| 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) -> Equal_ ()
compare0 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
unless !(isSubSing defs ctx =<< computeElimTypeE defs ctx e') $
compare0' ctx e' f' ne nf
private covering
compare0' : EqContext n ->
(e, f : Elim 0 n) ->
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
Equal_ ()
compare0' ctx e@(F x u _) f@(F y v _) _ _ =
unless (x == y && u == v) $ clashE e.loc ctx e f
compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f
compare0' ctx e@(B i _) f@(B j _) _ _ =
unless (i == j) $ clashE e.loc ctx e f
compare0' ctx e@(B {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
-- Ψ | Γ ⊢ s = t ⇐ A
-- -------------------------------
-- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
compare0' ctx (App e s eloc) (App f t floc) ne nf =
local_ Equal $ do
compare0 ctx e f
(_, arg, _) <- expectPi defs ctx eloc =<<
computeElimTypeE defs ctx e @{noOr1 ne}
Term.compare0 ctx arg s t
compare0' ctx e@(App {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
-- Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R
-- Ψ | Γ, x : A, y : B ⊢ s = t ⇐ Q[((x, y) ∷ (x : A) × B)/p]
-- -----------------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s }
-- = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
compare0' ctx (CasePair epi e eret ebody eloc)
(CasePair fpi f fret fbody {}) ne nf =
local_ Equal $ do
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
(fst, snd) <- expectSig defs ctx eloc ety
let [< x, y] = ebody.names
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
(substCasePairRet ebody.names ety eret)
ebody.term fbody.term
expectEqualQ e.loc epi fpi
compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R
-- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
-- --------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
-- = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
compare0' ctx (CaseEnum epi e eret earms eloc)
(CaseEnum fpi f fret farms floc) ne nf =
local_ Equal $ do
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
for_ !(expectEnum defs ctx eloc ety) $ \t => do
l <- lookupArm eloc t earms
r <- lookupArm floc t farms
compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
expectEqualQ eloc epi fpi
where
lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
lookupArm loc t arms = case lookup t arms of
Just arm => pure arm
Nothing => throw $ TagNotIn loc t (fromList $ keys arms)
compare0' ctx e@(CaseEnum {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒
-- Ψ | Γ, x : ⊢ Q = R
-- Ψ | Γ ⊢ s₀ = t₀ ⇐ Q[(0 ∷ )/x]
-- Ψ | Γ, x : , y : Q ⊢ s₁ = t₁ ⇐ Q[(succ x ∷ )/x]
-- -----------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ }
-- = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ }
-- ⇒ Q[e/x]
compare0' ctx (CaseNat epi epi' e eret ezer esuc eloc)
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
local_ Equal $ do
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
compare0 ctx
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
ezer fzer
let [< p, ih] = esuc.names
compare0
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term
expectEqualQ e.loc epi fpi
expectEqualQ e.loc epi' fpi'
compare0' ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ e = f ⇒ [ρ. A]
-- Ψ | Γ, x : [ρ. A] ⊢ Q = R
-- Ψ | Γ, x : A ⊢ s = t ⇐ Q[([x] ∷ [ρ. A])/x]
-- --------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s }
-- = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
compare0' ctx (CaseBox epi e eret ebody eloc)
(CaseBox fpi f fret fbody floc) ne nf =
local_ Equal $ do
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
(q, ty) <- expectBOX defs ctx eloc ety
compare0 (extendTy (epi * q) ebody.name ty ctx)
(substCaseBoxRet ebody.name ety eret)
ebody.term fbody.term
expectEqualQ eloc epi fpi
compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
-- all dim apps replaced with ends by whnf
compare0' _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
compare0' _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
-- Ψ | Γ ⊢ s <: t : B
-- --------------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
--
-- and similar for :> and A
compare0' ctx (Ann s a _) (Ann t b _) _ _ =
let ty = case !mode of Super => a; _ => b in
Term.compare0 ctx ty s t
-- Ψ | Γ ⊢ Ap₁/𝑖 <: Bp₂/𝑖
-- Ψ | Γ ⊢ Aq₁/𝑖 <: Bq₂/𝑖
-- Ψ | Γ ⊢ e <: f ⇒ _
-- (non-neutral forms have the coercion already pushed in)
-- -----------------------------------------------------------
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ Bq₂/𝑖
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
compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
-- (no neutral compositions in a closed dctx)
compare0' _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne
compare0' _ (Comp {r = B i _, _}) _ _ _ = absurd i
compare0' _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
-- (type case equality purely structural)
compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc)
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
local_ Equal $ do
compare0 ctx ty1 ty2
u <- expectTYPE defs ctx eloc =<<
computeElimTypeE defs ctx ty1 @{noOr1 ne}
compareType ctx ret1 ret2
compareType ctx def1 def2
for_ allKinds $ \k =>
compareArm ctx k ret1 u
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f
-- Ψ | Γ ⊢ s <: f ⇐ A
-- --------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
--
-- and vice versa
compare0' ctx (Ann s a _) f _ _ = Term.compare0 ctx a s (E f)
compare0' ctx e (Ann t b _) _ _ = Term.compare0 ctx b (E e) t
compare0' ctx e@(Ann {}) f _ _ = clashE e.loc ctx e 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.
private covering
compareArm : EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
(def : Term 0 n) ->
Equal_ ()
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) ->
Equal_ ()
compareArm_ ctx KTYPE ret u b1 b2 =
compare0 ctx ret b1.term b2.term
compareArm_ 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 ctx (weakT 2 ret) b1.term b2.term
compareArm_ 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 ctx (weakT 2 ret) b1.term b2.term
compareArm_ ctx KEnum ret u b1 b2 =
compare0 ctx ret b1.term b2.term
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)
-- [todo] only split on the dvars that are actually used anywhere in
-- the calls to `splits`
parameters (mode : EqMode)
private
fromEqual_ : Equal_ a -> Equal a
fromEqual_ act = lift $ evalState mode act
private
eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f ()
eachFace act =
for_ (splits loc ctx.dctx) $ \th => act (makeEqContext ctx th) th
private
runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
Equal ()
runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS)
namespace Term
export covering
compare : (ty, s, t : Term d n) -> Equal ()
compare ty s t = runCompare $ \defs, ectx, th =>
compare0 defs ectx (ty // th) (s // th) (t // th)
export covering
compareType : (s, t : Term d n) -> Equal ()
compareType s t = runCompare $ \defs, ectx, th =>
compareType defs ectx (s // th) (t // th)
namespace Elim
||| you don't have to pass the type in but the arguments must still be
||| of the same type!!
export covering
compare : (e, f : Elim d n) -> Equal ()
compare e f = runCompare $ \defs, ectx, th =>
compare0 defs ectx (e // th) (f // th)
namespace Term
export covering %inline
equal, sub, super : (ty, s, t : Term d n) -> Equal ()
equal = compare Equal
sub = compare Sub
super = compare Super
export covering %inline
equalType, subtype, supertype : (s, t : Term d n) -> Equal ()
equalType = compareType Equal
subtype = compareType Sub
supertype = compareType Super
namespace Elim
export covering %inline
equal, sub, super : (e, f : Elim d n) -> Equal ()
equal = compare Equal
sub = compare Sub
super = compare Super