quox/lib/Quox/Equal.idr

443 lines
16 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 public Control.Monad.Either
import public Control.Monad.Reader
import Data.Maybe
public export
record CmpContext where
constructor MkCmpContext
mode : EqMode
public export
0 HasCmpContext : (Type -> Type) -> Type
HasCmpContext = MonadReader CmpContext
public export
0 CanEqual : (q : Type) -> (Type -> Type) -> Type
CanEqual q m = (HasErr q m, HasCmpContext m)
private %inline
mode : HasCmpContext m => m EqMode
mode = asks mode
private %inline
clashT : CanEqual q m => Term q d n -> Term q d n -> Term q d n -> m a
clashT ty s t = throwError $ ClashT !mode ty s t
private %inline
clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a
clashE e f = throwError $ ClashE !mode e f
||| true if a term is syntactically a type, or is neutral.
|||
||| this function *doesn't* push substitutions, because its main use is as a
||| `So` argument to skip cases that are already known to be nonsense. and
||| the substitutions have already been pushed.
public export %inline
isTyCon : (t : Term {}) -> Bool
isTyCon (TYPE {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (E {}) = True
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
public export %inline
sameTyCon : (s, t : Term q d n) ->
(0 ts : So (isTyCon s)) => (0 tt : So (isTyCon 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 (E {}) (E {}) = True
sameTyCon (E {}) _ = False
parameters (defs : Definitions' q g)
||| 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.
||| * all equality types are subsingletons because uip is admissible by
||| boundary separation.
||| * an enum type is a subsingleton if it has zero or one tags.
public export
isSubSing : HasErr q m => Term q 0 n -> m Bool
isSubSing ty = do
Element ty nc <- whnfT defs ty
case ty of
TYPE _ => pure False
Pi {res, _} => isSubSing res.term
Lam {} => pure False
Sig {fst, snd} => isSubSing fst `andM` isSubSing snd.term
Pair {} => pure False
Enum tags => pure $ length (SortedSet.toList tags) <= 1
Tag {} => pure False
Eq {} => pure True
DLam {} => pure False
E (s :# _) => isSubSing s
E _ => pure False
parameters {auto _ : HasErr q m}
export %inline
ensure : (a -> Error q) -> (p : a -> Bool) -> (t : a) -> m (So (p t))
ensure e p t = case nchoose $ p t of
Left y => pure y
Right _ => throwError $ e t
export %inline
ensureTyCon : HasErr q m => (t : Term q d n) -> m (So (isTyCon t))
ensureTyCon = ensure NotType isTyCon
parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
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 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
compare0 ctx ty s t =
wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do
Element ty nty <- whnfT defs ty
Element s ns <- whnfT defs s
Element t nt <- whnfT defs t
tty <- ensureTyCon 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 q d n -> Term q d (S n)
toLamBody e = E $ weakE e :@ BVT 0
private covering
compare0' : TContext q 0 n ->
(ty, s, t : Term q 0 n) ->
(0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
(0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) =>
m ()
compare0' ctx (TYPE _) s t = compareType ctx s t
compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := 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
_ => throwError $ WrongType ty s t
where
ctx' : TContext q 0 (S n)
ctx' = ctx :< arg
eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
eta e (S _ (N _)) = clashT ty s t
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := 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) => compare0 ctx e f
_ => throwError $ WrongType ty s t
compare0' ctx ty@(Enum tags) s t = local {mode := 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 ty s t
(E e, E f) => compare0 ctx e f
_ => throwError $ WrongType ty s t
compare0' _ (Eq {}) _ _ =
-- ✨ uip ✨
--
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
pure ()
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 | _ => throwError $ WrongType ty s t
E f <- pure t | _ => throwError $ WrongType ty s 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 : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
compareType ctx s t = do
Element s ns <- whnfT defs s
Element t nt <- whnfT defs t
ts <- ensureTyCon s
tt <- ensureTyCon t
st <- either pure (const $ clashT (TYPE UAny) s t) $
nchoose $ sameTyCon s t
compareType' ctx s t
private covering
compareType' : TContext q 0 n -> (s, t : Term q 0 n) ->
(0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
(0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
(0 st : So (sameTyCon s t)) =>
m ()
-- 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 {mode $= flip} $ compareType ctx sArg tArg -- contra
compareType (ctx :< sArg) 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 (ctx :< sFst) 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 ctx sTy.zero tTy.zero
compareType ctx sTy.one tTy.one
local {mode := 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) $ clashT (TYPE UAny) s t
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
||| performs the minimum work required to recompute the type of an elim.
|||
||| ⚠ **assumes the elim is already typechecked.** ⚠
private covering
computeElimType : TContext q 0 n -> (e : Elim q 0 n) ->
(0 ne : NotRedex defs e) ->
m (Term q 0 n)
computeElimType ctx (F x) _ = do
defs <- lookupFree' defs x
pure $ defs.type.get
computeElimType ctx (B i) _ = do
pure $ ctx !! i
computeElimType ctx (f :@ s) ne = do
(_, arg, res) <- expectPi defs !(computeElimType ctx f (noOr1 ne))
pure $ sub1 res (s :# arg)
computeElimType ctx (CasePair {pair, ret, _}) _ = do
pure $ sub1 ret pair
computeElimType ctx (CaseEnum {tag, ret, _}) _ = do
pure $ sub1 ret tag
computeElimType ctx (f :% p) ne = do
(ty, _, _) <- expectEq defs !(computeElimType ctx f (noOr1 ne))
pure $ dsub1 ty p
computeElimType ctx (_ :# ty) _ = do
pure ty
private covering
replaceEnd : TContext q 0 n ->
(e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
m (Elim q 0 n)
replaceEnd ctx e p ne = do
(ty, l, r) <- expectEq defs !(computeElimType ctx e ne)
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 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
compare0 ctx e f =
wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do
Element e ne <- whnfT defs e
Element f nf <- whnfT defs f
-- [fixme] there is a better way to do this "isSubSing" stuff for sure
unless !(isSubSing defs !(computeElimType ctx e ne)) $
compare0' ctx e f ne nf
private covering
compare0' : TContext q 0 n ->
(e, f : Elim q 0 n) ->
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
m ()
-- 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' _ e@(F x) f@(F y) _ _ = unless (x == y) $ clashE e f
compare0' _ e@(F _) f _ _ = clashE e f
compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE e f
compare0' _ e@(B _) f _ _ = clashE e f
compare0' ctx (e :@ s) (f :@ t) ne nf =
local {mode := Equal} $ do
compare0 ctx e f
(_, arg, _) <- expectPi defs !(computeElimType ctx e (noOr1 ne))
Term.compare0 ctx arg s t
compare0' _ e@(_ :@ _) f _ _ = clashE e f
compare0' ctx (CasePair epi e eret ebody)
(CasePair fpi f fret fbody) ne nf =
local {mode := Equal} $ do
compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne)
compareType (ctx :< ety) eret.term fret.term
(fst, snd) <- expectSig defs ety
Term.compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
ebody.term fbody.term
expectEqualQ epi fpi
compare0' _ e@(CasePair {}) f _ _ = clashE e f
compare0' ctx (CaseEnum epi e eret earms)
(CaseEnum fpi f fret farms) ne nf =
local {mode := Equal} $ do
compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne)
compareType (ctx :< ety) eret.term fret.term
for_ !(expectEnum defs ety) $ \t =>
compare0 ctx (sub1 eret $ Tag t :# ety)
!(lookupArm t earms) !(lookupArm t farms)
expectEqualQ epi fpi
where
lookupArm : TagVal -> CaseEnumArms q d n -> m (Term q d n)
lookupArm t arms = case lookup t arms of
Just arm => pure arm
Nothing => throwError $ TagNotIn t (fromList $ keys arms)
compare0' _ e@(CaseEnum {}) f _ _ = clashE e f
compare0' ctx (s :# a) (t :# b) _ _ =
Term.compare0 ctx !(bigger a b) s t
where
bigger : forall a. a -> a -> m a
bigger l r = asks mode <&> \case Super => l; _ => r
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' _ e@(_ :# _) f _ _ = clashE e f
parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)} (ctx : TyContext q d n)
parameters (mode : EqMode)
namespace Term
export covering
compare : (ty, s, t : Term q d n) -> m ()
compare ty s t = do
defs <- ask
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
compare0 defs (map (// th) ctx.tctx)
(ty // th) (s // th) (t // th)
export covering
compareType : (s, t : Term q d n) -> m ()
compareType s t = do
defs <- ask
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
compareType defs (map (// th) ctx.tctx) (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 q d n) -> m ()
compare e f = do
defs <- ask
runReaderT {m} (MkCmpContext {mode}) $
for_ (splits ctx.dctx) $ \th =>
compare0 defs (map (// th) ctx.tctx) (e // th) (f // th)
namespace Term
export covering %inline
equal, sub, super : (ty, s, t : Term q d n) -> m ()
equal = compare Equal
sub = compare Sub
super = compare Super
export covering %inline
equalType, subtype, supertype : (s, t : Term q d n) -> m ()
equalType = compareType Equal
subtype = compareType Sub
supertype = compareType Super
namespace Elim
export covering %inline
equal, sub, super : (e, f : Elim q d n) -> m ()
equal = compare Equal
sub = compare Sub
super = compare Super