minor refactor
This commit is contained in:
parent
7f72ed56fb
commit
c9f66bb6af
|
|
@ -30,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
|
||||
|
|
@ -242,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
|
||||
|
|
@ -276,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}
|
||||
-- --------------------------------------------
|
||||
|
|
@ -302,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
|
||||
|
|
@ -327,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 ⇐ ℕ
|
||||
|
|
@ -354,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
|
||||
|
||||
|
|
@ -367,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
|
||||
-- -----------------------
|
||||
|
|
@ -445,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
|
||||
|
||||
|
|
@ -545,8 +549,8 @@ namespace Elim
|
|||
try act = lift $ catch putError $ lift act {fs' = EqualElim}
|
||||
|
||||
private %inline
|
||||
nested : Eff EqualInner a -> Eff EqualElim (Either Error a)
|
||||
nested act = lift $ runExcept act
|
||||
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) ->
|
||||
|
|
@ -618,16 +622,14 @@ namespace Elim
|
|||
-- Ψ | Γ ⊢ 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 _ _ = do
|
||||
tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one
|
||||
if isRight tyEq
|
||||
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) _ _ = do
|
||||
tyEq <- nested $ local_ Equal $ compareType defs ctx ty.zero ty.one
|
||||
if isRight tyEq
|
||||
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)
|
||||
|
||||
|
|
@ -659,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
|
||||
|
|
@ -678,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 _ _ =
|
||||
|
|
@ -688,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)
|
||||
|
|
@ -703,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
|
||||
|
|
@ -726,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
|
||||
|
|
@ -750,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
|
||||
|
|
@ -776,7 +778,7 @@ namespace Elim
|
|||
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue