quox/lib/Quox/Equal.idr

735 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
import Quox.FreeVars
%default total
public export
EqModeState : Type -> Type
EqModeState = State EqMode
public export
Equal : List (Type -> Type)
Equal = [ErrorEff, DefsReader, NameGen]
public export
EqualInner : List (Type -> Type)
EqualInner = [ErrorEff, NameGen, EqModeState]
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 -> Eff EqualInner a
clashT ty s t = throw $ ClashT loc ctx !mode ty s t
private %inline
clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a
clashTy s t = throw $ ClashTy loc ctx !mode s t
private %inline
wrongType : Term 0 n -> Term 0 n -> Eff EqualInner 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 ->
Eff EqualInner 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 (extendTy0 res.name arg ctx) res.term
Sig {fst, snd, _} =>
isSubSing defs ctx fst `andM`
isSubSing defs (extendTy0 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
||| the left argument if the current mode is `Super`; otherwise the right one.
private %inline
bigger : Has EqModeState fs => (left, right : Lazy a) -> Eff fs a
bigger l r = gets $ \case Super => l; _ => r
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)
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 : Definitions -> EqContext n -> (ty, s, t : Term 0 n) ->
Eff EqualInner ()
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 : 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
||| 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
namespace Term
private covering
compare0' : (defs : Definitions) -> EqContext n ->
(ty, s, t : Term 0 n) ->
(0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
(0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) =>
Eff EqualInner ()
compare0' defs ctx (TYPE {}) s t = compareType defs ctx s t
compare0' defs 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 defs 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) => ignore $ Elim.compare0 defs 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 -> Eff EqualInner ()
eta _ e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b
eta loc e (S _ (N _)) = clashT loc ctx ty s t
compare0' defs 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 defs ctx fst sFst tFst
compare0 defs ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
(E e, E f) => ignore $ Elim.compare0 defs 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' defs 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) => ignore $ Elim.compare0 defs 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' defs 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 defs ctx nat s' t'
(E e, E f) => ignore $ Elim.compare0 defs 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' defs ctx ty@(BOX q ty' {}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s = t : A
-- -----------------------
-- Γ ⊢ [s] = [t] : [π.A]
(Box s' {}, Box t' {}) => compare0 defs ctx ty' s' t'
(E e, E f) => ignore $ Elim.compare0 defs 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' defs 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
ignore $ Elim.compare0 defs ctx e f
private covering
compareType' : (defs : Definitions) -> 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)) =>
Eff EqualInner ()
-- equality is the same as subtyping, except with the
-- "≤" in the TYPE rule being replaced with "="
compareType' defs ctx a@(TYPE k {}) (TYPE l {}) =
-- 𝓀
-- ----------------------
-- Γ ⊢ Type 𝓀 <: Type
expectModeU a.loc !mode k l
compareType' defs ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
expectEqualQ loc sQty tQty
local flip $ compareType defs ctx sArg tArg -- contra
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
-- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- --------------------------------------
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
compareType defs ctx sFst tFst
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
-- Γ ⊢ A₁ε/i <: A₂ε/i
-- Γ ⊢ l₁ = l₂ : A₁𝟎/i Γ ⊢ r₁ = r₂ : A₁𝟏/i
-- ------------------------------------------------
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
compareType defs (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
compareType defs (extendDim sTy.name One ctx) sTy.one tTy.one
ty <- bigger sTy tTy
local_ Equal $ do
Term.compare0 defs ctx ty.zero sl tl
Term.compare0 defs ctx ty.one sr tr
compareType' defs 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' defs ctx (Nat {}) (Nat {}) =
-- ------------
-- Γ ⊢ <:
pure ()
compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
expectEqualQ loc pi rh
compareType defs ctx a b
compareType' defs ctx (E e) (E f) = do
-- no fanciness needed here cos anything other than a neutral
-- has been inlined by whnf
ignore $ Elim.compare0 defs ctx e f
private
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) $
lookup x defs
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.
private covering
compareArm : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
(def : Term 0 n) ->
Eff EqualElim ()
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 EqualElim ()
compareArm_ defs ctx KTYPE ret u b1 b2 =
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 = 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 = 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 =
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 = 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 =
try $ Term.compare0 defs ctx ret b1.term b2.term
compareArm_ defs ctx KBOX ret u b1 b2 = do
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 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 EqualElim (Term 0 n)
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 {}) 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 = 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
-- Ψ | Γ, 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]
compare0Inner' defs ctx (CasePair epi e eret ebody eloc)
(CasePair fpi f fret fbody floc) ne nf =
local_ Equal $ do
ety <- compare0Inner defs ctx e f
(fst, snd) <- expectSig defs ctx eloc ety
let [< x, y] = ebody.names
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
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
-- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
-- --------------------------------------------------
-- Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
-- = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
compare0Inner' defs ctx (CaseEnum epi e eret earms eloc)
(CaseEnum fpi f fret farms floc) ne nf =
local_ Equal $ do
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
-- Ψ | Γ ⊢ 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]
compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc)
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
local_ Equal $ do
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
Term.compare0 defs
(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'
pure $ sub1 eret e
compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE defs 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]
compare0Inner' defs ctx (CaseBox epi e eret ebody eloc)
(CaseBox fpi f fret fbody floc) ne nf =
local_ Equal $ do
ety <- compare0Inner defs ctx e f
(q, ty) <- expectBOX defs ctx eloc ety
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
expectEqualQ eloc epi fpi
pure $ sub1 eret e
compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE defs ctx e f
-- (no neutral dim apps in a closed dctx)
compare0Inner' _ _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
-- Ψ | Γ ⊢ s <: t : B
-- --------------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
--
-- and similar for :> and A
compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do
ty <- bigger a b
try $ Term.compare0 defs ctx ty s t
pure ty
-- Ψ | Γ ⊢ Ap₁/𝑖 <: Bp₂/𝑖
-- Ψ | Γ ⊢ Aq₁/𝑖 <: Bq₂/𝑖
-- Ψ | Γ ⊢ s <: t ⇐ Bp₂/𝑖
-- -----------------------------------------------------------
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ Bq₂/𝑖
compare0Inner' defs ctx (Coe ty1 p1 q1 val1 _)
(Coe ty2 p2 q2 val2 _) ne nf = do
let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
(ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
try $ do
compareType defs ctx ty1p ty2p
compareType defs ctx ty1q ty2q
Term.compare0 defs ctx 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
compare0Inner' _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
compare0Inner' _ _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
-- (type case equality purely structural)
compare0Inner' defs ctx (TypeCase ty1 ret1 arms1 def1 eloc)
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
local_ Equal $ do
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
-- --------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
--
-- and vice versa
compare0Inner' defs ctx (Ann s a _) f _ _ = do
try $ Term.compare0 defs ctx a s (E f)
pure a
compare0Inner' defs ctx e (Ann t b _) _ _ = do
try $ Term.compare0 defs ctx b (E e) t
pure b
compare0Inner' defs ctx e@(Ann {}) f _ _ =
clashE defs ctx e f
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
compare0 defs 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' defs ctx ty' s' t'
namespace Elim
compare0 defs ctx e f = do
(ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx e f
maybe (pure ty) throw err
compareType defs 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' 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`
parameters (mode : EqMode)
private
fromInner : Eff EqualInner a -> Eff Equal a
fromInner = lift . map fst . runState mode
private
eachFace : Applicative f => FreeVars d ->
(EqContext n -> DSubst d 0 -> f ()) -> f ()
eachFace fvs act =
let Val d = ctx.dimLen in
for_ (splits loc ctx.dctx fvs) $ \th =>
act (makeEqContext ctx th) th
private
CompareAction : Nat -> Nat -> Type
CompareAction d n =
Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
private
runCompare : FreeVars d -> CompareAction d n -> Eff Equal ()
runCompare fvs act = fromInner $ eachFace fvs $ act !(askAt DEFS)
private
fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
fdvAll ts =
let Val d = ctx.dimLen; Val n = ctx.termLen in foldMap fdv ts
namespace Term
export covering
compare : (ty, s, t : Term d n) -> Eff Equal ()
compare ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
compare0 defs ectx (ty // th) (s // th) (t // th)
export covering
compareType : (s, t : Term d n) -> Eff Equal ()
compareType s t = runCompare (fdvAll [s, t]) $ \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) -> Eff Equal ()
compare e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
ignore $ compare0 defs ectx (e // th) (f // th)
namespace Term
export covering %inline
equal, sub, super : (ty, s, t : Term d n) -> Eff Equal ()
equal = compare Equal
sub = compare Sub
super = compare Super
export covering %inline
equalType, subtype, supertype : (s, t : Term d n) -> Eff Equal ()
equalType = compareType Equal
subtype = compareType Sub
supertype = compareType Super
namespace Elim
export covering %inline
equal, sub, super : (e, f : Elim d n) -> Eff Equal ()
equal = compare Equal
sub = compare Sub
super = compare Super