diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2026-02-22 12:59:40 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2026-02-22 12:59:40 +0100 |
| commit | eb25e315ac8bd1e75498cc92c7f3326fa582171a (patch) | |
| tree | 71df3e761c127ad3ca301a0645ae7760099088ae /src/CHAD/Data.hs | |
| parent | f5b1b405fa4ba63bdffe0f2998f655f0b06534bf (diff) | |
WIP: Store subset of D1 Gamma for recompute at binding sitesrecompute-primalstores
Diffstat (limited to 'src/CHAD/Data.hs')
| -rw-r--r-- | src/CHAD/Data.hs | 5 |
1 files changed, 5 insertions, 0 deletions
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 |