module Quox.Equal import Quox.BoolExtra import public Quox.Typing import Quox.FreeVars import Quox.Pretty import Quox.EffExtra import Data.List1 import Data.Maybe import Data.Either %default total public export EqModeState : Type -> Type EqModeState = State EqMode public export Equal : List (Type -> Type) Equal = [ErrorEff, DefsReader, NameGen, Log] public export EqualInner : List (Type -> Type) EqualInner = [ErrorEff, NameGen, EqModeState, Log] export %inline mode : Has EqModeState fs => Eff fs EqMode mode = get private %inline withEqual : Has EqModeState fs => Eff fs a -> Eff fs a withEqual = local_ Equal parameters (loc : Loc) (ctx : EqContext n) private %inline clashT : Term 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner a clashT ty s t = throw $ ClashT loc ctx !mode ty s t private %inline clashTy : Term 0 n -> Term 0 n -> Eff EqualInner a clashTy s t = throw $ ClashTy loc ctx !mode s t private %inline wrongType : Term 0 n -> Term 0 n -> Eff EqualInner a wrongType ty s = throw $ WrongType loc ctx ty s public export %inline sameTyCon : (s, t : Term d n) -> (0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) => Bool sameTyCon (TYPE {}) (TYPE {}) = True sameTyCon (TYPE {}) _ = False sameTyCon (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 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 ||| 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 isEmpty : {default 30 logLevel : Nat} -> (0 _ : So (isLogLevel logLevel)) => Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool private covering isEmptyNoLog : Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool isEmpty defs ctx sg ty = do sayMany "equal" ty.loc [logLevel :> "isEmpty", 95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx], 95 :> hsep ["sg =", runPretty $ prettyQty sg.qty], logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]] res <- isEmptyNoLog defs ctx sg ty say "equal" logLevel ty.loc $ hsep ["isEmpty ⇝", pshow res] pure res isEmptyNoLog defs ctx sg ty0 = do Element ty0 nc <- whnf defs ctx sg ty0.loc ty0 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 {logLevel = 90} `orM` isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term {logLevel = 90} Enum {cases, _} => pure $ null cases Eq {} => pure False NAT {} => pure False STRING {} => pure False BOX {ty, _} => isEmpty defs ctx sg ty {logLevel = 90} E _ => pure 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, ||| or if its domain is empty. ||| * 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 : {default 30 logLevel : Nat} -> (0 _ : So (isLogLevel logLevel)) => Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool private covering isSubSingNoLog : Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool isSubSing defs ctx sg ty = do sayMany "equal" ty.loc [logLevel :> "isSubSing", 95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx], 95 :> hsep ["sg =", runPretty $ prettyQty sg.qty], logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]] res <- isSubSingNoLog defs ctx sg ty say "equal" logLevel ty.loc $ hsep ["isSubsing ⇝", pshow res] pure res isSubSingNoLog defs ctx sg ty0 = do Element ty0 nc <- whnf defs ctx sg ty0.loc ty0 let Left y = choose $ isTyConE ty0 | _ => pure False case ty0 of TYPE {} => pure False IOState {} => pure False Pi {arg, res, _} => isEmpty defs ctx sg arg {logLevel = 90} `orM` isSubSing defs (extendTy0 res.name arg ctx) sg res.term {logLevel = 90} Sig {fst, snd, _} => isSubSing defs ctx sg fst {logLevel = 90} `andM` isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term {logLevel = 90} Enum {cases, _} => pure $ length (SortedSet.toList cases) <= 1 Eq {} => pure True NAT {} => pure False STRING {} => pure False BOX {ty, _} => isSubSing defs ctx sg ty {logLevel = 90} E _ => pure False ||| 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 export ensureTyCon, ensureTyConNoLog : (Has Log fs, Has ErrorEff fs) => (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) -> Eff fs (So (isTyConE t)) ensureTyConNoLog loc ctx ty = do case nchoose $ isTyConE ty of Left y => pure y Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen) ensureTyCon loc ctx ty = do sayMany "equal" ty.loc [60 :> "ensureTyCon", 95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx], 60 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]] ensureTyConNoLog loc ctx ty 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) -> 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) -> 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 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 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 = withEqual $ -- Γ ⊢ A empty -- ------------------------------------------- -- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ π.(x : A) → B if !(isEmpty defs ctx sg arg) then pure () else case (s, t) of -- Γ, x : A ⊢ s = t ⇐ B -- ------------------------------------------- -- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ π.(x : A) → B (Lam b1 {}, Lam b2 {}) => compare0 defs ctx' sg res.term b1.term b2.term -- Γ, x : A ⊢ s = e x ⇐ B -- ----------------------------------- -- Γ ⊢ (λ x ⇒ s) = e ⇐ π.(x : A) → B (E e, Lam b {}) => eta s.loc e b (Lam b {}, E e) => eta s.loc e b (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f (Lam {}, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t (s, _) => wrongType s.loc ctx ty s where ctx' : EqContext (S n) ctx' = extendTy qty res.name arg ctx toLamBody : Elim d n -> Term d (S n) toLamBody e = E $ App (weakE 1 e) (BVT 0 e.loc) e.loc eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner () eta loc e (S _ (N b)) = if !(pure (qty /= One) `andM` isSubSing defs ctx sg arg) then compare0 defs ctx' sg res.term (toLamBody e) (weakT 1 b) else clashT loc ctx ty s t eta _ e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = withEqual $ case (s, t) of -- Γ ⊢ s₁ = t₁ ⇐ A Γ ⊢ s₂ = t₂ ⇐ B{s₁/x} -- -------------------------------------------- -- Γ ⊢ (s₁, t₁) = (s₂,t₂) ⇐ (x : A) × B (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 (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f (E e, Pair fst snd _) => eta s.loc e fst snd (Pair fst snd _, E f) => eta s.loc f fst snd (Pair {}, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t (s, _) => wrongType s.loc ctx ty s 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 compare0' defs ctx sg ty@(Enum cases _) s t = withEqual $ -- η for empty & singleton enums if length (SortedSet.toList cases) <= 1 then pure () else case (s, t) of -- -------------------- -- Γ ⊢ 't = 't ⇐ {ts} -- -- t ∈ ts is in the typechecker, not here, ofc (Tag t1 {}, Tag t2 {}) => unless (t1 == t2) $ clashT s.loc ctx ty s t (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f (Tag {}, E _) => clashT s.loc ctx ty s t (E _, Tag {}) => clashT s.loc ctx ty s t (Tag {}, t) => wrongType t.loc ctx ty t (E _, t) => wrongType t.loc ctx ty t (s, _) => wrongType s.loc ctx ty s compare0' _ _ _ (Eq {}) _ _ = -- ✨ uip ✨ -- -- ---------------------------- -- Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t pure () compare0' defs ctx sg nat@(NAT {}) s t = withEqual $ case (s, t) of -- --------------- -- Γ ⊢ n = n ⇐ ℕ (Nat x {}, Nat y {}) => unless (x == y) $ clashT s.loc ctx nat s t -- Γ ⊢ s = t ⇐ ℕ -- ------------------------- -- Γ ⊢ 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) (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f (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 compare0' defs ctx sg str@(STRING {}) s t = withEqual $ 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 = withEqual $ case (s, t) of -- Γ ⊢ s = t ⇐ A -- ----------------------- -- Γ ⊢ [s] = [t] ⇐ [π.A] (Box s _, Box t _) => compare0 defs ctx sg ty s t -- Γ ⊢ σ⨴ρ · 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 (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f (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 `subjMult` q) ty s (E e) compare0' defs ctx sg ty@(E _) s t = do -- a neutral type can only be inhabited by neutral values -- e.g. an abstract value in an abstract type, bound variables, … let E e = s | _ => wrongType s.loc ctx ty s E f = t | _ => wrongType t.loc ctx ty t ignore $ Elim.compare0 defs ctx sg e f 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)) => (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 () 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 compareType defs (extendTy0 sRes.name sArg ctx) sRes.term tRes.term 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 compareType defs (extendTy0 sSnd.name sFst ctx) sSnd.term tSnd.term 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 withEqual $ do Term.compare0 defs ctx SZero ty.zero sl tl Term.compare0 defs ctx SZero ty.one sr tr 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 compareType' defs ctx (NAT {}) (NAT {}) = -- ------------ -- Γ ⊢ ℕ <: ℕ pure () compareType' defs ctx (STRING {}) (STRING {}) = -- ------------ -- Γ ⊢ String <: String pure () 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 private lookupFree : Has ErrorEff fs => Definitions -> EqContext n -> Name -> Universe -> Loc -> Eff fs (Term 0 n) lookupFree defs ctx x u loc = case lookup x defs of Nothing => throw $ NotInScope loc x Just d => pure $ d.typeWithAt [|Z|] ctx.termLen u 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)] namespace Elim private data InnerErr : Type where private InnerErrEff : Type -> Type InnerErrEff = StateL InnerErr (Maybe Error) private EqualElim : List (Type -> Type) EqualElim = InnerErrEff :: EqualInner private covering %inline computeElimTypeE : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) -> (e : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) => Eff EqualElim (Term 0 n) computeElimTypeE defs ectx sg e = lift $ computeElimType defs (toWhnfContext ectx) sg e private %inline putError : Has InnerErrEff fs => Error -> Eff fs () putError err = modifyAt InnerErr (<|> Just err) private %inline try : Eff EqualInner () -> Eff EqualElim () try act = lift $ catch putError $ lift act {fs' = EqualElim} private %inline succeeds : Eff EqualInner a -> Eff EqualElim Bool succeeds act = lift $ map isRight $ runExcept act private covering %inline clashE : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) -> (e, f : Elim 0 n) -> (0 nf : NotRedexEq defs ctx sg f) => Eff EqualElim (Term 0 n) clashE defs ctx sg e f = do putError $ ClashE e.loc ctx !mode e f computeElimTypeE defs ctx sg 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 : Definitions -> EqContext n -> (k : TyConKind) -> (ret : Term 0 n) -> (u : Universe) -> (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) -> (def : Term 0 n) -> Eff EqualElim () 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 private covering compare0Inner : Definitions -> EqContext n -> (sg : SQty) -> (e, f : Elim 0 n) -> Eff EqualElim (Term 0 n) private covering compare0Inner' : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) -> (e, f : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) -> (0 nf : NotRedexEq defs ctx sg f) -> Eff EqualElim (Term 0 n) -- (no neutral dim apps or comps in a closed dctx) compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf 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 -- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖› -- Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖› -- Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖› -- ----------------------------------------------------------- -- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s -- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖› compare0Inner' defs ctx sg (Coe ty1 p1 q1 val1 _) (Coe ty2 p2 q2 val2 _) ne nf = do let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2 ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2 (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q) try $ do compareType defs ctx ty1p ty2p compareType defs ctx ty1q ty2q Term.compare0 defs ctx sg ty_p val1 val2 pure $ ty_q -- an adaptation of the rule -- -- Ψ | Γ ⊢ A‹0/𝑖› = A‹1/𝑖› ⇐ ★ -- ----------------------------------------------------- -- Ψ | Γ ⊢ coe (𝑖 ⇒ A) @p @q s ⇝ (s ∷ A‹1/𝑖›) ⇒ A‹1/𝑖› -- -- it's here so that whnf doesn't have to depend on the equality checker compare0Inner' defs ctx sg (Coe ty p q val loc) f _ _ = if !(succeeds $ withEqual $ compareType defs ctx ty.zero ty.one) then compare0Inner defs ctx sg (Ann val (dsub1 ty q) loc) f else clashE defs ctx sg (Coe ty p q val loc) f -- symmetric version of the above compare0Inner' defs ctx sg e (Coe ty p q val loc) _ _ = if !(succeeds $ withEqual $ compareType defs ctx ty.zero ty.one) then compare0Inner defs ctx sg e (Ann val (dsub1 ty q) loc) else clashE defs ctx sg e (Coe ty p q val loc) compare0Inner' defs ctx sg e@(F {}) f _ _ = do if e == f then computeElimTypeE defs ctx sg f else clashE defs ctx sg e f compare0Inner' defs ctx sg e@(B {}) f _ _ = do if e == f then computeElimTypeE defs ctx sg f else clashE defs ctx sg e f -- Ψ | Γ ⊢ 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 pure $ sub1 res $ Ann s arg s.loc compare0Inner' defs ctx sg e'@(App {}) f' ne nf = clashE defs ctx sg 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] compare0Inner' defs ctx sg (CasePair epi e eret ebody eloc) (CasePair fpi f fret fbody floc) ne nf = withEqual $ do ety <- compare0Inner defs ctx sg e f (fst, snd) <- expectSig defs ctx sg eloc ety let [< x, y] = ebody.names try $ do compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) sg (substCasePairRet ebody.names ety eret) ebody.term fbody.term expectEqualQ e.loc epi fpi pure $ sub1 eret e compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf = clashE defs ctx sg e' f' -- Ψ | Γ ⊢ e = f ⇒ (x : A) × B -- ------------------------------ -- Ψ | Γ ⊢ fst e = fst f ⇒ A compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf = withEqual $ 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 = withEqual $ 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 -- Ψ | Γ ⊢ 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 = withEqual $ do ety <- compare0Inner defs ctx sg e f 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 try $ expectEqualQ eloc epi fpi pure $ sub1 eret e compare0Inner' defs ctx sg e@(CaseEnum {}) f _ _ = clashE defs ctx sg 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] compare0Inner' defs ctx sg (CaseNat epi epi' e eret ezer esuc eloc) (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf = withEqual $ do ety <- compare0Inner defs ctx sg e f let [< p, ih] = esuc.names try $ do compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs ctx sg (sub1 eret (Ann (Zero ezer.loc) (NAT ezer.loc) ezer.loc)) ezer fzer Term.compare0 defs (extendTyN [< (epi, p, NAT p.loc), (epi', ih, eret.term)] ctx) sg (substCaseSuccRet esuc.names eret) esuc.term fsuc.term 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 -- Ψ | Γ ⊢ 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 = withEqual $ do ety <- compare0Inner defs ctx sg e f (q, ty) <- expectBOX defs ctx sg eloc ety try $ do compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) sg (substCaseBoxRet ebody.name ety eret) ebody.term fbody.term expectEqualQ eloc epi fpi pure $ sub1 eret e compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f -- Ψ | Γ ⊢ s <: t : B -- -------------------------------- -- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B -- -- and similar for :> and A compare0Inner' defs ctx sg (Ann s a _) (Ann t b _) _ _ = do ty <- bigger a b try $ Term.compare0 defs ctx sg ty s t pure ty -- (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 => withEqual $ 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 -- Ψ | Γ ⊢ 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) pure a compare0Inner' defs ctx sg e (Ann t b _) _ _ = do try $ Term.compare0 defs ctx sg b (E e) t pure b compare0Inner' defs ctx sg e@(Ann {}) f _ _ = clashE defs ctx sg e f 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) then putAt InnerErr Nothing else modifyAt InnerErr $ map $ WhileComparingE ctx !mode sg e f pure ty namespace Term export covering %inline compare0NoLog : Definitions -> EqContext n -> SQty -> (ty, s, t : Term 0 n) -> Eff EqualInner () compare0NoLog 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 tty <- ensureTyCon ty.loc ctx ty' compare0' defs ctx sg ty' s' t' compare0 defs ctx sg ty s t = do sayMany "equal" s.loc [30 :> "Term.compare0", 30 :> hsep ["mode =", pshow !mode], 95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx], 95 :> hsep ["sg =", runPretty $ prettyQty sg.qty], 31 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty], 30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s], 30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]] compare0NoLog defs ctx sg ty s t namespace Elim export covering %inline compare0NoLog : Definitions -> EqContext n -> SQty -> (e, f : Elim 0 n) -> Eff EqualInner (Term 0 n) compare0NoLog defs ctx sg e f = do (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f maybe (pure ty) throw err compare0 defs ctx sg e f = do sayMany "equal" e.loc [30 :> "Elim.compare0", 30 :> hsep ["mode =", pshow !mode], 95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx], 95 :> hsep ["sg =", runPretty $ prettyQty sg.qty], 30 :> hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e], 30 :> hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]] ty <- compare0NoLog defs ctx sg e f say "equal" 31 e.loc $ hsep ["Elim.compare0 ⇝", runPretty $ prettyTerm [<] ctx.tnames ty] pure ty export covering %inline compareTypeNoLog : Definitions -> EqContext n -> (s, t : Term 0 n) -> Eff EqualInner () compareTypeNoLog defs ctx s t = do Element s' _ <- whnf defs ctx SZero s.loc s Element t' _ <- whnf defs ctx SZero t.loc t ts <- ensureTyCon s.loc ctx s' tt <- ensureTyCon t.loc ctx t' let Left _ = choose $ sameTyCon s' t' | _ => clashTy s.loc ctx s' t' compareType' defs ctx s' t' compareType defs ctx s t = do sayMany "equal" s.loc [30 :> "compareType", 30 :> hsep ["mode =", pshow !mode], 95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx], 30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s], 30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]] compareTypeNoLog defs ctx s t private getVars : TyContext d _ -> FreeVars d -> List BindName getVars ctx (FV fvs) = case ctx.dctx of ZeroIsOne => [] C eqs => toList $ getVars' ctx.dnames eqs fvs where getVars' : BContext d' -> DimEq' d' -> FreeVars' d' -> SnocList BindName getVars' (names :< name) (eqs :< eq) (fvs :< fv) = let rest = getVars' names eqs fvs in case eq of Nothing => rest :< name Just _ => rest getVars' [<] [<] [<] = [<] parameters (loc : Loc) (ctx : TyContext d n) parameters (mode : EqMode) private fromInner : Eff EqualInner a -> Eff Equal a fromInner = lift . map fst . runState mode private eachCorner : Has Log fs => Loc -> FreeVars d -> (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs () eachCorner loc fvs act = do say "equal" 50 loc $ let vars = map prettyBind' (getVars ctx fvs) in hsep $ "eachCorner: split on" :: if null vars then ["(none)"] else vars for_ (splits loc ctx.dctx fvs) $ \th => act (makeEqContext ctx th) th private CompareAction : Nat -> Nat -> Type CompareAction d n = Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner () private runCompare : Loc -> FreeVars d -> CompareAction d n -> Eff Equal () runCompare loc fvs act = fromInner $ eachCorner loc fvs $ act !(askAt DEFS) private foldMap1 : Semigroup b => (a -> b) -> List1 a -> b foldMap1 f = foldl1By (\x, y => x <+> f y) f private fdvAll : HasFreeDVars t => (xs : List (t d n)) -> (0 _ : NonEmpty xs) => FreeVars d fdvAll (x :: xs) = foldMap1 (fdvWith ctx.dimLen ctx.termLen) (x ::: xs) namespace Term export covering compare : SQty -> (ty, s, t : Term d n) -> Eff Equal () compare sg ty s t = runCompare s.loc (fdvAll [ty, s, t]) $ \defs, ectx, th => compare0 defs ectx sg (ty // th) (s // th) (t // th) export covering compareType : (s, t : Term d n) -> Eff Equal () compareType s t = runCompare s.loc (fdvAll [s, t]) $ \defs, ectx, th => compareType defs ectx (s // th) (t // th) namespace Elim ||| you don't have to pass the type in but the arguments must still be ||| of the same type!! export covering compare : SQty -> (e, f : Elim d n) -> Eff Equal () compare sg e f = runCompare e.loc (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 () equal = compare Equal sub = compare Sub super = compare Super export covering %inline equalType, subtype, supertype : (s, t : Term d n) -> Eff Equal () equalType = compareType Equal subtype = compareType Sub supertype = compareType Super namespace Elim export covering %inline equal, sub, super : SQty -> (e, f : Elim d n) -> Eff Equal () equal = compare Equal sub = compare Sub super = compare Super