1 files changed, 2 insertions, 30 deletions
diff --git a/src/AST.hs b/src/AST.hs
index d1ef633..aeab1b7 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -24,22 +24,6 @@ import AST.Weaken
 import Data
 
 
-data Nat = Z | S Nat
-  deriving (Show, Eq, Ord)
-
-data SNat n where
-  SZ :: SNat Z
-  SS :: SNat n -> SNat (S n)
-deriving instance Show (SNat n)
-
-data Vec n t where
-  VNil :: Vec Z t
-  (:<) :: t -> Vec n t -> Vec (S n) t
-deriving instance Show t => Show (Vec n t)
-deriving instance Functor (Vec n)
-deriving instance Foldable (Vec n)
-deriving instance Traversable (Vec n)
-
 data Ty
   = TNil
   | TPair Ty Ty
@@ -205,14 +189,6 @@ unSScalTy = \case
   STF64 -> TF64
   STBool -> TBool
 
-fromNat :: Nat -> Int
-fromNat Z = 0
-fromNat (S n) = succ (fromNat n)
-
-vecLength :: Vec n t -> SNat n
-vecLength VNil = SZ
-vecLength (_ :< v) = SS (vecLength v)
-
 weakenExpr :: env :> env' -> Expr x env t -> Expr x env' t
 weakenExpr w = \case
   EVar x t i -> EVar x t (w @> i)
@@ -225,11 +201,11 @@ weakenExpr w = \case
   EInr x t e -> EInr x t (weakenExpr w e)
   ECase x e1 e2 e3 -> ECase x (weakenExpr w e1) (weakenExpr (WCopy w) e2) (weakenExpr (WCopy w) e3)
   EBuild1 x e1 e2 -> EBuild1 x (weakenExpr w e1) (weakenExpr (WCopy w) e2)
-  EBuild x es e -> EBuild x (weakenVec w es) (weakenExpr (wcopyN (vecLength es) w) e)
+  EBuild x es e -> EBuild x (weakenExpr w <$> es) (weakenExpr (wcopyN (vecLength es) w) e)
   EFold1 x e1 e2 -> EFold1 x (weakenExpr (WCopy (WCopy w)) e1) (weakenExpr w e2)
   EConst x t v -> EConst x t v
   EIdx1 x e1 e2 -> EIdx1 x (weakenExpr w e1) (weakenExpr w e2)
-  EIdx x e1 es -> EIdx x (weakenExpr w e1) (weakenVec w es)
+  EIdx x e1 es -> EIdx x (weakenExpr w e1) (weakenExpr w <$> es)
   EOp x op e -> EOp x op (weakenExpr w e)
   EMOne t i e -> EMOne t i (weakenExpr w e)
   EMScope e -> EMScope (weakenExpr w e)
@@ -249,10 +225,6 @@ wpopN :: SNat n -> ConsN n TIx env :> env' -> env :> env'
 wpopN SZ w = w
 wpopN (SS n) w = wpopN n (WPop w)
 
-weakenVec :: (env :> env') -> Vec n (Expr x env TIx) -> Vec n (Expr x env' TIx)
-weakenVec _ VNil = VNil
-weakenVec w (e :< v) = weakenExpr w e :< weakenVec w v
-
 slistIdx :: SList f list -> Idx list t -> f t
 slistIdx (SCons x _) IZ = x
 slistIdx (SCons _ list) (IS i) = slistIdx list i