improve handling of context lengths

lib/Quox/Definition.idr

@@ -7,6 +7,7 @@ import public Data.SortedMap
 import public Quox.Loc
 import Quox.Pretty
 import Control.Eff
+import Data.Singleton
 import Decidable.Decidable
 
 
@@ -63,6 +64,18 @@ parameters {d, n : Nat}
   toElim : Definition -> Universe -> Maybe $ Elim d n
   toElim def u = pure $ Ann !(def.termAt u) (def.typeAt u) def.loc
 
+public export
+(.typeWith) : Definition -> Singleton d -> Singleton n -> Term d n
+g.typeWith (Val d) (Val n) = g.type
+
+public export
+(.typeWithAt) : Definition -> Singleton d -> Singleton n -> Universe -> Term d n
+g.typeWithAt d n u = displace u $ g.typeWith d n
+
+public export
+(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Term d n)
+g.termWith (Val d) (Val n) = g.term
+
 
 public export %inline
 isZero : Definition -> Bool
@@ -84,11 +97,14 @@ public export
 DefsState : Type -> Type
 DefsState = StateL DEFS Definitions
 
-
 public export %inline
 lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
 lookupElim x u defs = toElim !(lookup x defs) u
 
+public export %inline
+lookupElim0 : Name -> Universe -> Definitions -> Maybe (Elim 0 0)
+lookupElim0 = lookupElim
+
 
 export
 prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)

lib/Quox/Equal.idr

@@ -70,7 +70,7 @@ sameTyCon (E    {}) _         = False
 ||| * `[π.A]` is empty if `A` is.
 ||| * that's it.
 public export covering
-isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
+isEmpty : Definitions -> EqContext n -> SQty -> Term 0 n ->
           Eff EqualInner Bool
 isEmpty defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
@@ -100,7 +100,7 @@ isEmpty defs ctx sg ty0 = do
 ||| * an enum type is a subsingleton if it has zero or one tags.
 ||| * a box type is a subsingleton if its content is
 public export covering
-isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
+isSubSing : Definitions -> EqContext n -> SQty -> Term 0 n ->
             Eff EqualInner Bool
 isSubSing defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
@@ -175,7 +175,7 @@ namespace Term
     --              Γ ⊢ A empty
     -- -------------------------------------------
     --  Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
-    if !(isEmpty' arg) then pure () else
+    if !(isEmpty defs ctx sg arg) then pure () else
     case (s, t) of
       --           Γ, x : A ⊢ s = t : B
       -- -------------------------------------------
@@ -195,9 +195,6 @@ namespace Term
       (E _,    t) => wrongType t.loc ctx ty t
       (s,      _) => wrongType s.loc ctx ty s
   where
-    isEmpty' : Term 0 n -> Eff EqualInner Bool
-    isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx sg arg
-
     ctx' : EqContext (S n)
     ctx' = extendTy qty res.name arg ctx
 
@@ -390,9 +387,9 @@ lookupFree : Has ErrorEff fs =>
              Definitions -> EqContext n -> Name -> Universe -> Loc ->
              Eff fs (Term 0 n)
 lookupFree defs ctx x u loc =
-  let Val n = ctx.termLen in
-  maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $
-  lookup x defs
+  case lookup x defs of
+    Nothing => throw $ NotInScope loc x
+    Just d  => pure $ d.typeWithAt [|Z|] ctx.termLen u
 
 
 namespace Elim
@@ -410,9 +407,8 @@ namespace Elim
   computeElimTypeE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
                      (e : Elim 0 n) -> (0 ne : NotRedex defs sg e) =>
                      Eff EqualElim (Term 0 n)
-  computeElimTypeE defs ectx sg e =
-    let Val n = ectx.termLen in
-    lift $ computeElimType defs (toWhnfContext ectx) sg e
+  computeElimTypeE defs ectx sg e = lift $
+    computeElimType defs (toWhnfContext ectx) sg e
 
   private
   putError : Has InnerErrEff fs => Error -> Eff fs ()
@@ -701,7 +697,6 @@ namespace Elim
     clashE defs ctx sg e f
 
   compare0Inner defs ctx sg e f = do
-    let Val n = ctx.termLen
     Element e ne <- whnf defs ctx sg e.loc e
     Element f nf <- whnf defs ctx sg f.loc f
     ty <- compare0Inner' defs ctx sg e f ne nf
@@ -714,7 +709,6 @@ namespace Elim
 namespace Term
   compare0 defs ctx sg ty s t =
     wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
-      let Val n = ctx.termLen
       Element ty' _ <- whnf defs ctx SZero ty.loc ty
       Element s'  _ <- whnf defs ctx sg s.loc  s
       Element t'  _ <- whnf defs ctx sg t.loc  t
@@ -727,7 +721,6 @@ namespace Elim
     maybe (pure ty) throw err
 
 compareType defs ctx s t = do
-  let Val n = ctx.termLen
   Element s' _ <- whnf defs ctx SZero s.loc s
   Element t' _ <- whnf defs ctx SZero t.loc t
   ts <- ensureTyCon s.loc ctx s'
@@ -747,7 +740,6 @@ parameters (loc : Loc) (ctx : TyContext d n)
     eachFace : Applicative f => FreeVars d ->
                (EqContext n -> DSubst d 0 -> f ()) -> f ()
     eachFace fvs act =
-      let Val d = ctx.dimLen in
       for_ (splits loc ctx.dctx fvs) $ \th =>
         act (makeEqContext ctx th) th
 
@@ -762,8 +754,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
 
     private
     fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
-    fdvAll ts =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in foldMap fdv ts
+    fdvAll = let Val d = ctx.dimLen in foldMap (fdvWith [|d|] ctx.termLen)
 
     namespace Term
       export covering

lib/Quox/FreeVars.idr

@@ -93,6 +93,14 @@ interface HasFreeDVars (0 tm : TermLike) where
   constructor HFDV
   fdv : {d, n : Nat} -> tm d n -> FreeVars d
 
+public export %inline
+fvWith : HasFreeVars tm => Singleton n -> tm n -> FreeVars n
+fvWith (Val n) = fv
+
+public export %inline
+fdvWith : HasFreeDVars tm => Singleton d -> Singleton n -> tm d n -> FreeVars d
+fdvWith (Val d) (Val n) = fdv
+
 export
 Fdv : (0 tm : TermLike) -> {n : Nat} ->
       HasFreeDVars tm => HasFreeVars (\d => tm d n)

lib/Quox/Typechecker.idr

@@ -328,8 +328,10 @@ mutual
     -- if σ ≤ π
     expectCompatQ loc sg.qty g.qty.qty
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
-    let Val d = ctx.dimLen; Val n = ctx.termLen
-    pure $ InfRes {type = g.typeAt u, qout = zeroFor ctx}
+    pure $ InfRes {
+      type = g.typeWithAt ctx.dimLen ctx.termLen u,
+      qout = zeroFor ctx
+    }
 
   infer' ctx sg (B i _) =
     -- if x : A ∈ Γ

lib/Quox/Typing.idr

@@ -118,7 +118,6 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
            tm 0 n -> Eff fs (NonRedex tm 0 n defs sg)
     whnf tm = do
-      let Val n = ctx.termLen
       res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 

lib/Quox/Typing/Context.idr

@@ -58,6 +58,8 @@ record EqContext n where
 public export
 record WhnfContext d n where
   constructor MkWhnfContext
+  {auto dimLen  : Singleton d}
+  {auto termLen : Singleton n}
   dnames : BContext d
   tnames : BContext n
   tctx   : TContext d n
@@ -232,6 +234,12 @@ namespace EqContext
   toWhnfContext (MkEqContext {tnames, tctx, _}) =
     MkWhnfContext {dnames = [<], tnames, tctx}
 
+  export
+  injElim : WhnfContext d n -> Elim 0 0 -> Elim d n
+  injElim ctx e =
+    let Val d = ctx.dimLen; Val n = ctx.termLen in
+    e // shift0 d // shift0 n
+
 namespace WhnfContext
   public export %inline
   empty : WhnfContext 0 0
@@ -240,8 +248,9 @@ namespace WhnfContext
   export
   extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
                WhnfContext (s + d) n
-  extendDimN ns (MkWhnfContext {dnames, tnames, tctx}) =
+  extendDimN ns (MkWhnfContext {dnames, tnames, tctx, dimLen}) =
     MkWhnfContext {
+      dimLen = [|Val s + dimLen|],
       dnames = dnames ++ toSnocVect' ns,
       tctx   = dweakT s <$> tctx,
       tnames

lib/Quox/Untyped/Erase.idr

@@ -86,18 +86,16 @@ export covering
 whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
         ErasureContext d n -> SQty ->
         tm d n -> Eff Erase (tm d n)
-whnf0 ctx sg tm = do
-  let Val n = ctx.termLen; Val d = ctx.dimLen
-  liftWhnf $ whnf0 !(askAt DEFS) (toWhnfContext ctx) sg tm
+whnf0 ctx sg tm = liftWhnf $ whnf0 !(askAt DEFS) (toWhnfContext ctx) sg tm
 
 export covering
 computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n)
 computeElimType ctx sg e = do
-  let Val n = ctx.termLen; Val d = ctx.dimLen
-      ctx   = toWhnfContext ctx
-  defs          <- askAt DEFS
-  Element e enf <- liftWhnf $ whnf defs ctx sg e
-  liftWhnf $ computeElimType defs ctx sg e
+  defs <- askAt DEFS
+  liftWhnf $ do
+    let ctx = toWhnfContext ctx
+    Element e enf <- whnf defs ctx sg e
+    computeElimType defs ctx sg e
 
 
 parameters (ctx : ErasureContext d n) (loc : Loc)
@@ -279,9 +277,7 @@ eraseElim ctx e@(F x u loc) = do
     | Nothing => throw $ NotInScope x
   case isErased def.qty.qty of
     Erased => throw $ CompileTimeOnly ctx $ E e
-    Kept =>
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      pure $ EraRes def.type $ F x loc
+    Kept   => pure $ EraRes (def.typeWith ctx.dimLen ctx.termLen) $ F x loc
 
 --            π ≠ 0
 -- ----------------------------

lib/Quox/Whnf/Coercion.idr

@@ -23,7 +23,7 @@ where
 
 parameters {auto _ : CanWhnf Term Interface.isRedexT}
            {auto _ : CanWhnf Elim Interface.isRedexE}
-           {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
+           (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
   ||| reduce a function application `App (Coe ty p q val) s loc`
   export covering
   piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->

lib/Quox/Whnf/ComputeElimType.idr

@@ -14,7 +14,6 @@ export covering
 computeElimType :
   CanWhnf Term Interface.isRedexT =>
   CanWhnf Elim Interface.isRedexE =>
-  {d, n : Nat} ->
   (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
   (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
   Eff Whnf (Term d n)
@@ -25,7 +24,6 @@ export covering
 computeWhnfElimType0 :
   CanWhnf Term Interface.isRedexT =>
   CanWhnf Elim Interface.isRedexE =>
-  {d, n : Nat} ->
   (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
   (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
   Eff Whnf (Term d n)
@@ -35,7 +33,7 @@ computeElimType defs ctx sg e =
     F x u loc => do
       let Just def = lookup x defs
         | Nothing => throw $ NotInScope loc x
-      pure $ def.typeAt u
+      pure $ def.typeWithAt ctx.dimLen ctx.termLen u
 
     B i _ =>
       pure $ ctx.tctx !! i

lib/Quox/Whnf/Interface.idr

@@ -18,13 +18,12 @@ Whnf = [NameGen, Except Error]
 
 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = {d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
+RedexTest tm = {0 d, n : Nat} -> Definitions -> SQty -> 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) -> (q : SQty) ->
+  whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
          tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs 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.
@@ -32,7 +31,7 @@ where
   -- 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 =>
+whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
         Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
 whnf0 defs ctx q t = fst <$> whnf defs ctx q t
 
@@ -194,8 +193,7 @@ mutual
   ||| 7. a closure
   public export
   isRedexE : RedexTest Elim
-  isRedexE defs sg (F {x, u, _}) {d, n} =
-    isJust $ lookupElim x u defs {d, n}
+  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

lib/Quox/Whnf/Main.idr

@@ -16,8 +16,8 @@ export covering CanWhnf Elim Interface.isRedexE
 
 covering
 CanWhnf Elim Interface.isRedexE where
-  whnf defs ctx sg (F x u loc) with (lookupElim x u defs) proof eq
-    _ | Just y  = whnf defs ctx sg $ setLoc loc y
+  whnf defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
+    _ | 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

lib/Quox/Whnf/TypeCase.idr

@@ -30,7 +30,7 @@ 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)
+           (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