From e52a3e7e89f6ad41d4291a467e4c1d3571614b0a Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sat, 16 Sep 2023 11:22:16 +0200
Subject: CHAD case

---
 src/AST/Weaken.hs | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 src/AST/Weaken.hs

(limited to 'src/AST/Weaken.hs')

diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
new file mode 100644
index 0000000..56b7a74
--- /dev/null
+++ b/src/AST/Weaken.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- The reason why this is a separate module with little in it:
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module AST.Weaken where
+
+
+data env :> env' where
+  WId :: env :> env
+  WSink :: env :> (t : env)
+  WCopy :: env :> env' -> (t : env) :> (t : env')
+  WPop :: (t : env) :> env' -> env :> env'
+  WThen :: env1 :> env2 -> env2 :> env3 -> env1 :> env3
+deriving instance Show (env :> env')
+
+(.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
+(.>) = flip WThen
+
+type family Append a b where
+  Append '[] l = l
+  Append (x : xs) l = x : Append xs l
+
+data ListSpine list where
+  LSNil :: ListSpine '[]
+  LSCons :: ListSpine list -> ListSpine (t : list)
+
+class KnownListSpine list where knownListSpine :: ListSpine list
+instance KnownListSpine '[] where knownListSpine = LSNil
+instance KnownListSpine list => KnownListSpine (t : list) where knownListSpine = LSCons knownListSpine
+
+wSinks :: forall list env. KnownListSpine list => env :> Append list env
+wSinks = go (knownListSpine :: ListSpine list)
+  where
+    go :: forall list'. ListSpine list' -> env :> Append list' env
+    go LSNil = WId
+    go (LSCons spine) = WSink .> go spine
-- 
cgit v1.2.3-70-g09d2