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 $ typeCase1 e ty KPi [< "Arg", "Ret"] (BVT 1) res' = typeCase1 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 $ typeCase1 e ty KSig [< "Fst", "Snd"] (BVT 1) snd' = typeCase1 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 $ typeCase1 e ty KBOX [< "Ty"] (BVT 0) tycaseBOX t = Left $ ExpectedBOX ctx.names t ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/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 $ typeCase1 e ty KEq names (BVT 4) a1 = E $ typeCase1 e ty KEq names (BVT 3) a' = typeCase1 e (Eq0 ty a0 a1) KEq names (BVT 2) a = SY [< "i"] $ E $ dweakE 1 a' :% BV 0 l = E $ typeCase1 e a0 KEq names (BVT 1) r = E $ typeCase1 e a1 KEq names (BVT 0) pure (a0, a1, a, l, r) tycaseEq t = Left $ ExpectedEq ctx.names t 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 = extendDimN i ctx Element ty tynf <- whnf defs ctx1 ty.term (arg, res) <- tycasePi defs ctx1 ty let s0 = Coe (SY i arg) q p s body = E $ (val :# (ty // one p)) :@ E s0 s1 = Coe (SY i (arg // (BV 0 ::: shift 2))) (weakD 1 q) (BV 0) (s // shift 1) whnf defs ctx $ Coe (SY 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 ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] } -- -- type-case is used to expose A,B if the type is neutral let ctx1 = extendDimN i ctx Element ty tynf <- whnf defs ctx1 ty.term (tfst, tsnd) <- tycaseSig defs ctx1 ty let a' = Coe (SY i $ weakT 2 tfst) p q (BVT 1) tsnd' = tsnd.term // (Coe (SY i $ weakT 2 $ tfst // (BV 0 ::: shift 2)) (weakD 1 p) (BV 0) (BVT 1) ::: shift 2) b' = Coe (SY i tsnd') p q (BVT 0) whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $ SY 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 ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›) -- { (r=0) j ⇒ L; (r=1) j ⇒ R } let ctx1 = extendDimN j ctx Element ty tynf <- whnf defs ctx1 ty.term (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty let a' = SY j $ dsub1 a (weakD 1 r) val' = E $ (val :# (ty // one p)) :% r whnf defs ctx $ CompH a' p q val' r (SY j s) (SY 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 = extendDimN i ctx Element ty tynf <- whnf defs ctx1 ty.term ta <- tycaseBOX defs ctx1 ty let a' = Coe (SY i $ weakT 1 ta) p q $ BVT 0 whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $ SY 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 ∷ A‹0/𝑗› -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗› -- ((δ 𝑖 ⇒ 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; ⋯ } ⇝ t‹q/j› ∷ A -- comp [A] @p @q s { (1=1) j ⇒ t; ⋯ } ⇝ t‹q/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[(A‹0/i› ∷ ★ᵢ)/a₀, (A‹1/i› ∷ ★ᵢ)/a₁, -- ((δ i ⇒ A) ∷ Eq [★ᵢ] A‹0/i› A‹1/i›)/a, -- (L ∷ A‹0/i›)/l, (R ∷ A‹1/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' = Coe (SY [< i] ty) p q (Lam body) term' = Lam (SY [< "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 ⇒ A‹j/i›] @q @i x)/x]] @p @q s) -- ∷ (π.(x: A‹q/i›) → B‹q/i›) Lam body => do let Pi {qty, arg, res} = ty | _ => Left $ ?err let arg' = SY [< "j"] $ weakT 1 $ arg // (BV 0 ::: shift 2) res' = SY [< i] $ res.term // (Coe arg' (weakD 1 q) (BV 0) (BVT 0) ::: shift 1) body = SY 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 ⇒ A‹j/i›] @p @i s)/x]] @p @q t) -- ∷ (x : A‹q/i›) × B‹q/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 $ Coe (SY [< i] tfst) p q fst tfst' = SY [< "j"] $ tfst `CanDSubst.(//)` (BV 0 ::: shift 2) tsnd' = SY [< i] $ sub1 tsnd $ Coe tfst' (weakD 1 p) (BV 0) $ dweakT 1 fst snd' = E $ Coe tsnd' p q snd pure $ Element (Pair fst' snd' :# Sig (tfst // one q) (tsnd // one q)) Ah -- η expand like λ DLam body => do let body' = Coe (SY [< i] ty) p q (DLam body) term' = DLam (SY [< "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] ∷ [π. A‹q/i›] Box val => do let BOX {qty, ty = a} = ty | _ => Left $ ExpectedBOX (extendDim i ctx.names) ty let a = SY [< i] a pure $ Element (Box (E $ Coe a p q s) :# BOX qty (dsub1 a q)) Ah E e => pure $ Element (Coe (SY [< 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