WIP stuff

1 files changed, 9 insertions, 73 deletions

diff --git a/src/CHAD/Fusion.hs b/src/CHAD/Fusion.hs
index 3358d30..f863944 100644
--- a/src/CHAD/Fusion.hs
+++ b/src/CHAD/Fusion.hs
@@ -11,26 +11,24 @@
 {-# LANGUAGE TypeOperators #-}
 module CHAD.Fusion where
 
-import Data.Dependent.Map (DMap)
 -- import Data.Dependent.Map qualified as DMap
-import Data.Functor.Const
-import Data.Kind (Type)
 import Data.Some
-import Numeric.Natural
 
 import CHAD.AST
 import CHAD.AST.Bindings
 import CHAD.AST.Count
 import CHAD.AST.Env
 import CHAD.Data
+import CHAD.Fusion.AST
 import CHAD.Lemmas
 
 
 -- TODO:
--- A bunch of data types are defined here that should be able to express a
--- graph of loop nests. A graph is a straight-line program whose statements
--- are, in this case, loop nests. A loop nest corresponds to what fusion
--- normally calls a "cluster", but is here represented as, well, a loop nest.
+-- A bunch of data types are defined here (in CHAD.Fusion.AST) that should be
+-- able to express a graph of loop nests. A graph is a straight-line program
+-- whose statements are, in this case, loop nests. A loop nest corresponds to
+-- what fusion normally calls a "cluster", but is here represented as, well, a
+-- loop nest.
 --
 -- No unzipping is done here, as I don't think it is necessary: I haven't been
 -- able to think of programs that get more fusion opportunities when unzipped
@@ -57,72 +55,10 @@ import CHAD.Lemmas
 --    and compile that to an actual C loop nest.
 -- 6. Extend to other cool operations like EFold1InnerD1
 
+-- :m *CHAD.Fusion CHAD.AST.Pretty CHAD.Language
+-- pprintExpr $ fromNamed $ body $ build (SS (SS SZ)) (pair (pair nil 3) 4) (#idx :-> snd_ #idx + snd_ (fst_ #idx))
+-- 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
 
-type FEx = Expr FGraph (Const ())
-
-type FGraph :: (Ty -> Type) -> [Ty] -> Ty -> Type
-data FGraph x env t where
-  FGraph :: DMap NodeId (Node env) -> Tuple NodeId t -> FGraph (Const ()) env t
-
-data Node env t where
-  FFreeVar :: STy t -> Idx env t -> Node env t
-  FLoop :: SList NodeId args
-        -> SList STy outs
-        -> LoopNest args outs
-        -> Tuple (Idx outs) t
-        -> Node env t
-
-data NodeId t = NodeId Natural (STy t)
-  deriving (Show)
-
-data Tuple f t where
-  TupNil :: Tuple f TNil
-  TupPair :: Tuple f a -> Tuple f b -> Tuple f (TPair a b)
-  TupSingle :: f t -> Tuple f t
-deriving instance (forall a. Show (f a)) => Show (Tuple f t)
-
-data LoopNest args outs where
-  Inner :: Bindings Ex args bs
-        -> SList (Idx (Append bs args)) outs
-        -> LoopNest args outs
-  -- this should be able to express a simple nesting of builds and sums.
-  Layer :: Bindings Ex args bs1
-        -> Idx bs1 TIx  -- ^ loop width (number of (parallel) iterations)
-        -> LoopNest (TIx : Append bs1 args) loopouts
-        -> Partition BuildUp RedSum loopouts mapouts sumouts
-        -> Bindings Ex (Append sumouts (Append bs1 args)) bs2
-        -> SList (Idx (Append bs2 (Append bs1 args))) outs
-        -> LoopNest args (Append outs mapouts)
-deriving instance Show (LoopNest args outs)
-
-type Partition :: (Ty -> Ty -> Type) -> (Ty -> Ty -> Type) -> [Ty] -> [Ty] -> [Ty] -> Type
-data Partition f1 f2 ts ts1 ts2 where
-  PNil :: Partition f1 f2 '[] '[] '[]
-  Part1 :: f1 t t1 -> Partition f1 f2 ts ts1 ts2 -> Partition f1 f2 (t : ts) (t1 : ts1) ts2
-  Part2 :: f2 t t2 -> Partition f1 f2 ts ts1 ts2 -> Partition f1 f2 (t : ts) ts1 (t2 : ts2)
-deriving instance (forall t t1. Show (f1 t t1), forall t t2. Show (f2 t t2)) => Show (Partition f1 f2 ts ts1 ts2)
-
-data BuildUp t t' where
-  BuildUp :: SNat n -> STy t -> BuildUp (TArr n t) (TArr (S n) t)
-deriving instance Show (BuildUp t t')
-
-data RedSum t t' where
-  RedSum :: SMTy t -> RedSum t t
-deriving instance Show (RedSum t t')
-
--- type family Unzip t where
---   Unzip (TPair a b) = TPair (Unzip a) (Unzip b)
---   Unzip (TArr n t) = UnzipA n t
-
--- type family UnzipA n t where
---   UnzipA n (TPair a b) = TPair (UnzipA n a) (UnzipA n b)
---   UnzipA n t = TArr n t
-
--- data Zipping ut t where
---   ZId :: Zipping t t
---   ZPair :: Zipping ua a -> Zipping ub b -> Zipping (TPair ua ub) (TPair a b)
---   ZZip :: Zipping ua (TArr n a) -> Zipping ub (TArr n b) -> Zipping (TPair ua ub) (TArr n (TPair a b))
--- deriving instance Show (Zipping ut t)
 
 prependBinding :: forall args outs t. Ex args t -> LoopNest (t : args) outs -> LoopNest args outs
 prependBinding e (Inner (bs :: Bindings Ex (t : args) bs) outs)