From 183e8b4a07231aae904b8234ddeb1c646c031173 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 19 Sep 2023 21:55:38 +0200
Subject: Stuff
---
src/AST.hs | 29 +++++++++++++++++++++++++----
1 file changed, 25 insertions(+), 4 deletions(-)
(limited to 'src/AST.hs')
diff --git a/src/AST.hs b/src/AST.hs
index 7c5de11..dfc114d 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -11,6 +11,7 @@
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
module AST (module AST, module AST.Weaken) where
import Data.Functor.Const
@@ -30,11 +31,12 @@ data SNat n where
deriving instance (Show (SNat n))
data Vec n t where
- VNil :: Vec n t
+ 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 SList f l where
SNil :: SList f '[]
@@ -92,6 +94,9 @@ type family ConsN n x l where
ConsN Z x l = l
ConsN (S n) x l = x : ConsN n x l
+-- General assumption: head of the list (whatever way it is associated) is the
+-- inner variable / inner array dimension. In pretty printing, the inner
+-- variable / inner dimension is printed on the _right_.
type Expr :: (Ty -> Type) -> [Ty] -> Ty -> Type
data Expr x env t where
-- lambda calculus
@@ -109,7 +114,7 @@ data Expr x env t where
-- array operations
EBuild1 :: x (TArr (S Z) t) -> Expr x env TIx -> Expr x (TIx : env) t -> Expr x env (TArr (S Z) t)
- EBuild :: x (TArr n t) -> SNat n -> Vec n (Expr x env TIx) -> Expr x (ConsN n TIx env) t -> Expr x env (TArr n t)
+ EBuild :: x (TArr n t) -> Vec n (Expr x env TIx) -> Expr x (ConsN n TIx env) t -> Expr x env (TArr n t)
EFold1 :: x (TArr n t) -> Expr x (t : t : env) t -> Expr x env (TArr (S n) t) -> Expr x env (TArr n t)
-- expression operations
@@ -168,7 +173,7 @@ typeOf = \case
ECase _ _ a _ -> typeOf a
EBuild1 _ _ e -> STArr (SS SZ) (typeOf e)
- EBuild _ n _ e -> STArr n (typeOf e)
+ EBuild _ es e -> STArr (vecLength es) (typeOf e)
EFold1 _ _ e | STArr (SS n) t <- typeOf e -> STArr n t
EConst _ t _ -> STScal t
@@ -212,6 +217,10 @@ 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)
+
infixr @>
(@>) :: env :> env' -> Idx env t -> Idx env' t
WId @> i = i
@@ -233,7 +242,7 @@ 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 n es e -> EBuild x n (weakenVec w es) (weakenExpr (wcopyN n w) e)
+ EBuild x es e -> EBuild x (weakenVec 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)
@@ -245,10 +254,18 @@ weakenExpr w = \case
EMBind e1 e2 -> EMBind (weakenExpr w e1) (weakenExpr (WCopy w) e2)
EError t s -> EError t s
+wsinkN :: SNat n -> env :> ConsN n TIx env
+wsinkN SZ = WId
+wsinkN (SS n) = WSink .> wsinkN n
+
wcopyN :: SNat n -> env :> env' -> ConsN n TIx env :> ConsN n TIx env'
wcopyN SZ w = w
wcopyN (SS n) w = WCopy (wcopyN n w)
+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
@@ -256,3 +273,7 @@ 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)
+
+idx2int :: Idx env t -> Int
+idx2int IZ = 0
+idx2int (IS n) = 1 + idx2int n
--
cgit v1.2.3-70-g09d2