quox/lib/Quox/Equal.idr

841 lines
30 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
import Quox.FreeVars
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-08-24 13:55:57 -04:00
Equal : List (Type -> Type)
Equal = [ErrorEff, DefsReader, NameGen]
2023-01-08 14:44:25 -05:00
public export
2023-08-24 13:55:57 -04:00
EqualInner : List (Type -> Type)
EqualInner = [ErrorEff, NameGen, EqModeState]
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-08-24 13:55:57 -04:00
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner a
2023-05-01 21:06:25 -04:00
clashT ty s t = throw $ ClashT loc ctx !mode ty s t
2023-01-08 14:44:25 -05:00
private %inline
2023-08-24 13:55:57 -04:00
clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a
2023-05-01 21:06:25 -04:00
clashTy s t = throw $ ClashTy loc ctx !mode s t
2023-03-26 08:38:37 -04:00
private %inline
2023-08-24 13:55:57 -04:00
wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a
2023-05-01 21:06:25 -04:00
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 (IOState {}) (IOState {}) = True
sameTyCon (IOState {}) _ = 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
2023-11-02 13:14:22 -04:00
sameTyCon (NAT {}) (NAT {}) = True
sameTyCon (NAT {}) _ = False
sameTyCon (STRING {}) (STRING {}) = True
sameTyCon (STRING {}) _ = False
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
2023-02-12 15:30:08 -05:00
||| true if a type is known to be empty.
|||
||| * a pair is empty if either element is.
||| * `{}` is empty.
||| * `[π.A]` is empty if `A` is.
||| * that's it.
public export covering
2023-10-15 10:23:38 -04:00
isEmpty : Definitions -> EqContext n -> SQty -> Term 0 n ->
Eff EqualInner Bool
isEmpty defs ctx sg ty0 = do
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
2023-09-30 12:32:26 -04:00
let Left y = choose $ isTyConE ty0
| Right n => pure False
case ty0 of
TYPE {} => pure False
IOState {} => pure False
Pi {arg, res, _} => pure False
Sig {fst, snd, _} =>
isEmpty defs ctx sg fst `orM`
isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term
Enum {cases, _} =>
pure $ null cases
Eq {} => pure False
2023-11-02 13:14:22 -04:00
NAT {} => pure False
STRING {} => pure False
BOX {ty, _} => isEmpty defs ctx sg ty
E _ => pure 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,
||| or if its domain is empty.
2023-04-15 09:13:01 -04:00
||| * 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-10-15 10:23:38 -04:00
isSubSing : Definitions -> EqContext n -> SQty -> Term 0 n ->
2023-08-24 13:55:57 -04:00
Eff EqualInner Bool
isSubSing defs ctx sg ty0 = do
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
2023-09-30 12:32:26 -04:00
let Left y = choose $ isTyConE ty0
| Right n => pure False
2023-04-15 09:13:01 -04:00
case ty0 of
2023-05-01 21:06:25 -04:00
TYPE {} => pure False
IOState {} => pure False
2023-05-01 21:06:25 -04:00
Pi {arg, res, _} =>
isEmpty defs ctx sg arg `orM`
isSubSing defs (extendTy0 res.name arg ctx) sg res.term
2023-05-01 21:06:25 -04:00
Sig {fst, snd, _} =>
isSubSing defs ctx sg fst `andM`
isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term
2023-05-01 21:06:25 -04:00
Enum {cases, _} =>
pure $ length (SortedSet.toList cases) <= 1
Eq {} => pure True
2023-11-02 13:14:22 -04:00
NAT {} => pure False
STRING {} => pure False
BOX {ty, _} => isSubSing defs ctx sg ty
2023-05-01 21:06:25 -04:00
E _ => pure False
2023-02-10 15:40:44 -05:00
2023-08-28 16:07:33 -04:00
||| 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
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-08-28 16:07:33 -04:00
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 -> SQty -> (ty, s, t : Term 0 n) ->
2023-08-28 16:07:33 -04:00
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 -> SQty -> (e, f : Elim 0 n) ->
2023-08-28 16:07:33 -04:00
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 ()
private
0 NotRedexEq : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> EqContext n -> SQty -> Pred (tm 0 n)
NotRedexEq defs ctx sg t = NotRedex defs (toWhnfContext ctx) sg t
2023-08-28 16:07:33 -04:00
namespace Term
private covering
compare0' : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) ->
(ty, s, t : Term 0 n) ->
(0 _ : NotRedexEq defs ctx SZero ty) =>
(0 _ : So (isTyConE ty)) =>
(0 _ : NotRedexEq defs ctx sg s) =>
(0 _ : NotRedexEq defs ctx sg t) =>
Eff EqualInner ()
compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t
2023-08-28 16:07:33 -04:00
compare0' defs ctx sg ty@(IOState {}) s t =
-- Γ ⊢ e = f ⇒ IOState
-- ----------------------
-- Γ ⊢ e = f ⇐ IOState
--
-- (no canonical values, ofc)
case (s, t) of
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(E _, _) => wrongType t.loc ctx ty t
_ => wrongType s.loc ctx ty s
compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
-- Γ ⊢ A empty
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
2023-10-15 10:23:38 -04:00
if !(isEmpty defs ctx sg arg) then pure () else
2023-08-28 16:07:33 -04:00
case (s, t) of
-- Γ, x : A ⊢ s = t ⇐ B
2023-08-28 16:07:33 -04:00
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
2023-08-28 16:07:33 -04:00
(Lam b1 {}, Lam b2 {}) =>
compare0 defs ctx' sg res.term b1.term b2.term
2023-08-28 16:07:33 -04:00
-- Γ, x : A ⊢ s = e x ⇐ B
2023-08-28 16:07:33 -04:00
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e ⇐ (π·x : A) → B
2023-08-28 16:07:33 -04:00
(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 sg e f
2023-08-28 16:07:33 -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-09-17 13:10:46 -04:00
where
ctx' : EqContext (S n)
ctx' = extendTy qty res.name arg ctx
toLamBody : Elim d n -> Term d (S n)
toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc
2023-08-28 16:07:33 -04:00
2023-09-17 13:10:46 -04:00
eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
eta loc e (S _ (N _)) = clashT loc ctx ty s t
eta _ e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b
2023-08-28 16:07:33 -04:00
compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
2023-08-28 16:07:33 -04:00
case (s, t) of
-- Γ ⊢ s₁ = t₁ ⇐ A Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
2023-08-28 16:07:33 -04:00
-- --------------------------------------------
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) ⇐ (x : A) × B
2023-05-01 21:06:25 -04:00
--
2023-08-28 16:07:33 -04:00
-- [todo] η for π ≥ 0 maybe
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
compare0 defs ctx sg fst sFst tFst
compare0 defs ctx sg (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
2023-08-28 16:07:33 -04:00
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
2023-08-28 16:07:33 -04:00
2023-09-18 18:41:17 -04:00
(E e, Pair fst snd _) => eta s.loc e fst snd
(Pair fst snd _, E f) => eta s.loc f fst snd
2023-08-28 16:07:33 -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-09-18 18:41:17 -04:00
where
eta : Loc -> Elim 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner ()
eta loc e s t =
case sg of
SZero => do
compare0 defs ctx sg fst (E $ Fst e e.loc) s
compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
SOne => clashT loc ctx ty s t
2023-08-28 16:07:33 -04:00
compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
2023-08-28 16:07:33 -04:00
case (s, t) of
-- --------------------
-- Γ ⊢ `t = `t ⇐ {ts}
2023-05-21 14:09:34 -04:00
--
2023-08-28 16:07:33 -04:00
-- 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 sg e f
2023-08-28 16:07:33 -04:00
(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 {}) _ _ =
2023-08-28 16:07:33 -04:00
-- ✨ uip ✨
--
-- ----------------------------
-- Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t
2023-08-28 16:07:33 -04:00
pure ()
2023-11-02 13:14:22 -04:00
compare0' defs ctx sg nat@(NAT {}) s t = local_ Equal $
2023-08-28 16:07:33 -04:00
case (s, t) of
-- ---------------
-- Γ ⊢ n = n ⇐
(Nat x {}, Nat y {}) => unless (x == y) $ clashT s.loc ctx nat s t
2023-08-28 16:07:33 -04:00
-- Γ ⊢ s = t ⇐
2023-08-28 16:07:33 -04:00
-- -------------------------
-- Γ ⊢ succ s = succ t ⇐
(Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
(Nat (S x) {}, Succ t' {}) => compare0 defs ctx sg nat (Nat x s.loc) t'
(Succ s' {}, Nat (S y) {}) => compare0 defs ctx sg nat s' (Nat y t.loc)
2023-08-28 16:07:33 -04:00
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
2023-08-28 16:07:33 -04:00
(Nat 0 {}, Succ {}) => clashT s.loc ctx nat s t
(Nat 0 {}, E _) => clashT s.loc ctx nat s t
(Succ {}, Nat 0 {}) => clashT s.loc ctx nat s t
(Succ {}, E _) => clashT s.loc ctx nat s t
(E _, Nat 0 {}) => clashT s.loc ctx nat s t
(E _, Succ {}) => clashT s.loc ctx nat s t
(Nat {}, 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-08-28 16:07:33 -04:00
compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
case (s, t) of
(Str x _, Str y _) => unless (x == y) $ clashT s.loc ctx str s t
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(Str {}, E _) => clashT s.loc ctx str s t
(E _, Str {}) => clashT s.loc ctx str s t
(Str {}, _) => wrongType t.loc ctx str t
(E _, _) => wrongType t.loc ctx str t
_ => wrongType s.loc ctx str s
compare0' defs ctx sg bty@(BOX q ty {}) s t = local_ Equal $
2023-08-28 16:07:33 -04:00
case (s, t) of
-- Γ ⊢ s = t ⇐ A
2023-08-28 16:07:33 -04:00
-- -----------------------
-- Γ ⊢ [s] = [t] ⇐ [π.A]
(Box s _, Box t _) => compare0 defs ctx sg ty s t
2023-09-17 13:10:46 -04:00
-- Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
-- -----------------------------------------------
-- Γ ⊢ [s] = e ⇐ [ρ.A]
(Box s loc, E f) => eta s f
(E e, Box t loc) => eta t e
2023-08-28 16:07:33 -04:00
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
2023-08-28 16:07:33 -04:00
2023-09-17 13:10:46 -04:00
(Box {}, _) => wrongType t.loc ctx bty t
(E _, _) => wrongType t.loc ctx bty t
_ => wrongType s.loc ctx bty s
where
eta : Term 0 n -> Elim 0 n -> Eff EqualInner ()
eta s e = do
nm <- mnb "inner" e.loc
let e = CaseBox One e (SN ty) (SY [< nm] (BVT 0 nm.loc)) e.loc
compare0 defs ctx sg ty s (E e)
2023-08-28 16:07:33 -04:00
compare0' defs ctx sg ty@(E _) s t = do
2023-08-28 16:07:33 -04:00
-- 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 sg e f
2023-08-28 16:07:33 -04:00
private covering
compareType' : (defs : Definitions) -> (ctx : EqContext n) ->
(s, t : Term 0 n) ->
(0 _ : NotRedexEq defs ctx SZero s) => (0 _ : So (isTyConE s)) =>
(0 _ : NotRedexEq defs ctx SZero t) => (0 _ : So (isTyConE t)) =>
2023-08-28 16:07:33 -04:00
(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 a@(IOState {}) (IOState {}) =
-- Γ ⊢ IOState <: IOState
pure ()
2023-08-28 16:07:33 -04:00
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
2023-09-12 00:48:51 -04:00
compareType defs (extendTy0 sRes.name sArg ctx) sRes.term tRes.term
2023-08-28 16:07:33 -04:00
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
2023-09-12 00:48:51 -04:00
compareType defs (extendTy0 sSnd.name sFst ctx) sSnd.term tSnd.term
2023-08-28 16:07:33 -04:00
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 SZero ty.zero sl tl
Term.compare0 defs ctx SZero ty.one sr tr
2023-08-28 16:07:33 -04:00
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
2023-11-02 13:14:22 -04:00
compareType' defs ctx (NAT {}) (NAT {}) =
2023-08-28 16:07:33 -04:00
-- ------------
-- Γ ⊢ <:
pure ()
compareType' defs ctx (STRING {}) (STRING {}) =
-- ------------
-- Γ ⊢ String <: String
pure ()
2023-08-28 16:07:33 -04:00
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 SZero e f
2023-08-28 16:07:33 -04:00
private
2023-09-12 00:48:51 -04:00
lookupFree : Has ErrorEff fs =>
Definitions -> EqContext n -> Name -> Universe -> Loc ->
Eff fs (Term 0 n)
2023-08-28 16:07:33 -04:00
lookupFree defs ctx x u loc =
2023-10-15 10:23:38 -04:00
case lookup x defs of
Nothing => throw $ NotInScope loc x
Just d => pure $ d.typeWithAt [|Z|] ctx.termLen u
2023-08-28 16:07:33 -04:00
export
typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
CtxExtension d n (arity k + n)
typecaseTel k xs u = case k of
KTYPE => [<]
KIOState => [<]
-- A : ★ᵤ, B : 0.A → ★ᵤ
KPi =>
let [< a, b] = xs in
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
KSig =>
let [< a, b] = xs in
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
KEnum => [<]
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
KEq =>
let [< a0, a1, a, l, r] = xs in
[< (Zero, a0, TYPE u a0.loc),
(Zero, a1, TYPE u a1.loc),
(Zero, a, Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
(Zero, l, BVT 2 l.loc),
(Zero, r, BVT 2 r.loc)]
KNat => [<]
KString => [<]
-- A : ★ᵤ
KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
2023-08-28 16:07:33 -04:00
namespace Elim
2023-09-12 00:48:51 -04:00
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) -> (ctx : EqContext n) ->
(sg : SQty) ->
(e : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) =>
2023-09-12 00:48:51 -04:00
Eff EqualElim (Term 0 n)
2023-10-15 10:23:38 -04:00
computeElimTypeE defs ectx sg e = lift $
computeElimType defs (toWhnfContext ectx) sg e
2023-09-12 00:48:51 -04:00
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) -> (ctx : EqContext n) -> (sg : SQty) ->
(e, f : Elim 0 n) -> (0 nf : NotRedexEq defs ctx sg f) =>
2023-09-12 00:48:51 -04:00
Eff EqualElim (Term 0 n)
clashE defs ctx sg e f = do
2023-09-12 00:48:51 -04:00
putError $ ClashE e.loc ctx !mode e f
computeElimTypeE defs ctx sg f
2023-09-12 00:48:51 -04:00
2023-08-28 16:07:33 -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 : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
(def : Term 0 n) ->
2023-09-12 00:48:51 -04:00
Eff EqualElim ()
2023-08-28 16:07:33 -04:00
compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
compareArm defs ctx k ret u b1 b2 def = do
let def = SN def
left = fromMaybe def b1; right = fromMaybe def b2
names = (fromMaybe def $ b1 <|> b2).names
try $ compare0 defs (extendTyN (typecaseTel k names u) ctx)
SZero (weakT (arity k) ret) left.term right.term
2023-08-28 16:07:33 -04:00
private covering
compare0Inner : Definitions -> EqContext n -> (sg : SQty) ->
(e, f : Elim 0 n) -> Eff EqualElim (Term 0 n)
2023-08-28 16:07:33 -04:00
private covering
compare0Inner' : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) ->
2023-08-28 16:07:33 -04:00
(e, f : Elim 0 n) ->
(0 ne : NotRedexEq defs ctx sg e) ->
(0 nf : NotRedexEq defs ctx sg f) ->
2023-09-12 00:48:51 -04:00
Eff EqualElim (Term 0 n)
2023-08-28 16:07:33 -04:00
compare0Inner' defs ctx sg e@(F {}) f _ _ = do
if e == f then computeElimTypeE defs ctx sg f
else clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
compare0Inner' defs ctx sg e@(B {}) f _ _ = do
if e == f then computeElimTypeE defs ctx sg f
else clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
-- Ψ | Γ ⊢ s = t ⇐ A
-- -------------------------------
-- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
compare0Inner' defs ctx sg (App e s eloc) (App f t floc) ne nf = do
ety <- compare0Inner defs ctx sg e f
(_, arg, res) <- expectPi defs ctx sg eloc ety
try $ Term.compare0 defs ctx sg arg s t
2023-09-12 00:48:51 -04:00
pure $ sub1 res $ Ann s arg s.loc
compare0Inner' defs ctx sg e'@(App {}) f' ne nf =
clashE defs ctx sg e' f'
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ 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 sg (CasePair epi e eret ebody eloc)
(CasePair fpi f fret fbody floc) ne nf =
2023-08-28 16:07:33 -04:00
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
(fst, snd) <- expectSig defs ctx sg eloc ety
2023-08-28 16:07:33 -04:00
let [< x, y] = ebody.names
2023-09-12 00:48:51 -04:00
try $ do
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
2023-08-28 16:07:33 -04:00
Term.compare0 defs
(extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) sg
2023-08-28 16:07:33 -04:00
(substCasePairRet ebody.names ety eret)
ebody.term fbody.term
2023-09-12 00:48:51 -04:00
expectEqualQ e.loc epi fpi
pure $ sub1 eret e
compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf =
clashE defs ctx sg e' f'
2023-08-28 16:07:33 -04:00
2023-09-18 15:52:51 -04:00
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
-- ------------------------------
-- Ψ | Γ ⊢ fst e = fst f ⇒ A
compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
fst <$> expectSig defs ctx sg eloc ety
compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
clashE defs ctx sg e f
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
-- ------------------------------------
-- Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
(_, tsnd) <- expectSig defs ctx sg eloc ety
pure $ sub1 tsnd (Fst e eloc)
compare0Inner' defs ctx sg e@(Snd {}) f _ _ =
clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ 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 sg (CaseEnum epi e eret earms eloc)
(CaseEnum fpi f fret farms floc) ne nf =
2023-08-28 16:07:33 -04:00
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
2023-09-12 00:48:51 -04:00
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 sg (sub1 eret t') l r
2023-09-12 00:48:51 -04:00
try $ expectEqualQ eloc epi fpi
pure $ sub1 eret e
compare0Inner' defs ctx sg e@(CaseEnum {}) f _ _ = clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ 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 sg (CaseNat epi epi' e eret ezer esuc eloc)
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
2023-08-28 16:07:33 -04:00
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
2023-09-12 00:48:51 -04:00
let [< p, ih] = esuc.names
try $ do
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
Term.compare0 defs ctx sg
2023-11-02 13:14:22 -04:00
(sub1 eret (Ann (Zero ezer.loc) (NAT ezer.loc) ezer.loc))
2023-08-28 16:07:33 -04:00
ezer fzer
Term.compare0 defs
2023-11-02 13:14:22 -04:00
(extendTyN [< (epi, p, NAT p.loc), (epi', ih, eret.term)] ctx) sg
2023-08-28 16:07:33 -04:00
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term
2023-09-12 00:48:51 -04:00
expectEqualQ e.loc epi fpi
expectEqualQ e.loc epi' fpi'
pure $ sub1 eret e
compare0Inner' defs ctx sg e@(CaseNat {}) f _ _ = clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ 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 sg (CaseBox epi e eret ebody eloc)
(CaseBox fpi f fret fbody floc) ne nf =
2023-08-28 16:07:33 -04:00
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
(q, ty) <- expectBOX defs ctx sg eloc ety
2023-09-12 00:48:51 -04:00
try $ do
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) sg
2023-08-28 16:07:33 -04:00
(substCaseBoxRet ebody.name ety eret)
ebody.term fbody.term
2023-09-12 00:48:51 -04:00
expectEqualQ eloc epi fpi
pure $ sub1 eret e
compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
2023-09-12 00:48:51 -04:00
-- (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
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ s <: t : B
-- --------------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
--
-- and similar for :> and A
compare0Inner' defs ctx sg (Ann s a _) (Ann t b _) _ _ = do
2023-08-28 16:07:33 -04:00
ty <- bigger a b
try $ Term.compare0 defs ctx sg ty s t
2023-09-12 00:48:51 -04:00
pure ty
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ Ap₁/𝑖 <: Bp₂/𝑖
-- Ψ | Γ ⊢ Aq₁/𝑖 <: Bq₂/𝑖
-- Ψ | Γ ⊢ s <: t ⇐ Bp₂/𝑖
-- -----------------------------------------------------------
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ Bq₂/𝑖
compare0Inner' defs ctx sg (Coe ty1 p1 q1 val1 _)
(Coe ty2 p2 q2 val2 _) ne nf = do
2023-08-28 16:07:33 -04:00
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)
2023-09-12 00:48:51 -04:00
try $ do
compareType defs ctx ty1p ty2p
compareType defs ctx ty1q ty2q
Term.compare0 defs ctx sg ty_p val1 val2
2023-09-12 00:48:51 -04:00
pure $ ty_q
compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
-- (no neutral compositions in a closed dctx)
compare0Inner' _ _ _ (Comp {r = K {}, _}) _ ne _ = void $ absurd $ noOr2 ne
compare0Inner' _ _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
compare0Inner' _ _ _ _ (Comp {r = K {}, _}) _ nf = void $ absurd $ noOr2 nf
2023-08-28 16:07:33 -04:00
-- (type case equality purely structural)
compare0Inner' defs ctx sg (TypeCase ty1 ret1 arms1 def1 eloc)
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
case sg `decEq` SZero of
Yes Refl => local_ Equal $ do
ety <- compare0Inner defs ctx SZero ty1 ty2
u <- expectTYPE defs ctx SZero 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
No _ => do
putError $ ClashQ eloc sg.qty Zero
computeElimTypeE defs ctx sg $ TypeCase ty1 ret1 arms1 def1 eloc
compare0Inner' defs ctx sg e@(TypeCase {}) f _ _ = clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
-- Ψ | Γ ⊢ s <: f ⇐ A
-- --------------------------
-- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
--
-- and vice versa
compare0Inner' defs ctx sg (Ann s a _) f _ _ = do
try $ Term.compare0 defs ctx sg a s (E f)
2023-09-12 00:48:51 -04:00
pure a
compare0Inner' defs ctx sg e (Ann t b _) _ _ = do
try $ Term.compare0 defs ctx sg b (E e) t
2023-09-12 00:48:51 -04:00
pure b
compare0Inner' defs ctx sg e@(Ann {}) f _ _ =
clashE defs ctx sg e f
2023-08-28 16:07:33 -04:00
compare0Inner defs ctx sg e f = do
Element e ne <- whnf defs ctx sg e.loc e
Element f nf <- whnf defs ctx sg f.loc f
ty <- compare0Inner' defs ctx sg e f ne nf
if !(lift $ isSubSing defs ctx sg ty) && isJust !(getAt InnerErr)
2023-09-12 00:48:51 -04:00
then putAt InnerErr Nothing
else modifyAt InnerErr $ map $ WhileComparingE ctx !mode sg e f
2023-09-12 00:48:51 -04:00
pure ty
2023-08-28 16:07:33 -04:00
namespace Term
compare0 defs ctx sg ty s t =
wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
Element ty' _ <- whnf defs ctx SZero ty.loc ty
Element s' _ <- whnf defs ctx sg s.loc s
Element t' _ <- whnf defs ctx sg t.loc t
2023-08-28 16:07:33 -04:00
tty <- ensureTyCon ty.loc ctx ty'
compare0' defs ctx sg ty' s' t'
2023-08-28 16:07:33 -04:00
namespace Elim
compare0 defs ctx sg e f = do
(ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f
2023-08-28 16:07:33 -04:00
maybe (pure ty) throw err
compareType defs ctx s t = do
Element s' _ <- whnf defs ctx SZero s.loc s
Element t' _ <- whnf defs ctx SZero t.loc t
2023-08-28 16:07:33 -04:00
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'
2023-04-15 09:13:01 -04:00
2023-05-01 21:06:25 -04:00
parameters (loc : Loc) (ctx : TyContext d n)
2023-02-10 15:40:44 -05:00
parameters (mode : EqMode)
2023-05-01 21:06:25 -04:00
private
2023-08-24 13:55:57 -04:00
fromInner : Eff EqualInner a -> Eff Equal a
2023-08-25 12:09:06 -04:00
fromInner = lift . map fst . runState mode
2023-05-01 21:06:25 -04:00
private
eachFace : Applicative f => FreeVars d ->
(EqContext n -> DSubst d 0 -> f ()) -> f ()
eachFace fvs act =
for_ (splits loc ctx.dctx fvs) $ \th =>
act (makeEqContext ctx th) th
2023-05-01 21:06:25 -04:00
private
2023-08-24 13:55:57 -04:00
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
2023-10-15 10:23:38 -04:00
fdvAll = let Val d = ctx.dimLen in foldMap (fdvWith [|d|] ctx.termLen)
2023-05-01 21:06:25 -04:00
namespace Term
2023-02-10 15:40:44 -05:00
export covering
compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
compare0 defs ectx sg (ty // th) (s // th) (t // th)
2023-02-10 15:40:44 -05:00
export covering
2023-08-24 13:55:57 -04:00
compareType : (s, t : Term d n) -> Eff Equal ()
compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th =>
2023-05-01 21:06:25 -04:00
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 : SQty -> (e, f : Elim d n) -> Eff Equal ()
compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
ignore $ compare0 defs ectx sg (e // th) (f // th)
namespace Term
export covering %inline
equal, sub, super : SQty -> (ty, s, t : Term d n) -> Eff 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-08-24 13:55:57 -04:00
equalType, subtype, supertype : (s, t : Term d n) -> Eff 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
equal, sub, super : SQty -> (e, f : Elim d n) -> Eff 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