use a SnocVect for subN

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 =>

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
+fromSnocVect : SnocVect s (f n) -> Subst f (s + n) n
-fromVect []        = id
+fromSnocVect [<]       = id
-fromVect (x :: xs) = x ::: fromVect xs
+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`,

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 : ScopeTermN s q d n -> SnocVect s (Elim q d n) -> Term q d n
-subN (S _ (Y body)) es = body // fromVect es
+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 : DScopeTermN s q d n -> SnocVect s (Dim d) -> Term q d n
-dsubN (S _ (Y body)) ps = body // fromVect ps
+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

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