Linear-time tape reconstruction

A tutorial of the method here: https://play.haskell.org/saved/uHuGLfHZ

1 files changed, 0 insertions, 16 deletions

diff --git a/src/AST.hs b/src/AST.hs
index 2acc5a7..d1ef633 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -72,12 +72,6 @@ deriving instance Show (SScalTy t)
 
 type TIx = TScal TI64
 
-type Idx :: [k] -> k -> Type
-data Idx env t where
-  IZ :: Idx (t : env) t
-  IS :: Idx env t -> Idx (a : env) t
-deriving instance Show (Idx env t)
-
 type family ScalRep t where
   ScalRep TI32 = Int32
   ScalRep TI64 = Int64
@@ -219,16 +213,6 @@ vecLength :: Vec n t -> SNat n
 vecLength VNil = SZ
 vecLength (_ :< v) = SS (vecLength v)
 
-infixr @>
-(@>) :: env :> env' -> Idx env t -> Idx env' t
-WId @> i = i
-WSink @> i = IS i
-WCopy _ @> IZ = IZ
-WCopy w @> (IS i) = IS (w @> i)
-WPop w @> i = w @> IS i
-WThen w1 w2 @> i = w2 @> w1 @> i
-WClosed _ @> i = case i of {}
-
 weakenExpr :: env :> env' -> Expr x env t -> Expr x env' t
 weakenExpr w = \case
   EVar x t i -> EVar x t (w @> i)