add local bindings to context

- without this, inside the body of `let x = e in …`, the typechecker would forget that `x = e` - now bound variables can reduce, if they have a definition, so RedexTest needs to take the context too
2023-12-07 01:35:39 +01:00 · 2023-12-07 01:35:39 +01:00 · 03c197bd04
commit 03c197bd04
parent cdf1ec6deb
13 changed files with 300 additions and 211 deletions
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@ -28,7 +28,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  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 sg))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
  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›)
@ -49,7 +49,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  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 sg))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
  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 }
    --   ⇝
@ -74,7 +74,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  ||| reduce a pair projection `Fst (Coe ty p q val) loc`
  export covering
  fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-           Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
+           Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
  fstCoe sty@(S [< i] ty) p q val loc = do
    -- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s)
    --   ⇝
@ -91,7 +91,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  ||| reduce a pair projection `Snd (Coe ty p q val) loc`
  export covering
  sndCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-           Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
+           Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
  sndCoe sty@(S [< i] ty) p q val loc = do
    -- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s)
    --   ⇝
@ -115,7 +115,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  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 sg))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
  eqCoe sty@(S [< j] ty) p q val r loc = do
    -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
    --   ⇝
@ -133,7 +133,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  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 sg))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
  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 }
    --   ⇝
@ -151,7 +151,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  pushCoe : BindName ->
            (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
            (0 pc : So (canPushCoe sg ty s)) =>
-            Eff Whnf (NonRedex Elim d n defs sg)
+            Eff Whnf (NonRedex Elim d n defs ctx sg)
  pushCoe i ty p q s loc =
    case ty of
      -- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/lib/Quox/Whnf/ComputeElimType.idr
@ -14,8 +14,8 @@ export covering
 computeElimType :
  CanWhnf Term Interface.isRedexT =>
  CanWhnf Elim Interface.isRedexE =>
-  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
-  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
+  (defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
  Eff Whnf (Term d n)


@ -24,8 +24,8 @@ export covering
 computeWhnfElimType0 :
  CanWhnf Term Interface.isRedexT =>
  CanWhnf Elim Interface.isRedexE =>
-  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
-  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
+  (defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
  Eff Whnf (Term d n)

 computeElimType defs ctx sg e =
@ -36,7 +36,7 @@ computeElimType defs ctx sg e =
      pure $ def.typeWithAt ctx.dimLen ctx.termLen u

    B i _ =>
-      pure $ ctx.tctx !! i
+      pure (ctx.tctx !! i).type

    App f s loc =>
      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@ -18,13 +18,14 @@ Whnf = [Except Error, NameGen]

 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = {0 d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
+RedexTest tm =
+  {0 d, n : Nat} -> Definitions -> WhnfContext d n -> SQty -> tm d n -> Bool

 public export
 interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
  whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
-         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs q))
+         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
  -- 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
@ -37,19 +38,20 @@ whnf0 defs ctx q t = fst <$> whnf defs ctx q t

 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-                      Definitions -> SQty -> Pred (tm d n)
-IsRedex  defs q = So . isRedex defs q
-NotRedex defs q = No . isRedex defs q
+                      Definitions -> WhnfContext d n -> SQty -> Pred (tm d n)
+IsRedex  defs ctx q = So . isRedex defs ctx q
+NotRedex defs ctx q = No . isRedex defs ctx q

 public export
 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
             CanWhnf tm isRedex => (d, n : Nat) ->
-             (defs : Definitions) -> SQty -> Type
-NonRedex tm d n defs q = Subset (tm d n) (NotRedex defs q)
+             Definitions -> WhnfContext d n -> SQty -> Type
+NonRedex tm d n defs ctx q = Subset (tm d n) (NotRedex defs ctx q)

 public export %inline
 nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
-       (t : tm d n) -> (0 nr : NotRedex defs q t) => NonRedex tm d n defs q
+       (t : tm d n) -> (0 nr : NotRedex defs ctx q t) =>
+       NonRedex tm d n defs ctx q
 nred t = Element t nr


@ -193,50 +195,52 @@ mutual
  ||| a reducible elimination
  |||
  ||| 1. a free variable, if its definition is known
-  ||| 2. an elimination whose head is reducible
-  ||| 3. an "active" elimination:
+  ||| 2. a bound variable pointing to a `let`
+  ||| 3. an elimination whose head is reducible
+  ||| 4. an "active" elimination:
  |||    an application whose head is an annotated lambda,
  |||    a case expression whose head is an annotated constructor form, etc
-  ||| 4. a redundant annotation, or one whose term or type is reducible
-  ||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
+  ||| 5. a redundant annotation, or one whose term or type is reducible
+  ||| 6. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
  |||      a. `A` is reducible or a type constructor, or
  |||      b. `𝑖` is not mentioned in `A`
  |||         ([fixme] should be A‹0/𝑖› = A‹1/𝑖›), or
  |||      c. `p = q`
-  ||| 6. a composition `comp A @p @q s @r {⋯}`
+  ||| 7. a composition `comp A @p @q s @r {⋯}`
  |||    where `p = q`, `r = 0`, or `r = 1`
-  ||| 7. a closure
+  ||| 8. a closure
  public export
  isRedexE : RedexTest Elim
-  isRedexE defs sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
-  isRedexE _ sg (B {}) = False
-  isRedexE defs sg (App {fun, _}) =
-    isRedexE defs sg fun || isLamHead fun
-  isRedexE defs sg (CasePair {pair, _}) =
-    isRedexE defs sg pair || isPairHead pair || isYes (sg `decEq` SZero)
-  isRedexE defs sg (Fst pair _) =
-    isRedexE defs sg pair || isPairHead pair
-  isRedexE defs sg (Snd pair _) =
-    isRedexE defs sg pair || isPairHead pair
-  isRedexE defs sg (CaseEnum {tag, _}) =
-    isRedexE defs sg tag || isTagHead tag
-  isRedexE defs sg (CaseNat {nat, _}) =
-    isRedexE defs sg nat || isNatHead nat
-  isRedexE defs sg (CaseBox {box, _}) =
-    isRedexE defs sg box || isBoxHead box
-  isRedexE defs sg (DApp {fun, arg, _}) =
-    isRedexE defs sg fun || isDLamHead fun || isK arg
-  isRedexE defs sg (Ann {tm, ty, _}) =
-    isE tm || isRedexT defs sg tm || isRedexT defs SZero ty
-  isRedexE defs sg (Coe {ty = S _ (N _), _}) = True
-  isRedexE defs sg (Coe {ty = S _ (Y ty), p, q, val, _}) =
-    isRedexT defs SZero ty || canPushCoe sg ty val || isYes (p `decEqv` q)
-  isRedexE defs sg (Comp {ty, p, q, r, _}) =
+  isRedexE defs ctx sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
+  isRedexE _    ctx sg (B {i, _}) = isJust (ctx.tctx !! i).term
+  isRedexE defs ctx sg (App {fun, _}) =
+    isRedexE defs ctx sg fun || isLamHead fun
+  isRedexE defs ctx sg (CasePair {pair, _}) =
+    isRedexE defs ctx sg pair || isPairHead pair || isYes (sg `decEq` SZero)
+  isRedexE defs ctx sg (Fst pair _) =
+    isRedexE defs ctx sg pair || isPairHead pair
+  isRedexE defs ctx sg (Snd pair _) =
+    isRedexE defs ctx sg pair || isPairHead pair
+  isRedexE defs ctx sg (CaseEnum {tag, _}) =
+    isRedexE defs ctx sg tag || isTagHead tag
+  isRedexE defs ctx sg (CaseNat {nat, _}) =
+    isRedexE defs ctx sg nat || isNatHead nat
+  isRedexE defs ctx sg (CaseBox {box, _}) =
+    isRedexE defs ctx sg box || isBoxHead box
+  isRedexE defs ctx sg (DApp {fun, arg, _}) =
+    isRedexE defs ctx sg fun || isDLamHead fun || isK arg
+  isRedexE defs ctx sg (Ann {tm, ty, _}) =
+    isE tm || isRedexT defs ctx sg tm || isRedexT defs ctx SZero ty
+  isRedexE defs ctx sg (Coe {ty = S _ (N _), _}) = True
+  isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, q, val, _}) =
+    isRedexT defs (extendDim i ctx) SZero ty ||
+    canPushCoe sg ty val || isYes (p `decEqv` q)
+  isRedexE defs ctx sg (Comp {ty, p, q, r, _}) =
    isYes (p `decEqv` q) || isK r
-  isRedexE defs sg (TypeCase {ty, ret, _}) =
-    isRedexE defs sg ty || isRedexT defs sg ret || isAnnTyCon ty
-  isRedexE _ _ (CloE  {}) = True
-  isRedexE _ _ (DCloE {}) = True
+  isRedexE defs ctx sg (TypeCase {ty, ret, _}) =
+    isRedexE defs ctx sg ty || isRedexT defs ctx sg ret || isAnnTyCon ty
+  isRedexE _ _ _ (CloE  {}) = True
+  isRedexE _ _ _ (DCloE {}) = True

  ||| a reducible term
  |||
@ -248,9 +252,9 @@ mutual
  ||| 5. a `let` expression
  public export
  isRedexT : RedexTest Term
-  isRedexT _    _  (CloT  {})  = True
-  isRedexT _    _  (DCloT {})  = True
-  isRedexT _    _  (Let   {})  = True
-  isRedexT defs sg (E {e, _})  = isAnn e || isRedexE defs sg e
-  isRedexT _    _  (Succ p {}) = isNatConst p
-  isRedexT _    _  _           = False
+  isRedexT _    _   _  (CloT  {})  = True
+  isRedexT _    _   _  (DCloT {})  = True
+  isRedexT _    _   _  (Let   {})  = True
+  isRedexT defs ctx sg (E {e, _})  = isAnn e || isRedexE defs ctx sg e
+  isRedexT _    _   _  (Succ p {}) = isNatConst p
+  isRedexT _    _   _  _           = False
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@ -20,7 +20,10 @@ CanWhnf Elim Interface.isRedexE where
    _ | Just y  = whnf defs ctx sg $ setLoc loc $ injElim ctx y
    _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah

-  whnf _ _ _ (B i loc) = pure $ nred $ B i loc
+  whnf defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
+    _ | l with (l.term) proof eq2
+      _ | Just y  = whnf defs ctx sg $ Ann y l.type loc
+      _ | Nothing = pure $ Element (B i loc) $ rewrite eq1 in rewrite eq2 in Ah

  -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
  whnf defs ctx sg (App f s appLoc) = do
--- a/lib/Quox/Whnf/TypeCase.idr
+++ b/lib/Quox/Whnf/TypeCase.idr
@ -35,7 +35,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  ||| 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 SZero t)) =>
+  tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
             Eff Whnf (Term d n, ScopeTerm d n)
  tycasePi (Pi {arg, res, _}) = pure (arg, res)
  tycasePi (E e) {tnf} = do
@ -53,7 +53,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  ||| 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 SZero t)) =>
+  tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
              Eff Whnf (Term d n, ScopeTerm d n)
  tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
  tycaseSig (E e) {tnf} = do
@ -71,7 +71,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  ||| 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 SZero t)) =>
+  tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
              Eff Whnf (Term d n)
  tycaseBOX (BOX {ty, _}) = pure ty
  tycaseBOX (E e) {tnf} = do
@ -83,7 +83,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  ||| 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 SZero t)) =>
+  tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero 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
@ -107,7 +107,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
  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 SZero))
+                   Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx SZero))
  reduceTypeCase ty u ret arms def loc = case ty of
    -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
    TYPE {} =>