rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

Whnf ⇒ CanWhnf; WhnfM ⇒ Eff Whnf

Browse source
This commit is contained in:
rhiannon morris 2023-05-21 20:11:01 +02:00
parent 2af8ee20ea
commit 282565c7a3
2 changed files with 30 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
lib/Quox/Reduce.idr
View file

@ -16,15 +16,15 @@ import Control.Eff
-- [fixme] rename this to Whnf and the interface to CanWhnf -- [fixme] rename this to Whnf and the interface to CanWhnf
public export public export
WhnfM : Type -> Type Whnf : List (Type -> Type)
WhnfM = Eff [NameGen, Except Error] Whnf = [NameGen, Except Error]
export export
runWhnfWith : NameSuf -> WhnfM a -> (Either Error a, NameSuf) runWhnfWith : NameSuf -> Eff Whnf a -> (Either Error a, NameSuf)
runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act
export export
runWhnf : WhnfM a -> Either Error a runWhnf : Eff Whnf a -> Either Error a
runWhnf = fst . runWhnfWith 0 runWhnf = fst . runWhnfWith 0
@ -33,30 +33,30 @@ public export
RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
public export public export
interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where where
whnf : {d, n : Nat} -> (defs : Definitions) -> whnf : {d, n : Nat} -> (defs : Definitions) ->
(ctx : WhnfContext d n) -> (ctx : WhnfContext d n) ->
tm d n -> WhnfM (Subset (tm d n) (No . isRedex defs)) tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
public export %inline public export %inline
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex => whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
(defs : Definitions) -> WhnfContext d n -> tm d n -> WhnfM (tm d n) (defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n)
whnf0 defs ctx t = fst <$> whnf defs ctx t whnf0 defs ctx t = fst <$> whnf defs ctx t
public export public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex => 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> Pred (tm d n) Definitions -> Pred (tm d n)
IsRedex defs = So . isRedex defs IsRedex defs = So . isRedex defs
NotRedex defs = No . isRedex defs NotRedex defs = No . isRedex defs
public export public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} -> 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
Whnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type CanWhnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
NonRedex tm d n defs = Subset (tm d n) (NotRedex defs) NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
public export %inline public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) => nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
nred t = Element t nr nred t = Element t nr
@ -226,10 +226,10 @@ coeScoped ty p q loc (S names (N body)) =
export covering export covering
Whnf Term Reduce.isRedexT CanWhnf Term Reduce.isRedexT
export covering export covering
Whnf Elim Reduce.isRedexE CanWhnf Elim Reduce.isRedexE
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
||| performs the minimum work required to recompute the type of an elim. ||| performs the minimum work required to recompute the type of an elim.
@ -237,7 +237,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
||| ⚠ **assumes the elim is already typechecked.** ⚠ ||| ⚠ **assumes the elim is already typechecked.** ⚠
export covering export covering
computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) => computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
WhnfM (Term d n) Eff Whnf (Term d n)
computeElimType (F {x, u, loc}) = do computeElimType (F {x, u, loc}) = do
let Just def = lookup x defs | Nothing => throw $ NotInScope loc x let Just def = lookup x defs | Nothing => throw $ NotInScope loc x
pure $ displace u def.type pure $ displace u def.type
@ -265,7 +265,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
WhnfM (Term (S d) n, ScopeTerm (S d) n) Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
tycasePi (Pi {arg, res, _}) = pure (arg, res) tycasePi (Pi {arg, res, _}) = pure (arg, res)
tycasePi (E e) {tnf} = do tycasePi (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -283,7 +283,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
WhnfM (Term (S d) n, ScopeTerm (S d) n) Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd) tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
tycaseSig (E e) {tnf} = do tycaseSig (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -301,7 +301,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
WhnfM (Term (S d) n) Eff Whnf (Term (S d) n)
tycaseBOX (BOX {ty, _}) = pure ty tycaseBOX (BOX {ty, _}) = pure ty
tycaseBOX (E e) {tnf} = do tycaseBOX (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -313,8 +313,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for other intro forms error ||| for other intro forms error
private covering private covering
tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) => tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
WhnfM (Term (S d) n, Term (S d) n, DScopeTerm (S d) n, Eff Whnf (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
Term (S d) n, Term (S d) n) Term (S d) n, Term (S d) n)
tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r) tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
tycaseEq (E e) {tnf} = do tycaseEq (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf} ty <- computeElimType defs ctx e @{noOr2 tnf}
@ -336,7 +336,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
private covering private covering
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
(val, s : Term d n) -> Loc -> (val, s : Term d n) -> Loc ->
WhnfM (Subset (Elim d n) (No . isRedexE defs)) Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
piCoe sty@(S [< i] ty) p q val s loc = do piCoe sty@(S [< i] ty) p q val s loc = do
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝ -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
-- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›) -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@ -357,7 +357,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
sigCoe : (qty : Qty) -> sigCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc -> (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
WhnfM (Subset (Elim d n) (No . isRedexE defs)) Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
sigCoe qty sty@(S [< i] ty) p q val ret body loc = do sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e } -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
-- ⇝ -- ⇝
@ -383,7 +383,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
private covering private covering
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(r : Dim d) -> Loc -> (r : Dim d) -> Loc ->
WhnfM (Subset (Elim d n) (No . isRedexE defs)) Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
eqCoe sty@(S [< j] ty) p q val r loc = do eqCoe sty@(S [< j] ty) p q val r loc = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
-- ⇝ -- ⇝
@ -401,7 +401,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
boxCoe : (qty : Qty) -> boxCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc -> (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
WhnfM (Subset (Elim d n) (No . isRedexE defs)) Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
boxCoe qty sty@(S [< i] ty) p q val ret body loc = do boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e } -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
-- ⇝ -- ⇝
@ -421,7 +421,7 @@ reduceTypeCase : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
(ty : Term d n) -> (u : Universe) -> (ret : Term d n) -> (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
(arms : TypeCaseArms d n) -> (def : Term d n) -> (arms : TypeCaseArms d n) -> (def : Term d n) ->
(0 _ : So (isTyCon ty)) => Loc -> (0 _ : So (isTyCon ty)) => Loc ->
WhnfM (Subset (Elim d n) (No . isRedexE defs)) Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
reduceTypeCase defs ctx ty u ret arms def loc = case ty of reduceTypeCase defs ctx ty u ret arms def loc = case ty of
-- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
TYPE {} => TYPE {} =>
@ -483,7 +483,7 @@ pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
(ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) => (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
Dim d -> Dim d -> Dim d -> Dim d ->
(s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc -> (s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc ->
WhnfM (NonRedex Elim d n defs) Eff Whnf (NonRedex Elim d n defs)
pushCoe defs ctx i ty p q s loc = pushCoe defs ctx i ty p q s loc =
if p == q then whnf defs ctx $ Ann s (ty // one q) loc else if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
case s of case s of
@ -562,13 +562,13 @@ pushCoe defs ctx i ty p q s loc =
E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah) E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah)
where where
unwrapTYPE : Term (S d) n -> WhnfM Universe unwrapTYPE : Term (S d) n -> Eff Whnf Universe
unwrapTYPE (TYPE {l, _}) = pure l unwrapTYPE (TYPE {l, _}) = pure l
unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty
export covering export covering
Whnf Elim Reduce.isRedexE where CanWhnf Elim Reduce.isRedexE where
whnf defs ctx (F x u loc) with (lookupElim x defs) proof eq whnf defs ctx (F x u loc) with (lookupElim x defs) proof eq
_ | Just y = whnf defs ctx $ setLoc loc $ displace u y _ | Just y = whnf defs ctx $ setLoc loc $ displace u y
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
@ -725,7 +725,7 @@ Whnf Elim Reduce.isRedexE where
whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el
export covering export covering
Whnf Term Reduce.isRedexT where CanWhnf Term Reduce.isRedexT where
whnf _ _ t@(TYPE {}) = pure $ nred t whnf _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ t@(Pi {}) = pure $ nred t whnf _ _ t@(Pi {}) = pure $ nred t
whnf _ _ t@(Lam {}) = pure $ nred t whnf _ _ t@(Lam {}) = pure $ nred t

4
lib/Quox/Typing.idr
View file

@ -69,7 +69,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
namespace TyContext namespace TyContext
parameters (ctx : TyContext d n) (loc : Loc) parameters (ctx : TyContext d n) (loc : Loc)
export covering export covering
whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex => whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm d n -> Eff fs (NonRedex tm d n defs) tm d n -> Eff fs (NonRedex tm d n defs)
whnf tm = do whnf tm = do
let Val n = ctx.termLen; Val d = ctx.dimLen let Val n = ctx.termLen; Val d = ctx.dimLen
@ -115,7 +115,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
namespace EqContext namespace EqContext
parameters (ctx : EqContext n) (loc : Loc) parameters (ctx : EqContext n) (loc : Loc)
export covering export covering
whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex => whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm 0 n -> Eff fs (NonRedex tm 0 n defs) tm 0 n -> Eff fs (NonRedex tm 0 n defs)
whnf tm = do whnf tm = do
let Val n = ctx.termLen let Val n = ctx.termLen