rhiannon morris
add2eb400c
it now recovers from (most) errors and always returns a type, so that isSubSing doesn't have to recalculate it it already assumed the inputs had the same type. now it just leans on that assumption harder
705 lines
27 KiB
Idris
705 lines
27 KiB
Idris
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 : 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
|
||
clashE : Elim 0 n -> Elim 0 n -> Eff EqualInner a
|
||
clashE e f = throw $ ClashE loc ctx !mode e f
|
||
|
||
private %inline
|
||
wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a
|
||
wrongType ty s = throw $ WrongType loc ctx ty s
|
||
|
||
|
||
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 (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
|
||
|
||
|
||
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)
|
||
|
||
||| 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
|
||
|
||
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) -> Eff EqualInner ()
|
||
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) =>
|
||
Eff EqualInner ()
|
||
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) => ignore $ 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 -> Eff EqualInner ()
|
||
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) => ignore $ 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) => ignore $ 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) => ignore $ 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) => ignore $ 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
|
||
ignore $ 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) -> 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
|
||
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)) =>
|
||
Eff EqualInner ()
|
||
-- 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
|
||
ty <- bigger 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
|
||
ignore $ Elim.compare0 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
|
||
try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error)
|
||
try_ act = lift $ catch (pure . Just) $ act $> Nothing
|
||
|
||
private
|
||
lookupFree : EqContext n -> Name -> Universe -> Loc ->
|
||
Eff EqualInner (Term 0 n)
|
||
lookupFree ctx x u loc =
|
||
let Val n = ctx.termLen in
|
||
maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $
|
||
lookup x defs
|
||
|
||
private covering
|
||
compare0' : EqContext n ->
|
||
(e, f : Elim 0 n) ->
|
||
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
|
||
Eff EqualInner (Maybe Error, Term 0 n)
|
||
|
||
compare0' ctx e@(F x u loc) f@(F y v _) _ _ = do
|
||
pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f,
|
||
!(lookupFree ctx x u loc))
|
||
compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f
|
||
|
||
compare0' ctx e@(B i loc) f@(B j _) _ _ =
|
||
pure (guard (i /= j) $> ClashE loc ctx !mode e f,
|
||
ctx.tctx !! i)
|
||
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
|
||
(err1, ety) <- compare0Inner ctx e f
|
||
(_, arg, res) <- expectPi defs ctx eloc ety
|
||
err2 <- try_ $ Term.compare0 ctx arg s t
|
||
pure (err1 <|> err2, sub1 res $ Ann s arg s.loc)
|
||
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
|
||
(err1, ety) <- compare0Inner ctx e f
|
||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||
(fst, snd) <- expectSig defs ctx eloc ety
|
||
let [< x, y] = ebody.names
|
||
err2 <- try_ $
|
||
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
|
||
(substCasePairRet ebody.names ety eret)
|
||
ebody.term fbody.term
|
||
err3 <- try_ $ expectEqualQ e.loc epi fpi
|
||
pure (concat [err1, err2, err3], sub1 eret e)
|
||
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
|
||
(err1, ety) <- compare0Inner ctx e f
|
||
err2 <- try_ $
|
||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||
cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety
|
||
exs <- for cases $ \t => do
|
||
l <- lookupArm eloc t earms
|
||
r <- lookupArm floc t farms
|
||
try_ $
|
||
Term.compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
|
||
err3 <- try_ $ expectEqualQ eloc epi fpi
|
||
pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e)
|
||
where
|
||
lookupArm : Loc -> TagVal -> CaseEnumArms d n ->
|
||
Eff EqualInner (Term d n)
|
||
lookupArm loc t arms = case lookup t arms of
|
||
Just arm => pure arm
|
||
Nothing => throw $ TagNotIn loc t (fromList $ keys arms)
|
||
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
|
||
(err1, ety) <- compare0Inner ctx e f
|
||
err2 <- try_ $
|
||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||
err3 <- try_ $
|
||
Term.compare0 ctx
|
||
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
|
||
ezer fzer
|
||
let [< p, ih] = esuc.names
|
||
err4 <- try_ $
|
||
Term.compare0
|
||
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
|
||
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term
|
||
err5 <- try_ $ expectEqualQ e.loc epi fpi
|
||
err6 <- try_ $ expectEqualQ e.loc epi' fpi'
|
||
pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e)
|
||
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
|
||
(err1, ety) <- compare0Inner ctx e f
|
||
err2 <- try_ $
|
||
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
|
||
(q, ty) <- expectBOX defs ctx eloc ety
|
||
err3 <- try_ $
|
||
Term.compare0 (extendTy (epi * q) ebody.name ty ctx)
|
||
(substCaseBoxRet ebody.name ety eret)
|
||
ebody.term fbody.term
|
||
err4 <- try_ $ expectEqualQ eloc epi fpi
|
||
pure (concat [err1, err2, err3, err4], sub1 eret e)
|
||
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 _) _ _ = do
|
||
ty <- bigger a b
|
||
err <- try_ $ Term.compare0 ctx ty s t
|
||
pure (err, ty)
|
||
|
||
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
|
||
-- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
|
||
-- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
|
||
-- -----------------------------------------------------------
|
||
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
|
||
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
|
||
compare0' 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
|
||
err1 <- try_ $ compareType ctx ty1p ty2p
|
||
err2 <- try_ $ compareType ctx ty1q ty2q
|
||
(ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
|
||
err3 <- try_ $ Term.compare0 ctx ty_p val1 val2
|
||
pure (concat [err1, err2, err3], ty_q)
|
||
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
|
||
-- try
|
||
(err1, ety) <- compare0Inner ctx ty1 ty2
|
||
u <- expectTYPE defs ctx eloc ety
|
||
err2 <- try_ $ compareType ctx ret1 ret2
|
||
err3 <- try_ $ compareType ctx def1 def2
|
||
exs <- for allKinds $ \k =>
|
||
try_ $
|
||
compareArm ctx k ret1 u
|
||
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
|
||
pure (concat $ [err1, err2, err3] ++ exs, ret1)
|
||
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 _ _ = do
|
||
err <- try_ $ Term.compare0 ctx a s (E f)
|
||
pure (err, a)
|
||
compare0' ctx e (Ann t b _) _ _ = do
|
||
err <- try_ $ Term.compare0 ctx b (E e) t
|
||
pure (err, b)
|
||
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) ->
|
||
Eff EqualInner ()
|
||
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
|
||
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
|
||
fromInner : Eff EqualInner a -> Eff Equal a
|
||
fromInner = lift . map fst . runState mode
|
||
|
||
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
|
||
CompareAction : Nat -> Nat -> Type
|
||
CompareAction d n =
|
||
Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
|
||
|
||
private
|
||
runCompare : CompareAction d n -> Eff Equal ()
|
||
runCompare act = fromInner $ eachFace $ act !(askAt DEFS)
|
||
|
||
namespace Term
|
||
export covering
|
||
compare : (ty, s, t : Term d n) -> Eff 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) -> Eff 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) -> Eff Equal ()
|
||
compare e f = runCompare $ \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
|