quox/lib/Quox/Reduce.idr

710 lines
27 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Quox.Reduce
import Quox.No
import Quox.Syntax
import Quox.Definition
import Quox.Typing.Context
import Quox.Typing.Error
import Data.SnocVect
import Data.Maybe
import Data.List
%default total
public export
0 RedexTest : TermLike -> Type
RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
public export
interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
whnf : {d, n : Nat} -> (defs : Definitions) ->
(ctx : WhnfContext d n) ->
tm d n -> Either Error (Subset (tm d n) (No . isRedex defs))
public export %inline
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
(defs : Definitions) ->
WhnfContext d n -> tm d n -> Either Error (tm d n)
whnf0 defs ctx t = fst <$> whnf defs ctx t
public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
Definitions -> Pred (tm d n)
IsRedex defs = So . isRedex defs
NotRedex defs = No . isRedex defs
public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
Whnf tm isRedex => (d, n : Nat) ->
(defs : Definitions) -> Type
NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
nred t = Element t nr
public export %inline
isLamHead : Elim {} -> Bool
isLamHead (Lam {} :# Pi {}) = True
isLamHead (Coe {}) = True
isLamHead _ = False
public export %inline
isDLamHead : Elim {} -> Bool
isDLamHead (DLam {} :# Eq {}) = True
isDLamHead (Coe {}) = True
isDLamHead _ = False
public export %inline
isPairHead : Elim {} -> Bool
isPairHead (Pair {} :# Sig {}) = True
isPairHead (Coe {}) = True
isPairHead _ = False
public export %inline
isTagHead : Elim {} -> Bool
isTagHead (Tag t :# Enum _) = True
isTagHead (Coe {}) = True
isTagHead _ = False
public export %inline
isNatHead : Elim {} -> Bool
isNatHead (Zero :# Nat) = True
isNatHead (Succ n :# Nat) = True
isNatHead (Coe {}) = True
isNatHead _ = False
public export %inline
isBoxHead : Elim {} -> Bool
isBoxHead (Box {} :# BOX {}) = True
isBoxHead (Coe {}) = True
isBoxHead _ = False
public export %inline
isE : Term {} -> Bool
isE (E _) = True
isE _ = False
public export %inline
isAnn : Elim {} -> Bool
isAnn (_ :# _) = True
isAnn _ = False
||| true if a term is syntactically a type.
public export %inline
isTyCon : Term {} -> Bool
isTyCon (TYPE {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon Nat = True
isTyCon Zero = False
isTyCon (Succ {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
||| true if a term is syntactically a type, or a neutral.
public export %inline
isTyConE : Term {} -> Bool
isTyConE s = isTyCon s || isE s
||| true if a term is syntactically a type.
public export %inline
isAnnTyCon : Elim {} -> Bool
isAnnTyCon (ty :# TYPE _) = isTyCon ty
isAnnTyCon _ = False
public export %inline
isK : Dim d -> Bool
isK (K _) = True
isK _ = False
mutual
public export
isRedexE : RedexTest Elim
isRedexE defs (F x) {d, n} =
isJust $ lookupElim x defs {d, n}
isRedexE _ (B _) = False
isRedexE defs (f :@ _) =
isRedexE defs f || isLamHead f
isRedexE defs (CasePair {pair, _}) =
isRedexE defs pair || isPairHead pair
isRedexE defs (CaseEnum {tag, _}) =
isRedexE defs tag || isTagHead tag
isRedexE defs (CaseNat {nat, _}) =
isRedexE defs nat || isNatHead nat
isRedexE defs (CaseBox {box, _}) =
isRedexE defs box || isBoxHead box
isRedexE defs (f :% p) =
isRedexE defs f || isDLamHead f || isK p
isRedexE defs (t :# a) =
isE t || isRedexT defs t || isRedexT defs a
isRedexE defs (Coe {val, _}) =
isRedexT defs val || not (isE val)
isRedexE defs (Comp {ty, r, _}) =
isRedexT defs ty || isK r
isRedexE defs (TypeCase {ty, ret, _}) =
isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
isRedexE _ (CloE {}) = True
isRedexE _ (DCloE {}) = True
public export
isRedexT : RedexTest Term
isRedexT _ (CloT {}) = True
isRedexT _ (DCloT {}) = True
isRedexT defs (E e) = isAnn e || isRedexE defs e
isRedexT _ _ = False
public export
tycaseRhs : (k : TyConKind) -> TypeCaseArms d n ->
Maybe (ScopeTermN (arity k) d n)
tycaseRhs k arms = lookupPrecise k arms
public export
tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
ScopeTermN (arity k) d n
tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms
public export
tycaseRhs0 : (k : TyConKind) -> TypeCaseArms d n ->
(0 eq : arity k = 0) => Maybe (Term d n)
tycaseRhs0 k arms {eq} with (tycaseRhs k arms) | (arity k)
tycaseRhs0 k arms {eq = Refl} | res | 0 = map (.term) res
public export
tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
(0 eq : arity k = 0) => Term d n
tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms
private
weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
weakDS by (S names (Y body)) = S names $ Y $ weakT by body
weakDS by (S names (N body)) = S names $ N $ weakT by body
private
dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n
dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
dweakS by (S names (N body)) = S names $ N $ dweakT by body
private
coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d ->
ScopeTermN s d n -> ScopeTermN s d n
coeScoped ty p q (S names (Y body)) =
S names $ Y $ E $ Coe (weakDS s ty) p q body
coeScoped ty p q (S names (N body)) =
S names $ N $ E $ Coe ty p q body
mutual
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
||| performs the minimum work required to recompute the type of an elim.
|||
||| ⚠ **assumes the elim is already typechecked.** ⚠
export covering
computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
Either Error (Term d n)
computeElimType (F x) = do
let Just def = lookup x defs | Nothing => Left $ NotInScope x
pure $ def.type
computeElimType (B i) = pure $ ctx.tctx !! i
computeElimType (f :@ s) {ne} = do
-- can't use `expectPi` (or `expectEq` below) without making this
-- mutual block from hell even worse lol
Pi {arg, res, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
| t => Left $ ExpectedPi ctx.names t
pure $ sub1 res (s :# arg)
computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
computeElimType (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag
computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
computeElimType (f :% p) {ne} = do
Eq {ty, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
| t => Left $ ExpectedEq ctx.names t
pure $ dsub1 ty p
computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q
computeElimType (Comp {ty, _}) = pure ty
computeElimType (TypeCase {ret, _}) = pure ret
computeElimType (_ :# ty) = pure ty
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
||| for π.(x : A) → B, returns (A, B);
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
private covering
tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
Either Error (Term (S d) n, ScopeTerm (S d) n)
tycasePi (Pi {arg, res, _}) = pure (arg, res)
tycasePi (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf}
let arg = E $ typeCase1Y e ty KPi [< "Arg", "Ret"] (BVT 1)
res' = typeCase1Y e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
res = SY [< "Arg"] $ E $ weakE 1 res' :@ BVT 0
pure (arg, res)
tycasePi t = Left $ ExpectedPi ctx.names t
||| for (x : A) × B, returns (A, B);
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
private covering
tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
Either Error (Term (S d) n, ScopeTerm (S d) n)
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
tycaseSig (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf}
let fst = E $ typeCase1Y e ty KSig [< "Fst", "Snd"] (BVT 1)
snd' = typeCase1Y e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
snd = SY [< "Fst"] $ E $ weakE 1 snd' :@ BVT 0
pure (fst, snd)
tycaseSig t = Left $ ExpectedSig ctx.names t
||| for [π. A], returns A;
||| for an elim returns a type-case that will reduce to that;
||| for other intro forms error
private covering
tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
Either Error (Term (S d) n)
tycaseBOX (BOX _ a) = pure a
tycaseBOX (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf}
pure $ E $ typeCase1Y e ty KBOX [< "Ty"] (BVT 0)
tycaseBOX t = Left $ ExpectedBOX ctx.names t
||| for Eq [i ⇒ A] l r, returns (A0/i, A1/i, A, l, r);
||| for an elim returns five type-cases that will reduce to that;
||| for other intro forms error
private covering
tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
Either Error (Term (S d) n, Term (S d) n, DScopeTerm (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 (E e) {tnf} = do
ty <- computeElimType defs ctx e @{noOr2 tnf}
let names = [< "A0", "A1", "A", "L", "R"]
a0 = E $ typeCase1Y e ty KEq names (BVT 4)
a1 = E $ typeCase1Y e ty KEq names (BVT 3)
a' = typeCase1Y e (Eq0 ty a0 a1) KEq names (BVT 2)
a = SY [< "i"] $ E $ dweakE 1 a' :% BV 0
l = E $ typeCase1Y e a0 KEq names (BVT 1)
r = E $ typeCase1Y e a1 KEq names (BVT 0)
pure (a0, a1, a, l, r)
tycaseEq t = Left $ ExpectedEq ctx.names t
-- new block because the functions below might pass a different ctx
-- into the ones above
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
||| reduce a function application `Coe ty p q val :@ s`
private covering
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val, s : Term d n) ->
Either Error (Subset (Elim d n) (No . isRedexE defs))
piCoe sty@(S [< i] ty) p q val s = do
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
-- coe [i ⇒ B[𝒔i/x] @p @q ((t ∷ (π.(x : A) → B)p/i) 𝒔p)
-- where 𝒔j ≔ coe [i ⇒ A] @q @j s
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 ty.term
(arg, res) <- tycasePi defs ctx1 ty
let s0 = CoeT i arg q p s
body = E $ (val :# (ty // one p)) :@ E s0
s1 = CoeT i (arg // (BV 0 ::: shift 2)) (weakD 1 q) (BV 0)
(s // shift 1)
whnf defs ctx $ CoeT i (sub1 res s1) p q body
||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body`
private covering
sigCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) ->
Either Error (Subset (Elim d n) (No . isRedexE defs))
sigCoe qty sty@(S [< i] ty) p q val ret body = do
-- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
-- ⇝
-- caseπ s ∷ ((x : A) × B)p/i return z ⇒ C
-- of { (a, b) ⇒
-- e[(coe [i ⇒ A] @p @q a)/a,
-- (coe [i ⇒ B[(coe [j ⇒ Aj/i] @p @i a)/x]] @p @q b)/b] }
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 ty.term
(tfst, tsnd) <- tycaseSig defs ctx1 ty
let a' = CoeT i (weakT 2 tfst) p q (BVT 1)
tsnd' = tsnd.term //
(CoeT i (weakT 2 $ tfst // (BV 0 ::: shift 2))
(weakD 1 p) (BV 0) (BVT 1) ::: shift 2)
b' = CoeT i tsnd' p q (BVT 0)
whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $
ST body.names $ body.term // (a' ::: b' ::: shift 2)
||| reduce a dimension application `Coe ty p q val :% r`
private covering
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(r : Dim d) ->
Either Error (Subset (Elim d n) (No . isRedexE defs))
eqCoe sty@(S [< j] ty) p q val r = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
-- ⇝
-- comp [j ⇒ Ar/i] @p @q (eq ∷ (Eq [i ⇒ A] L R)p/j)
-- { (r=0) j ⇒ L; (r=1) j ⇒ R }
let ctx1 = extendDim j ctx
Element ty tynf <- whnf defs ctx1 ty.term
(a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
let a' = dsub1 a (weakD 1 r)
val' = E $ (val :# (ty // one p)) :% r
whnf defs ctx $ CompH j a' p q val' r j s j t
||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
private covering
boxCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTerm d n) ->
Either Error (Subset (Elim d n) (No . isRedexE defs))
boxCoe qty sty@(S [< i] ty) p q val ret body = do
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
-- ⇝
-- caseπ s ∷ [ρ. A]p/i return z ⇒ C
-- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 ty.term
ta <- tycaseBOX defs ctx1 ty
let a' = CoeT i (weakT 1 ta) p q $ BVT 0
whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
ST body.names $ body.term // (a' ::: shift 1)
export covering
Whnf Elim Reduce.isRedexE where
whnf defs ctx (F x) with (lookupElim x defs) proof eq
_ | Just y = whnf defs ctx y
_ | Nothing = pure $ Element (F x) $ rewrite eq in Ah
whnf _ _ (B i) = pure $ nred $ B i
-- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
whnf defs ctx (f :@ s) = do
Element f fnf <- whnf defs ctx f
case nchoose $ isLamHead f of
Left _ => case f of
Lam body :# Pi {arg, res, _} =>
let s = s :# arg in
whnf defs ctx $ sub1 body s :# sub1 res s
Coe ty p q val => piCoe defs ctx ty p q val s
Right nlh => pure $ Element (f :@ s) $ fnf `orNo` nlh
-- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
-- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
whnf defs ctx (CasePair pi pair ret body) = do
Element pair pairnf <- whnf defs ctx pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} =>
let fst = fst :# tfst
snd = snd :# sub1 tsnd fst
in
whnf defs ctx $ subN body [< fst, snd] :# sub1 ret pair
Coe ty p q val => do
sigCoe defs ctx pi ty p q val ret body
Right np =>
pure $ Element (CasePair pi pair ret body) $ pairnf `orNo` np
-- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
-- u ∷ C['a∷{a,…}/p]
whnf defs ctx (CaseEnum pi tag ret arms) = do
Element tag tagnf <- whnf defs ctx tag
case nchoose $ isTagHead tag of
Left t => case tag of
Tag t :# Enum ts =>
let ty = sub1 ret tag in
case lookup t arms of
Just arm => whnf defs ctx $ arm :# ty
Nothing => Left $ MissingEnumArm t (keys arms)
Coe ty p q val =>
-- there is nowhere an equality can be hiding inside an Enum
whnf defs ctx $ CaseEnum pi (val :# dsub1 ty q) ret arms
Right nt =>
pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
-- case zero ∷ return p ⇒ C of { zero ⇒ u; … } ⇝
-- u ∷ C[zero∷/p]
--
-- case succ n ∷ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
-- u[n∷/n', (case n ∷ ⋯)/ih] ∷ C[succ n ∷ /p]
whnf defs ctx (CaseNat pi piIH nat ret zer suc) = do
Element nat natnf <- whnf defs ctx nat
case nchoose $ isNatHead nat of
Left _ =>
let ty = sub1 ret nat in
case nat of
Zero :# Nat => whnf defs ctx (zer :# ty)
Succ n :# Nat =>
let nn = n :# Nat
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc]
in
whnf defs ctx $ tm :# ty
Coe ty p q val =>
-- same deal as Enum
whnf defs ctx $ CaseNat pi piIH (val :# dsub1 ty q) ret zer suc
Right nn =>
pure $ Element (CaseNat pi piIH nat ret zer suc) $ natnf `orNo` nn
-- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
-- u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
whnf defs ctx (CaseBox pi box ret body) = do
Element box boxnf <- whnf defs ctx box
case nchoose $ isBoxHead box of
Left _ => case box of
Box val :# BOX q bty =>
let ty = sub1 ret box in
whnf defs ctx $ sub1 body (val :# bty) :# ty
Coe ty p q val =>
boxCoe defs ctx pi ty p q val ret body
Right nb =>
pure $ Element (CaseBox pi box ret body) $ boxnf `orNo` nb
-- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @0 ⇝ t ∷ A0/𝑗
-- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A1/𝑗
-- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s𝑘/𝑖 ∷ A𝑘/𝑗
-- (if 𝑘 is a variable)
whnf defs ctx (f :% p) = do
Element f fnf <- whnf defs ctx f
case nchoose $ isDLamHead f of
Left _ => case f of
DLam body :# Eq {ty = ty, l, r, _} =>
let body = endsOr l r (dsub1 body p) p in
whnf defs ctx $ body :# dsub1 ty p
Coe ty p' q' val =>
eqCoe defs ctx ty p' q' val p
Right ndlh => case p of
K e => do
Eq {l, r, ty, _} <- whnf0 defs ctx =<< computeElimType defs ctx f
| ty => Left $ ExpectedEq ctx.names ty
whnf defs ctx $ ends (l :# ty.zero) (r :# ty.one) e
B _ => pure $ Element (f :% p) $ fnf `orNo` ndlh `orNo` Ah
-- e ∷ A ⇝ e
whnf defs ctx (s :# a) = do
Element s snf <- whnf defs ctx s
case nchoose $ isE s of
Left _ => let E e = s in pure $ Element e $ noOr2 snf
Right ne => do
Element a anf <- whnf defs ctx a
pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf
whnf defs ctx (Coe (S _ (N ty)) _ _ val) =
whnf defs ctx $ val :# ty
whnf defs ctx (Coe (S [< i] ty) p q val) = do
Element ty tynf <- whnf defs (extendDim i ctx) ty.term
Element val valnf <- whnf defs ctx val
pushCoe defs ctx i ty p q val
whnf defs ctx (Comp ty p q val r zero one) =
-- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
if p == q then whnf defs ctx $ val :# ty else
case nchoose (isK r) of
-- comp [A] @p @q s { (0=0) j ⇒ t; ⋯ } ⇝ tq/j ∷ A
-- comp [A] @p @q s { (1=1) j ⇒ t; ⋯ } ⇝ tq/j ∷ A
Left y => case r of
K Zero => whnf defs ctx $ dsub1 zero q :# ty
K One => whnf defs ctx $ dsub1 one q :# ty
Right nk => do
Element ty tynf <- whnf defs ctx ty
pure $ Element (Comp ty p q val r zero one) $ tynf `orNo` nk
-- [todo] anything other than just the boundaries??
whnf defs ctx (TypeCase ty ret arms def) = do
Element ty tynf <- whnf defs ctx ty
Element ret retnf <- whnf defs ctx ret
case nchoose $ isAnnTyCon ty of
Left y => let ty :# TYPE u = ty in
reduceTypeCase defs ctx ty u ret arms def
Right nt => pure $ Element (TypeCase ty ret arms def) $
tynf `orNo` retnf `orNo` nt
whnf defs ctx (CloE el th) = whnf defs ctx $ pushSubstsWith' id th el
whnf defs ctx (DCloE el th) = whnf defs ctx $ pushSubstsWith' th id el
export covering
Whnf Term Reduce.isRedexT where
whnf _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ t@(Pi {}) = pure $ nred t
whnf _ _ t@(Lam {}) = pure $ nred t
whnf _ _ t@(Sig {}) = pure $ nred t
whnf _ _ t@(Pair {}) = pure $ nred t
whnf _ _ t@(Enum {}) = pure $ nred t
whnf _ _ t@(Tag {}) = pure $ nred t
whnf _ _ t@(Eq {}) = pure $ nred t
whnf _ _ t@(DLam {}) = pure $ nred t
whnf _ _ Nat = pure $ nred Nat
whnf _ _ Zero = pure $ nred Zero
whnf _ _ t@(Succ {}) = pure $ nred t
whnf _ _ t@(BOX {}) = pure $ nred t
whnf _ _ t@(Box {}) = pure $ nred t
-- s ∷ A ⇝ s (in term context)
whnf defs ctx (E e) = do
Element e enf <- whnf defs ctx e
case nchoose $ isAnn e of
Left _ => let tm :# _ = e in pure $ Element tm $ noOr1 $ noOr2 enf
Right na => pure $ Element (E e) $ na `orNo` enf
whnf defs ctx (CloT tm th) = whnf defs ctx $ pushSubstsWith' id th tm
whnf defs ctx (DCloT tm th) = whnf defs ctx $ pushSubstsWith' th id tm
||| reduce a type-case applied to a type constructor
private covering
reduceTypeCase : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
(ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
(arms : TypeCaseArms d n) -> (def : Term d n) ->
(0 _ : So (isTyCon ty)) =>
Either Error (Subset (Elim d n) (No . isRedexE defs))
reduceTypeCase defs ctx ty u ret arms def = case ty of
-- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
TYPE _ =>
whnf defs ctx $ tycaseRhsDef0 def KTYPE arms :# ret
-- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
Pi _ arg res =>
let arg = arg :# TYPE u
res = Lam res :# Arr Zero (TYPE u) (TYPE u)
in
whnf defs ctx $ subN (tycaseRhsDef def KPi arms) [< arg, res] :# ret
-- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
Sig fst snd =>
let fst = fst :# TYPE u
snd = Lam snd :# Arr Zero (TYPE u) (TYPE u)
in
whnf defs ctx $ subN (tycaseRhsDef def KSig arms) [< fst, snd] :# ret
-- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
Enum _ =>
whnf defs ctx $ tycaseRhsDef0 def KEnum arms :# ret
-- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
-- of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
-- s[(A0/i ∷ ★ᵢ)/a₀, (A1/i ∷ ★ᵢ)/a₁,
-- ((δ i ⇒ A) ∷ Eq [★ᵢ] A0/i A1/i)/a,
-- (L ∷ A0/i)/l, (R ∷ A1/i)/r] ∷ Q
Eq a l r =>
let a0 = a.zero; a1 = a.one in
whnf defs ctx $
subN (tycaseRhsDef def KEq arms)
[< a0 :# TYPE u, a1 :# TYPE u,
DLam a :# Eq0 (TYPE u) a0 a1, l :# a0, r :# a1]
:# ret
-- (type-case ∷ _ return Q of { ⇒ s; ⋯ }) ⇝ s ∷ Q
Nat =>
whnf defs ctx $ tycaseRhsDef0 def KNat arms :# ret
-- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
BOX _ s =>
whnf defs ctx $ sub1 (tycaseRhsDef def KBOX arms) (s :# TYPE u) :# ret
||| pushes a coercion inside a whnf-ed term
private covering
pushCoe : {n, d : Nat} -> (defs : Definitions) -> WhnfContext d n ->
BaseName ->
(ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
Dim d -> Dim d ->
(s : Term d n) -> (0 snf : No (isRedexT defs s)) =>
Either Error (NonRedex Elim d n defs)
pushCoe defs ctx i ty p q s =
if p == q then whnf defs ctx $ s :# (ty // one q) else
case s of
-- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
TYPE {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
Pi {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
Sig {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
Enum {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
Eq {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
Nat => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
BOX {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
-- just η expand it. then whnf for (:@) will handle it later
-- this is how @xtt does it
Lam body => do
let body' = CoeT i ty p q $ Lam body
term' = [< "y"] :\\ E (weakE 1 body' :@ BVT 0)
type' = ty // one q
whnf defs ctx $ term' :# type'
{-
-- maybe:
-- (coe [i ⇒ π.(x : A) → B] @p @q (λ x ⇒ s)) ⇝
-- (λ x ⇒ coe [i ⇒ B[(coe [j ⇒ Aj/i] @q @i x)/x]] @p @q s)
-- ∷ (π.(x: Aq/i) → Bq/i)
Lam body => do
let Pi {qty, arg, res} = ty
| _ => Left $ ?err
let arg' = ST [< "j"] $ weakT 1 $ arg // (BV 0 ::: shift 2)
res' = ST [< i] $ res.term //
(Coe arg' (weakD 1 q) (BV 0) (BVT 0) ::: shift 1)
body = ST body.names $ E $ Coe res' p q body.term
pure $ Element (Lam body :# Pi qty (arg // one q) (res // one q)) Ah
-}
-- (coe [i ⇒ (x : A) × B] @p @q (s, t)) ⇝
-- (coe [i ⇒ A] @p @q s,
-- coe [i ⇒ B[(coe [j ⇒ Aj/i] @p @i s)/x]] @p @q t)
-- ∷ (x : Aq/i) × Bq/i
--
-- can't use η here because... it doesn't exist
Pair fst snd => do
let Sig {fst = tfst, snd = tsnd} = ty
| _ => Left $ ExpectedSig (extendDim i ctx.names) ty
let fst' = E $ CoeT i tfst p q fst
tfst' = tfst // (BV 0 ::: shift 2)
tsnd' = sub1 tsnd $ CoeT "j" tfst' (weakD 1 p) (BV 0) $ dweakT 1 fst
snd' = E $ CoeT i tsnd' p q snd
pure $
Element (Pair fst' snd' :# Sig (tfst // one q) (tsnd // one q)) Ah
-- η expand like λ
DLam body => do
let body' = CoeT i ty p q $ DLam body
term' = [< "j"] :\\% E (dweakE 1 body' :% BV 0)
type' = ty // one q
whnf defs ctx $ term' :# type'
-- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
Tag tag => do
let Enum ts = ty
| _ => Left $ ExpectedEnum (extendDim i ctx.names) ty
pure $ Element (Tag tag :# Enum ts) Ah
-- (coe [_ ⇒ ] @_ @_ n) ⇝ (n ∷ )
Zero => pure $ Element (Zero :# Nat) Ah
Succ t => pure $ Element (Succ t :# Nat) Ah
-- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
-- [coe [i ⇒ A] @p @q s] ∷ [π. Aq/i]
Box val => do
let BOX {qty, ty = a} = ty
| _ => Left $ ExpectedBOX (extendDim i ctx.names) ty
pure $ Element (Box (E $ CoeT i a p q s) :# BOX qty (a // one q)) Ah
E e => pure $ Element (CoeT i ty p q (E e)) (snf `orNo` Ah)
where
unwrapTYPE : Term (S d) n -> Either Error Universe
unwrapTYPE (TYPE u) = pure u
unwrapTYPE ty = Left $ ExpectedTYPE (extendDim i ctx.names) ty