From 84e1cc78cce7f895da8b9da3da50301a18edab5a Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Mar 2023 16:09:47 +0200
Subject: [PATCH] use a SnocVect for subN

---
 lib/Quox/Reduce.idr            |  6 +++---
 lib/Quox/Syntax/Subst.idr      | 10 +++++-----
 lib/Quox/Syntax/Term/Subst.idr | 14 +++++++-------
 lib/Quox/Typechecker.idr       |  6 ++----
 4 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index e52a0f8..940c648 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -3,7 +3,7 @@ module Quox.Reduce
 import Quox.No
 import Quox.Syntax
 import Quox.Definition
-import Data.Vect
+import Data.SnocVect
 import Data.Maybe
 import Data.List
 
@@ -138,7 +138,7 @@ mutual
               fst = fst :# tfst
               snd = snd :# sub1 tsnd fst
           in
-          whnf defs $ subN body [fst, snd] :# sub1 ret pair
+          whnf defs $ subN body [< fst, snd] :# sub1 ret pair
         Right np =>
           pure $ Element (CasePair pi pair ret body)
                          (pairnf `orNo` np)
@@ -165,7 +165,7 @@ mutual
             Zero :# Nat => whnf defs (zer :# ty)
             Succ n :# Nat =>
               let nn = n :# Nat
-                  tm = subN suc [nn, CaseNat pi piIH nn ret zer suc]
+                  tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc]
               in
               whnf defs $ tm :# ty
         Right nn =>
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index 157698f..4c744bc 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -7,7 +7,7 @@ import Quox.Pretty
 
 import Data.Nat
 import Data.List
-import Data.Vect
+import Data.SnocVect
 
 %default total
 
@@ -101,13 +101,13 @@ drop1 (t ::: th) = th
 
 
 public export
-fromVect : Vect s (f n) -> Subst f (s + n) n
-fromVect []        = id
-fromVect (x :: xs) = x ::: fromVect xs
+fromSnocVect : SnocVect s (f n) -> Subst f (s + n) n
+fromSnocVect [<]       = id
+fromSnocVect (xs :< x) = x ::: fromSnocVect xs
 
 public export %inline
 one : f n -> Subst f (S n) n
-one x = fromVect [x]
+one x = fromSnocVect [< x]
 
 
 ||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 49e4211..55be4a4 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -2,7 +2,7 @@ module Quox.Syntax.Term.Subst
 
 import Quox.No
 import Quox.Syntax.Term.Base
-import Data.Vect
+import Data.SnocVect
 
 %default total
 
@@ -172,22 +172,22 @@ parameters {s : Nat}
 
 
 export %inline
-subN : ScopeTermN s q d n -> Vect s (Elim q d n) -> Term q d n
-subN (S _ (Y body)) es = body // fromVect es
+subN : ScopeTermN s q d n -> SnocVect s (Elim q d n) -> Term q d n
+subN (S _ (Y body)) es = body // fromSnocVect es
 subN (S _ (N body)) _  = body
 
 export %inline
 sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
-sub1 t e = subN t [e]
+sub1 t e = subN t [< e]
 
 export %inline
-dsubN : DScopeTermN s q d n -> Vect s (Dim d) -> Term q d n
-dsubN (S _ (Y body)) ps = body // fromVect ps
+dsubN : DScopeTermN s q d n -> SnocVect s (Dim d) -> Term q d n
+dsubN (S _ (Y body)) ps = body // fromSnocVect ps
 dsubN (S _ (N body)) _  = body
 
 export %inline
 dsub1 : DScopeTerm q d n -> Dim d -> Term q d n
-dsub1 t p = dsubN t [p]
+dsub1 t p = dsubN t [< p]
 
 
 public export %inline
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 2be7811..b71b50b 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -4,6 +4,7 @@ import public Quox.Typing
 import public Quox.Equal
 
 import Data.List
+import Data.SnocVect
 
 %default total
 
@@ -17,7 +18,6 @@ public export
 CanTC q = CanTC' q IsGlobal
 
 
-
 private
 popQs : HasErr q m => IsQty q =>
         QOutput q s -> QOutput q (s + n) -> m (QOutput q n)
@@ -29,8 +29,6 @@ popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
 popQ pi = popQs [< pi]
 
 
-
-
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
@@ -364,7 +362,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
     unless (zerout == sucout) $ do
       let sucp = Succ $ FT $ unq p
-          suc  = subN suc [F $ unq ih, F $ unq p]
+          suc  = subN suc [< F $ unq p, F $ unq ih]
       throwError $ BadCaseQtys ctx [(zerout, Zero, zer), (sucout, sucp, suc)]
     expectCompatQ qih pi'
     -- [fixme] better error here