quox/lib/Quox/Equal.idr

686 lines
26 KiB
Idris
Raw Normal View History

2022-02-26 20:18:16 -05:00
module Quox.Equal
import Quox.BoolExtra
import public Quox.Typing
import Data.Maybe
2023-03-31 13:23:30 -04:00
import Quox.EffExtra
2022-02-26 20:18:16 -05:00
2023-03-26 18:07:39 -04:00
%default total
2022-02-26 20:18:16 -05:00
public export
2023-05-01 21:06:25 -04:00
EqModeState : Type -> Type
2023-03-31 13:23:30 -04:00
EqModeState = State EqMode
2023-01-08 14:44:25 -05:00
public export
2023-05-01 21:06:25 -04:00
Equal : Type -> Type
Equal = Eff [ErrorEff, DefsReader, NameGen]
2023-01-08 14:44:25 -05:00
public export
2023-05-01 21:06:25 -04:00
Equal_ : Type -> Type
Equal_ = Eff [ErrorEff, NameGen, EqModeState]
export
2023-05-01 21:06:25 -04:00
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
2023-01-08 14:44:25 -05:00
2023-03-31 13:23:30 -04:00
export %inline
mode : Has EqModeState fs => Eff fs EqMode
mode = get
2023-01-08 14:44:25 -05:00
2023-05-01 21:06:25 -04:00
parameters (loc : Loc) (ctx : EqContext n)
private %inline
2023-05-01 21:06:25 -04:00
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal_ a
clashT ty s t = throw $ ClashT loc ctx !mode ty s t
2023-01-08 14:44:25 -05:00
private %inline
2023-05-01 21:06:25 -04:00
clashTy : Term 0 n -> Term 0 n -> Equal_ a
clashTy s t = throw $ ClashTy loc ctx !mode s t
private %inline
2023-05-01 21:06:25 -04:00
clashE : Elim 0 n -> Elim 0 n -> Equal_ a
clashE e f = throw $ ClashE loc ctx !mode e f
2023-01-08 14:44:25 -05:00
2023-03-26 08:38:37 -04:00
private %inline
2023-05-01 21:06:25 -04:00
wrongType : Term 0 n -> Term 0 n -> Equal_ a
wrongType ty s = throw $ WrongType loc ctx ty s
2023-03-26 08:38:37 -04:00
2023-01-08 14:44:25 -05:00
2023-02-12 15:30:08 -05:00
public export %inline
2023-04-01 13:16:43 -04:00
sameTyCon : (s, t : Term d n) ->
2023-04-03 11:46:23 -04:00
(0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) =>
2023-02-12 15:30:08 -05:00
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
2023-02-12 15:30:08 -05:00
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
2023-05-01 21:06:25 -04:00
sameTyCon (Nat {}) (Nat {}) = True
sameTyCon (Nat {}) _ = False
2023-03-31 13:11:35 -04:00
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
2023-02-12 15:30:08 -05:00
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
2023-04-15 09:13:01 -04:00
||| 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
2023-05-01 21:06:25 -04:00
isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n -> Equal_ Bool
isSubSing defs ctx ty0 = do
2023-05-01 21:06:25 -04:00
Element ty0 nc <- whnf defs ctx ty0.loc ty0
2023-04-15 09:13:01 -04:00
case ty0 of
2023-05-01 21:06:25 -04:00
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
2023-02-10 15:40:44 -05:00
2023-03-15 10:54:51 -04:00
export
2023-04-01 13:16:43 -04:00
ensureTyCon : Has ErrorEff fs =>
2023-05-01 21:06:25 -04:00
(loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
2023-04-03 11:46:23 -04:00
Eff fs (So (isTyConE t))
2023-05-01 21:06:25 -04:00
ensureTyCon loc ctx t = case nchoose $ isTyConE t of
2023-03-15 10:54:51 -04:00
Left y => pure y
2023-05-01 21:06:25 -04:00
Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen)
2023-03-15 10:54:51 -04:00
2023-04-15 09:13:01 -04:00
||| 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) =>
2023-05-01 21:06:25 -04:00
Equal_ (Term 0 n)
computeElimTypeE defs ectx e =
2023-04-15 09:13:01 -04:00
let Val n = ectx.termLen in
2023-05-01 21:06:25 -04:00
lift $ computeElimType defs (toWhnfContext ectx) e
2023-04-15 09:13:01 -04:00
parameters (defs : Definitions)
mutual
namespace Term
2023-02-19 11:04:57 -05:00
||| `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`**. ⚠
2023-02-10 15:40:44 -05:00
export covering %inline
2023-05-01 21:06:25 -04:00
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal_ ()
2023-02-19 11:54:39 -05:00
compare0 ctx ty s t =
wrapErr (WhileComparingT ctx !mode ty s t) $ do
let Val n = ctx.termLen
2023-05-01 21:06:25 -04:00
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'
2023-02-10 15:40:44 -05:00
2023-02-19 11:04:57 -05:00
||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
2023-02-10 15:40:44 -05:00
private %inline
2023-04-01 13:16:43 -04:00
toLamBody : Elim d n -> Term d (S n)
2023-05-01 21:06:25 -04:00
toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
2023-02-10 15:40:44 -05:00
private covering
2023-04-01 13:16:43 -04:00
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) =>
2023-05-01 21:06:25 -04:00
Equal_ ()
compare0' ctx (TYPE {}) s t = compareType ctx s t
2023-02-10 15:40:44 -05:00
2023-05-01 21:06:25 -04:00
compare0' ctx ty@(Pi {qty, arg, res, _}) s t {n} = local_ Equal $
2023-02-10 15:40:44 -05:00
case (s, t) of
2023-03-15 10:54:51 -04:00
-- Γ, x : A ⊢ s = t : B
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
2023-05-01 21:06:25 -04:00
(Lam b1 {}, Lam b2 {}) =>
compare0 ctx' res.term b1.term b2.term
2023-02-19 11:04:57 -05:00
-- Γ, x : A ⊢ s = e x : B
2023-03-15 10:54:51 -04:00
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
2023-05-01 21:06:25 -04:00
(E e, Lam b {}) => eta s.loc e b
(Lam b {}, E e) => eta s.loc e b
2023-02-19 11:04:57 -05:00
(E e, E f) => Elim.compare0 ctx e f
2023-03-15 10:54:51 -04:00
2023-05-01 21:06:25 -04:00
(Lam {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
2023-02-19 11:04:57 -05:00
where
2023-04-01 13:16:43 -04:00
ctx' : EqContext (S n)
2023-03-15 10:54:51 -04:00
ctx' = extendTy qty res.name arg ctx
2023-02-19 11:04:57 -05:00
2023-05-01 21:06:25 -04:00
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
2023-02-10 15:40:44 -05:00
2023-03-31 13:23:30 -04:00
compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
2023-02-10 15:40:44 -05:00
case (s, t) of
2023-02-19 11:04:57 -05:00
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
2023-03-15 10:54:51 -04:00
-- --------------------------------------------
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
2023-02-19 11:04:57 -05:00
--
-- [todo] η for π ≥ 0 maybe
2023-05-01 21:06:25 -04:00
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
2023-02-10 15:40:44 -05:00
compare0 ctx fst sFst tFst
2023-05-01 21:06:25 -04:00
compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
2023-02-19 11:04:57 -05:00
2023-03-15 10:54:51 -04:00
(E e, E f) => Elim.compare0 ctx e f
2023-05-01 21:06:25 -04:00
(Pair {}, E _) => clashT s.loc ctx ty s t
(E _, Pair {}) => clashT s.loc ctx ty s t
2023-03-26 08:38:37 -04:00
2023-05-01 21:06:25 -04:00
(Pair {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
2023-02-10 15:40:44 -05:00
2023-05-01 21:06:25 -04:00
compare0' ctx ty@(Enum {}) s t = local_ Equal $
case (s, t) of
-- --------------------
-- Γ ⊢ `t = `t : {ts}
--
-- t ∈ ts is in the typechecker, not here, ofc
2023-05-01 21:06:25 -04:00
(Tag t1 {}, Tag t2 {}) =>
unless (t1 == t2) $ clashT s.loc ctx ty s t
(E e, E f) => Elim.compare0 ctx e f
2023-03-15 10:54:51 -04:00
2023-05-01 21:06:25 -04:00
(Tag {}, E _) => clashT s.loc ctx ty s t
(E _, Tag {}) => clashT s.loc ctx ty s t
2023-03-26 08:38:37 -04:00
2023-05-01 21:06:25 -04:00
(Tag {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
2023-02-19 11:04:57 -05:00
compare0' _ (Eq {}) _ _ =
-- ✨ uip ✨
--
2023-04-15 09:13:01 -04:00
-- ----------------------------
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
2023-02-19 11:04:57 -05:00
pure ()
2023-02-10 15:40:44 -05:00
2023-05-01 21:06:25 -04:00
compare0' ctx nat@(Nat {}) s t = local_ Equal $
2023-03-26 08:40:54 -04:00
case (s, t) of
-- ---------------
-- Γ ⊢ 0 = 0 :
2023-05-01 21:06:25 -04:00
(Zero {}, Zero {}) => pure ()
2023-03-26 08:40:54 -04:00
2023-05-01 21:06:25 -04:00
-- Γ ⊢ s = t :
2023-03-26 08:40:54 -04:00
-- -------------------------
2023-05-01 21:06:25 -04:00
-- Γ ⊢ succ s = succ t :
(Succ s' {}, Succ t' {}) => compare0 ctx nat s' t'
2023-03-26 08:40:54 -04:00
(E e, E f) => Elim.compare0 ctx e f
2023-05-01 21:06:25 -04:00
(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
2023-03-26 08:40:54 -04:00
2023-05-01 21:06:25 -04:00
(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
2023-03-26 08:40:54 -04:00
2023-05-01 21:06:25 -04:00
compare0' ctx ty@(BOX q ty' {}) s t = local_ Equal $
2023-03-31 13:11:35 -04:00
case (s, t) of
-- Γ ⊢ s = t : A
-- -----------------------
-- Γ ⊢ [s] = [t] : [π.A]
2023-05-01 21:06:25 -04:00
(Box s' {}, Box t' {}) => compare0 ctx ty' s' t'
2023-03-31 13:11:35 -04:00
(E e, E f) => Elim.compare0 ctx e f
2023-05-01 21:06:25 -04:00
(Box {}, t) => wrongType t.loc ctx ty t
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
2023-03-31 13:11:35 -04:00
2023-02-10 15:40:44 -05:00
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, …
2023-05-01 21:06:25 -04:00
let E e = s | _ => wrongType s.loc ctx ty s
E f = t | _ => wrongType t.loc ctx ty t
2023-02-12 15:30:08 -05:00
Elim.compare0 ctx e f
2023-02-10 15:40:44 -05:00
2023-02-19 11:04:57 -05:00
||| compares two types, using the current variance `mode` for universes.
||| fails if they are not types, even if they would happen to be equal.
2023-02-19 11:43:14 -05:00
export covering %inline
2023-05-01 21:06:25 -04:00
compareType : EqContext n -> (s, t : Term 0 n) -> Equal_ ()
2023-02-10 15:40:44 -05:00
compareType ctx s t = do
let Val n = ctx.termLen
2023-05-01 21:06:25 -04:00
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'
2023-02-10 15:40:44 -05:00
private covering
2023-04-01 13:16:43 -04:00
compareType' : EqContext n -> (s, t : Term 0 n) ->
(0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
(0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
2023-04-17 17:58:24 -04:00
(0 _ : So (sameTyCon s t)) =>
2023-05-01 21:06:25 -04:00
Equal_ ()
2023-02-19 11:04:57 -05:00
-- equality is the same as subtyping, except with the
-- "≤" in the TYPE rule being replaced with "="
2023-05-01 21:06:25 -04:00
compareType' ctx a@(TYPE k {}) (TYPE l {}) =
2023-02-19 11:04:57 -05:00
-- 𝓀
-- ----------------------
-- Γ ⊢ Type 𝓀 <: Type
2023-05-01 21:06:25 -04:00
expectModeU a.loc !mode k l
2023-02-12 15:30:08 -05:00
2023-05-01 21:06:25 -04:00
compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
2023-02-19 11:04:57 -05:00
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
2023-05-01 21:06:25 -04:00
expectEqualQ a.loc sQty tQty
2023-03-31 13:23:30 -04:00
local flip $ compareType ctx sArg tArg -- contra
2023-04-01 13:16:43 -04:00
compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
2023-02-12 15:30:08 -05:00
compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
(Sig {fst = tFst, snd = tSnd, _}) = do
2023-02-19 11:04:57 -05:00
-- Γ ⊢ A₁ <: A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- --------------------------------------
-- Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
2023-02-12 15:30:08 -05:00
compareType ctx sFst tFst
2023-04-01 13:16:43 -04:00
compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
2023-02-12 15:30:08 -05:00
compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
(Eq {ty = tTy, l = tl, r = tr, _}) = do
2023-02-19 11:04:57 -05:00
-- Γ ⊢ 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
2023-03-31 13:23:30 -04:00
local_ Equal $ do
2023-02-12 15:30:08 -05:00
Term.compare0 ctx sTy.zero sl tl
Term.compare0 ctx sTy.one sr tr
2023-05-01 21:06:25 -04:00
compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
-- ------------------
-- Γ ⊢ {ts} <: {ts}
--
-- no subtyping based on tag subsets, since that would need
-- a runtime coercion
2023-05-01 21:06:25 -04:00
unless (tags1 == tags2) $ clashTy s.loc ctx s t
2023-05-01 21:06:25 -04:00
compareType' ctx (Nat {}) (Nat {}) =
2023-03-26 08:40:54 -04:00
-- ------------
-- Γ ⊢ <:
pure ()
2023-05-01 21:06:25 -04:00
compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
expectEqualQ loc pi rh
2023-03-31 13:11:35 -04:00
compareType ctx a b
2023-02-12 15:30:08 -05:00
compareType' ctx (E e) (E f) = do
-- no fanciness needed here cos anything other than a neutral
-- has been inlined by whnf
2023-02-12 15:30:08 -05:00
Elim.compare0 ctx e f
2023-02-11 12:15:50 -05:00
2023-05-01 21:06:25 -04:00
-- Ψ | Γ ⊢₀ e ⇒ Eq [𝑖 ⇒ A] s t
-- -----------------------------
-- Ψ | Γ ⊢ e @0 = s ⇒ A[0/𝑖]
-- Ψ | Γ ⊢ e @1 = s ⇒ A[1/𝑖]
2023-02-11 12:15:50 -05:00
private covering
2023-04-01 13:16:43 -04:00
replaceEnd : EqContext n ->
2023-05-01 21:06:25 -04:00
(e : Elim 0 n) -> Loc -> DimConst -> Loc ->
(0 ne : NotRedex defs e) -> Equal_ (Elim 0 n)
replaceEnd ctx e eloc p ploc ne = do
(ty, l, r) <- expectEq defs ctx eloc !(computeElimTypeE defs ctx e)
pure $ Ann (ends l r p) (dsub1 ty (K p ploc)) eloc
namespace Elim
2023-02-11 12:15:50 -05:00
-- [fixme] the following code ends up repeating a lot of work in the
-- computeElimType calls. the results should be shared better
2023-02-19 11:04:57 -05:00
||| compare two eliminations according to the given variance `mode`.
|||
||| ⚠ **assumes that they have both been typechecked, and have
||| equal types.** ⚠
2023-02-10 15:40:44 -05:00
export covering %inline
2023-05-01 21:06:25 -04:00
compare0 : EqContext n -> (e, f : Elim 0 n) -> Equal_ ()
2023-02-10 15:40:44 -05:00
compare0 ctx e f =
wrapErr (WhileComparingE ctx !mode e f) $ do
let Val n = ctx.termLen
2023-05-01 21:06:25 -04:00
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
2023-02-10 15:40:44 -05:00
private covering
2023-04-01 13:16:43 -04:00
compare0' : EqContext n ->
(e, f : Elim 0 n) ->
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
2023-05-01 21:06:25 -04:00
Equal_ ()
2023-02-11 12:15:50 -05:00
-- replace applied equalities with the appropriate end first
2023-05-01 21:06:25 -04:00
-- (see `replaceEnd`)
compare0' ctx (DApp e (K p ploc) loc) f ne nf =
compare0 ctx !(replaceEnd ctx e loc p ploc $ noOr1 ne) f
compare0' ctx e (DApp f (K q qloc) loc) ne nf =
compare0 ctx e !(replaceEnd ctx f loc q qloc $ noOr1 nf)
compare0' ctx e@(F x {}) f@(F y {}) _ _ =
unless (x == y) $ 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 =
2023-03-31 13:23:30 -04:00
local_ Equal $ do
2023-02-12 15:30:08 -05:00
compare0 ctx e f
2023-05-01 21:06:25 -04:00
(_, arg, _) <- expectPi defs ctx eloc =<<
computeElimTypeE defs ctx e @{noOr1 ne}
2023-02-12 15:30:08 -05:00
Term.compare0 ctx arg s t
2023-05-01 21:06:25 -04:00
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 =
2023-03-31 13:23:30 -04:00
local_ Equal $ do
2023-02-11 12:15:50 -05:00
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
2023-04-01 13:16:43 -04:00
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
2023-05-01 21:06:25 -04:00
(fst, snd) <- expectSig defs ctx eloc ety
let [< x, y] = ebody.names
2023-03-15 10:54:51 -04:00
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
2023-05-01 21:06:25 -04:00
(substCasePairRet ebody.names ety eret)
ebody.term fbody.term
2023-05-01 21:06:25 -04:00
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 =
2023-03-31 13:23:30 -04:00
local_ Equal $ do
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
2023-04-01 13:16:43 -04:00
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
2023-05-01 21:06:25 -04:00
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
2023-05-01 21:06:25 -04:00
lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
lookupArm loc t arms = case lookup t arms of
Just arm => pure arm
2023-05-01 21:06:25 -04:00
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 =
2023-03-31 13:23:30 -04:00
local_ Equal $ do
2023-03-26 08:40:54 -04:00
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
2023-04-01 13:16:43 -04:00
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
2023-05-01 21:06:25 -04:00
compare0 ctx
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
ezer fzer
2023-03-26 08:40:54 -04:00
let [< p, ih] = esuc.names
2023-05-01 21:06:25 -04:00
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 =
2023-03-31 13:23:30 -04:00
local_ Equal $ do
2023-03-31 13:11:35 -04:00
compare0 ctx e f
ety <- computeElimTypeE defs ctx e @{noOr1 ne}
2023-04-01 13:16:43 -04:00
compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
2023-05-01 21:06:25 -04:00
(q, ty) <- expectBOX defs ctx eloc ety
2023-03-31 13:11:35 -04:00
compare0 (extendTy (epi * q) ebody.name ty ctx)
2023-05-01 21:06:25 -04:00
(substCaseBoxRet ebody.name ety eret)
2023-03-31 13:11:35 -04:00
ebody.term fbody.term
2023-05-01 21:06:25 -04:00
expectEqualQ eloc epi fpi
compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
2023-03-31 13:11:35 -04:00
2023-05-01 21:06:25 -04:00
-- Ψ | Γ ⊢ s <: t : B
-- --------------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
--
-- and similar for :> and A
compare0' ctx (Ann s a _) (Ann t b _) _ _ =
2023-04-15 09:13:01 -04:00
let ty = case !mode of Super => a; _ => b in
Term.compare0 ctx ty s t
2023-05-01 21:06:25 -04:00
-- Ψ | Γ ⊢ 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
2023-04-15 09:13:01 -04:00
compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
compare0 ctx val1 val2
2023-05-01 21:06:25 -04:00
compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
2023-02-22 01:40:19 -05:00
2023-05-01 21:06:25 -04:00
-- (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
2023-04-15 09:13:01 -04:00
2023-05-01 21:06:25 -04:00
compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc)
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
2023-04-03 11:46:23 -04:00
local_ Equal $ do
compare0 ctx ty1 ty2
2023-05-01 21:06:25 -04:00
u <- expectTYPE defs ctx eloc =<<
computeElimTypeE defs ctx ty1 @{noOr1 ne}
2023-04-03 11:46:23 -04:00
compareType ctx ret1 ret2
2023-04-15 09:13:01 -04:00
compareType ctx def1 def2
for_ allKinds $ \k =>
compareArm ctx k ret1 u
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
2023-05-01 21:06:25 -04:00
compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f
2023-04-03 11:46:23 -04:00
2023-05-01 21:06:25 -04:00
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
2023-02-10 15:40:44 -05:00
2023-04-15 09:13:01 -04:00
||| 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) ->
2023-05-01 21:06:25 -04:00
Equal_ ()
2023-04-15 09:13:01 -04:00
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) ->
2023-05-01 21:06:25 -04:00
Equal_ ()
2023-04-15 09:13:01 -04:00
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
2023-05-01 21:06:25 -04:00
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
2023-04-15 09:13:01 -04:00
compare0 ctx (weakT 2 ret) b1.term b2.term
compareArm_ ctx KSig ret u b1 b2 = do
let [< a, b] = b1.names
ctx = extendTyN
2023-05-01 21:06:25 -04:00
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
2023-04-15 09:13:01 -04:00
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
2023-05-01 21:06:25 -04:00
[< (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
2023-04-15 09:13:01 -04:00
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
2023-05-01 21:06:25 -04:00
let ctx = extendTy Zero b1.name (TYPE u b1.name.loc) ctx
2023-04-15 09:13:01 -04:00
compare0 ctx (weakT 1 ret) b1.term b1.term
2023-02-10 15:40:44 -05:00
2023-05-01 21:06:25 -04:00
parameters (loc : Loc) (ctx : TyContext d n)
-- [todo] only split on the dvars that are actually used anywhere in
-- the calls to `splits`
2023-02-10 15:40:44 -05:00
parameters (mode : EqMode)
2023-05-01 21:06:25 -04:00
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 !defs
namespace Term
2023-02-10 15:40:44 -05:00
export covering
2023-05-01 21:06:25 -04:00
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)
2023-02-10 15:40:44 -05:00
export covering
2023-05-01 21:06:25 -04:00
compareType : (s, t : Term d n) -> Equal ()
compareType s t = runCompare $ \defs, ectx, th =>
compareType defs ectx (s // th) (t // th)
namespace Elim
2023-02-11 12:15:50 -05:00
||| you don't have to pass the type in but the arguments must still be
||| of the same type!!
2023-05-01 21:06:25 -04:00
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
2023-05-01 21:06:25 -04:00
equal, sub, super : (ty, s, t : Term d n) -> Equal ()
2023-02-10 15:40:44 -05:00
equal = compare Equal
sub = compare Sub
2023-02-14 16:29:06 -05:00
super = compare Super
export covering %inline
2023-05-01 21:06:25 -04:00
equalType, subtype, supertype : (s, t : Term d n) -> Equal ()
2023-02-10 15:40:44 -05:00
equalType = compareType Equal
subtype = compareType Sub
2023-02-14 16:29:06 -05:00
supertype = compareType Super
namespace Elim
export covering %inline
2023-05-01 21:06:25 -04:00
equal, sub, super : (e, f : Elim d n) -> Equal ()
2023-02-10 15:40:44 -05:00
equal = compare Equal
sub = compare Sub
2023-02-14 16:29:06 -05:00
super = compare Super