From 8221d714169d5d3961de8d38b3f7b3bab504da07 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 17 Sep 2023 13:54:26 +0200
Subject: [PATCH] some refactors

---
 lib/Quox/Syntax/Term/Subst.idr    | 40 +++++++++----------
 lib/Quox/Syntax/Term/Tighten.idr  | 65 +++++++++++++------------------
 lib/Quox/Typechecker.idr          |  6 +--
 lib/Quox/Whnf/Coercion.idr        |  8 ++--
 lib/Quox/Whnf/ComputeElimType.idr | 36 +++++++++++------
 lib/Quox/Whnf/Interface.idr       |  2 +-
 lib/Quox/Whnf/Main.idr            | 36 ++++++++---------
 lib/Quox/Whnf/TypeCase.idr        |  4 +-
 8 files changed, 96 insertions(+), 101 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 6a9c899..60f1a11 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -117,6 +117,9 @@ namespace DScopeTermN
 export %inline CanShift (Term d) where s // by = s // Shift by
 export %inline CanShift (Elim d) where e // by = e // Shift by
 
+export %inline CanShift (flip Term n) where s // by = s // Shift by
+export %inline CanShift (flip Elim n) where e // by = e // Shift by
+
 export %inline
 {s : Nat} -> CanShift (ScopeTermN s d) where
   b // by = b // Shift by
@@ -145,29 +148,26 @@ weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
 weakE by t = t // shift by
 
 
-parameters {s : Nat}
-  namespace ScopeTermBody
-    export %inline
-    (.term) : ScopedBody s (Term d) n -> Term d (s + n)
-    (Y b).term = b
-    (N b).term = weakT s b
+parameters {auto _ : CanShift f} {s : Nat}
+  export %inline
+  getTerm : ScopedBody s f n -> f (s + n)
+  getTerm (Y b) = b
+  getTerm (N b) = b // fromNat s
 
-  namespace ScopeTermN
-    export %inline
-    (.term) : ScopeTermN s d n -> Term d (s + n)
-    t.term = t.body.term
+  export %inline
+  (.term) : Scoped s f n -> f (s + n)
+  t.term = getTerm t.body
 
-  namespace DScopeTermBody
-    export %inline
-    (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
-    (Y b).term = b
-    (N b).term = dweakT s b
-
-  namespace DScopeTermN
-    export %inline
-    (.term) : DScopeTermN s d n -> Term (s + d) n
-    t.term = t.body.term
+namespace ScopeTermBody
+  export %inline
+  getTerm0 : ScopedBody 0 f n -> f n
+  getTerm0 (Y b) = b
+  getTerm0 (N b) = b
 
+namespace ScopeTermN
+  export %inline
+  (.term0) : Scoped 0 f n -> f n
+  t.term0 = getTerm0 t.body
 
 export %inline
 subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
index c954070..384ddb1 100644
--- a/lib/Quox/Syntax/Term/Tighten.idr
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -244,25 +244,41 @@ mutual
   dtightenDS = assert_total $ tightenScope dtightenT
 
 
-export [TermD] Tighten (\d => Term d n) where tighten p t = dtightenT p t
-export [ElimD] Tighten (\d => Elim d n) where tighten p e = dtightenE p e
+export Tighten (\d => Term d n) where tighten p t = dtightenT p t
+export Tighten (\d => Elim d n) where tighten p e = dtightenE p e
+
+
+parameters {auto _ : Tighten f} {s : Nat}
+  export
+  squeeze : Scoped s f n -> Either (BContext s, f (s + n)) (f n)
+  squeeze (S ns (N t)) = Right t
+  squeeze (S ns (Y t)) = maybe (Left (ns, t)) Right $ tightenN s t
+
+  export
+  squeeze' : Scoped s f n -> Scoped s f n
+  squeeze' = either (uncurry SY) SN . squeeze
+
+parameters {0 f : Nat -> Nat -> Type}
+           {auto tt : Tighten (\d => f d n)} {s : Nat}
+  export
+  dsqueeze : Scoped s (\d => f d n) d ->
+             Either (BContext s, f (s + d) n) (f d n)
+  dsqueeze = squeeze
+
+  export
+  dsqueeze' : Scoped s (\d => f d n) d -> Scoped s (\d => f d n) d
+  dsqueeze' = squeeze'
 
 
 -- versions of SY, etc, that try to tighten and use SN automatically
 
 public export
 ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n
-ST names body =
-  case tightenN s body of
-    Just body => S names $ N body
-    Nothing   => S names $ Y body
+ST names body = squeeze' $ SY names body
 
 public export
 DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n
-DST names body =
-  case tightenN @{TermD} s body of
-    Just body => S names $ N body
-    Nothing   => S names $ Y body
+DST names body = dsqueeze' {f = Term} $ SY names body
 
 public export %inline
 PiT : (qty : Qty) -> (x : BindName) ->
@@ -302,38 +318,11 @@ typeCase1T ty ret k ns body loc {def} =
   typeCase ty ret [(k ** ST ns body)] def loc
 
 
-export
-squeeze : {s : Nat} -> ScopeTermN s d n -> ScopeTermN s d n
-squeeze (S names (Y body)) = S names $ maybe (Y body) N $ tightenN s body
-squeeze (S names (N body)) = S names $ N body
-
-export
-dsqueeze : {s : Nat} -> DScopeTermN s d n -> DScopeTermN s d n
-dsqueeze (S names (Y body)) =
-  S names $ maybe (Y body) N $ tightenN s body @{TermD}
-dsqueeze (S names (N body)) = S names $ N body
-
-
-export
-squeezed : {s : Nat} -> ScopeTermN s d n ->
-           Either (BContext s, Term d (s + n)) (Term d n)
-squeezed (S ns (N t)) = Right t
-squeezed (S ns (Y t)) = maybe (Left (ns, t)) Right $ tightenN s t
-
-export
-dsqueezed : {s : Nat} -> DScopeTermN s d n ->
-            Either (BContext s, Term (s + d) n) (Term d n)
-dsqueezed (S ns (N t)) = Right t
-dsqueezed (S ns (Y t)) = maybe (Left (ns, t)) Right $ tightenN s t @{TermD}
-
-
-
 public export %inline
 CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
          (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
 CompH' {ty, p, q, val, r, zero, one, loc} =
-  -- [fixme] maintain location of existing B VZ
-  let ty' = DST ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
+  let ty' = DST ty.names $ ty.term // (B VZ ty.name.loc ::: shift 2) in
   Comp {
     ty = dsub1 ty q, p, q,
     val = E $ Coe ty p q val val.loc, r,
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 92c8a5e..3809760 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -460,11 +460,11 @@ mutual
     qout <- checkC ctx sg val ty
     let ty'  = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
         ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
-        val0 = val0.term
+        val0 = getTerm val0
     qout0 <- check ctx0 sg val0 ty'
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) ty' val0 val'
     let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
-        val1  = val1.term
+        val1  = getTerm val1
     qout1 <- check ctx1 sg val1 ty'
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) ty' val1 val'
     let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
@@ -481,7 +481,7 @@ mutual
     for_ allKinds $ \k =>
       for_ (lookupPrecise k arms) $ \(S names t) =>
         check0 (extendTyN (typecaseTel k names u) ctx)
-               t.term (weakT (arity k) ret)
+               (getTerm t) (weakT (arity k) ret)
     -- then Ψ, Γ ⊢₀ type-case ⋯ ⇒ C
     pure $ InfRes {type = ret, qout = zeroFor ctx}
 
diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index 3e6d8a4..de00b91 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -36,7 +36,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     --
     -- 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
+    Element ty tynf <- whnf defs ctx1 $ getTerm ty
     (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
@@ -60,7 +60,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     --
     -- 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
+    Element ty tynf <- whnf defs ctx1 $ getTerm ty
     (tfst, tsnd) <- tycaseSig defs ctx1 ty
     let [< x, y] = body.names
         a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
@@ -82,7 +82,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- 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
+    Element ty tynf <- whnf defs ctx1 $ getTerm ty
     (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
@@ -99,7 +99,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- ⇝
     -- 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
+    Element ty tynf <- whnf defs ctx1 $ getTerm ty
     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
diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr
index dcc5246..7a5d09d 100644
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/lib/Quox/Whnf/ComputeElimType.idr
@@ -17,21 +17,31 @@ computeElimType : CanWhnf Term Interface.isRedexT =>
                   (defs : Definitions) -> WhnfContext d n ->
                   (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
                   Eff Whnf (Term d n)
+
+
+||| computes a type and then reduces it to whnf
+export covering
+computeWhnfElimType0 : 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
+    F x u loc => do
       let Just def = lookup x defs
         | Nothing => throw $ NotInScope loc x
       pure $ def.typeAt u
 
-    B {i, _} =>
+    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
+    App f s loc =>
+      case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
+        Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
+        t                => throw $ ExpectedPi loc ctx.names t
 
     CasePair {pair, ret, _} =>
       pure $ sub1 ret pair
@@ -45,11 +55,10 @@ computeElimType defs ctx e {ne} =
     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
+    DApp {fun = f, arg = p, loc} =>
+      case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
+        Eq {ty, _} => pure $ dsub1 ty p
+        t          => throw $ ExpectedEq loc ctx.names t
 
     Ann {ty, _} =>
       pure ty
@@ -62,3 +71,6 @@ computeElimType defs ctx e {ne} =
 
     TypeCase {ret, _} =>
       pure ret
+
+computeWhnfElimType0 defs ctx e =
+  computeElimType defs ctx e >>= whnf0 defs ctx
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index 5b0aae6..596a812 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -213,7 +213,7 @@ mutual
   isRedexE defs (Coe {ty = S _ (N _), _}) = True
   isRedexE defs (Coe {ty = S _ (Y ty), p, q, val, _}) =
     isRedexT defs ty || canPushCoe ty val || isYes (p `decEqv` q)
-  isRedexE defs (Comp {ty, r, p, q, _}) =
+  isRedexE defs (Comp {ty, p, q, r, _}) =
     isYes (p `decEqv` q) || isK r
   isRedexE defs (TypeCase {ty, ret, _}) =
     isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 0502fa1..fa928ff 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -122,7 +122,7 @@ CanWhnf Elim Interface.isRedexE where
           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
+          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx f
             | ty => throw $ ExpectedEq ty.loc ctx.names ty
           whnf defs ctx $
             ends (Ann (setLoc appLoc l) ty.zero appLoc)
@@ -138,26 +138,25 @@ CanWhnf Elim Interface.isRedexE where
         Element a anf <- whnf defs ctx a
         pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
 
-  whnf defs ctx (Coe ty p q val coeLoc) =
+  whnf defs ctx (Coe sty p q val coeLoc) =
     --   𝑖 ∉ fv(A)
     -- -------------------------------
     --   coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
     --
-    -- [fixme] needs a real equality check between ty.zero and ty.one
-    case dsqueezed ty of
-      Right ty => whnf defs ctx $ Ann val ty coeLoc
+    -- [fixme] needs a real equality check between A‹0/𝑖› and A‹1/𝑖›
+    case dsqueeze sty {f = Term} of
       Left ([< i], ty) =>
         case p `decEqv` q of
           -- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
-          Yes _   => whnf defs ctx $ Ann val (ty // one p) coeLoc
+          Yes _   => whnf defs ctx $ Ann val (dsub1 sty p) coeLoc
           No  npq => do
             Element ty tynf <- whnf defs (extendDim i ctx) ty
             case nchoose $ canPushCoe ty val of
-              Left pc =>
-                pushCoe defs ctx i ty p q val coeLoc
-              Right npc =>
-                pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
-                               (tynf `orNo` npc `orNo` notYesNo npq)
+              Left  pc  => pushCoe defs ctx i ty p q val coeLoc
+              Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
+                                          (tynf `orNo` npc `orNo` notYesNo npq)
+      Right ty =>
+        whnf defs ctx $ Ann val ty coeLoc
 
   whnf defs ctx (Comp ty p q val r zero one compLoc) =
     case p `decEqv` q of
@@ -168,20 +167,17 @@ CanWhnf Elim Interface.isRedexE where
         K Zero _ => whnf defs ctx $ Ann (dsub1 zero q) ty compLoc
         -- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
         K One  _ => whnf defs ctx $ Ann (dsub1 one  q) ty compLoc
-        B {}     =>
-          pure $ Element (Comp ty p q val r zero one compLoc)
-                         (notYesNo npq `orNo` Ah)
+        B {}     => pure $ Element (Comp ty p q val r zero one compLoc)
+                                   (notYesNo npq `orNo` Ah)
 
   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)
+      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
diff --git a/lib/Quox/Whnf/TypeCase.idr b/lib/Quox/Whnf/TypeCase.idr
index 8bc7fd6..ae38a29 100644
--- a/lib/Quox/Whnf/TypeCase.idr
+++ b/lib/Quox/Whnf/TypeCase.idr
@@ -20,8 +20,7 @@ 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
+tycaseRhs0 k arms = map (.term0) $ rewrite sym eq in tycaseRhs k arms
 
 private
 tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
@@ -29,7 +28,6 @@ tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms 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)