From 4acecc1099caefc2bd2fbe252d30d52ead2c74be Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sun, 27 Oct 2024 22:02:18 +0100
Subject: WIP preserve only subset of D0 bindings in dual (...)

The point of this is to ensure that when an expression occurs in a
Build, then the parts of D0 that are only there to make sharing work out
for D1 are not laboriously taped in an array and preserved for D2, only
for D2 to ignore them.

However, while the subtape machinery is a good first step, this is not
everything: the current Build translation makes a Build for the
(elementwise) tape and separately a build for the primal. Because the
primal _does_ generally need the subtaped-away stuff, we can't just not
tape those.

TODO: figure out how to resolve this / what the next step is.
---
 src/AST/Env.hs | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

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

diff --git a/src/AST/Env.hs b/src/AST/Env.hs
index c33bad3..4f34166 100644
--- a/src/AST/Env.hs
+++ b/src/AST/Env.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -14,8 +15,8 @@ import Data
 -- @env'@ ('SEYes') or not included in @env'@ ('SENo').
 data Subenv env env' where
   SETop :: Subenv '[] '[]
-  SEYes :: Subenv env env' -> Subenv (t : env) (t : env')
-  SENo  :: Subenv env env' -> Subenv (t : env) env'
+  SEYes :: forall t env env'. Subenv env env' -> Subenv (t : env) (t : env')
+  SENo  :: forall t env env'. Subenv env env' -> Subenv (t : env) env'
 deriving instance Show (Subenv env env')
 
 subList :: SList f env -> Subenv env env' -> SList f env'
@@ -41,3 +42,18 @@ subenvCompose SETop SETop = SETop
 subenvCompose (SEYes sub1) (SEYes sub2) = SEYes (subenvCompose sub1 sub2)
 subenvCompose (SEYes sub1) (SENo sub2) = SENo (subenvCompose sub1 sub2)
 subenvCompose (SENo sub1) sub2 = SENo (subenvCompose sub1 sub2)
+
+subenvConcat :: Subenv env1 env1' -> Subenv env2 env2' -> Subenv (Append env2 env1) (Append env2' env1')
+subenvConcat sub1 SETop = sub1
+subenvConcat sub1 (SEYes sub2) = SEYes (subenvConcat sub1 sub2)
+subenvConcat sub1 (SENo sub2) = SENo (subenvConcat sub1 sub2)
+
+sinkWithSubenv :: Subenv env env' -> env0 :> Append env' env0
+sinkWithSubenv SETop = WId
+sinkWithSubenv (SEYes sub) = WSink .> sinkWithSubenv sub
+sinkWithSubenv (SENo sub) = sinkWithSubenv sub
+
+wUndoSubenv :: Subenv env env' -> env' :> env
+wUndoSubenv SETop = WId
+wUndoSubenv (SEYes sub) = WCopy (wUndoSubenv sub)
+wUndoSubenv (SENo sub) = WSink .> wUndoSubenv sub
-- 
cgit v1.2.3-70-g09d2