rename EqualE to just Equal & add runEqual
This commit is contained in:
parent
38dbd275a1
commit
e1dbf272df
1 changed files with 21 additions and 17 deletions
|
|
@ -17,8 +17,12 @@ public export
|
|||
EqualEff = [ErrorEff, EqModeState]
|
||||
|
||||
public export
|
||||
0 EqualE : Type -> Type
|
||||
EqualE = Eff $ EqualEff
|
||||
0 Equal : Type -> Type
|
||||
Equal = Eff $ EqualEff
|
||||
|
||||
export
|
||||
runEqual : EqMode -> Equal a -> Either Error a
|
||||
runEqual mode = extract . runExcept . evalState mode
|
||||
|
||||
|
||||
export %inline
|
||||
|
|
@ -28,19 +32,19 @@ mode = get
|
|||
|
||||
parameters (ctx : EqContext n)
|
||||
private %inline
|
||||
clashT : Term 0 n -> Term 0 n -> Term 0 n -> EqualE a
|
||||
clashT : Term 0 n -> Term 0 n -> Term 0 n -> Equal a
|
||||
clashT ty s t = throw $ ClashT ctx !mode ty s t
|
||||
|
||||
private %inline
|
||||
clashTy : Term 0 n -> Term 0 n -> EqualE a
|
||||
clashTy : Term 0 n -> Term 0 n -> Equal a
|
||||
clashTy s t = throw $ ClashTy ctx !mode s t
|
||||
|
||||
private %inline
|
||||
clashE : Elim 0 n -> Elim 0 n -> EqualE a
|
||||
clashE : Elim 0 n -> Elim 0 n -> Equal a
|
||||
clashE e f = throw $ ClashE ctx !mode e f
|
||||
|
||||
private %inline
|
||||
wrongType : Term 0 n -> Term 0 n -> EqualE a
|
||||
wrongType : Term 0 n -> Term 0 n -> Equal a
|
||||
wrongType ty s = throw $ WrongType ctx ty s
|
||||
|
||||
|
||||
|
|
@ -141,7 +145,7 @@ parameters (defs : Definitions)
|
|||
|||
|
||||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
|
||||
export covering %inline
|
||||
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> EqualE ()
|
||||
compare0 : EqContext n -> (ty, s, t : Term 0 n) -> Equal ()
|
||||
compare0 ctx ty s t =
|
||||
wrapErr (WhileComparingT ctx !mode ty s t) $ do
|
||||
let Val n = ctx.termLen
|
||||
|
|
@ -162,7 +166,7 @@ parameters (defs : Definitions)
|
|||
(ty, s, t : Term 0 n) ->
|
||||
(0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
|
||||
(0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) =>
|
||||
EqualE ()
|
||||
Equal ()
|
||||
compare0' ctx (TYPE _) s t = compareType ctx s t
|
||||
|
||||
compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local_ Equal $
|
||||
|
|
@ -187,7 +191,7 @@ parameters (defs : Definitions)
|
|||
ctx' : EqContext (S n)
|
||||
ctx' = extendTy qty res.name arg ctx
|
||||
|
||||
eta : Elim 0 n -> ScopeTerm 0 n -> EqualE ()
|
||||
eta : Elim 0 n -> ScopeTerm 0 n -> Equal ()
|
||||
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
|
||||
eta e (S _ (N _)) = clashT ctx ty s t
|
||||
|
||||
|
|
@ -281,7 +285,7 @@ parameters (defs : Definitions)
|
|||
||| 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 : EqContext n -> (s, t : Term 0 n) -> EqualE ()
|
||||
compareType : EqContext n -> (s, t : Term 0 n) -> Equal ()
|
||||
compareType ctx s t = do
|
||||
let Val n = ctx.termLen
|
||||
Element s ns <- whnfT defs s
|
||||
|
|
@ -297,7 +301,7 @@ parameters (defs : Definitions)
|
|||
(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)) =>
|
||||
EqualE ()
|
||||
Equal ()
|
||||
-- equality is the same as subtyping, except with the
|
||||
-- "≤" in the TYPE rule being replaced with "="
|
||||
compareType' ctx (TYPE k) (TYPE l) =
|
||||
|
|
@ -363,7 +367,7 @@ parameters (defs : Definitions)
|
|||
private covering
|
||||
computeElimType : EqContext n -> (e : Elim 0 n) ->
|
||||
(0 ne : NotRedex defs e) ->
|
||||
EqualE (Term 0 n)
|
||||
Equal (Term 0 n)
|
||||
computeElimType ctx (F x) _ = do
|
||||
defs <- lookupFree' defs x
|
||||
pure $ injectT ctx defs.type
|
||||
|
|
@ -383,7 +387,7 @@ parameters (defs : Definitions)
|
|||
private covering
|
||||
replaceEnd : EqContext n ->
|
||||
(e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
|
||||
EqualE (Elim 0 n)
|
||||
Equal (Elim 0 n)
|
||||
replaceEnd ctx e p ne = do
|
||||
(ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne)
|
||||
pure $ ends l r p :# dsub1 ty (K p)
|
||||
|
|
@ -397,7 +401,7 @@ parameters (defs : Definitions)
|
|||
||| ⚠ **assumes that they have both been typechecked, and have
|
||||
||| equal types.** ⚠
|
||||
export covering %inline
|
||||
compare0 : EqContext n -> (e, f : Elim 0 n) -> EqualE ()
|
||||
compare0 : EqContext n -> (e, f : Elim 0 n) -> Equal ()
|
||||
compare0 ctx e f =
|
||||
wrapErr (WhileComparingE ctx !mode e f) $ do
|
||||
let Val n = ctx.termLen
|
||||
|
|
@ -411,7 +415,7 @@ parameters (defs : Definitions)
|
|||
compare0' : EqContext n ->
|
||||
(e, f : Elim 0 n) ->
|
||||
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
|
||||
EqualE ()
|
||||
Equal ()
|
||||
-- replace applied equalities with the appropriate end first
|
||||
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
|
||||
--
|
||||
|
|
@ -459,7 +463,7 @@ parameters (defs : Definitions)
|
|||
!(lookupArm t earms) !(lookupArm t farms)
|
||||
expectEqualQ epi fpi
|
||||
where
|
||||
lookupArm : TagVal -> CaseEnumArms d n -> EqualE (Term d n)
|
||||
lookupArm : TagVal -> CaseEnumArms d n -> Equal (Term d n)
|
||||
lookupArm t arms = case lookup t arms of
|
||||
Just arm => pure arm
|
||||
Nothing => throw $ TagNotIn t (fromList $ keys arms)
|
||||
|
|
@ -496,7 +500,7 @@ parameters (defs : Definitions)
|
|||
compare0' ctx (s :# a) (t :# b) _ _ =
|
||||
Term.compare0 ctx !(bigger a b) s t
|
||||
where
|
||||
bigger : forall a. a -> a -> EqualE a
|
||||
bigger : forall a. a -> a -> Equal a
|
||||
bigger l r = mode <&> \case Super => l; _ => r
|
||||
|
||||
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
|
||||
|
|
|
|||
Loading…
Reference in a new issue