feat: Stack Machine + compile only kernels + test framework

brat/Brat/Checker/Helpers.hs

@@ -634,7 +634,10 @@ solveVal Nat it@(InEnd inn) v@(VNum nv) = do
   dangling <- buildNatVal nv
   req (Wire (end dangling, TNat, inn))
   defineEnd "solveValNat" it v
-solveVal _ it v = defineEnd "solveVal" it v
+solveVal k@(TypeFor _ _) it@(InEnd inn) v = do
+  (_, _, [(dummySrc, _)], _) <- anext "" (Dummy k) (S0, Some (Zy :* S0)) R0 (REx ("dummy", k) R0)
+  req $ Wire (end dummySrc, kindType k, inn)
+  defineEnd "solveVal" it v
   -- Do we also need dummy wiring here?
 
 solveSem :: TypeKind -> End -> Sem -> Checking ()

brat/Brat/Compiler.hs

@@ -3,23 +3,30 @@ module Brat.Compiler (printAST
                      ,writeDot
                      ,compileFile
                      ,compileAndPrintFile
+                     ,compileToGraph
                      ,CompilingHoles(..)
                      ) where
 
-import Brat.Checker.Types (TypedHole)
+import Brat.Checker.Types (TypedHole, Modey(Kerny), VEnv)
 import Brat.Compile.Hugr
 import Brat.Dot (toDotString)
 import Brat.Elaborator
 import Brat.Error
+import Brat.Graph(Graph, Node(BratNode), NodeType(Box, Id))
 import Brat.Load
-import Brat.Naming (root, split)
+import Brat.Naming (Namespace, root, split, Name)
+import Brat.QualName (QualName)
+import Brat.Syntax.Port (NamedPort(..), OutPort(..), InPort(..))
+import Brat.Syntax.Value (Val(VFun))
 
 import Control.Exception (evaluate)
 import Control.Monad (forM, when)
 import Control.Monad.Except
 import Data.List (intercalate)
 import qualified Data.Map as M
 import qualified Data.ByteString.Lazy as BS
+import Data.Foldable (for_)
+import Data.HugrGraph (HugrGraph, NodeId, to_json)
 import System.Exit (die)
 
 printDeclsHoles :: [FilePath] -> String -> IO ()
@@ -74,18 +81,43 @@ instance Show CompilingHoles where
   show (CompilingHoles hs) = unlines $
     "Can't compile file with remaining holes": fmap (("  " ++) . show) hs
 
-compileFile :: [FilePath] -> String -> IO (Either CompilingHoles BS.ByteString)
-compileFile libDirs file = do
+compileToGraph :: [FilePath] -> String -> IO (Namespace, VMod)
+compileToGraph libDirs file = do
   let (checkRoot, newRoot) = split "checking" root
   env <- runExceptT $ loadFilename checkRoot libDirs file
-  (declEnv, holes, defs, outerGraph, capSets) <- eitherIO env
+  (newRoot,) <$> eitherIO env
+
+-- Map from box name to (compiled hugr, list of hole nodes in it)
+type CompilationResult = M.Map Name (HugrGraph NodeId, [NodeId])
+
+compileFile :: [FilePath] -> String -> IO (Either CompilingHoles CompilationResult)
+compileFile libDirs file = do
+  (newRoot, (declEnv, holes, st, outerGraph, _)) <- compileToGraph libDirs file
   let venv = M.map fst declEnv
   case holes of
-    [] -> Right <$> evaluate -- turns 'error' into IO 'die'
-                    (compile defs newRoot outerGraph capSets venv)
+    [] -> let box_decls = (M.keys declEnv) >>= (findBoxes venv outerGraph)
+          in Right <$> (evaluate -- turns 'error' into IO 'die'
+            $ M.fromList [(n, let (hugr, holes) = compileKernel (newRoot, st, outerGraph) "root" n
+                               in (hugr, map fst holes))
+                         | n <- box_decls])
     hs -> pure $ Left (CompilingHoles hs)
+ where
+  findBoxes :: VEnv -> Graph -> QualName -> [Name]
+  findBoxes venv (ns, es) name = case M.lookup name venv of
+        Nothing -> error $ (show name) ++ ".... not found in VEnv"
+        Just vals -> vals >>= \(NamedPort (Ex n _) _, _) -> case M.lookup n ns of
+            Just (BratNode Id _ _) ->
+               [src | (Ex src 0, _, In tgt _) <- es, tgt == n, isKernelBox src ns]
+            _ -> []
+  isKernelBox :: Name -> M.Map Name Node -> Bool
+  isKernelBox name ns
+    | Just (BratNode (Box _ _ ) [] [(_, VFun Kerny _cty)]) <- M.lookup name ns = True
+    | otherwise = False
 
 compileAndPrintFile :: [FilePath] -> String -> IO ()
 compileAndPrintFile libDirs file = compileFile libDirs file >>= \case
-  Right bs -> BS.putStr bs
+  Right hs -> for_ (M.toList hs) $ \(n, (hugr, splices)) -> do
+    putStrLn $ "Compiled box: " ++ show n
+    BS.putStr (to_json hugr)
+    putStrLn $ "With splices: " ++ show splices
   Left err -> die (show err)

brat/Brat/Constructors/Patterns.hs

@@ -2,10 +2,11 @@ module Brat.Constructors.Patterns where
 
 import Brat.QualName
 
-pattern CSucc, CDoub, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
+pattern CSucc, CDoub, CFull, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
         CConcatEqEven, CConcatEqOdd, CRiffle :: QualName
 pattern CSucc = PrefixName [] "succ"
 pattern CDoub = PrefixName [] "doub"
+pattern CFull = PrefixName [] "full"
 pattern CNil = PrefixName [] "nil"
 pattern CSome = PrefixName [] "some"
 pattern CNone = PrefixName [] "none"

brat/Brat/Graph.hs

@@ -51,6 +51,8 @@ data NodeType :: Mode -> Type where
   ArithNode :: ArithOp -> NodeType Brat
   Replicate :: NodeType Brat
   MapFun :: NodeType a
+  -- The thing that gets plugged into type hopes when we solve them
+  Dummy :: TypeKind -> NodeType Brat
 
 deriving instance Show (NodeType a)
 
@@ -110,9 +112,6 @@ toGraph (ns, ws) = G.graphFromEdges adj
           )
         | (name, node) <- M.toList ns]
 
-wiresFrom :: Name -> Graph -> [Wire]
-wiresFrom src (_, ws) = [ w | w@(Ex a _, _, _) <- ws, a == src ]
-
 lookupNode :: Name -> Graph -> Maybe Node
 lookupNode name (ns, _) = M.lookup name ns
 
@@ -121,3 +120,10 @@ wireStart (Ex x _, _, _) = x
 
 wireEnd :: Wire -> Name
 wireEnd (_, _, In x _) = x
+
+-- These are horribly inefficient until we use a better structure for graph edges
+wiresFrom :: Name -> Graph -> [Wire]
+wiresFrom src (_, ws) = [ w | w@(Ex a _, _, _) <- ws, a == src ]
+
+wiresTo :: Name -> Graph -> [Wire]
+wiresTo tgt (_, ws) = [ w | w@(_, _, In a _) <- ws, a == tgt ]

brat/Brat/Load.hs

@@ -2,6 +2,7 @@ module Brat.Load (loadFilename
                  ,loadFiles
                  ,parseFile
                  ,desugarEnv
+                 ,VMod
                  ) where
 
 import Brat.Checker