diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-12-09 21:48:39 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-12-09 21:48:39 +0100 |
| commit | 8cdef3f10594a69037d45340029f8e795ecfee4a (patch) | |
| tree | b0edf7e7692c4da34bcbb4332607d1511975116f /src/CHAD/Fusion.hs | |
| parent | d5ea985f9d252af55ea0a5c3f00374a41b562369 (diff) | |
WIP fusion stufffusion
Diffstat (limited to 'src/CHAD/Fusion.hs')
| -rw-r--r-- | src/CHAD/Fusion.hs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/CHAD/Fusion.hs b/src/CHAD/Fusion.hs index f863944..29c1f12 100644 --- a/src/CHAD/Fusion.hs +++ b/src/CHAD/Fusion.hs @@ -60,7 +60,7 @@ import CHAD.Lemmas -- putStrLn $ case fromNamed $ body $ build (SS (SS SZ)) (pair (pair nil 3) 4) (#idx :-> snd_ #idx + snd_ (fst_ #idx)) of EBuild _ n esh ebody -> let env = knownEnv in buildLoopNest env n esh ebody $ \sub nest -> show sub ++ "\n" ++ ppLoopNest (subList env sub) nest -prependBinding :: forall args outs t. Ex args t -> LoopNest (t : args) outs -> LoopNest args outs +prependBinding :: forall args outs bouts t. Ex args t -> LoopNest (t : args) outs bouts -> LoopNest args outs bouts prependBinding e (Inner (bs :: Bindings Ex (t : args) bs) outs) | Refl <- lemAppendAssoc @bs @'[t] @args = Inner (bconcat (BTop `bpush` e) bs) outs @@ -72,7 +72,7 @@ prependBinding e (Layer (bs1 :: Bindings Ex (t : args) bs1) wid nest part bs2 ou nest part bs2 outs buildLoopNest :: SList STy env -> SNat n -> Ex env (Tup (Replicate n TIx)) -> Ex (Tup (Replicate n TIx) : env) t - -> (forall args. Subenv env args -> LoopNest args '[TArr n t] -> r) -> r + -> (forall args. Subenv env args -> LoopNest args '[] '[TArr n t] -> r) -> r buildLoopNest = \env sn esh ebody k -> withSome (occCountAll ebody) $ \occBody' -> occEnvPop' occBody' $ \occBody -> @@ -87,8 +87,8 @@ buildLoopNest = \env sn esh ebody k -> Inner (BTop `bpush` elet idx (EUnit ext (weakenExpr (WCopy (WPop w)) ebody'))) (IZ `SCons` SNil) where nestMapN :: SNat n -> STy t -> SList (Ex args) (Replicate n TIx) - -> (forall args'. args :> args' -> Ex args' (Tup (Replicate n TIx)) -> LoopNest args' '[TArr Z t]) - -> LoopNest args '[TArr n t] + -> (forall args'. args :> args' -> Ex args' (Tup (Replicate n TIx)) -> LoopNest args' '[TArr Z t] '[]) + -> LoopNest args '[] '[TArr n t] nestMapN SZ _ SNil inner = inner WId (ENil ext) nestMapN (SS sn) ty (wid `SCons` sh) inner = Layer (BTop `bpush` wid) |