From 8264a1bb819a69bdc3305dcc868f0f5bcfa85a4d Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 24 Aug 2023 18:42:26 +0200 Subject: [PATCH] split up whnf module --- lib/Quox/Reduce.idr | 786 ------------------------------ lib/Quox/Typing.idr | 2 +- lib/Quox/Whnf.idr | 5 + lib/Quox/Whnf/Coercion.idr | 198 ++++++++ lib/Quox/Whnf/ComputeElimType.idr | 64 +++ lib/Quox/Whnf/Interface.idr | 216 ++++++++ lib/Quox/Whnf/Main.idr | 199 ++++++++ lib/Quox/Whnf/TypeCase.idr | 165 +++++++ lib/quox-lib.ipkg | 7 +- 9 files changed, 854 insertions(+), 788 deletions(-) delete mode 100644 lib/Quox/Reduce.idr create mode 100644 lib/Quox/Whnf.idr create mode 100644 lib/Quox/Whnf/Coercion.idr create mode 100644 lib/Quox/Whnf/ComputeElimType.idr create mode 100644 lib/Quox/Whnf/Interface.idr create mode 100644 lib/Quox/Whnf/Main.idr create mode 100644 lib/Quox/Whnf/TypeCase.idr diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr deleted file mode 100644 index 4525b93..0000000 --- a/lib/Quox/Reduce.idr +++ /dev/null @@ -1,786 +0,0 @@ -module Quox.Reduce - -import Quox.No -import Quox.Syntax -import Quox.Definition -import Quox.Displace -import Quox.Typing.Context -import Quox.Typing.Error -import Data.SnocVect -import Data.Maybe -import Data.List -import Control.Eff - -%default total - - -public export -Whnf : List (Type -> Type) -Whnf = [NameGen, Except Error] - -export -runWhnfWith : NameSuf -> Eff Whnf a -> (Either Error a, NameSuf) -runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act - -export -runWhnf : Eff Whnf a -> Either Error a -runWhnf = fst . runWhnfWith 0 - - -public export -0 RedexTest : TermLike -> Type -RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool - -public export -interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm -where - whnf : {d, n : Nat} -> (defs : Definitions) -> - (ctx : WhnfContext d n) -> - tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs)) - -- having isRedex be part of the class header, and needing to be explicitly - -- quantified on every use since idris can't infer its type, is a little ugly. - -- but none of the alternatives i've thought of so far work. e.g. in some - -- cases idris can't tell that `isRedex` and `isRedexT` are the same thing - -public export %inline -whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => - (defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n) -whnf0 defs ctx t = fst <$> whnf defs ctx t - -public export -0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf 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} -> - CanWhnf 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 _ : CanWhnf tm isRedex) => - (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs -nred t = Element t nr - - -||| an expression like `(λ x ⇒ s) ∷ π.(x : A) → B` -public export %inline -isLamHead : Elim {} -> Bool -isLamHead (Ann (Lam {}) (Pi {}) _) = True -isLamHead (Coe {}) = True -isLamHead _ = False - -||| an expression like `(δ 𝑖 ⇒ s) ∷ Eq (𝑖 ⇒ A) s t` -public export %inline -isDLamHead : Elim {} -> Bool -isDLamHead (Ann (DLam {}) (Eq {}) _) = True -isDLamHead (Coe {}) = True -isDLamHead _ = False - -||| an expression like `(s, t) ∷ (x : A) × B` -public export %inline -isPairHead : Elim {} -> Bool -isPairHead (Ann (Pair {}) (Sig {}) _) = True -isPairHead (Coe {}) = True -isPairHead _ = False - -||| an expression like `'a ∷ {a, b, c}` -public export %inline -isTagHead : Elim {} -> Bool -isTagHead (Ann (Tag {}) (Enum {}) _) = True -isTagHead (Coe {}) = True -isTagHead _ = False - -||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ` -public export %inline -isNatHead : Elim {} -> Bool -isNatHead (Ann (Zero {}) (Nat {}) _) = True -isNatHead (Ann (Succ {}) (Nat {}) _) = True -isNatHead (Coe {}) = True -isNatHead _ = False - -||| an expression like `[s] ∷ [π. A]` -public export %inline -isBoxHead : Elim {} -> Bool -isBoxHead (Ann (Box {}) (BOX {}) _) = True -isBoxHead (Coe {}) = True -isBoxHead _ = False - -||| an elimination in a term context -public export %inline -isE : Term {} -> Bool -isE (E {}) = True -isE _ = False - -||| an expression like `s ∷ A` -public export %inline -isAnn : Elim {} -> Bool -isAnn (Ann {}) = True -isAnn _ = False - -||| a syntactic 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 - -||| a syntactic type, or a neutral -public export %inline -isTyConE : Term {} -> Bool -isTyConE s = isTyCon s || isE s - -||| a syntactic type with an annotation `★ᵢ` -public export %inline -isAnnTyCon : Elim {} -> Bool -isAnnTyCon (Ann ty (TYPE {}) _) = isTyCon ty -isAnnTyCon _ = False - -||| 0 or 1 -public export %inline -isK : Dim d -> Bool -isK (K {}) = True -isK _ = False - - -mutual - ||| a reducible elimination - ||| - ||| - a free variable, if its definition is known - ||| - an application whose head is an annotated lambda, - ||| a case expression whose head is an annotated constructor form, etc - ||| - a redundant annotation, or one whose term or type is reducible - ||| - coercions `coe (𝑖 ⇒ A) @p @q s` where: - ||| - `A` is in whnf, or - ||| - `𝑖` is not mentioned in `A`, or - ||| - `p = q` - ||| - [fixme] this is not true right now but that's because i wrote it - ||| wrong - ||| - compositions `comp A @p @q s @r {⋯}` where: - ||| - `A` is in whnf, or - ||| - `p = q`, or - ||| - `r = 0` or `r = 1` - ||| - [fixme] the p=q condition is also missing here - ||| - closures - public export - isRedexE : RedexTest Elim - isRedexE defs (F {x, _}) {d, n} = - isJust $ lookupElim x defs {d, n} - isRedexE _ (B {}) = False - isRedexE defs (App {fun, _}) = - isRedexE defs fun || isLamHead fun - 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 (DApp {fun, arg, _}) = - isRedexE defs fun || isDLamHead fun || isK arg - isRedexE defs (Ann {tm, ty, _}) = - isE tm || isRedexT defs tm || isRedexT defs ty - 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 - - ||| a reducible term - ||| - ||| - a reducible elimination, as `isRedexE` - ||| - an annotated elimination - ||| (the annotation is redundant in a checkable context) - ||| - a closure - public export - isRedexT : RedexTest Term - isRedexT _ (CloT {}) = True - isRedexT _ (DCloT {}) = True - isRedexT defs (E {e, _}) = isAnn e || isRedexE defs e - isRedexT _ _ = False - - -private -tycaseRhs : (k : TyConKind) -> TypeCaseArms d n -> - Maybe (ScopeTermN (arity k) d n) -tycaseRhs k arms = lookupPrecise k arms - -private -tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n -> - ScopeTermN (arity k) d n -tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms - -private -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 - -private -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 -> Loc -> - ScopeTermN s d n -> ScopeTermN s d n -coeScoped ty p q loc (S names (Y body)) = - ST names $ E $ Coe (weakDS s ty) p q body loc -coeScoped ty p q loc (S names (N body)) = - S names $ N $ E $ Coe ty p q body loc - - -export covering CanWhnf Term Reduce.isRedexT -export covering CanWhnf Elim Reduce.isRedexE - -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)) => - Eff Whnf (Term d n) - computeElimType (F {x, u, loc}) = do - let Just def = lookup x defs | Nothing => throw $ NotInScope loc x - pure $ displace u def.type - computeElimType (B {i, _}) = pure $ ctx.tctx !! i - computeElimType (App {fun = f, arg = s, loc}) {ne} = do - Pi {arg, res, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne} - | t => throw $ ExpectedPi loc ctx.names t - pure $ sub1 res $ Ann s arg loc - 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 (DApp {fun = f, arg = p, loc}) {ne} = do - Eq {ty, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne} - | t => throw $ ExpectedEq loc ctx.names t - pure $ dsub1 ty p - computeElimType (Ann {ty, _}) = pure ty - computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q - computeElimType (Comp {ty, _}) = pure ty - computeElimType (TypeCase {ret, _}) = pure ret - - -parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext 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 d n) -> (0 tnf : No (isRedexT defs t)) => - Eff Whnf (Term d n, ScopeTerm d n) - tycasePi (Pi {arg, res, _}) = pure (arg, res) - tycasePi (E e) {tnf} = do - ty <- computeElimType defs ctx e @{noOr2 tnf} - let loc = e.loc - narg = mnb "Arg"; nret = mnb "Ret" - arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc - res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret] - (BVT 0 loc) loc - res = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc - pure (arg, res) - tycasePi t = throw $ ExpectedPi t.loc 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 d n) -> (0 tnf : No (isRedexT defs t)) => - Eff Whnf (Term d n, ScopeTerm d n) - tycaseSig (Sig {fst, snd, _}) = pure (fst, snd) - tycaseSig (E e) {tnf} = do - ty <- computeElimType defs ctx e @{noOr2 tnf} - let loc = e.loc - nfst = mnb "Fst"; nsnd = mnb "Snd" - fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc - snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd] - (BVT 0 loc) loc - snd = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc - pure (fst, snd) - tycaseSig t = throw $ ExpectedSig t.loc 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 d n) -> (0 tnf : No (isRedexT defs t)) => - Eff Whnf (Term d n) - tycaseBOX (BOX {ty, _}) = pure ty - tycaseBOX (E e) {tnf} = do - ty <- computeElimType defs ctx e @{noOr2 tnf} - pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty")] (BVT 0 e.loc) e.loc - tycaseBOX t = throw $ ExpectedBOX t.loc 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 d n) -> (0 tnf : No (isRedexT defs t)) => - Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term 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 loc = e.loc - names = traverse' (\x => mnb x) [< "A0", "A1", "A", "L", "R"] - a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc - a1 = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc - a' = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc - a = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc - l = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc - r = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc - pure (a0, a1, a, l, r) - tycaseEq t = throw $ ExpectedEq t.loc ctx.names t - - --- new block because the functions below pass a different ctx --- into the ones above -parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) - ||| reduce a function application `App (Coe ty p q val) s loc` - private covering - piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> - (val, s : Term d n) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) - piCoe sty@(S [< i] ty) p q val s loc = 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 s.loc - body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc - s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc) - (s // shift 1) s.loc - whnf defs ctx $ CoeT i (sub1 res s1) p q body loc - - ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc` - 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) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) - 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π 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 = extendDim i ctx - Element ty tynf <- whnf defs ctx1 ty.term - (tfst, tsnd) <- tycaseSig defs ctx1 ty - let [< x, y] = body.names - a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc - tsnd' = tsnd.term // - (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2)) - (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2) - b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc - whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret - (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc - - ||| reduce a dimension application `DApp (Coe ty p q val) r loc` - private covering - eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - (r : Dim d) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) - eqCoe sty@(S [< j] ty) p q val r loc = 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; 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 $ DApp (Ann val (ty // one p) val.loc) r loc - whnf defs ctx $ CompH j a' p q val' r j s j t loc - - ||| 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) -> Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) - 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π 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 noLoc) body.name.loc - whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret - (ST body.names $ body.term // (a' ::: shift 1)) loc - - -||| 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)) => Loc -> - Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) -reduceTypeCase defs ctx ty u ret arms def loc = case ty of - -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q - TYPE {} => - whnf defs ctx $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc - - -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝ - -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q - Pi {arg, res, loc = piLoc, _} => - let arg' = Ann arg (TYPE u noLoc) arg.loc - res' = Ann (Lam res res.loc) - (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc - in - whnf defs ctx $ - Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc - - -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝ - -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q - Sig {fst, snd, loc = sigLoc, _} => - let fst' = Ann fst (TYPE u noLoc) fst.loc - snd' = Ann (Lam snd snd.loc) - (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc - in - whnf defs ctx $ - Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc - - -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q - Enum {} => - whnf defs ctx $ Ann (tycaseRhsDef0 def KEnum arms) ret loc - - -- (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 {ty = a, l, r, loc = eqLoc, _} => - let a0 = a.zero; a1 = a.one in - whnf defs ctx $ Ann - (subN (tycaseRhsDef def KEq arms) - [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc, - Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc, - Ann l a0 l.loc, Ann r a1 r.loc]) - ret loc - - -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q - Nat {} => - whnf defs ctx $ Ann (tycaseRhsDef0 def KNat arms) ret loc - - -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q - BOX {ty = a, loc = boxLoc, _} => - whnf defs ctx $ Ann - (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc)) - ret loc - - -||| pushes a coercion inside a whnf-ed term -private covering -pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n -> - BindName -> - (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)) => Loc -> - Eff Whnf (NonRedex Elim d n defs) -pushCoe defs ctx i ty p q s loc = - if p == q then whnf defs ctx $ Ann s (ty // one q) loc else - case s of - -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ) - TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Pi {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Sig {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Eq {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - Nat {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - BOX {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc - - -- just η expand it. then whnf for App will handle it later - -- this is how @xtt does it - -- - -- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝ - -- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯ - lam@(Lam {body, _}) => do - let lam' = CoeT i ty p q lam loc - term' = LamY !(fresh body.name) - (E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc - type' = ty // one q - whnf defs ctx $ Ann term' type' loc - - -- (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, loc = pairLoc} => do - let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty - | _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty - let fst' = E $ CoeT i tfst p q fst fst.loc - tfst' = tfst // (B VZ noLoc ::: shift 2) - tsnd' = sub1 tsnd $ - CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc) - (dweakT 1 fst) fst.loc - snd' = E $ CoeT i tsnd' p q snd snd.loc - pure $ - Element (Ann (Pair fst' snd' pairLoc) - (Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah - - -- η expand, like for Lam - -- - -- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝ - -- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯ - dlam@(DLam {body, _}) => do - let dlam' = CoeT i ty p q dlam loc - term' = DLamY !(mnb "j") - (E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc - type' = ty // one q - whnf defs ctx $ Ann term' type' loc - - -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯}) - Tag {tag, loc = tagLoc} => do - let Enum {cases, loc = enumLoc} = ty - | _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty - pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah - - -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ) - Zero {loc = zeroLoc} => do - pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah - Succ {p = pred, loc = succLoc} => do - pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah - - -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝ - -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›] - Box {val, loc = boxLoc} => do - let BOX {qty, ty = a, loc = tyLoc} = ty - | _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty - pure $ Element - (Ann (Box (E $ CoeT i a p q val val.loc) boxLoc) - (BOX qty (a // one q) tyLoc) loc) - Ah - - E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah) -where - unwrapTYPE : Term (S d) n -> Eff Whnf Universe - unwrapTYPE (TYPE {l, _}) = pure l - unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty - - -export covering -CanWhnf Elim Reduce.isRedexE where - whnf defs ctx (F x u loc) with (lookupElim x defs) proof eq - _ | Just y = whnf defs ctx $ setLoc loc $ displace u y - _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah - - whnf _ _ (B i loc) = pure $ nred $ B i loc - - -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x] - whnf defs ctx (App f s appLoc) = do - Element f fnf <- whnf defs ctx f - case nchoose $ isLamHead f of - Left _ => case f of - Ann (Lam {body, _}) (Pi {arg, res, _}) floc => - let s = Ann s arg s.loc in - whnf defs ctx $ Ann (sub1 body s) (sub1 res s) appLoc - Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc - Right nlh => pure $ Element (App f s appLoc) $ 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 caseLoc) = do - Element pair pairnf <- whnf defs ctx pair - case nchoose $ isPairHead pair of - Left _ => case pair of - Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc => - let fst = Ann fst tfst fst.loc - snd = Ann snd (sub1 tsnd fst) snd.loc - in - whnf defs ctx $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc - Coe ty p q val _ => do - sigCoe defs ctx pi ty p q val ret body caseLoc - Right np => - pure $ Element (CasePair pi pair ret body caseLoc) $ 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 caseLoc) = do - Element tag tagnf <- whnf defs ctx tag - case nchoose $ isTagHead tag of - Left _ => case tag of - Ann (Tag t _) (Enum ts _) _ => - let ty = sub1 ret tag in - case lookup t arms of - Just arm => whnf defs ctx $ Ann arm ty arm.loc - Nothing => throw $ MissingEnumArm caseLoc t (keys arms) - Coe ty p q val _ => - -- there is nowhere an equality can be hiding inside an enum type - whnf defs ctx $ - CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc - Right nt => - pure $ Element (CaseEnum pi tag ret arms caseLoc) $ 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 caseLoc) = do - Element nat natnf <- whnf defs ctx nat - case nchoose $ isNatHead nat of - Left _ => - let ty = sub1 ret nat in - case nat of - Ann (Zero _) (Nat _) _ => - whnf defs ctx $ Ann zer ty zer.loc - Ann (Succ n succLoc) (Nat natLoc) _ => - let nn = Ann n (Nat natLoc) succLoc - tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc] - in - whnf defs ctx $ Ann tm ty caseLoc - Coe ty p q val _ => - -- same deal as Enum - whnf defs ctx $ - CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc - Right nn => pure $ - Element (CaseNat pi piIH nat ret zer suc caseLoc) $ 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 caseLoc) = do - Element box boxnf <- whnf defs ctx box - case nchoose $ isBoxHead box of - Left _ => case box of - Ann (Box val boxLoc) (BOX q bty tyLoc) _ => - let ty = sub1 ret box in - whnf defs ctx $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc - Coe ty p q val _ => - boxCoe defs ctx pi ty p q val ret body caseLoc - Right nb => - pure $ Element (CaseBox pi box ret body caseLoc) $ boxnf `orNo` nb - - -- e : Eq (𝑗 ⇒ A) t u ⊢ e @0 ⇝ t ∷ A‹0/𝑗› - -- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗› - -- - -- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗› - whnf defs ctx (DApp f p appLoc) = do - Element f fnf <- whnf defs ctx f - case nchoose $ isDLamHead f of - Left _ => case f of - Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ => - whnf defs ctx $ - Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p) - (dsub1 ty p) appLoc - Coe ty p' q' val _ => - eqCoe defs ctx ty p' q' val p appLoc - Right ndlh => case p of - K e _ => do - Eq {l, r, ty, _} <- whnf0 defs ctx =<< computeElimType defs ctx f - | ty => throw $ ExpectedEq ty.loc ctx.names ty - whnf defs ctx $ - ends (Ann (setLoc appLoc l) ty.zero appLoc) - (Ann (setLoc appLoc r) ty.one appLoc) e - B {} => pure $ Element (DApp f p appLoc) $ fnf `orNo` ndlh `orNo` Ah - - -- e ∷ A ⇝ e - whnf defs ctx (Ann s a annLoc) = 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 (Ann s a annLoc) $ ne `orNo` snf `orNo` anf - - whnf defs ctx (Coe (S _ (N ty)) _ _ val coeLoc) = - whnf defs ctx $ Ann val ty coeLoc - whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do - Element ty tynf <- whnf defs (extendDim i ctx) ty - Element val valnf <- whnf defs ctx val - pushCoe defs ctx i ty p q val coeLoc - - whnf defs ctx (Comp ty p q val r zero one compLoc) = - -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A - if p == q then whnf defs ctx $ Ann val ty compLoc 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 $ Ann (dsub1 zero q) ty compLoc - K One _ => whnf defs ctx $ Ann (dsub1 one q) ty compLoc - Right nk => do - Element ty tynf <- whnf defs ctx ty - pure $ Element (Comp ty p q val r zero one compLoc) $ tynf `orNo` nk - - whnf defs ctx (TypeCase ty ret arms def tcLoc) = do - Element ty tynf <- whnf defs ctx ty - Element ret retnf <- whnf defs ctx ret - case nchoose $ isAnnTyCon ty of - Left y => - let Ann ty (TYPE u _) _ = ty in - reduceTypeCase defs ctx ty u ret arms def tcLoc - Right nt => pure $ - Element (TypeCase ty ret arms def tcLoc) (tynf `orNo` retnf `orNo` nt) - - whnf defs ctx (CloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' id th el - whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el - -export covering -CanWhnf 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 _ _ t@(Nat {}) = pure $ nred t - whnf _ _ t@(Zero {}) = pure $ nred t - 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 Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf - Right na => pure $ Element (E e) $ na `orNo` enf - - whnf defs ctx (CloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' id th tm - whnf defs ctx (DCloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' th id tm diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index 2d0a215..065961e 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -6,7 +6,7 @@ import public Quox.Typing.Error as Typing import public Quox.Syntax import public Quox.Definition -import public Quox.Reduce +import public Quox.Whnf import Language.Reflection import Control.Eff diff --git a/lib/Quox/Whnf.idr b/lib/Quox/Whnf.idr new file mode 100644 index 0000000..fb25a58 --- /dev/null +++ b/lib/Quox/Whnf.idr @@ -0,0 +1,5 @@ +module Quox.Whnf + +import public Quox.Whnf.Interface as Quox.Whnf +import public Quox.Whnf.ComputeElimType as Quox.Whnf +import public Quox.Whnf.Main as Quox.Whnf diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr new file mode 100644 index 0000000..b70c8f1 --- /dev/null +++ b/lib/Quox/Whnf/Coercion.idr @@ -0,0 +1,198 @@ +module Quox.Whnf.Coercion + +import Quox.Whnf.Interface +import Quox.Whnf.ComputeElimType +import Quox.Whnf.TypeCase + +%default total + + + +private +coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc -> + ScopeTermN s d n -> ScopeTermN s d n +coeScoped ty p q loc (S names (N body)) = + S names $ N $ E $ Coe ty p q body loc +coeScoped ty p q loc (S names (Y body)) = + ST names $ E $ Coe (weakDS s ty) p q body loc +where + 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 + + +parameters {auto _ : CanWhnf Term Interface.isRedexT} + {auto _ : CanWhnf Elim Interface.isRedexE} + {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) + ||| reduce a function application `App (Coe ty p q val) s loc` + export covering + piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> + (val, s : Term d n) -> Loc -> + Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) + piCoe sty@(S [< i] ty) p q val s loc = 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 s.loc + body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc + s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc) + (s // shift 1) s.loc + whnf defs ctx $ CoeT i (sub1 res s1) p q body loc + + ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc` + export 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) -> Loc -> + Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) + 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π 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 = extendDim i ctx + Element ty tynf <- whnf defs ctx1 ty.term + (tfst, tsnd) <- tycaseSig defs ctx1 ty + let [< x, y] = body.names + a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc + tsnd' = tsnd.term // + (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2)) + (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2) + b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc + whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret + (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc + + ||| reduce a dimension application `DApp (Coe ty p q val) r loc` + export covering + eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> + (r : Dim d) -> Loc -> + Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) + eqCoe sty@(S [< j] ty) p q val r loc = 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; 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 $ DApp (Ann val (ty // one p) val.loc) r loc + whnf defs ctx $ CompH j a' p q val' r j s j t loc + + ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body` + export covering + boxCoe : (qty : Qty) -> + (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> + (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc -> + Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) + 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π 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 noLoc) body.name.loc + whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret + (ST body.names $ body.term // (a' ::: shift 1)) loc + + + + ||| pushes a coercion inside a whnf-ed term + export covering + pushCoe : BindName -> + (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)) => Loc -> + Eff Whnf (NonRedex Elim d n defs) + pushCoe i ty p q s loc {snf} = + if p == q then whnf defs ctx $ Ann s (ty // one q) loc else + case s of + -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ) + TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + Pi {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + Sig {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + Eq {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + Nat {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + BOX {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc + + -- just η expand it. then whnf for App will handle it later + -- this is how @xtt does it + -- + -- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝ + -- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯ + lam@(Lam {body, _}) => do + let lam' = CoeT i ty p q lam loc + term' = LamY !(fresh body.name) + (E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc + type' = ty // one q + whnf defs ctx $ Ann term' type' loc + + -- (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, loc = pairLoc} => do + let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty + | _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty + let fst' = E $ CoeT i tfst p q fst fst.loc + tfst' = tfst // (B VZ noLoc ::: shift 2) + tsnd' = sub1 tsnd $ + CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc) + (dweakT 1 fst) fst.loc + snd' = E $ CoeT i tsnd' p q snd snd.loc + pure $ + Element (Ann (Pair fst' snd' pairLoc) + (Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah + + -- η expand, like for Lam + -- + -- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝ + -- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯ + dlam@(DLam {body, _}) => do + let dlam' = CoeT i ty p q dlam loc + term' = DLamY !(mnb "j") + (E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc + type' = ty // one q + whnf defs ctx $ Ann term' type' loc + + -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯}) + Tag {tag, loc = tagLoc} => do + let Enum {cases, loc = enumLoc} = ty + | _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty + pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah + + -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ) + Zero {loc = zeroLoc} => do + pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah + Succ {p = pred, loc = succLoc} => do + pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah + + -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝ + -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›] + Box {val, loc = boxLoc} => do + let BOX {qty, ty = a, loc = tyLoc} = ty + | _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty + pure $ Element + (Ann (Box (E $ CoeT i a p q val val.loc) boxLoc) + (BOX qty (a // one q) tyLoc) loc) + Ah + + E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah) + where + unwrapTYPE : Term (S d) n -> Eff Whnf Universe + unwrapTYPE (TYPE {l, _}) = pure l + unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr new file mode 100644 index 0000000..91c4d07 --- /dev/null +++ b/lib/Quox/Whnf/ComputeElimType.idr @@ -0,0 +1,64 @@ +module Quox.Whnf.ComputeElimType + +import Quox.Whnf.Interface +import Quox.Displace + +%default total + + +||| performs the minimum work required to recompute the type of an elim. +||| +||| - assumes the elim is already typechecked +||| - the return value is not reduced +export covering +computeElimType : CanWhnf Term Interface.isRedexT => + CanWhnf Elim Interface.isRedexE => + {d, n : Nat} -> + (defs : Definitions) -> WhnfContext d n -> + (e : Elim d n) -> (0 ne : No (isRedexE defs e)) => + Eff Whnf (Term d n) +computeElimType defs ctx e {ne} = + case e of + F {x, u, loc} => do + let Just def = lookup x defs + | Nothing => throw $ NotInScope loc x + pure $ displace u def.type + + B {i, _} => + pure $ ctx.tctx !! i + + App {fun = f, arg = s, loc} => do + fty' <- computeElimType defs ctx f {ne = noOr1 ne} + Pi {arg, res, _} <- whnf0 defs ctx fty' + | t => throw $ ExpectedPi loc ctx.names t + pure $ sub1 res $ Ann s arg loc + + CasePair {pair, ret, _} => + pure $ sub1 ret pair + + CaseEnum {tag, ret, _} => + pure $ sub1 ret tag + + CaseNat {nat, ret, _} => + pure $ sub1 ret nat + + CaseBox {box, ret, _} => + pure $ sub1 ret box + + DApp {fun = f, arg = p, loc} => do + fty' <- computeElimType defs ctx f {ne = noOr1 ne} + Eq {ty, _} <- whnf0 defs ctx fty' + | t => throw $ ExpectedEq loc ctx.names t + pure $ dsub1 ty p + + Ann {ty, _} => + pure ty + + Coe {ty, q, _} => + pure $ dsub1 ty q + + Comp {ty, _} => + pure ty + + TypeCase {ret, _} => + pure ret diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr new file mode 100644 index 0000000..dfefdd0 --- /dev/null +++ b/lib/Quox/Whnf/Interface.idr @@ -0,0 +1,216 @@ +module Quox.Whnf.Interface + +import public Quox.No +import public Quox.Syntax +import public Quox.Definition +import public Quox.Typing.Context +import public Quox.Typing.Error +import public Data.Maybe +import public Control.Eff + +%default total + + +public export +Whnf : List (Type -> Type) +Whnf = [NameGen, Except Error] + +export +runWhnfWith : NameSuf -> Eff Whnf a -> (Either Error a, NameSuf) +runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act + +export +runWhnf : Eff Whnf a -> Either Error a +runWhnf = fst . runWhnfWith 0 + + +public export +0 RedexTest : TermLike -> Type +RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool + +public export +interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm +where + whnf : {d, n : Nat} -> (defs : Definitions) -> + (ctx : WhnfContext d n) -> + tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs)) + -- having isRedex be part of the class header, and needing to be explicitly + -- quantified on every use since idris can't infer its type, is a little ugly. + -- but none of the alternatives i've thought of so far work. e.g. in some + -- cases idris can't tell that `isRedex` and `isRedexT` are the same thing + +public export %inline +whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => + (defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n) +whnf0 defs ctx t = fst <$> whnf defs ctx t + +public export +0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf 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} -> + CanWhnf 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 _ : CanWhnf tm isRedex) => + (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs +nred t = Element t nr + + +||| an expression like `(λ x ⇒ s) ∷ π.(x : A) → B` +public export %inline +isLamHead : Elim {} -> Bool +isLamHead (Ann (Lam {}) (Pi {}) _) = True +isLamHead (Coe {}) = True +isLamHead _ = False + +||| an expression like `(δ 𝑖 ⇒ s) ∷ Eq (𝑖 ⇒ A) s t` +public export %inline +isDLamHead : Elim {} -> Bool +isDLamHead (Ann (DLam {}) (Eq {}) _) = True +isDLamHead (Coe {}) = True +isDLamHead _ = False + +||| an expression like `(s, t) ∷ (x : A) × B` +public export %inline +isPairHead : Elim {} -> Bool +isPairHead (Ann (Pair {}) (Sig {}) _) = True +isPairHead (Coe {}) = True +isPairHead _ = False + +||| an expression like `'a ∷ {a, b, c}` +public export %inline +isTagHead : Elim {} -> Bool +isTagHead (Ann (Tag {}) (Enum {}) _) = True +isTagHead (Coe {}) = True +isTagHead _ = False + +||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ` +public export %inline +isNatHead : Elim {} -> Bool +isNatHead (Ann (Zero {}) (Nat {}) _) = True +isNatHead (Ann (Succ {}) (Nat {}) _) = True +isNatHead (Coe {}) = True +isNatHead _ = False + +||| an expression like `[s] ∷ [π. A]` +public export %inline +isBoxHead : Elim {} -> Bool +isBoxHead (Ann (Box {}) (BOX {}) _) = True +isBoxHead (Coe {}) = True +isBoxHead _ = False + +||| an elimination in a term context +public export %inline +isE : Term {} -> Bool +isE (E {}) = True +isE _ = False + +||| an expression like `s ∷ A` +public export %inline +isAnn : Elim {} -> Bool +isAnn (Ann {}) = True +isAnn _ = False + +||| a syntactic 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 + +||| a syntactic type, or a neutral +public export %inline +isTyConE : Term {} -> Bool +isTyConE s = isTyCon s || isE s + +||| a syntactic type with an annotation `★ᵢ` +public export %inline +isAnnTyCon : Elim {} -> Bool +isAnnTyCon (Ann ty (TYPE {}) _) = isTyCon ty +isAnnTyCon _ = False + +||| 0 or 1 +public export %inline +isK : Dim d -> Bool +isK (K {}) = True +isK _ = False + + +mutual + ||| a reducible elimination + ||| + ||| - a free variable, if its definition is known + ||| - an application whose head is an annotated lambda, + ||| a case expression whose head is an annotated constructor form, etc + ||| - a redundant annotation, or one whose term or type is reducible + ||| - coercions `coe (𝑖 ⇒ A) @p @q s` where: + ||| - `A` is in whnf, or + ||| - `𝑖` is not mentioned in `A`, or + ||| - `p = q` + ||| - [fixme] this is not true right now but that's because i wrote it + ||| wrong + ||| - compositions `comp A @p @q s @r {⋯}` where: + ||| - `A` is in whnf, or + ||| - `p = q`, or + ||| - `r = 0` or `r = 1` + ||| - [fixme] the p=q condition is also missing here + ||| - closures + public export + isRedexE : RedexTest Elim + isRedexE defs (F {x, _}) {d, n} = + isJust $ lookupElim x defs {d, n} + isRedexE _ (B {}) = False + isRedexE defs (App {fun, _}) = + isRedexE defs fun || isLamHead fun + 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 (DApp {fun, arg, _}) = + isRedexE defs fun || isDLamHead fun || isK arg + isRedexE defs (Ann {tm, ty, _}) = + isE tm || isRedexT defs tm || isRedexT defs ty + 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 + + ||| a reducible term + ||| + ||| - a reducible elimination, as `isRedexE` + ||| - an annotated elimination + ||| (the annotation is redundant in a checkable context) + ||| - a closure + public export + isRedexT : RedexTest Term + isRedexT _ (CloT {}) = True + isRedexT _ (DCloT {}) = True + isRedexT defs (E {e, _}) = isAnn e || isRedexE defs e + isRedexT _ _ = False diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr new file mode 100644 index 0000000..0274c65 --- /dev/null +++ b/lib/Quox/Whnf/Main.idr @@ -0,0 +1,199 @@ +module Quox.Whnf.Main + +import Quox.Whnf.Interface +import Quox.Whnf.ComputeElimType +import Quox.Whnf.TypeCase +import Quox.Whnf.Coercion +import Quox.Displace +import Data.SnocVect + +%default total + + +export covering CanWhnf Term Interface.isRedexT +export covering CanWhnf Elim Interface.isRedexE + + +covering +CanWhnf Elim Interface.isRedexE where + whnf defs ctx (F x u loc) with (lookupElim x defs) proof eq + _ | Just y = whnf defs ctx $ setLoc loc $ displace u y + _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah + + whnf _ _ (B i loc) = pure $ nred $ B i loc + + -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x] + whnf defs ctx (App f s appLoc) = do + Element f fnf <- whnf defs ctx f + case nchoose $ isLamHead f of + Left _ => case f of + Ann (Lam {body, _}) (Pi {arg, res, _}) floc => + let s = Ann s arg s.loc in + whnf defs ctx $ Ann (sub1 body s) (sub1 res s) appLoc + Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc + Right nlh => pure $ Element (App f s appLoc) $ 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 caseLoc) = do + Element pair pairnf <- whnf defs ctx pair + case nchoose $ isPairHead pair of + Left _ => case pair of + Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc => + let fst = Ann fst tfst fst.loc + snd = Ann snd (sub1 tsnd fst) snd.loc + in + whnf defs ctx $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc + Coe ty p q val _ => do + sigCoe defs ctx pi ty p q val ret body caseLoc + Right np => + pure $ Element (CasePair pi pair ret body caseLoc) $ 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 caseLoc) = do + Element tag tagnf <- whnf defs ctx tag + case nchoose $ isTagHead tag of + Left _ => case tag of + Ann (Tag t _) (Enum ts _) _ => + let ty = sub1 ret tag in + case lookup t arms of + Just arm => whnf defs ctx $ Ann arm ty arm.loc + Nothing => throw $ MissingEnumArm caseLoc t (keys arms) + Coe ty p q val _ => + -- there is nowhere an equality can be hiding inside an enum type + whnf defs ctx $ + CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc + Right nt => + pure $ Element (CaseEnum pi tag ret arms caseLoc) $ 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 caseLoc) = do + Element nat natnf <- whnf defs ctx nat + case nchoose $ isNatHead nat of + Left _ => + let ty = sub1 ret nat in + case nat of + Ann (Zero _) (Nat _) _ => + whnf defs ctx $ Ann zer ty zer.loc + Ann (Succ n succLoc) (Nat natLoc) _ => + let nn = Ann n (Nat natLoc) succLoc + tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc] + in + whnf defs ctx $ Ann tm ty caseLoc + Coe ty p q val _ => + -- same deal as Enum + whnf defs ctx $ + CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc + Right nn => pure $ + Element (CaseNat pi piIH nat ret zer suc caseLoc) $ 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 caseLoc) = do + Element box boxnf <- whnf defs ctx box + case nchoose $ isBoxHead box of + Left _ => case box of + Ann (Box val boxLoc) (BOX q bty tyLoc) _ => + let ty = sub1 ret box in + whnf defs ctx $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc + Coe ty p q val _ => + boxCoe defs ctx pi ty p q val ret body caseLoc + Right nb => + pure $ Element (CaseBox pi box ret body caseLoc) $ boxnf `orNo` nb + + -- e : Eq (𝑗 ⇒ A) t u ⊢ e @0 ⇝ t ∷ A‹0/𝑗› + -- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗› + -- + -- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗› + whnf defs ctx (DApp f p appLoc) = do + Element f fnf <- whnf defs ctx f + case nchoose $ isDLamHead f of + Left _ => case f of + Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ => + whnf defs ctx $ + Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p) + (dsub1 ty p) appLoc + Coe ty p' q' val _ => + eqCoe defs ctx ty p' q' val p appLoc + Right ndlh => case p of + K e _ => do + Eq {l, r, ty, _} <- whnf0 defs ctx =<< computeElimType defs ctx f + | ty => throw $ ExpectedEq ty.loc ctx.names ty + whnf defs ctx $ + ends (Ann (setLoc appLoc l) ty.zero appLoc) + (Ann (setLoc appLoc r) ty.one appLoc) e + B {} => pure $ Element (DApp f p appLoc) $ fnf `orNo` ndlh `orNo` Ah + + -- e ∷ A ⇝ e + whnf defs ctx (Ann s a annLoc) = 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 (Ann s a annLoc) $ ne `orNo` snf `orNo` anf + + whnf defs ctx (Coe (S _ (N ty)) _ _ val coeLoc) = + whnf defs ctx $ Ann val ty coeLoc + whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do + Element ty tynf <- whnf defs (extendDim i ctx) ty + Element val valnf <- whnf defs ctx val + pushCoe defs ctx i ty p q val coeLoc + + whnf defs ctx (Comp ty p q val r zero one compLoc) = + -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A + if p == q then whnf defs ctx $ Ann val ty compLoc 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 $ Ann (dsub1 zero q) ty compLoc + K One _ => whnf defs ctx $ Ann (dsub1 one q) ty compLoc + Right nk => do + Element ty tynf <- whnf defs ctx ty + pure $ Element (Comp ty p q val r zero one compLoc) $ tynf `orNo` nk + + whnf defs ctx (TypeCase ty ret arms def tcLoc) = do + Element ty tynf <- whnf defs ctx ty + Element ret retnf <- whnf defs ctx ret + case nchoose $ isAnnTyCon ty of + Left y => + let Ann ty (TYPE u _) _ = ty in + reduceTypeCase defs ctx ty u ret arms def tcLoc + Right nt => pure $ + Element (TypeCase ty ret arms def tcLoc) (tynf `orNo` retnf `orNo` nt) + + whnf defs ctx (CloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' id th el + whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el + +covering +CanWhnf Term Interface.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 _ _ t@(Nat {}) = pure $ nred t + whnf _ _ t@(Zero {}) = pure $ nred t + 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 Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf + Right na => pure $ Element (E e) $ na `orNo` enf + + whnf defs ctx (CloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' id th tm + whnf defs ctx (DCloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' th id tm diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr new file mode 100644 index 0000000..f6344bb --- /dev/null +++ b/lib/Quox/Whnf/TypeCase.idr @@ -0,0 +1,165 @@ +module Quox.Whnf.TypeCase + +import Quox.Whnf.Interface +import Quox.Whnf.ComputeElimType +import Data.SnocVect + +%default total + + +private +tycaseRhs : (k : TyConKind) -> TypeCaseArms d n -> + Maybe (ScopeTermN (arity k) d n) +tycaseRhs k arms = lookupPrecise k arms + +private +tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n -> + ScopeTermN (arity k) d n +tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms + +private +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 + +private +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 + + + +parameters {auto _ : CanWhnf Term Interface.isRedexT} + {auto _ : CanWhnf Elim Interface.isRedexE} + {d, n : Nat} (defs : Definitions) (ctx : WhnfContext 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 + export covering + tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) => + Eff Whnf (Term d n, ScopeTerm d n) + tycasePi (Pi {arg, res, _}) = pure (arg, res) + tycasePi (E e) {tnf} = do + ty <- computeElimType defs ctx e {ne = noOr2 tnf} + let loc = e.loc + narg = mnb "Arg"; nret = mnb "Ret" + arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc + res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret] + (BVT 0 loc) loc + res = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc + pure (arg, res) + tycasePi t = throw $ ExpectedPi t.loc 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 + export covering + tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) => + Eff Whnf (Term d n, ScopeTerm d n) + tycaseSig (Sig {fst, snd, _}) = pure (fst, snd) + tycaseSig (E e) {tnf} = do + ty <- computeElimType defs ctx e {ne = noOr2 tnf} + let loc = e.loc + nfst = mnb "Fst"; nsnd = mnb "Snd" + fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc + snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd] + (BVT 0 loc) loc + snd = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc + pure (fst, snd) + tycaseSig t = throw $ ExpectedSig t.loc ctx.names t + + ||| for [π. A], returns A; + ||| for an elim returns a type-case that will reduce to that; + ||| for other intro forms error + export covering + tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) => + Eff Whnf (Term d n) + tycaseBOX (BOX {ty, _}) = pure ty + tycaseBOX (E e) {tnf} = do + ty <- computeElimType defs ctx e {ne = noOr2 tnf} + pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty")] (BVT 0 e.loc) e.loc + tycaseBOX t = throw $ ExpectedBOX t.loc 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 + export covering + tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) => + Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term 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 {ne = noOr2 tnf} + let loc = e.loc + names = traverse' (\x => mnb x) [< "A0", "A1", "A", "L", "R"] + a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc + a1 = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc + a' = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc + a = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc + l = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc + r = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc + pure (a0, a1, a, l, r) + tycaseEq t = throw $ ExpectedEq t.loc ctx.names t + + + ||| reduce a type-case applied to a type constructor + ||| + ||| `reduceTypeCase A i Q arms def _` reduces an expression + ||| `type-case A ∷ ★ᵢ return Q of { arms; _ ⇒ def }` + export covering + reduceTypeCase : (ty : Term d n) -> (u : Universe) -> (ret : Term d n) -> + (arms : TypeCaseArms d n) -> (def : Term d n) -> + (0 _ : So (isTyCon ty)) => Loc -> + Eff Whnf (Subset (Elim d n) (No . isRedexE defs)) + reduceTypeCase ty u ret arms def loc = case ty of + -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q + TYPE {} => + whnf defs ctx $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc + + -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝ + -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q + Pi {arg, res, loc = piLoc, _} => + let arg' = Ann arg (TYPE u noLoc) arg.loc + res' = Ann (Lam res res.loc) + (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc + in + whnf defs ctx $ + Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc + + -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝ + -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q + Sig {fst, snd, loc = sigLoc, _} => + let fst' = Ann fst (TYPE u noLoc) fst.loc + snd' = Ann (Lam snd snd.loc) + (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc + in + whnf defs ctx $ + Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc + + -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q + Enum {} => + whnf defs ctx $ Ann (tycaseRhsDef0 def KEnum arms) ret loc + + -- (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 {ty = a, l, r, loc = eqLoc, _} => + let a0 = a.zero; a1 = a.one in + whnf defs ctx $ Ann + (subN (tycaseRhsDef def KEq arms) + [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc, + Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc, + Ann l a0 l.loc, Ann r a1 r.loc]) + ret loc + + -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q + Nat {} => + whnf defs ctx $ Ann (tycaseRhsDef0 def KNat arms) ret loc + + -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q + BOX {ty = a, loc = boxLoc, _} => + whnf defs ctx $ Ann + (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc)) + ret loc diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 77285c5..832f07d 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -33,7 +33,12 @@ modules = Quox.Syntax.Var, Quox.Displace, Quox.Definition, - Quox.Reduce, + Quox.Whnf.Interface, + Quox.Whnf.ComputeElimType, + Quox.Whnf.TypeCase, + Quox.Whnf.Coercion, + Quox.Whnf.Main, + Quox.Whnf, Quox.Context, Quox.Equal, Quox.Name,