From eb25e315ac8bd1e75498cc92c7f3326fa582171a Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sun, 22 Feb 2026 12:59:40 +0100
Subject: WIP: Store subset of D1 Gamma for recompute at binding sites

---
 src/CHAD/Data.hs | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/CHAD/Data.hs')

diff --git a/src/CHAD/Data.hs b/src/CHAD/Data.hs
index 8c7605c..63bce5d 100644
--- a/src/CHAD/Data.hs
+++ b/src/CHAD/Data.hs
@@ -10,6 +10,7 @@
 {-# LANGUAGE TypeOperators #-}
 module CHAD.Data (module CHAD.Data, (:~:)(Refl), If) where
 
+import Data.Bifunctor (first)
 import Data.Functor.Product
 import Data.GADT.Compare
 import Data.GADT.Show
@@ -55,6 +56,10 @@ sappend :: SList f l1 -> SList f l2 -> SList f (Append l1 l2)
 sappend SNil l = l
 sappend (SCons x xs) l = SCons x (sappend xs l)
 
+sunappend :: forall l2 l1 f g. SList f l1 -> SList g (Append l1 l2) -> (SList g l1, SList g l2)
+sunappend SNil l = (SNil, l)
+sunappend (SCons _ l1) (SCons x l) = first (SCons x) (sunappend l1 l)
+
 type family Replicate n x where
   Replicate Z x = '[]
   Replicate (S n) x = x : Replicate n x
-- 
cgit v1.2.3-70-g09d2