diff options
Diffstat (limited to 'src/AST.hs')
| -rw-r--r-- | src/AST.hs | 12 |
1 files changed, 2 insertions, 10 deletions
@@ -21,6 +21,7 @@ import Data.Kind (Type) import Data.Int import AST.Weaken +import Data data Nat = Z | S Nat @@ -39,12 +40,6 @@ deriving instance Functor (Vec n) deriving instance Foldable (Vec n) deriving instance Traversable (Vec n) -data SList f l where - SNil :: SList f '[] - SCons :: f a -> SList f l -> SList f (a : l) -deriving instance (forall a. Show (f a)) => Show (SList f l) -infixr `SCons` - data Ty = TNil | TPair Ty Ty @@ -232,6 +227,7 @@ 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 @@ -273,10 +269,6 @@ 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 -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) - slistIdx :: SList f list -> Idx list t -> f t slistIdx (SCons x _) IZ = x slistIdx (SCons _ list) (IS i) = slistIdx list i |