quox/lib/Quox/Equal.idr

603 lines
22 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
0 EqModeState : Type -> Type
EqModeState = State EqMode
public export
0 EqualEff : List (Type -> Type)
EqualEff = [ErrorEff, EqModeState]
public export
0 Equal : Type -> Type
Equal = Eff $ EqualEff
export
runEqual : EqMode -> Equal a -> Either Error a
runEqual mode = extract . runExcept . evalState mode
export %inline
mode : Has EqModeState fs => Eff fs EqMode
mode = get
parameters (ctx : EqContext n)
private %inline
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal a
clashT ty s t = throw $ ClashT ctx !mode ty s t
private %inline
clashTy : Term 0 n -> Term 0 n -> Equal a
clashTy s t = throw $ ClashTy ctx !mode s t
private %inline
clashE : Elim 0 n -> Elim 0 n -> Equal a
clashE e f = throw $ ClashE ctx !mode e f
private %inline
wrongType : Term 0 n -> Term 0 n -> Equal a
wrongType ty s = throw $ WrongType 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 : Has ErrorEff fs => {n : Nat} ->
Definitions -> EqContext n -> Term 0 n -> Eff fs Bool
isSubSing defs ctx ty0 = do
Element ty0 nc <- whnf defs ctx 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 tags => pure $ length (SortedSet.toList tags) <= 1
Eq {} => pure True
Nat => pure False
BOX _ ty => isSubSing defs ctx ty
E (s :# _) => isSubSing defs ctx s
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 =>
(ctx : EqContext n) -> (t : Term 0 n) ->
Eff fs (So (isTyConE t))
ensureTyCon ctx t = case nchoose $ isTyConE t of
Left y => pure y
Right n => throw $ NotType (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
rethrow $ 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
Element s _ <- whnf defs ctx s
Element t _ <- whnf defs ctx t
tty <- ensureTyCon 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 $ weakE 1 e :@ BVT 0
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 e b
(Lam b, E e) => eta e b
(E e, E f) => Elim.compare0 ctx e f
(Lam _, t) => wrongType ctx ty t
(E _, t) => wrongType ctx ty t
(s, _) => wrongType ctx ty s
where
ctx' : EqContext (S n)
ctx' = extendTy qty res.name arg ctx
eta : Elim 0 n -> ScopeTerm 0 n -> Equal ()
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
eta e (S _ (N _)) = clashT 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 (sFst :# fst)) sSnd tSnd
(E e, E f) => Elim.compare0 ctx e f
(Pair {}, E _) => clashT ctx ty s t
(E _, Pair {}) => clashT ctx ty s t
(Pair {}, t) => wrongType ctx ty t
(E _, t) => wrongType ctx ty t
(s, _) => wrongType ctx ty s
compare0' ctx ty@(Enum tags) 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 ctx ty s t
(E e, E f) => Elim.compare0 ctx e f
(Tag _, E _) => clashT ctx ty s t
(E _, Tag _) => clashT ctx ty s t
(Tag _, t) => wrongType ctx ty t
(E _, t) => wrongType ctx ty t
(s, _) => wrongType ctx ty s
compare0' _ (Eq {}) _ _ =
-- ✨ uip ✨
--
-- ----------------------------
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
pure ()
compare0' ctx Nat s t = local_ Equal $
case (s, t) of
-- ---------------
-- Γ ⊢ 0 = 0 :
(Zero, Zero) => pure ()
-- Γ ⊢ m = n :
-- -------------------------
-- Γ ⊢ succ m = succ n :
(Succ m, Succ n) => compare0 ctx Nat m n
(E e, E f) => Elim.compare0 ctx e f
(Zero, Succ _) => clashT ctx Nat s t
(Zero, E _) => clashT ctx Nat s t
(Succ _, Zero) => clashT ctx Nat s t
(Succ _, E _) => clashT ctx Nat s t
(E _, Zero) => clashT ctx Nat s t
(E _, Succ _) => clashT ctx Nat s t
(Zero, t) => wrongType ctx Nat t
(Succ _, t) => wrongType ctx Nat t
(E _, t) => wrongType ctx Nat t
(s, _) => wrongType 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 ctx ty t
(E _, t) => wrongType ctx ty t
(s, _) => wrongType 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, …
E e <- pure s | _ => wrongType ctx ty s
E f <- pure t | _ => wrongType 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
Element t _ <- whnf defs ctx t
ts <- ensureTyCon ctx s
tt <- ensureTyCon ctx t
st <- either pure (const $ clashTy 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 (TYPE k) (TYPE l) =
-- 𝓀
-- ----------------------
-- Γ ⊢ Type 𝓀 <: Type
expectModeU !mode k l
compareType' ctx (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 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
local_ Equal $ do
Term.compare0 ctx sTy.zero sl tl
Term.compare0 ctx sTy.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 ctx s t
compareType' ctx Nat Nat =
-- ------------
-- Γ ⊢ <:
pure ()
compareType' ctx (BOX pi a) (BOX rh b) = do
expectEqualQ 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
private covering
replaceEnd : EqContext n ->
(e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
Equal (Elim 0 n)
replaceEnd ctx e p ne = do
(ty, l, r) <- expectEq defs ctx !(computeElimTypeE defs ctx e)
pure $ ends l r p :# dsub1 ty (K p)
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
Element f nf <- whnf defs ctx f
-- [fixme] there is a better way to do this "isSubSing" stuff for sure
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 ()
-- replace applied equalities with the appropriate end first
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A𝟎/i
--
-- [todo] maybe have typed whnf and do this (and η???) there instead
compare0' ctx (e :% K p) f ne nf =
compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
compare0' ctx e (f :% K q) ne nf =
compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
compare0' ctx e@(F x) f@(F y) _ _ = unless (x == y) $ clashE ctx e f
compare0' ctx e@(F _) f _ _ = clashE ctx e f
compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE ctx e f
compare0' ctx e@(B _) f _ _ = clashE ctx e f
compare0' ctx (e :@ s) (f :@ t) ne nf =
local_ Equal $ do
compare0 ctx e f
(_, arg, _) <- expectPi defs ctx =<<
computeElimTypeE defs ctx e @{noOr1 ne}
Term.compare0 ctx arg s t
compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f
compare0' ctx (CasePair epi e eret ebody)
(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 ety
let [< x, y] = ebody.names
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
(substCasePairRet ety eret)
ebody.term fbody.term
expectEqualQ epi fpi
compare0' ctx e@(CasePair {}) f _ _ = clashE ctx e f
compare0' ctx (CaseEnum epi e eret earms)
(CaseEnum fpi f fret farms) 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 ety) $ \t =>
compare0 ctx (sub1 eret $ Tag t :# ety)
!(lookupArm t earms) !(lookupArm t farms)
expectEqualQ epi fpi
where
lookupArm : TagVal -> CaseEnumArms d n -> Equal (Term d n)
lookupArm t arms = case lookup t arms of
Just arm => pure arm
Nothing => throw $ TagNotIn t (fromList $ keys arms)
compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f
compare0' ctx (CaseNat epi epi' e eret ezer esuc)
(CaseNat fpi fpi' f fret fzer fsuc) 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 (Zero :# Nat)) ezer fzer
let [< p, ih] = esuc.names
compare0 (extendTyN [< (epi, p, Nat), (epi', ih, eret.term)] ctx)
(substCaseSuccRet eret)
esuc.term fsuc.term
expectEqualQ epi fpi
expectEqualQ epi' fpi'
compare0' ctx e@(CaseNat {}) f _ _ = clashE ctx e f
compare0' ctx (CaseBox epi e eret ebody)
(CaseBox 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
(q, ty) <- expectBOX defs ctx ety
compare0 (extendTy (epi * q) ebody.name ty ctx)
(substCaseBoxRet ety eret)
ebody.term fbody.term
expectEqualQ epi fpi
compare0' ctx e@(CaseBox {}) f _ _ = clashE ctx e f
compare0' ctx (s :# a) (t :# b) _ _ =
let ty = case !mode of Super => a; _ => b in
Term.compare0 ctx ty s t
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 ctx e f
compare0' ctx (Comp _ _ _ _ (K _) _ _) _ ne _ = void $ absurd $ noOr2 ne
compare0' ctx (Comp _ _ _ _ (B i) _ _) _ _ _ = absurd i
compare0' ctx _ (Comp _ _ _ _ (K _) _ _) _ nf = void $ absurd $ noOr2 nf
compare0' ctx (TypeCase ty1 ret1 arms1 def1)
(TypeCase ty2 ret2 arms2 def2)
ne _ =
local_ Equal $ do
compare0 ctx ty1 ty2
u <- expectTYPE defs ctx =<< 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 ctx e f
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t
compare0' ctx e@(_ :# _) f _ _ = clashE 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),
(Zero, b, Arr Zero (BVT 0) (TYPE u))] 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),
(Zero, b, Arr Zero (BVT 0) (TYPE u))] 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),
(Zero, a1, TYPE u),
(Zero, a, Eq0 (TYPE u) (BVT 1) (BVT 0)),
(Zero, l, BVT 2),
(Zero, r, BVT 2)] 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) ctx
compare0 ctx (weakT 1 ret) b1.term b1.term
parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
-- [todo] only split on the dvars that are actually used anywhere in
-- the calls to `splits`
parameters (mode : EqMode)
namespace Term
export covering
compare : (ty, s, t : Term d n) -> Eff fs ()
compare ty s t =
map fst $ runState @{Z} mode $
for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in
lift $ compare0 !defs ectx (ty // th) (s // th) (t // th)
export covering
compareType : (s, t : Term d n) -> Eff fs ()
compareType s t =
map fst $ runState @{Z} mode $
for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in
lift $ 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 %inline
compare : (e, f : Elim d n) -> Eff fs ()
compare e f =
map fst $ runState @{Z} mode $
for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in
lift $ compare0 !defs ectx (e // th) (f // th)
namespace Term
export covering %inline
equal, sub, super : (ty, s, t : Term d n) -> Eff fs ()
equal = compare Equal
sub = compare Sub
super = compare Super
export covering %inline
equalType, subtype, supertype : (s, t : Term d n) -> Eff fs ()
equalType = compareType Equal
subtype = compareType Sub
supertype = compareType Super
namespace Elim
export covering %inline
equal, sub, super : (e, f : Elim d n) -> Eff fs ()
equal = compare Equal
sub = compare Sub
super = compare Super