Move some definitions from AST to Data

3 files changed, 28 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
diff --git a/src/Data.hs b/src/Data.hs
index bd7f3af..728dafe 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveTraversable #-}
 module Data where
 
 
@@ -17,3 +18,27 @@ infixr `SCons`
 slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list
 slistMap _ SNil = SNil
 slistMap f (SCons x list) = SCons (f x) (slistMap f list)
+
+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)
+
+fromSNat :: SNat n -> Int
+fromSNat SZ = 0
+fromSNat (SS n) = succ (fromSNat 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)
+
+vecLength :: Vec n t -> SNat n
+vecLength VNil = SZ
+vecLength (_ :< v) = SS (vecLength v)
diff --git a/src/Simplify.hs b/src/Simplify.hs
index cbeee75..44de164 100644
--- a/src/Simplify.hs
+++ b/src/Simplify.hs
@@ -7,6 +7,7 @@ module Simplify where
 
 import AST
 import AST.Count
+import Data
 
 
 simplifyN :: Int -> Ex env t -> Ex env t