|
|
|
@ -8,6 +8,7 @@ import Quox.EffExtra
|
|
|
|
|
|
|
|
|
|
import Data.List1
|
|
|
|
|
import Data.Maybe
|
|
|
|
|
import Data.Either
|
|
|
|
|
|
|
|
|
|
%default total
|
|
|
|
|
|
|
|
|
@ -29,6 +30,10 @@ 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
|
|
|
|
@ -241,7 +246,7 @@ namespace Term
|
|
|
|
|
(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 $
|
|
|
|
|
compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = withEqual $
|
|
|
|
|
-- Γ ⊢ A empty
|
|
|
|
|
-- -------------------------------------------
|
|
|
|
|
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
|
|
|
|
@ -275,7 +280,7 @@ namespace Term
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
|
|
|
|
|
compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = withEqual $
|
|
|
|
|
case (s, t) of
|
|
|
|
|
-- Γ ⊢ s₁ = t₁ ⇐ A Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
|
|
|
|
|
-- --------------------------------------------
|
|
|
|
@ -301,7 +306,7 @@ namespace Term
|
|
|
|
|
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 = local_ Equal $
|
|
|
|
|
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
|
|
|
|
@ -326,7 +331,7 @@ namespace Term
|
|
|
|
|
-- Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t
|
|
|
|
|
pure ()
|
|
|
|
|
|
|
|
|
|
compare0' defs ctx sg nat@(NAT {}) s t = local_ Equal $
|
|
|
|
|
compare0' defs ctx sg nat@(NAT {}) s t = withEqual $
|
|
|
|
|
case (s, t) of
|
|
|
|
|
-- ---------------
|
|
|
|
|
-- Γ ⊢ n = n ⇐ ℕ
|
|
|
|
@ -353,7 +358,7 @@ namespace Term
|
|
|
|
|
(E _, t) => wrongType t.loc ctx nat t
|
|
|
|
|
(s, _) => wrongType s.loc ctx nat s
|
|
|
|
|
|
|
|
|
|
compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
@ -366,7 +371,7 @@ namespace Term
|
|
|
|
|
(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 $
|
|
|
|
|
compare0' defs ctx sg bty@(BOX q ty {}) s t = withEqual $
|
|
|
|
|
case (s, t) of
|
|
|
|
|
-- Γ ⊢ s = t ⇐ A
|
|
|
|
|
-- -----------------------
|
|
|
|
@ -444,7 +449,7 @@ compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _})
|
|
|
|
|
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
|
|
|
|
|
withEqual $ do
|
|
|
|
|
Term.compare0 defs ctx SZero ty.zero sl tl
|
|
|
|
|
Term.compare0 defs ctx SZero ty.one sr tr
|
|
|
|
|
|
|
|
|
@ -527,7 +532,7 @@ namespace Elim
|
|
|
|
|
EqualElim : List (Type -> Type)
|
|
|
|
|
EqualElim = InnerErrEff :: EqualInner
|
|
|
|
|
|
|
|
|
|
private covering
|
|
|
|
|
private covering %inline
|
|
|
|
|
computeElimTypeE : (defs : Definitions) -> (ctx : EqContext n) ->
|
|
|
|
|
(sg : SQty) ->
|
|
|
|
|
(e : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) =>
|
|
|
|
@ -535,14 +540,18 @@ namespace Elim
|
|
|
|
|
computeElimTypeE defs ectx sg e = lift $
|
|
|
|
|
computeElimType defs (toWhnfContext ectx) sg e
|
|
|
|
|
|
|
|
|
|
private
|
|
|
|
|
private %inline
|
|
|
|
|
putError : Has InnerErrEff fs => Error -> Eff fs ()
|
|
|
|
|
putError err = modifyAt InnerErr (<|> Just err)
|
|
|
|
|
|
|
|
|
|
private
|
|
|
|
|
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) =>
|
|
|
|
@ -580,6 +589,50 @@ namespace Elim
|
|
|
|
|
(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
|
|
|
|
@ -608,7 +661,7 @@ namespace Elim
|
|
|
|
|
-- = 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 =
|
|
|
|
|
local_ Equal $ do
|
|
|
|
|
withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx sg e f
|
|
|
|
|
(fst, snd) <- expectSig defs ctx sg eloc ety
|
|
|
|
|
let [< x, y] = ebody.names
|
|
|
|
@ -627,7 +680,7 @@ namespace Elim
|
|
|
|
|
-- ------------------------------
|
|
|
|
|
-- Ψ | Γ ⊢ fst e = fst f ⇒ A
|
|
|
|
|
compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
|
|
|
|
|
local_ Equal $ do
|
|
|
|
|
withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx sg e f
|
|
|
|
|
fst <$> expectSig defs ctx sg eloc ety
|
|
|
|
|
compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
|
|
|
|
@ -637,7 +690,7 @@ namespace Elim
|
|
|
|
|
-- ------------------------------------
|
|
|
|
|
-- Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
|
|
|
|
|
compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
|
|
|
|
|
local_ Equal $ do
|
|
|
|
|
withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx sg e f
|
|
|
|
|
(_, tsnd) <- expectSig defs ctx sg eloc ety
|
|
|
|
|
pure $ sub1 tsnd (Fst e eloc)
|
|
|
|
@ -652,7 +705,7 @@ namespace Elim
|
|
|
|
|
-- = 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 =
|
|
|
|
|
local_ Equal $ do
|
|
|
|
|
withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx sg e f
|
|
|
|
|
try $
|
|
|
|
|
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
|
|
|
|
@ -675,7 +728,7 @@ namespace Elim
|
|
|
|
|
-- ⇒ 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 =
|
|
|
|
|
local_ Equal $ do
|
|
|
|
|
withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx sg e f
|
|
|
|
|
let [< p, ih] = esuc.names
|
|
|
|
|
try $ do
|
|
|
|
@ -699,7 +752,7 @@ namespace Elim
|
|
|
|
|
-- = 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 =
|
|
|
|
|
local_ Equal $ do
|
|
|
|
|
withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx sg e f
|
|
|
|
|
(q, ty) <- expectBOX defs ctx sg eloc ety
|
|
|
|
|
try $ do
|
|
|
|
@ -711,12 +764,6 @@ namespace Elim
|
|
|
|
|
pure $ sub1 eret e
|
|
|
|
|
compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f
|
|
|
|
|
|
|
|
|
|
-- (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
|
|
|
|
|
|
|
|
|
|
-- Ψ | Γ ⊢ s <: t : B
|
|
|
|
|
-- --------------------------------
|
|
|
|
|
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
|
|
|
|
@ -727,34 +774,11 @@ namespace Elim
|
|
|
|
|
try $ Term.compare0 defs ctx sg ty s t
|
|
|
|
|
pure ty
|
|
|
|
|
|
|
|
|
|
-- Ψ | Γ ⊢ 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
|
|
|
|
|
compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f
|
|
|
|
|
|
|
|
|
|
-- (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
|
|
|
|
|
|
|
|
|
|
-- (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
|
|
|
|
|
Yes Refl => withEqual $ do
|
|
|
|
|
ety <- compare0Inner defs ctx SZero ty1 ty2
|
|
|
|
|
u <- expectTYPE defs ctx SZero eloc ety
|
|
|
|
|
try $ do
|
|
|
|
|