diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
index 38d78c63..618fc4f6 100644
--- a/brat/Brat/Checker/Helpers.hs
+++ b/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 ()
diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs
index 12f15aca..025be2b2 100644
--- a/brat/Brat/Checker/Monad.hs
+++ b/brat/Brat/Checker/Monad.hs
@@ -22,18 +22,18 @@ import Data.List (intercalate)
 import qualified Data.Map as M
 import qualified Data.Set as S
 
--- import Debug.Trace
+import Debug.Trace
 
 -- Used for messages about thread forking / spawning
 thTrace = const id
 --thTrace = trace
 
 trackM :: Monad m => String -> m ()
-trackM = const (pure ())
---trackM = traceM
+--trackM = const (pure ())
+trackM = traceM
 
-track = const id
---track = trace
+--track = const id
+track = trace
 trackShowId x = track (show x) x
 
 -- Data for using a type alias. E.g.
@@ -120,6 +120,7 @@ data CheckingSig ty where
   ANewDynamic :: InPort -> FC -> CheckingSig ()
   AskDynamics :: CheckingSig (M.Map InPort FC)
   AddCapture :: Name -> (QualName, [(Src, BinderType Brat)]) -> CheckingSig ()
+  WiresIn :: Name -> CheckingSig [Wire]
 
 wrapper :: (forall a. CheckingSig a -> Checking (Maybe a)) -> Checking v -> Checking v
 wrapper _ (Ret v) = Ret v
@@ -319,6 +320,8 @@ handler (Req s k) ctx g
       AddCapture n (var, ends) ->
         handler (k ()) ctx {captureSets=M.insertWith M.union n (M.singleton var ends) (captureSets ctx)} g
 
+      WiresIn n -> handler (k (wiresTo n g)) ctx g
+
 handler (Define lbl end v k) ctx g = let st@Store{typeMap=tm, valueMap=vm} = store ctx in
   case track ("Define(" ++ lbl ++ ")" ++ show end ++ " = " ++ show v) $ M.lookup end vm of
       Just _ -> Left $ dumbErr (InternalError $ "Redefining " ++ show end)
diff --git a/brat/Brat/Checker/SolveNumbers.hs b/brat/Brat/Checker/SolveNumbers.hs
index 8089c506..40685bbb 100644
--- a/brat/Brat/Checker/SolveNumbers.hs
+++ b/brat/Brat/Checker/SolveNumbers.hs
@@ -12,13 +12,14 @@ import Brat.Naming
 import Hasochism
 import Control.Monad.Freer
 
--- import Debug.Trace
+import Debug.Trace
 import qualified Data.Set as S
 
 trailM :: Applicative f => String -> f ()
-trailM = const (pure ())
-trail = const id
---trail = trace
+--trailM = const (pure ())
+trailM = traceM
+--trail = const id
+trail = trace
 
 -- This is currently lifted from SolvePatterns, which still imports it.
 -- It is also used in SolveHoles, where it does the right mathematics
@@ -90,15 +91,18 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
   lhsFun00 (StrictMonoFun sm) num = lhsStrictMono sm num
 
   flexFlex :: VVar Z -> VVar Z -> Checking ()
+  flexFlex v v' | trace ("flexFlex " ++ show v ++ " " ++ show v') False = undefined
   flexFlex v v' = case compare v v' of
-    GT -> flexFlex v' v
-    EQ -> pure ()
+    GT | trace "GT" False -> undefined | otherwise -> flexFlex v' v
+    EQ | trace "EQ" False -> undefined | otherwise -> pure ()
     LT -> case (v, v') of
       (VPar e@(ExEnd p), VPar e'@(ExEnd p'))
+       | trace "ExEx" False -> undefined
        | Just _ <- mine e -> defineSrc (NamedPort p "") (VNum (nVar v'))
        | Just _ <- mine e' -> defineSrc (NamedPort p' "") (VNum (nVar v))
        | otherwise -> typeErr $ "Can't force " ++ show v ++ " to be " ++ show v'
       (VPar e@(InEnd p), VPar e'@(ExEnd dangling))
+       | trace "InEx" False -> undefined
        | Just _ <- mine e -> do
           req (Wire (dangling, TNat, p))
           defineTgt' ("flex-flex In Ex") (NamedPort p "") (VNum (nVar v'))
@@ -107,10 +111,36 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
           defineSrc' ("flex-flex In Ex") (NamedPort dangling "") (VNum (nVar v))
        | otherwise -> mkYield "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
       (VPar e@(InEnd p), VPar e'@(InEnd p'))
-       | Just _ <- mine e -> defineTgt' "flex-flex In In1" (NamedPort p "") (VNum (nVar v'))
-       | Just _ <- mine e' -> defineTgt' "flex-flex In In0"(NamedPort p' "") (VNum (nVar v))
+       | trace "InIn" False -> undefined
+       | Just _ <- mine e -> solveInIn p p'
+       | Just _ <- mine e' -> solveInIn p' p
        | otherwise -> mkYield "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
 
+  -- INVARIANT: The first argument is ours to solve
+  solveInIn :: InPort -> InPort -> Checking ()
+  solveInIn e0@(In node0 _) e1@(In node1  _) = do
+    ws0 <- req $ WiresIn node0
+    ws1 <- req $ WiresIn node1
+    mine <- mineToSolve
+    me <- whoAmI
+    case (ws0, ws1) of
+      ([], [(dangling, ty, _)]) -> do
+        req $ Wire (dangling, ty, e0)
+        defineTgt' "solveInIn" (NamedPort e0 "") (VNum (nVar (VPar (toEnd e1))))
+      ([], [])
+       | Just _ <- mine (InEnd e1) -> do
+        (_, [(tgt,_)], [(src0, _), (src1, _)], _) <- anext "copyInIn" Copy (S0, Some (Zy :* S0)) (REx ("clonee", Nat) R0) (REx ("clone0", Nat) (REx ("clone1", Nat) R0))
+        defineTgt' "solveInInCopy" (NamedPort e0 "") (VNum (nVar (VPar (toEnd tgt))))
+        defineTgt' "solveInInCopy" (NamedPort e1 "") (VNum (nVar (VPar (toEnd tgt))))
+        req $ Wire (end src0, TNat, e0)
+        req $ Wire (end src1, TNat, e1)
+       | otherwise -> error $ "solveInIn: rhs not ours to solve: " ++ show e1 ++ "\n we are " ++ show me
+      (_, []) -> err (Unimplemented  "solveInIn: ours defined; other not" [])
+      -- Both things already wired up; just do the statics
+      _ -> defineTgt' "solveInInStatic" (NamedPort e0 "") (VNum (nVar (VPar (toEnd e1))))
+
+
+
   lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
   lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
   lhsStrictMono (StrictMono n mono) num = do
diff --git a/brat/Brat/Compile/Hugr.hs b/brat/Brat/Compile/Hugr.hs
index 6c169733..4187d034 100644
--- a/brat/Brat/Compile/Hugr.hs
+++ b/brat/Brat/Compile/Hugr.hs
@@ -7,15 +7,15 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
-module Brat.Compile.Hugr (compile) where
+module Brat.Compile.Hugr (compileKernel) where
 
 import Brat.Constructors.Patterns (pattern CFalse, pattern CTrue)
 import Brat.Checker.Monad (track, trackM, CheckingSig(..), CaptureSets)
 import Brat.Checker.Helpers (binderToValue)
-import Brat.Checker.Types (Store(..), VEnv)
+import Brat.Checker.Types (Store(..))
 import Brat.Eval (eval, evalCTy, kindType)
 import Brat.Graph hiding (lookupNode)
-import Brat.Naming
+import Brat.Naming hiding (root)
 import Brat.QualName
 import Brat.Syntax.Port
 import Brat.Syntax.Common
@@ -24,111 +24,93 @@ import Brat.Syntax.Value
 import Bwd
 import Control.Monad.Freer
 import Data.Hugr
+import Data.HugrGraph (HugrGraph(..), NodeId)
+import qualified Data.HugrGraph as H
 import Hasochism
 
 import Control.Monad (unless)
-import Data.Aeson
-import Data.Bifunctor (first, second)
-import qualified Data.ByteString.Lazy as BS
+import Data.Bifunctor (second)
 import Data.Foldable (traverse_, for_)
-import Data.Functor ((<&>), ($>))
-import Data.List (partition, sort, sortBy)
+import Data.Functor ((<&>))
 import qualified Data.Map as M
-import Data.Maybe (catMaybes, fromJust, isJust)
-import Data.Ord (comparing)
+import Data.Maybe (catMaybes, fromJust)
 import Data.Traversable (for)
 import Control.Monad.State
 import Data.List.NonEmpty (NonEmpty, nonEmpty)
 import GHC.Base (NonEmpty(..))
-import Data.Tuple (swap)
 
 {-
 For each top level function definition or value in BRAT: we should have a FuncDef node in
 hugr, whose child graph is the body of the function
 -}
 
-newtype NodeId = NodeId Name deriving (Eq, Ord, Show)
-
 type TypedPort = (PortId NodeId, HugrType)
 
 data CompilationState = CompilationState
  { bratGraph :: Graph -- the input BRAT Graph; should not be written
- , capSets :: CaptureSets -- environments captured by Box nodes in previous
- , nameSupply :: Namespace
- , nodes :: M.Map NodeId (HugrOp NodeId) -- this node's id => HugrOp containing parent id
- , edges :: [(PortId NodeId, PortId NodeId)]
+ , hugr :: HugrGraph
  , compiled :: M.Map Name NodeId  -- Mapping from Brat nodes to Hugr nodes
  -- When lambda lifting, captured variables become extra function inputs.
  -- This maps from the captured value (in the BRAT graph, perhaps outside the current func/lambda)
  -- to the Hugr port capturing it in the current context.
  , liftedOutPorts :: M.Map OutPort (PortId NodeId)
- , holes :: Bwd Name -- for Kernel graphs, list of Splices found in order
+ , holes :: Bwd (NodeId, OutPort) -- where to splice in result of another Brat computation
  , store :: Store -- Kinds and values of global variables, for compiling types
- -- A map from Id nodes representing functions and values in the brat graph,
- -- to the FuncDef nodes that we create for them. The bool, if true, says that
- -- we must insert an *extra* call, beyond what's required in Brat, to compute the value
- -- of the decl (e.g. `x :: Int` `x = 1+2` requires calling the FuncDefn to calculate 1+2).
- -- Note that in the future this could be extended to allow top-level Consts too.
- , decls :: M.Map Name (NodeId, Bool)
  }
 
-emptyCS g cs ns store = CompilationState
-  { bratGraph = g
-  , capSets = cs
-  , nameSupply = ns
-  , nodes = M.empty
-  , edges = []
-  , compiled = M.empty
-  , holes = B0
-  , liftedOutPorts = M.empty
-  , store = store
-  , decls = M.empty
-  }
-
-registerFuncDef :: Name -> (NodeId, Bool) -> Compile ()
-registerFuncDef name hugrDef = do
-  st <- get
-  put (st { decls = M.insert name hugrDef (decls st) })
-
+type Compile = State CompilationState
 
-freshNode :: String -> Compile NodeId
-freshNode str = do
-  st <- get
-  let ns = nameSupply st
-  let (freshName, newSupply) = fresh str ns
-  put (st { nameSupply = newSupply })
-  pure (NodeId freshName)
+onHugr :: State HugrGraph a -> Compile a
+onHugr f = get >>= \s -> let (r, h') = runState f (hugr s) in put (s {hugr=h'}) >> pure r
+
+data Container = Ctr {
+  parent :: NodeId,
+  input :: NodeId,
+  output :: NodeId
+}
+
+makeCS :: (Graph, Store) -> HugrGraph -> CompilationState
+makeCS (g, store) hugr =
+  CompilationState
+    { bratGraph = g
+    , hugr = hugr
+    , compiled = M.empty
+    , holes = B0
+    , liftedOutPorts = M.empty
+    , store = store
+    }
+
+freshNode :: String -> NodeId -> Compile NodeId
+freshNode name parent = onHugr (H.freshNode parent name)
+
+makeIO :: String -> NodeId -> Compile Container
+makeIO name parent = do
+  input <- freshNode (name ++ "_Input") parent
+  output <- freshNode (name ++ "_Input") parent
+  onHugr $ H.setFirstChildren parent [input, output]
+  pure $ Ctr {parent, input, output}
+
+freshNodeWithIO :: String -> NodeId -> Compile Container
+freshNodeWithIO name parent = freshNode name parent >>= makeIO name
 
 addEdge :: (PortId NodeId, PortId NodeId) -> Compile ()
-addEdge e = do
+addEdge e = onHugr (H.addEdge e)
+
+addNode :: String -> (NodeId, HugrOp) -> Compile NodeId
+addNode nam (parent, op) = do
+  name <- freshNode nam parent
+  setOp name (addMetadata [("id", show name)] op)
+  pure name
+
+-- Add a hole, record that it should be filled from the specified OutPort
+addHole :: NodeId -> FunctionType -> OutPort -> Compile NodeId
+addHole parent sig outPort = do
+  -- hole index is not important now, we identify holes by NodeId
+  hole <- gets (length . holes) -- but anyway
+  h <- addNode ("hole " ++ show hole) (parent, OpCustom (holeOp hole sig))
   st <- get
-  let es = edges st
-  put (st { edges = e:es })
-
-addNode :: String -> HugrOp NodeId -> Compile NodeId
-addNode name op = do
-  id <- freshNode name
-  addOp (addMetadata [("id", show id)] op) id
-  pure id
-
-type Compile = State CompilationState
-
-instance FreshMonad Compile where
-  freshName x = do
-    s <- get
-    let (name, newSupply) = fresh x (nameSupply s)
-    put (s { nameSupply = newSupply })
-    pure name
-
-  x -! c = do
-    s <- get
-    let (nsx, nsNew) = split x (nameSupply s)
-    put (s { nameSupply = nsx })
-    v <- c
-    put (s { nameSupply = nsNew })
-    pure v
-
-  whoAmI = gets (fst . nameSupply)
+  put (st { holes = (holes st) :< (h, outPort)})
+  pure h
 
 runCheckingInCompile :: Free CheckingSig t -> Compile t
 runCheckingInCompile (Ret t) = pure t
@@ -181,97 +163,28 @@ compileGraphTypes = traverse ((<&> compileType) . runCheckingInCompile . eval S0
 compilePorts :: [(a, Val Z)] -> Compile [HugrType]
 compilePorts = compileGraphTypes . map snd
 
-addOp :: HugrOp NodeId -> NodeId -> Compile ()
-addOp op name | track ("addOp " ++ show op ++ show name) False = undefined
-addOp op name = do
-  st <- get
-  let new_nodes = M.alter (\Nothing -> Just op) name (nodes st) -- fail if key already present
-  put (st { nodes = new_nodes })
+setOp :: NodeId -> HugrOp -> Compile ()
+setOp name op | track ("addOp " ++ show op ++ show name) False = undefined
+setOp name op = onHugr (H.setOp name op)
 
 registerCompiled :: Name -> NodeId -> Compile ()
 registerCompiled from to | track (show from ++ " |-> " ++ show to) False = undefined
 registerCompiled from to = do
   st <- get
-  put (st { compiled = M.insert from to (compiled st) })
+  let new_compiled = M.alter (\Nothing -> Just to) from (compiled st)
+  put (st { compiled = new_compiled })
 
 compileConst :: NodeId -> SimpleTerm -> HugrType -> Compile NodeId
 compileConst parent tm ty = do
-  constId <- addNode "Const" (OpConst (ConstOp parent (valFromSimple tm)))
+  constId <- addNode "Const" (parent, OpConst (ConstOp (valFromSimple tm)))
   loadId <- case ty of
     HTFunc poly@(PolyFuncType [] _) ->
-      addNode "LoadFunction" (OpLoadFunction (LoadFunctionOp parent poly [] (FunctionType [] [HTFunc poly] [])))
+      addNode "LoadFunction" (parent, OpLoadFunction (LoadFunctionOp poly [] (FunctionType [] [HTFunc poly] [])))
     HTFunc (PolyFuncType _ _) -> error "Trying to compile function with type args"
-    _ -> addNode "LoadConst" (OpLoadConstant (LoadConstantOp parent ty))
+    _ -> addNode "LoadConst" (parent, OpLoadConstant (LoadConstantOp ty))
   addEdge (Port constId 0, Port loadId 0)
   pure loadId
 
-compileArithNode :: NodeId -> ArithOp -> Val Z -> Compile NodeId
-compileArithNode parent op TNat  = addNode (show op ++ "_Nat") $ OpCustom $ case op of
-  Add -> binaryIntOp parent "iadd"
-  Sub -> binaryIntOp parent "isub"
-  Mul-> binaryIntOp parent "imul"
-  Div -> intOp parent "idiv_u" [hugrInt, hugrInt] [hugrInt] [TANat intWidth, TANat intWidth]
-  Pow -> error "TODO: Pow"  -- Not defined in extension
-compileArithNode parent op TInt  = addNode (show op ++ "_Int") $ OpCustom $ case op of
-  Add -> binaryIntOp parent "iadd"
-  Sub -> binaryIntOp parent "isub"
-  Mul-> binaryIntOp parent "imul"
-  Div -> intOp parent "idiv_u" [hugrInt, hugrInt] [hugrInt] [TANat intWidth, TANat intWidth]
-  Pow -> error "TODO: Pow"  -- Not defined in extension
-compileArithNode parent op TFloat  = addNode (show op ++ "_Float") $ OpCustom $ case op of
-  Add -> binaryFloatOp parent "fadd"
-  Sub -> binaryFloatOp parent "fsub"
-  Mul-> binaryFloatOp parent "fmul"
-  Div-> binaryFloatOp parent "fdiv"
-  Pow -> error "TODO: Pow"  -- Not defined in extension
-compileArithNode _ _ ty = error $ "compileArithNode: Unexpected type " ++ show ty
-
-renameAndSortHugr :: M.Map NodeId (HugrOp NodeId) -> [(PortId NodeId, PortId NodeId)] -> Hugr Int
-renameAndSortHugr nodes edges = indexMetadata $ fmap update (Hugr (fst <$> sorted_nodes) (edges ++ orderEdges)) where
-  indexMetadata :: Hugr Int -> Hugr Int
-  indexMetadata (Hugr ops edges) = Hugr [addMetadata [("index", show ix)] op | (ix, op) <- zip [0..] ops] edges
-
-
-  sorted_nodes = let ([root], rest) = partition (\(n, nid) -> nid == getParent n) (swap <$> M.assocs nodes) in
-                   root : sort rest
-
-  names2Pos = M.fromList $ zip (snd <$> sorted_nodes) ([0..] :: [Int])
-  parentOf n = getParent (nodes M.! n)
-
-  update :: NodeId -> Int
-  update name = case M.lookup name names2Pos of
-                  Just ans -> ans
-                  Nothing -> error ("Couldn't find node " ++ show name ++ "???")
-
-  orderEdges :: [(PortId NodeId, PortId NodeId)]
-  orderEdges =
-    -- Nonlocal edges (from a node to another which is a *descendant* of a sibling of the source)
-    -- require an extra order edge from the source to the sibling that is ancestor of the target
-    let interEdges = [(n1, n2) | (Port n1 _, Port n2 _) <- edges,
-            parentOf n1 /= parentOf n2 ,
-            requiresOrderEdge (nodes M.! n1),
-            requiresOrderEdge (nodes M.! n2) ] in
-    [(Port src orderEdgeOffset, Port tgt orderEdgeOffset) | (src, tgt) <- walkUp <$> interEdges]
-
-  requiresOrderEdge :: HugrOp NodeId -> Bool
-  requiresOrderEdge (OpMod _) = False
-  requiresOrderEdge (OpDefn _) = False
-  requiresOrderEdge (OpConst _) = False
-  requiresOrderEdge _ = True
-
-  -- Walk up the hierarchy from the tgt until we hit a node at the same level as src
-  walkUp :: (NodeId, NodeId) -> (NodeId, NodeId)
-  walkUp (src, tgt) | parentOf src == parentOf tgt = (src, tgt)
-  walkUp (_, tgt) | parentOf tgt == tgt = error "Tgt was not descendant of Src-parent"
-  walkUp (src, tgt) = walkUp (src, parentOf tgt)
-
-
-dumpJSON :: Compile BS.ByteString
-dumpJSON = do
-  ns <- gets nodes
-  es <- gets edges
-  pure $ encode (renameAndSortHugr ns es)
-
 compileClauses :: NodeId -> [TypedPort] -> NonEmpty (TestMatchData m, Name) -> Compile [TypedPort]
 compileClauses parent ins ((matchData, rhs) :| clauses) = do
   (ns, _) <- gets bratGraph
@@ -298,84 +211,92 @@ compileClauses parent ins ((matchData, rhs) :| clauses) = do
     Just clauses -> compileClauses parent ins clauses
     -- If there are no more clauses left to test, then the Hugr panics
     Nothing -> let sig = FunctionType (snd <$> ins) outTys ["BRAT"] in
-      addNodeWithInputs "Panic" (OpCustom (CustomOp parent "BRAT" "panic" sig [])) ins outTys
+      addNodeWithInputs "Panic" (parent, OpCustom (CustomOp "BRAT" "panic" sig [])) ins outTys
 
   didMatch :: [HugrType] -> NodeId -> [TypedPort] -> Compile [TypedPort]
   didMatch outTys parent ins = gets bratGraph >>= \(ns,_) -> case ns M.! rhs of
     BratNode (Box src tgt) _ _ -> do
-      dfgId <- addNode "DidMatch_DFG" (OpDFG (DFG parent (FunctionType (snd <$> ins) outTys bratExts) []))
-      compileBox (src, tgt) dfgId
+      ctr@Ctr {parent=dfgId} <- freshNodeWithIO "DidMatch" parent
+      setOp dfgId (OpDFG (DFG (FunctionType (snd <$> ins) outTys bratExts) []))
+      compileBox ctr (src, tgt)
       for_ (zip (fst <$> ins) (Port dfgId <$> [0..])) addEdge
       pure $ zip (Port dfgId <$> [0..]) outTys
     _ -> error "RHS should be a box node"
 
-compileBox :: (Name, Name) -> NodeId -> Compile ()
+compileBox :: Container  -> (Name, Name) -> Compile ()
 -- note: we used to compile only KernelNode's here, this may not be right
-compileBox (src, tgt) parent = for_ [src, tgt] (compileWithInputs parent)
+compileBox (Ctr parent srcN tgtN) (src, tgt) = do
+  -- Compile Source
+  node <- gets ((M.! src) . fst . bratGraph)
+  trackM ("compileSource (" ++ show parent ++ ") " ++ show src ++ " " ++ show node)
+  let src_outs = case node of
+               (BratNode Source [] outs) -> outs
+               (KernelNode Source [] outs) -> outs
+  srcTys <- compilePorts src_outs
+  setOp srcN (OpIn (InputNode srcTys [("source", "Source"), ("parent", show parent)]))
+  registerCompiled src srcN
+  compileTarget parent tgtN tgt
+
+compileTarget :: NodeId -> NodeId -> Name -> Compile ()
+compileTarget parent tgtN tgt = do
+  node <- gets ((M.! tgt) . fst . bratGraph)
+  trackM ("compileTarget (" ++ show parent ++ ") " ++ show tgt ++ " " ++ show node)
+  let tgt_ins = case node of
+               (BratNode Target ins []) -> ins
+               (KernelNode Target ins []) -> ins
+  tgtTys <- compilePorts tgt_ins
+  setOp tgtN (OpOut (OutputNode tgtTys [("source", "Target")]))
+  edges <- compileInEdges parent tgt
+  -- registerCompiled tgt tgtN -- really shouldn't be necessary, not reachable
+  for_ edges (\(src, tgtPort) -> addEdge (src, Port tgtN tgtPort))
+  pure ()
+
+in_edges :: Name -> Compile [((OutPort, Val Z), Int)]
+in_edges name = gets bratGraph <&> \(_, es) -> [((src, ty), portNum) | (src, ty, In edgTgt portNum) <- es, edgTgt == name]
+
+compileInEdges :: NodeId -> Name -> Compile [(PortId NodeId, Int)]
+compileInEdges parent name = do
+  in_edges <- in_edges name
+  catMaybes <$> for in_edges (\((src, _), tgtPort) -> getOutPort parent src <&> fmap (, tgtPort))
 
 compileWithInputs :: NodeId -> Name -> Compile (Maybe NodeId)
-compileWithInputs parent name = gets compiled >>= (\case
+compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
   Just nid -> pure (Just nid)
   Nothing -> do
-    (_, es) <- gets bratGraph
-    let in_edges = [((src, ty), portNum) | (src, ty, In edgTgt portNum) <- es, edgTgt == name]
-    compileNode in_edges >>= \case
+    compileNode >>= \case
       Nothing -> pure Nothing
       Just (tgtNodeId, edges) -> do
         registerCompiled name tgtNodeId
         for_ edges (\(src, tgtPort) -> addEdge (src, Port tgtNodeId tgtPort))
-        pure $ Just tgtNodeId) . M.lookup name
+        pure $ Just tgtNodeId
  where
   -- If we only care about the node for typechecking, then drop it and return `Nothing`.
   -- Otherwise, NodeId of compiled node, and list of Hugr in-edges (source and target-port)
-  compileNode :: [((OutPort, Val Z), Int)] -> Compile (Maybe (NodeId, [(PortId NodeId, Int)]))
-  compileNode in_edges | isJust (hasPrefix ["checking", "globals", "decl"] name) = do
-    -- reference to a top-level decl. Every such should be in the decls map.
-    -- We need to return value of each type (perhaps to be indirectCalled by successor).
-    -- Note this is where we must compile something different *for each caller* by clearing out the `compiled` map for each function
-    let hTys = map (compileType . snd . fst) $ sortBy (comparing snd) in_edges
-
-    decls <- gets decls
-    let (funcDef, extra_call) = decls M.! name
-    nod <- if extra_call
-           then addNode ("direct_call(" ++ show funcDef ++ ")")
-                        (OpCall (CallOp parent (FunctionType [] hTys bratExts)))
-           -- We are loading idNode as a value (not an Eval'd thing), and it is a FuncDef directly
-           -- corresponding to a Brat TLD (not that produces said TLD when eval'd)
-           else case hTys of
-             [HTFunc poly@(PolyFuncType [] _)] ->
-               addNode ("load_thunk(" ++ show funcDef ++ ")")
-               (OpLoadFunction (LoadFunctionOp parent poly [] (FunctionType [] [HTFunc poly] [])))
-             [HTFunc (PolyFuncType args _)] -> error $ unwords ["Unexpected type args to"
-                                                               ,show funcDef ++ ":"
-                                                               ,show args
-                                                               ]
-             _ -> error $ "Expected a function argument when loading thunk, got: " ++ show hTys
-    -- the only input
-    pure $ Just (nod, [(Port funcDef 0, 0)])
-  compileNode in_edges = do
-    (ns, _) <- gets bratGraph
-    let node = ns M.! name
-    trackM ("compileNode (" ++ show parent ++ ") " ++ show name ++ " " ++ show node)
-    nod_edge_info <- case node of
-      (BratNode thing ins outs) -> compileNode' thing ins outs
-      (KernelNode thing ins outs) -> compileNode' thing ins outs
-    case nod_edge_info of
-      Nothing -> pure Nothing
-      Just (node, tgtOffset, extra_edges) -> do
-        trans_edges <- catMaybes <$> for in_edges (\((src, _), tgtPort) ->
-            getOutPort parent src <&> fmap (, tgtPort + tgtOffset))
-        pure $ Just (node, extra_edges ++ trans_edges)
+  compileNode :: Compile (Maybe (NodeId, [(PortId NodeId, Int)]))
+  compileNode = case (hasPrefix ["checking", "globals", "decl"] name) of
+    Just _ -> error "Kernel contained call to global; should have been a splice"
+    _ -> do
+      (ns, _) <- gets bratGraph
+      let node = ns M.! name
+      trackM ("compileNode (" ++ show parent ++ ") " ++ show name ++ " " ++ show node)
+      nod_edge_info <- case node of
+        (BratNode _ _ _) -> error "Can't compile classical Brat"
+        (KernelNode thing ins outs) -> compileNode' thing ins outs
+      case nod_edge_info of
+        Nothing -> pure Nothing
+        Just (node, tgtOffset, extra_edges) -> do
+          trans_edges <- compileInEdges parent name <&> map (second (+tgtOffset))
+          pure $ Just (node, extra_edges ++ trans_edges)
 
   default_edges :: NodeId -> Maybe (NodeId, Int, [(PortId NodeId, Int)])
   default_edges nid = Just (nid, 0, [])
 
-  compileNode' :: NodeType m -> [(PortName, Val Z)] -> [(PortName, Val Z)]
+  compileNode' :: NodeType Kernel -> [(PortName, Val Z)] -> [(PortName, Val Z)]
                   -- Result is nodeid, port offset, *extra* edges
                -> Compile (Maybe (NodeId, Int, [(PortId NodeId, Int)]))
   compileNode' thing ins outs = case thing of
     Const tm -> default_edges <$> (compilePorts outs >>= (compileConst parent tm . head))
-    Splice (Ex outNode _) -> default_edges <$> do
+    Splice outPort@(Ex outNode _) -> default_edges <$> do
       ins <- compilePorts ins
       outs <- compilePorts outs
       let sig = FunctionType ins outs bratExts
@@ -385,89 +306,20 @@ compileWithInputs parent name = gets compiled >>= (\case
           (ns, _) <- gets bratGraph
           case M.lookup outNode ns of
             Just (BratNode (Prim (ext,op)) _ [(_, VFun Kerny _)]) -> do
-              addNode (show suffix) (OpCustom (CustomOp parent ext op sig []))
+              addNode (show suffix) (parent, OpCustom (CustomOp ext op sig []))
             x -> error $ "Expected a Prim kernel node but got " ++ show x
         -- All other evaled things are turned into holes to be substituted later
-        Nothing -> do
-          hole <- do
-            st <- get
-            let h = holes st
-            put (st { holes = h :< name})
-            pure (length h)
-          addNode ("hole " ++ show hole) (OpCustom (holeOp parent hole sig))
-    -- A reference to a primitive op which exists in hugr.
-    -- This should only have one outgoing wire which leads to an `Id` node for
-    -- the brat representation of the function, and that wire should have a
-    -- function type
-    Prim (ext,op) -> do
-      let n = ext ++ ('_':op)
-      let [] = ins
-      -- TODO: Handle primitives which aren't functions
-      let [(_, VFun Braty cty)] = outs
-      boxSig@(inputTys, outputTys) <- compileSig Braty cty
-      let boxFunTy = FunctionType inputTys outputTys bratExts
-      ((Port loadConst _, _ty), ()) <- compileConstDfg parent n boxSig $ \dfgId -> do
-        ins <- addNodeWithInputs ("Inputs" ++ n) (OpIn (InputNode dfgId inputTys [("source", "Prim")])) [] inputTys
-        outs <- addNodeWithInputs n (OpCustom (CustomOp dfgId ext op boxFunTy [])) ins outputTys
-        addNodeWithInputs ("Outputs" ++ n) (OpOut (OutputNode dfgId outputTys [("source", "Prim")])) outs []
-        pure ()
-      pure $ default_edges loadConst
-
-    -- Check if the node has prefix "globals", hence should be a direct call
-    Eval (Ex outNode outPort) -> do
-      ins <- compilePorts ins
-      outs <- compilePorts outs
-      (ns, _) <- gets bratGraph
-      decls <- gets decls
-      case hasPrefix ["checking", "globals", "prim"] outNode of
-        -- Callee is a Prim node, insert Hugr Op; first look up outNode in the BRAT graph to get the Prim data
-        Just suffix -> default_edges <$> case M.lookup outNode ns of
-          Just (BratNode (Prim (ext,op)) _ _) -> do
-            addNode (show suffix) (OpCustom (CustomOp parent ext op (FunctionType ins outs [ext]) []))
-          x -> error $ "Expected a Prim node but got " ++ show x
-        Nothing -> case hasPrefix ["checking", "globals"] outNode of
-          -- Callee is a user-defined global def that, since it does not require an "extra" call, can be turned from IndirectCall to direct.
-          Just _ | (funcDef, False) <- fromJust (M.lookup outNode decls) -> do
-                callerId <- addNode ("direct_call(" ++ show funcDef ++ ")")
-                                    (OpCall (CallOp parent (FunctionType ins outs bratExts)))
-                -- Add the static edge from the FuncDefn node to the port *after*
-                -- all of the dynamic arguments to the Call node.
-                -- This is because in hugr, static edges (like the graph arg to a
-                -- Call) come after dynamic edges
-                pure $ Just (callerId, 0, [(Port funcDef 0, length ins)])
-          -- Either not global, or we must evaluate the global -- so an indirect call of a graph on a wire
-          -- (If it's a global, compileWithInputs will generate extra no-args Call,
-          -- since extra_call==True; we just turned the (Eval+)LoadFunction case into a direct Call above)
-          _ -> compileWithInputs parent outNode >>= \case
-            Just calleeId -> do
-              callerId <- addNode ("indirect_call(" ++ show calleeId ++ ")")
-                                  (OpCallIndirect (CallIndirectOp parent (FunctionType ins outs bratExts {-[]-})))
-              -- for an IndirectCall, the callee (thunk, function value) is the *first*
-              -- Hugr input. So move all the others along, and add that extra edge.
-              pure $ Just (callerId, 1, [(Port calleeId outPort, 0)])
-            Nothing -> error "Callee has been erased"
-
-    -- We need to figure out if this thunk contains a brat- or a kernel-computation
-    (Box src tgt) -> case outs of
-      [(_, VFun Kerny cty)] -> default_edges . nodeId . fst <$>
-           compileKernBox parent name (compileBox (src, tgt)) cty
-      [(_, VFun Braty cty)] -> do
-        cs <- gets (M.findWithDefault M.empty name . capSets)
-        (partialNode, captures) <- compileBratBox parent name (cs, src, tgt) cty
-        pure $ Just (partialNode, 1, captures) -- 1 is arbitrary, Box has no real inputs
-      outs -> error $ "Unexpected outs of box: " ++ show outs
-
-    Source -> default_edges <$> do
-      outs <- compilePorts outs
-      addNode "Input" (OpIn (InputNode parent outs [("source", "Source"), ("parent", show parent)]))
-    Target -> default_edges <$> do
-      ins <- compilePorts ins
-      addNode "Output" (OpOut (OutputNode parent ins [("source", "Target")]))
+
+        Nothing -> addHole parent sig outPort
+
+    Source -> error "Source found outside of compileBox"
+      
+    Target -> error "Target found outside of compileBox"
 
     Id | Nothing <- hasPrefix ["checking", "globals", "decl"] name -> default_edges <$> do
       -- not a top-level decl, just compile it as an Id (TLDs handled in compileNode)
       let [(_,ty)] = ins -- fail if more than one input
-      addNode "Id" (OpNoop (NoopOp parent (compileType ty)))
+      addNode "Id" (parent, OpNoop (NoopOp (compileType ty)))
 
     Constructor c -> default_edges <$> do
       ins <- compilePorts ins
@@ -478,19 +330,14 @@ compileWithInputs parent name = gets compiled >>= (\case
     PatternMatch cs -> default_edges <$> do
       ins <- compilePorts ins
       outs <- compilePorts outs
-      dfgId <- addNode "DidMatch_DFG" (OpDFG (DFG parent (FunctionType ins outs bratExts) []))
-      inputNode <- addNode "PatternMatch.Input" (OpIn (InputNode dfgId ins [("source", "PatternMatch"), ("parent", show dfgId)]))
+      (Ctr dfgId inputNode outputNode) <- freshNodeWithIO "PatternMatch" parent
+      setOp dfgId (OpDFG (DFG (FunctionType ins outs bratExts) []))
+      setOp inputNode (OpIn (InputNode ins [("source", "PatternMatch"), ("parent", show dfgId)]))
       ccOuts <- compileClauses dfgId (zip (Port inputNode <$> [0..]) ins) cs
-      addNodeWithInputs "PatternMatch.Output" (OpOut (OutputNode dfgId (snd <$> ccOuts)  [("source", "PatternMatch"), ("parent", show dfgId)])) ccOuts []
+      setOp outputNode (OpOut (OutputNode (snd <$> ccOuts)  [("source", "PatternMatch"), ("parent", show dfgId)]))
+      for_ (zip (fst <$> ccOuts) (Port outputNode <$> [0..])) addEdge
       pure dfgId
-    ArithNode op -> default_edges <$> compileArithNode parent op (snd $ head ins)
     Selector _c -> error "Todo: selector"
-    Replicate -> default_edges <$> do
-      ins <- compilePorts ins
-      let [_, elemTy] = ins
-      outs <- compilePorts outs
-      let sig = FunctionType ins outs bratExts
-      addNode "Replicate" (OpCustom (CustomOp parent "BRAT" "Replicate" sig [TAType elemTy]))
     x -> error $ show x ++ " should have been compiled outside of compileNode"
 
 compileConstructor :: NodeId -> QualName -> QualName -> FunctionType -> Compile NodeId
@@ -499,9 +346,9 @@ compileConstructor parent tycon con sig
       -- A boolean value is a tag which takes no inputs and produces an empty tuple
       -- This is the same thing that happens in Brat.Checker.Clauses to make the
       -- discriminator (makeRowTag)
-      addNode "bool.tag" (OpTag (TagOp parent (if b then 1 else 0) [[], []] [("hint", "bool")]))
+      addNode "bool.tag" (parent, OpTag (TagOp (if b then 1 else 0) [[], []] [("hint", "bool")]))
   | otherwise = let name = "Constructor " ++ show tycon ++ "::" ++ show con in
-                  addNode name (constructorOp parent tycon con sig)
+                  addNode name (parent, constructorOp tycon con sig)
  where
   isBool :: QualName -> Maybe Bool
   isBool CFalse = Just False
@@ -519,93 +366,6 @@ getOutPort parent p@(Ex srcNode srcPort) = do
       Just intercept -> pure $ Just intercept
       Nothing -> compileWithInputs parent srcNode <&> (\maybe -> maybe <&> flip Port srcPort)
 
--- Execute a compilation (which takes a DFG parent) in a nested monad;
--- produce a Const node containing the resulting Hugr, and a LoadConstant,
--- and return the latter.
-compileConstDfg :: NodeId -> String -> ([HugrType], [HugrType]) -> (NodeId -> Compile a) -> Compile (TypedPort, a)
-compileConstDfg parent desc (inTys, outTys) contents = do
-  st <- gets store
-  g <- gets bratGraph
-  cs <- gets capSets
-  let funTy = FunctionType inTys outTys bratExts
-  -- First, we fork off a new namespace
-  (a, cs) <- desc -! do
-    ns <- gets nameSupply
-    pure $ flip runState (emptyCS g cs ns st) $ do
-      -- make a DFG node at the root. We can't use `addNode` since the
-      -- DFG needs itself as parent
-      dfg_id <- freshNode ("Box_" ++ show desc)
-      addOp (OpDFG $ DFG dfg_id funTy []) dfg_id
-      contents dfg_id
-  let nestedHugr = renameAndSortHugr (nodes cs) (edges cs)
-  let ht = HTFunc $ PolyFuncType [] funTy
-
-  constNode <- addNode ("ConstTemplate_" ++ desc) (OpConst (ConstOp parent (HVFunction nestedHugr)))
-  lcPort <- head <$> addNodeWithInputs ("LoadTemplate_" ++ desc) (OpLoadConstant (LoadConstantOp parent ht))
-            [(Port constNode 0, ht)] [ht]
-  pure (lcPort, a)
-
--- Brat computations may capture some local variables. Thus, we need
--- to lambda-lift, producing (as results) a Partial node and a list of
--- extra arguments i.e. the captured values
-compileBratBox :: NodeId -> Name -> (VEnv, Name, Name) -> CTy Brat Z -> Compile (NodeId, [(PortId NodeId, Int)])
-compileBratBox parent name (venv, src, tgt) cty = do
-  -- we'll "Partial" over every value in the environment.
-  -- (TODO in the future capture which ones are actually used in the sub-hugr. We may need
-  -- to put captured values after the original params, and have a reversed Partial.)
-  let params :: [(OutPort, BinderType Brat)] = map (first end) (concat $ M.elems venv)
-  parmTys <- compileGraphTypes (map (binderToValue Braty . snd) params)
-
-  -- Create a FuncDefn for the lambda that takes the params as first inputs
-  (inputTys, outputTys) <- compileSig Braty cty
-  let allInputTys = parmTys ++ inputTys
-  let boxInnerSig = FunctionType allInputTys outputTys bratExts
-
-  (templatePort, _) <- compileConstDfg parent ("BB" ++ show name) (allInputTys, outputTys) $ \dfgId -> do
-    src_id <- addNode ("LiftedCapturesInputs" ++ show name) (OpIn (InputNode dfgId allInputTys [("source", "compileBratBox")]))
-    -- Now map ports in the BRAT Graph to their Hugr equivalents.
-          -- Each captured value is read from an element of src_id, starting from 0
-    let lifted = [(src, Port src_id i) | ((src, _ty), i) <- zip params [0..]]
-          -- and the original BRAT-Graph Src outports become the Hugr Input node ports *after* the captured values
-          ++ [(Ex src i, Port src_id (i + length params)) | i <- [0..length inputTys]]
-    st <- get
-    put $ st {liftedOutPorts = M.fromList lifted}
-    -- no need to return any holes
-    compileWithInputs dfgId tgt
-
-  -- Finally, we add a `Partial` node to supply the captured params.
-  partialNode <- addNode "Partial" (OpCustom $ partialOp parent boxInnerSig (length params))
-  addEdge (fst templatePort, Port partialNode 0)
-  edge_srcs <- for (map fst params) $ getOutPort parent
-  pure (partialNode, zip (map fromJust edge_srcs) [1..])
-    -- error on Nothing, the Partial is expecting a value
-
-compileKernBox :: NodeId -> Name -> (NodeId -> Compile ()) -> CTy Kernel Z -> Compile TypedPort
-compileKernBox parent name contents cty = do
-  -- compile kernel nodes only into a Hugr with "Holes"
-  -- when we see a Splice, we'll record the func-port onto a list
-  -- return a Hugr with holes
-  boxInnerSig@(inTys, outTys) <- compileSig Kerny cty
-  let boxTy = HTFunc $ PolyFuncType [] (FunctionType inTys outTys bratExts)
-  (templatePort, holelist) <- compileConstDfg parent ("KB" ++ show name) boxInnerSig $ \dfg_id -> do
-    contents dfg_id
-    gets holes
-
-  -- For each hole in the template (index 0 i.e. earliest, first)
-  -- compile the kernel that should be spliced in and record its signature.
-  ns <- gets (fst . bratGraph)
-  hole_ports <- for (holelist <>> []) (\splice -> do
-    let (KernelNode (Splice (Ex kernel_src port)) ins outs) = ns M.! splice
-    ins <- compilePorts ins
-    outs <- compilePorts outs
-    kernel_src <- compileWithInputs parent kernel_src <&> fromJust
-    pure (Port kernel_src port, HTFunc (PolyFuncType [] (FunctionType ins outs bratExts))))
-
-  -- Add a substitute node to fill the holes in the template
-  let hole_sigs = [ body poly | (_, HTFunc poly) <- hole_ports ]
-  head <$> addNodeWithInputs ("subst_" ++ show name) (OpCustom (substOp parent (FunctionType inTys outTys bratExts) hole_sigs)) (templatePort : hole_ports) [boxTy]
-
-
 -- We get a bunch of TypedPorts which are associated with Srcs in the BRAT graph.
 -- Then, we'll perform a sequence of matches on those ports
 -- Return a sum whose first component is the types we started with in the order
@@ -702,7 +462,7 @@ compileMatchSequence parent portTable (MatchSequence {..}) = do
 makeRowTag :: String -> NodeId -> Int -> SumOfRows -> [TypedPort] -> Compile [TypedPort]
 makeRowTag hint parent tag sor@(SoR sumRows) ins =
   if sumRows !! tag == (snd <$> ins)
-  then addNodeWithInputs (hint ++ "_Tag") (OpTag (TagOp parent tag sumRows [("hint", hint), ("tag", show tag), ("row", show (sumRows!!tag))])) ins [compileSumOfRows sor]
+  then addNodeWithInputs (hint ++ "_Tag") (parent, OpTag (TagOp tag sumRows [("hint", hint), ("tag", show tag), ("row", show (sumRows!!tag))])) ins [compileSumOfRows sor]
   else error $ "In makeRowTag " ++ hint ++ ", Elements " ++ show (snd <$> ins) ++ " do not match tag " ++ show tag ++ " of " ++ show sumRows
 
 getSumVariants :: HugrType -> [[HugrType]]
@@ -713,7 +473,7 @@ getSumVariants ty = error $ "Expected a sum type, got " ++ show ty
 
 -- This should only be called by the logic which creates conditionals, because
 -- wires that exist in the brat graph are already going to be added at the end.
-addNodeWithInputs :: String -> HugrOp NodeId -> [TypedPort]
+addNodeWithInputs :: String -> (NodeId, HugrOp) -> [TypedPort]
                    -> [HugrType] -- The types of the outputs
                    -> Compile [TypedPort] -- The output wires
 addNodeWithInputs name op inWires outTys = do
@@ -728,28 +488,29 @@ makeConditional :: String    -- Label
                 -> [(String, NodeId -> [TypedPort] -> Compile [TypedPort])] -- Must be ordered
                 -> Compile [TypedPort]
 makeConditional lbl parent discrim otherInputs cases = do
-  condId <- freshNode "Conditional"
+  condId <- freshNode "Conditional" parent
   let rows = getSumVariants (snd discrim)
-  outTyss <- for (zip (zip [0..] cases) rows) (\((ix, (name, f)), row) -> makeCase condId name ix (row ++ (snd <$> otherInputs)) f)
-  unless
-    (allRowsEqual outTyss)
-    (error "Conditional output types didn't match")
-  let condOp = OpConditional (Conditional parent rows (snd <$> otherInputs) (head outTyss) [("label", lbl)])
-  addOp condOp condId
+  (outTyss_cases) <- for (zip (zip [0..] cases) rows) (\((ix, (name, f)), row) -> makeCase condId name ix (row ++ (snd <$> otherInputs)) f)
+  let outTys = if allRowsEqual (fst <$> outTyss_cases)
+               then fst (head outTyss_cases)
+               else (error "Conditional output types didn't match")
+  let condOp = OpConditional (Conditional rows (snd <$> otherInputs) outTys [("label", lbl)])
+  setOp condId condOp
+  onHugr $ H.setFirstChildren condId (snd <$> outTyss_cases)
   addEdge (fst discrim, Port condId 0)
   traverse_ addEdge (zip (fst <$> otherInputs) (Port condId <$> [1..]))
-  pure $ zip (Port condId <$> [0..]) (head outTyss)
+  pure $ zip (Port condId <$> [0..]) outTys
  where
-  makeCase :: NodeId -> String -> Int -> [HugrType] -> (NodeId -> [TypedPort] -> Compile [TypedPort]) -> Compile [HugrType]
+  makeCase :: NodeId -> String -> Int -> [HugrType] -> (NodeId -> [TypedPort] -> Compile [TypedPort]) -> Compile ([HugrType], NodeId)
   makeCase parent name ix tys f = do
-    caseId <- freshNode name
-    inpId <- addNode ("Input_" ++ name) (OpIn (InputNode caseId tys [("source", "makeCase." ++ show ix), ("context", lbl ++ "/" ++ name), ("parent", show parent)]))
+    (Ctr caseId inpId outId) <- freshNodeWithIO name parent
+    setOp inpId (OpIn (InputNode tys [("source", "makeCase." ++ show ix), ("context", lbl ++ "/" ++ name), ("parent", show parent)]))
     outs <- f caseId (zipWith (\offset ty -> (Port inpId offset, ty)) [0..] tys)
     let outTys = snd <$> outs
-    outId <- addNode ("Output" ++ name) (OpOut (OutputNode caseId outTys [("source", "makeCase")]))
+    setOp outId (OpOut (OutputNode outTys [("source", "makeCase")]))
     for_ (zip (fst <$> outs) (Port outId <$> [0..])) addEdge
-    addOp (OpCase (ix, Case parent (FunctionType tys outTys bratExts) [("name",lbl ++ "/" ++ name)])) caseId
-    pure outTys
+    setOp caseId (OpCase (Case (FunctionType tys outTys bratExts) [("name",lbl ++ "/" ++ name)]))
+    pure (outTys, caseId)
 
   allRowsEqual :: [[HugrType]] -> Bool
   allRowsEqual [] = True
@@ -764,8 +525,8 @@ compilePrimTest parent (port, ty) (PrimCtorTest c tycon unpackingNode outputs) =
   let sumOut = HTSum (SG (GeneralSum [[ty], snd <$> outputs]))
   let sig = FunctionType [ty] [sumOut] ["BRAT"]
   testId <- addNode ("PrimCtorTest " ++ show c)
-            (OpCustom (CustomOp
-                       parent
+            (parent
+            ,OpCustom (CustomOp
                        "BRAT"
                        ("PrimCtorTest::" ++ show tycon ++ "::" ++ show c)
                        sig
@@ -775,19 +536,19 @@ compilePrimTest parent (port, ty) (PrimCtorTest c tycon unpackingNode outputs) =
   pure (Port testId 0, sumOut)
 compilePrimTest parent port@(_, ty) (PrimLitTest tm) = do
   -- Make a Const node that holds the value we test against
-  constId <- addNode "LitConst" (OpConst (ConstOp parent (valFromSimple tm)))
-  loadPort <- head <$> addNodeWithInputs "LitLoad" (OpLoadConstant (LoadConstantOp parent ty))
+  constId <- addNode "LitConst" (parent, OpConst (ConstOp (valFromSimple tm)))
+  loadPort <- head <$> addNodeWithInputs "LitLoad" (parent, OpLoadConstant (LoadConstantOp ty))
                        [(Port constId 0, ty)] [ty]
   -- Connect to a test node
   let sumOut = HTSum (SG (GeneralSum [[ty], []]))
   let sig = FunctionType [ty, ty] [sumOut] ["BRAT"]
   head <$> addNodeWithInputs ("PrimLitTest " ++ show tm)
-           (OpCustom (CustomOp parent "BRAT" ("PrimLitTest::" ++ show ty) sig []))
+           (parent, OpCustom (CustomOp "BRAT" ("PrimLitTest::" ++ show ty) sig []))
            [port, loadPort]
            [sumOut]
 
-constructorOp :: NodeId -> QualName -> QualName -> FunctionType -> HugrOp NodeId
-constructorOp parent tycon c sig = OpCustom (CustomOp parent "BRAT" ("Ctor::" ++ show tycon ++ "::" ++ show c) sig [])
+constructorOp :: QualName -> QualName -> FunctionType -> HugrOp
+constructorOp tycon c sig = OpCustom (CustomOp "BRAT" ("Ctor::" ++ show tycon ++ "::" ++ show c) sig [])
 
 undoPrimTest :: NodeId
              -> [TypedPort] -- The inputs we have to put back together
@@ -798,113 +559,38 @@ undoPrimTest parent inPorts outTy (PrimCtorTest c tycon _ _) = do
   let sig = FunctionType (snd <$> inPorts) [outTy] ["BRAT"]
   head <$> addNodeWithInputs
            ("UndoCtorTest " ++ show c)
-           (constructorOp parent tycon c sig)
+           (parent, constructorOp tycon c sig)
            inPorts
            [outTy]
 undoPrimTest parent inPorts outTy (PrimLitTest tm) = do
   unless (null inPorts) $ error "Unexpected inPorts"
-  constId <- addNode "LitConst" (OpConst (ConstOp parent (valFromSimple tm)))
-  head <$> addNodeWithInputs "LitLoad" (OpLoadConstant (LoadConstantOp parent outTy))
+  constId <- addNode "LitConst" (parent, OpConst (ConstOp (valFromSimple tm)))
+  head <$> addNodeWithInputs "LitLoad" (parent, OpLoadConstant (LoadConstantOp outTy))
            [(Port constId 0, outTy)] [outTy]
 
--- Create a module and FuncDecl nodes inside it for all of the functions given as argument
-compileModule :: VEnv
-              -> Compile ()
-compileModule venv = do
-  moduleNode <- mkModuleNode
-  -- Prepare FuncDef nodes for all functions. Every "noun" also requires a Function
-  -- to compute its value.
-  bodies <- for decls (\(fnName, idNode) -> do
-    (funTy, extra_call, body) <- analyseDecl idNode
-    defNode <- addNode (show fnName ++ "_def") (OpDefn $ FuncDefn moduleNode (show fnName) funTy [])
-    registerFuncDef idNode (defNode, extra_call)
-    pure (body defNode)
-    )
-  for_ bodies (\body -> do
-    st <- get
-    -- At the start of each function, clear out the `compiled` map - these are
-    -- the nodes compiled (usable) within that function. Generally Brat-graph nodes
-    -- are only reachable from one TLD, but the `Id` nodes are shared, and must have
-    -- their own LoadConstant/extra-Call/etc. *within each function*.
-    put st { compiled = M.empty }
-    body)
- where
-  -- Given the Brat-Graph Id node for the decl, work out how to compile it (later);
-  -- return the type of the Hugr FuncDefn, whether said FuncDefn requires an extra Call,
-  -- and the procedure for compiling the contents of the FuncDefn for execution later,
-  -- *after* all such FuncDefns have been registered
-  analyseDecl :: Name -> Compile (PolyFuncType, Bool, NodeId -> Compile ())
-  analyseDecl idNode = do
-    (ns, es) <- gets bratGraph
-    let srcPortTys = [(srcPort, ty) | (srcPort, ty, In tgt _) <- es, tgt == idNode ]
-    case srcPortTys of
+compileKernel :: (Namespace, Store, Graph)
+              -> String -> Name
+              -> (HugrGraph, [(NodeId, OutPort)])
+compileKernel (nsp, store, g@(ns, es)) desc name = (hgr, holelist) where
+  (src_tgt, outs) = case ns M.! name of
+    (BratNode Id _ _) -> case [srcPort | (srcPort, _, In tgt _) <- es, tgt == name ] of
       -- All top-level functions are compiled into Box-es, which should look like this:
-      [(Ex input 0, _)] | Just (BratNode (Box src tgt) _ outs) <- M.lookup input ns ->
-        case outs of
-          [(_, VFun Braty cty)] -> do
-            (inTys, outTys) <- compileSig Braty cty
-            pure (PolyFuncType [] (FunctionType inTys outTys bratExts), False, compileBox (src, tgt))
-          [(_, VFun Kerny cty)] -> do
-            -- We're compiling, e.g.
-            --   f :: { Qubit -o Qubit }
-            --   f = { h; circ(pi) }
-            -- Although this looks like a constant kernel, we'll have to compile the
-            -- computation that produces this constant. We do so by making a FuncDefn
-            -- that takes no arguments and produces the constant kernel graph value.
-            thunkTy <- HTFunc . PolyFuncType [] . (\(ins, outs) -> FunctionType ins outs bratExts) <$> compileSig Kerny cty
-            pure (funcReturning [thunkTy], True, \parent ->
-              withIO parent thunkTy $ compileKernBox parent input (compileBox (src, tgt)) cty)
-          _ -> error "Box should have exactly one output of Thunk type"
-      _ -> do -- a computation, or several values
-        outs <- compilePorts srcPortTys -- note compiling already-erased types, is this right?
-        pure (funcReturning outs, True, compileNoun outs (map fst srcPortTys))
-
-  withIO :: NodeId -> HugrType -> Compile TypedPort -> Compile ()
-  withIO parent output c = do
-    addNode "input" (OpIn (InputNode parent [] [("source", "analyseDecl")]))
-    output <- addNode "output" (OpOut (OutputNode parent [output] [("source", "analyseDecl")]))
-    wire <- c
-    addEdge (fst wire, Port output 0)
-
-  -- top-level decls that are not Prims. RHS is the brat idNode
-  decls :: [(QualName, Name)]
-  decls = do -- in list monad, no Compile here
-            (fnName, wires) <- M.toList venv
-            let (Ex idNode _) = end (fst $ head wires) -- would be better to check same for all rather than just head
-            case hasPrefix ["checking","globals","decl"] idNode of
-              Just _ -> pure (fnName, idNode) -- assume all ports are 0,1,2...
-              Nothing -> []
-
-  mkModuleNode :: Compile NodeId
-  mkModuleNode = do
-    id <- freshNode "module"
-    addOp (OpMod $ ModuleOp id) id
-    pure id
-
-  funcReturning :: [HugrType] -> PolyFuncType
-  funcReturning outs = PolyFuncType [] (FunctionType [] outs bratExts)
-
-compileNoun :: [HugrType] -> [OutPort] -> NodeId -> Compile ()
-compileNoun outs srcPorts parent = do
-  addNode "input" (OpIn (InputNode parent [] [("source", "compileNoun")]))
-  output <- addNode "output" (OpOut (OutputNode parent outs [("source", "compileNoun")]))
-  for_ (zip [0..] srcPorts) (\(outport, Ex src srcPort) ->
-    compileWithInputs parent src >>= \case
-      Just nodeId -> addEdge (Port nodeId srcPort, Port output outport) $> ()
-      Nothing -> pure () -- if input not compilable, leave edge missing in Hugr - or just error?
-    )
-
-compile :: Store
-        -> Namespace
-        -> Graph
-        -> CaptureSets
-        -> VEnv
-        -> BS.ByteString
-compile store ns g capSets venv
-  = evalState
-    (trackM "compileFunctions" *>
-     compileModule venv *>
-     trackM "dumpJSON" *>
-     dumpJSON
-    )
-    (emptyCS g capSets ns store)
+      [Ex input 0] | Just (BratNode (Box src tgt) [] outs) <- M.lookup input ns -> ((src, tgt), outs)
+    (BratNode (Box src tgt) [] outs) -> ((src, tgt), outs)
+    nt -> error $ "Can only compile Box nodes or Id from them, not " ++ show nt ++ " (for " ++ show name ++ ")"
+  cty = case outs of
+    [(_, VFun Kerny cty)] -> cty
+  startHugr = H.new nsp desc (OpDFG $ DFG (FunctionType hInTys hOutTys bratExts) [])
+  (hgr, holelist) = flip evalState (makeCS (g,store) startHugr) $ do
+    ctr <- makeIO desc (root startHugr)
+    compileBox ctr src_tgt
+    hugr <- gets hugr
+    hs <- gets holes
+    pure (hugr, hs <>> [])
+
+  (hInTys, hOutTys) = runLocalChecking (evalCTy S0 Kerny cty <&> (\(ss :->> ts) -> (compileRo ss, compileRo ts)))
+
+  runLocalChecking :: Free CheckingSig t -> t
+  runLocalChecking (Ret t) = t
+  runLocalChecking (Req (ELup e) k) = runLocalChecking (k (M.lookup e (valueMap store)))
+  runLocalChecking (Req _ _) = error "Compile monad found a command it can't handle"
diff --git a/brat/Brat/Compiler.hs b/brat/Brat/Compiler.hs
index 093195be..8959f510 100644
--- a/brat/Brat/Compiler.hs
+++ b/brat/Brat/Compiler.hs
@@ -3,21 +3,29 @@ module Brat.Compiler (printAST
                      ,writeDot
                      ,compileFile
                      ,compileAndPrintFile
+                     ,compileToGraph
                      ,CompilingHoles(..)
                      ) where
 
-import Brat.Checker.Types (TypedHole)
+import Brat.Checker.Types (TypedHole, Modey(Kerny))
 import Brat.Compile.Hugr
 import Brat.Dot (toDotString)
 import Brat.Elaborator
 import Brat.Error
+import Brat.Graph(Node(BratNode), NodeType(Box))
 import Brat.Load
-import Brat.Naming (root, split)
+import Brat.Naming (Namespace, root, split, Name)
+import Brat.Syntax.Port (OutPort)
+import Brat.Syntax.Value (Val(VFun))
+
 
 import Control.Exception (evaluate)
 import Control.Monad (when)
 import Control.Monad.Except
 import qualified Data.ByteString.Lazy as BS
+import Data.Foldable (for_)
+import Data.HugrGraph (HugrGraph, NodeId, to_json)
+import qualified Data.Map as M
 import System.Exit (die)
 
 printDeclsHoles :: [FilePath] -> String -> IO ()
@@ -71,17 +79,29 @@ 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
-  (venv, _, holes, defs, outerGraph, capSets) <- eitherIO env
+  (newRoot,) <$> eitherIO env
+
+-- Map from box name to (compiled bytes, list of splices)
+-- TODO: should keep Hugr as struct not ByteString
+type CompilationResult = M.Map Name (HugrGraph, [(NodeId, OutPort)])
+
+compileFile :: [FilePath] -> String -> IO (Either CompilingHoles CompilationResult)
+compileFile libDirs file = do
+  (newRoot, (_, _, holes, st, outerGraph, _)) <- compileToGraph libDirs file
   case holes of
-    [] -> Right <$> evaluate -- turns 'error' into IO 'die'
-                    (compile defs newRoot outerGraph capSets venv)
+    [] -> let boxes :: [Name] = [n | (n, BratNode (Box _ _) [] [(_, VFun Kerny _)]) <- (M.toList $ fst outerGraph)]
+          in Right <$> (evaluate -- turns 'error' into IO 'die'
+                    $ M.fromList [(n, compileKernel (newRoot, st, outerGraph) "root" n) | n <- boxes])
     hs -> pure $ Left (CompilingHoles hs)
 
 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)
diff --git a/brat/Brat/Graph.hs b/brat/Brat/Graph.hs
index 62c4619b..fb86645b 100644
--- a/brat/Brat/Graph.hs
+++ b/brat/Brat/Graph.hs
@@ -51,6 +51,9 @@ 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
+  Copy :: NodeType Brat
 
 deriving instance Show (NodeType a)
 
@@ -110,9 +113,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 +121,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 ]
diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
index 75570454..0df3f0ad 100644
--- a/brat/Brat/Load.hs
+++ b/brat/Brat/Load.hs
@@ -2,6 +2,7 @@ module Brat.Load (loadFilename
                  ,loadFiles
                  ,parseFile
                  ,desugarEnv
+                 ,VMod
                  ) where
 
 import Brat.Checker
diff --git a/brat/Brat/Machine.hs b/brat/Brat/Machine.hs
new file mode 100644
index 00000000..364cd8af
--- /dev/null
+++ b/brat/Brat/Machine.hs
@@ -0,0 +1,283 @@
+module Brat.Machine (runInterpreter) where
+
+import Brat.Checker.Monad (CaptureSets)
+import Brat.Checker.Types (Store)
+import Brat.Compiler (compileToGraph)
+import Brat.Compile.Hugr (compileKernel)
+import Brat.Constructors.Patterns
+import Brat.Naming (Name, Namespace, split)
+import Brat.Graph (Graph, NodeType (..), Node (BratNode, KernelNode), wiresTo, MatchSequence (..), PrimTest (..), TestMatchData (..))
+import Brat.QualName (QualName, plain)
+import Brat.Syntax.Simple (SimpleTerm(..))
+import Brat.Syntax.Port (OutPort(..))
+import Brat.Syntax.Common
+import Brat.Syntax.Value
+
+import qualified Data.HugrGraph as HG
+import Hasochism
+
+import qualified Data.ByteString.Lazy as BS
+import Data.Maybe (fromMaybe, fromJust)
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Bwd
+import Util (zipSameLength)
+
+import Debug.Trace
+
+type GraphInfo = (Graph, Store, Namespace, CaptureSets)
+
+runInterpreter :: [FilePath] -> String -> String -> IO ()
+runInterpreter libDirs file runFunc = do
+    (root, (venv, _, _, st, outerGraph, capSets)) <- compileToGraph libDirs file
+    print (show outerGraph)
+    let outPorts = [op | (NamedPort op _, _ty) <- venv M.! (plain runFunc)]
+    let outTask = evalPorts (outerGraph, st, root, capSets) (B0 :< BratValues M.empty) B0 outPorts
+    -- we hope outTask is a Finished. Or a Suspend.
+    case outTask of
+      Finished [(KernelV hugr)] -> do
+        putStrLn "Final Hugr Graph:"
+        BS.putStr (HG.to_json hugr)
+      _ -> print outTask
+
+data Frame where
+    BratValues :: EvalEnv -> Frame
+    -- Optionally "what to do when all ports evaled" - Node weight, name+offset requested
+    -- then state of evaluating inputs: (values computed, ports whose values still needed)
+    EvalPorts :: Bwd Value -> [OutPort] -> Frame
+    PortOfNode :: OutPort -> Frame
+    HandleNodeOutputs :: OutPort -> Frame
+    -- have arguments to function, waiting for the function:
+    CallWith :: [Value] -> Frame
+    ReturnTo :: Bwd Frame -> Frame
+    Alternatives :: [(TestMatchData Brat, Name)] -> [Value] -> Frame
+    PerformMatchTests :: [(Src, PrimTest (BinderType Brat))] -> [(Src, BinderType Brat)] -> Name -> Frame
+    DoSplices :: HG.HugrGraph -> HG.NodeId -> [(HG.NodeId, OutPort)] -> Frame
+  deriving Show
+
+data Task where
+    EvalPort :: OutPort -> Task
+    Suspend :: [Frame] -> Task -> Task
+    EvalNode :: Name -> [Value] -> Task
+    Use :: Value -> Task -- searches for EvalPorts or DoSplices
+    Finished :: [Value] -> Task -- searches for HandleNodeOutputs, or final result
+    TryNextMatch :: Task
+    NoMatch :: Task
+    StuckOnNode :: Name -> Node -> Task
+  deriving Show
+
+lookupOutport :: Bwd Frame -> OutPort -> Maybe Value
+lookupOutport B0 _ = Nothing
+lookupOutport (_ :< BratValues env) p | Just v <- M.lookup p env = Just v
+lookupOutport (fz :< _) p = lookupOutport fz p
+
+evalPorts :: GraphInfo -> Bwd Frame -> Bwd Value -> [OutPort] -> Task
+-- EvalPorts is "missing" one input (between valz and ports), i.e. the one that's the current Task
+-- (whereas evalPorts has them all)
+evalPorts g fz valz (p:ps) = run g (fz :< EvalPorts valz ps) (EvalPort p)
+evalPorts g fz valz [] = run g fz (Finished (valz <>> []))
+
+getNodeInputs :: GraphInfo -> Name -> [OutPort]
+getNodeInputs (g, _, _, _) name = M.elems (M.fromList [(tgtPort, src) | (src, _, In _ tgtPort) <- wiresTo name g])
+
+evalNodeInputs :: GraphInfo -> Bwd Frame -> Name -> Task
+evalNodeInputs gi fz name =
+    -- might be good to check M.keys == [0,1,....] here
+    evalPorts gi fz B0 (getNodeInputs gi name)
+
+updateCache (fz :< BratValues env) port_vals = fz :< (BratValues $ foldr (uncurry M.insert) env port_vals)
+updateCache (fz :< f) pvs = (updateCache fz pvs) :< f
+-- updateCache B0 pvs = B0 :< (M.fromList pvs)
+
+evalSplices :: GraphInfo -> Bwd Frame -> HG.HugrGraph -> [(HG.NodeId, OutPort)] -> Task
+evalSplices gi fz hugr [] = run gi fz (Finished [KernelV hugr])
+evalSplices gi fz hugr ((nid, outport):rest) =
+    run gi (fz :< DoSplices hugr nid rest) (EvalPort outport)
+
+run :: GraphInfo -> Bwd Frame -> Task -> Task
+run g fz t | trace ("RUN: " ++ show fz ++ "\n" ++ show t) False = undefined
+
+-- Tasks that push new frames onto the stack to do things
+run gi@(g@(nodes, wires), _, _, _) fz (EvalPort p@(Ex name offset)) = case lookupOutport fz p of
+    Just v -> run gi fz (Use v)
+    Nothing -> evalNodeInputs gi (fz :< PortOfNode p) name
+run gi@(g@(nodes, _), st, root, cs) fz t@(EvalNode n ins) = case nodes M.! n of
+    nw | trace ("EVALNODE " ++ show nw) False -> undefined
+    (BratNode (Const st) _ _) -> run gi fz (Finished [evalSimpleTerm st])
+    (BratNode (ArithNode op) _ _) -> run gi fz (Finished [evalArith op ins])
+    (BratNode Id _ _) -> run gi fz (Finished ins)
+    (BratNode (Eval func) _ _) -> run gi (fz :< CallWith ins) (EvalPort func)
+    (BratNode (Box src tgt) [] [(_, VFun Kerny _)]) ->
+        let (sub, newRoot) = split "box" root
+            (hugr, splices) = compileKernel (sub, st, g) "box" n
+        in evalSplices (g, st, newRoot, cs) fz hugr splices
+    (BratNode (Box src tgt) _ _) ->
+        let captureSet = fromMaybe M.empty (M.lookup n cs)
+            capturedSrcs = S.fromList [src | (NamedPort src _name, _ty) <- concat (M.elems captureSet)]
+        in run gi fz (Finished [ThunkV $ BratClosure (captureEnv fz capturedSrcs) src tgt])
+    (BratNode (PatternMatch (c:|cs)) _ _) -> run gi (fz :< Alternatives (c:cs) ins) TryNextMatch
+    (BratNode (Constructor c) _ _) -> run gi fz (Finished [evalConstructor c ins])
+    (BratNode (Dummy k) _ _) -> run gi fz (Finished [DummyV])
+    nw -> run gi fz (StuckOnNode n nw)
+
+
+-- Tasks that unwind the stack looking for what to do with the result
+----Suspend
+run gi (fz :< f) (Suspend fs t) = run gi fz (Suspend (f:fs) t)
+run _ B0 t@(Suspend _ _) = t
+---- Use (single value)
+run gi (fz :< EvalPorts valz rem) (Use v) = evalPorts gi fz (valz :< v) rem
+run gi (fz :< DoSplices hugr nid rest) (Use v) =
+    let (KernelV sub_hugr) = v
+        hugr' = HG.splice hugr nid sub_hugr
+    in evalSplices gi fz hugr' rest
+run gi (fz :< CallWith inputs) (Use (ThunkV (BratClosure env src tgt))) =
+    let env_with_args = foldr (uncurry M.insert) env [(Ex src off, val) | (off, val) <- zip [0..] inputs]
+    in evalNodeInputs gi (B0 :< ReturnTo fz :< (BratValues env_with_args)) tgt
+
+---- Finished (list of values)
+run gi (fz :< PortOfNode req@(Ex name offset)) (Finished inputs) =
+    run gi (fz :< HandleNodeOutputs req) (EvalNode name inputs)
+run gi (fz :< HandleNodeOutputs req@(Ex name offset)) (Finished outputs) =
+    run gi (updateCache fz [(Ex name i, val) | (i, val) <- zip [0..] outputs]) (Use (outputs !! offset))
+run gi (B0 :< ReturnTo fz) (Finished vals) = run gi fz (Finished vals)
+
+-- TryNextMatch
+run gi (fz :< Alternatives [] _) TryNextMatch = run gi fz NoMatch
+run gi (fz :< Alternatives ((TestMatchData _ ms, box):cs) ins) TryNextMatch =
+    let MatchSequence matchInputs matchTests matchOutputs = ms
+        testInputs = M.fromList (fromJust $ zipSameLength [src | (NamedPort src _,_ty) <- matchInputs] ins)
+        outEnv = doAllTests testInputs matchTests
+    in case trace ("outEnv: " ++ show outEnv ++ "\nmatchOutputs: " ++ show matchOutputs) outEnv of
+        Nothing -> run gi (fz :< Alternatives cs ins) TryNextMatch
+        Just env ->
+            let vals = [miniEval gi env src | (NamedPort src _, _) <- matchOutputs]
+            in run gi (fz :< CallWith vals) (EvalPort $ Ex box 0)
+
+run gi (fz :< BratValues _) t = run gi fz t
+run gi B0 t = t
+run gi fz t = run gi fz (Suspend [] t)
+
+miniEval :: GraphInfo -> EvalEnv -> OutPort -> Value
+miniEval _ env x | Just v <- M.lookup x env = v
+miniEval gi@((nodes, _), _, _, _) env (Ex node 0) =
+  let inputs = miniEval gi env <$> getNodeInputs gi node
+  in  case nodes M.! node of
+        BratNode (ArithNode op) _ _ -> evalArith op inputs
+        BratNode (Const x) _ _ -> evalSimpleTerm x
+        BratNode (Constructor c) _ _ -> evalConstructor c inputs
+        BratNode Id _ _ | [v] <- inputs -> v
+        nw -> error $ "miniEval: " ++ show nw
+
+evalConstructor :: QualName -> [Value] -> Value
+evalConstructor CTrue [] = BoolV True
+evalConstructor CFalse [] = BoolV False
+evalConstructor CZero [] = IntV 0
+evalConstructor CSucc [IntV n] = IntV (n + 1)
+evalConstructor CDoub [IntV n] = IntV (2 * n)
+evalConstructor CNil [] = VecV []
+evalConstructor CCons [hd, VecV tl] = VecV (hd:tl)
+evalConstructor CSnoc [VecV tl, hd] = VecV (tl ++ [hd])
+evalConstructor CConcatEqEven [VecV ls, VecV rs] = VecV (ls ++ rs)
+evalConstructor CRiffle [VecV evens, VecV odds] = VecV (riffle evens odds)
+ where
+  riffle [] [] = []
+  riffle (e:es) (o:os) = e:o:riffle es os
+evalConstructor CQubit [] = DummyV
+evalConstructor CConcatEqOdd [VecV ls, mid, VecV rs] = VecV (ls ++ mid:rs)
+evalConstructor name _ = error $ "Internal error: Unhandled constructor " ++ show name
+
+doAllTests :: EvalEnv -> [(Src, PrimTest (BinderType Brat))] -> Maybe EvalEnv
+doAllTests env [] = Just env
+doAllTests env ((NamedPort outport _, test):tests) =
+  case test of
+    PrimLitTest term -> if testLiteral term (env M.! outport)
+                        then doAllTests env tests
+                        else Nothing
+    PrimCtorTest ctor ty _ outSrcs -> do
+      outputs <- testCtor ty ctor (env M.! outport)
+      doAllTests (env `M.union` M.fromList (zip (end . fst <$> outSrcs) outputs)) tests
+
+captureEnv :: Bwd Frame -> S.Set OutPort -> EvalEnv
+captureEnv B0 _ = M.empty
+captureEnv (fz :< BratValues env) keys = M.union (captureEnv fz keys) (M.filterWithKey (\k _ -> S.member k keys) env)
+captureEnv (fz :< _) keys = captureEnv fz keys
+
+evalSimpleTerm :: SimpleTerm -> Value
+evalSimpleTerm (Num x) = IntV x
+evalSimpleTerm (Float x) = FloatV x
+evalSimpleTerm t = error ("todo " ++ show t)
+
+evalArith :: ArithOp -> [Value] -> Value
+evalArith op [IntV x, IntV y] = IntV $ case op of
+  Add -> x + y
+  Sub -> x - y
+  Mul -> x * y
+  Div -> div x y
+  Pow -> x ^ y
+evalArith op [FloatV x, FloatV y] = FloatV $ case op of
+  Add -> x + y
+  Sub -> x - y
+  Mul -> x * y
+  Div -> x / y
+  Pow -> x ** y
+evalArith _ _ = error "Bad arith inputs"
+
+testLiteral :: SimpleTerm -> Value -> Bool
+testLiteral (Num x) (IntV y) = x == y
+testLiteral (Float x) (FloatV y) = x == y
+testLiteral _ _ = error "Internal error: Unexpected literal test"
+
+testCtor :: QualName -> QualName -> Value -> Maybe [Value]
+testCtor CBool CTrue (BoolV True) = Just []
+testCtor CBool CFalse (BoolV False) = Just []
+testCtor CNat CZero (IntV 0) = Just []
+testCtor CNat CSucc (IntV x) | x > 0 = Just [IntV (x - 1)]
+testCtor CVec CNil (VecV []) = Just []
+testCtor CVec CCons (VecV (v:vs)) = Just [v, VecV vs]
+testCtor CVec CConcatEqEven (VecV vs) = do
+  (half, 0) <- pure (length vs `divMod` 2)
+  (xs, ys) <- pure (splitAt half vs)
+  pure [VecV xs, VecV ys]
+testCtor CVec CRiffle (VecV vs) = do
+  (evens, odds) <- evenOdds vs
+  pure [VecV evens, VecV odds]
+ where
+  evenOdds :: [a] -> Maybe ([a], [a])
+  evenOdds [] = pure ([], [])
+  evenOdds [x] = Nothing
+  evenOdds (x:y:xs) = do
+    (evens, odds) <- evenOdds xs
+    pure (x:evens, y:odds)
+
+testCtor CVec CConcatEqOdd (VecV vs) = do
+  (half, 1) <- pure (length vs `divMod` 2)
+  (xs, y:zs) <- pure (splitAt half vs)
+  pure [VecV xs, y, VecV zs]
+testCtor _ _ _ = Nothing
+
+data Value =
+    IntV Int
+  | FloatV Double
+  | BoolV Bool
+  | VecV [Value]
+  | ThunkV BratThunk
+  | KernelV HG.HugrGraph
+  | DummyV
+
+data BratThunk =
+    -- this might want to be [EvalEnv] or something like that
+    BratClosure EvalEnv Name Name  -- Captured environment, src node, tgt node
+  | BratPrim String String (CTy Brat Z)
+
+instance Show Value where
+  show (IntV x) = show x
+  show (FloatV x) = show x
+  show (BoolV x) = show x
+  show (VecV xs) = show xs
+  show (ThunkV _) = "<thunk>"
+  show (KernelV k) = "Kernel (" ++ show k ++ ")"
+  show DummyV = "Dummy"
+
+type EvalEnv = M.Map OutPort Value
diff --git a/brat/Data/Hugr.hs b/brat/Data/Hugr.hs
index d08e6418..6ea8b202 100644
--- a/brat/Data/Hugr.hs
+++ b/brat/Data/Hugr.hs
@@ -14,6 +14,19 @@ import Data.Text (Text, pack)
 
 import Brat.Syntax.Simple
 
+orderEdgeOffset :: Int
+orderEdgeOffset = -1
+
+data PortId node = Port
+  { nodeId :: node
+  , offset :: Int
+  }
+ deriving (Eq, Functor, Show)
+
+instance ToJSON node => ToJSON (PortId node) where
+  toJSON (Port node offset) = toJSON (node, offset')
+    where offset' = if offset == orderEdgeOffset then Nothing else Just offset
+
 -- We should be able to work out exact extension requirements for our functions,
 -- but instead we'll overapproximate.
 bratExts :: [ExtensionId]
@@ -63,6 +76,9 @@ data HugrType
   | HTFunc PolyFuncType
  deriving (Eq, Show)
 
+class JSONParent n where
+  toJSONp :: n -> Value -> Value
+
 instance ToJSON HugrType where
   toJSON HTQubit = object ["t" .= ("Q" :: Text)]
   toJSON (HTSum (SU (UnitSum size))) = object ["t" .= ("Sum" :: Text)
@@ -225,33 +241,26 @@ valFromSimple Unit = hvUnit
 -------------------------------------- OPS -------------------------------------
 ---------------------  (Depends on HugrValue and HugrType) ---------------------
 
-data ModuleOp node = ModuleOp { parent :: node } deriving (Eq, Functor, Show)
+data ModuleOp = ModuleOp deriving (Eq, Show)
 
-instance Eq a => Ord (ModuleOp a) where
-  compare _ _ = EQ
+instance JSONParent ModuleOp where
+  toJSONp ModuleOp parent = object ["parent" .= parent
+                                   ,"op" .= ("Module" :: Text)
+                                   ]
 
-instance ToJSON node => ToJSON (ModuleOp node) where
-  toJSON (ModuleOp parent) = object ["parent" .= parent
-                                    ,"op" .= ("Module" :: Text)
-                                    ]
-
-data FuncDefn node = FuncDefn
- { parent :: node
- , name :: String
+data FuncDefn = FuncDefn
+ { name :: String
  , signature_ :: PolyFuncType
  , metadata :: [(String, String)]
- } deriving (Eq, Functor, Show)
-
-instance Eq a => Ord (FuncDefn a) where
-  compare _ _ = EQ
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (FuncDefn node) where
-  toJSON (FuncDefn { .. }) = object ["parent" .= parent
-                                    ,"op" .= ("FuncDefn" :: Text)
-                                    ,"name" .= name
-                                    ,"signature" .= signature_
-                                    ,"metadata" .= metadata
-                                    ]
+instance JSONParent FuncDefn where
+  toJSONp (FuncDefn { .. }) parent = object ["parent" .= parent
+                                            ,"op" .= ("FuncDefn" :: Text)
+                                            ,"name" .= name
+                                            ,"signature" .= signature_
+                                            ,"metadata" .= metadata
+                                            ]
 
 data CustomConst where
   CC :: forall a. (Eq a, Show a, ToJSON a) => String -> a -> CustomConst
@@ -269,67 +278,51 @@ instance ToJSON CustomConst where
 
 type ExtensionName = String
 
-data ConstOp node = ConstOp
- { parent :: node
- , const :: HugrValue
- } deriving (Eq, Functor, Show)
-
-instance Eq a => Ord (ConstOp a) where
-  compare _ _ = EQ
+data ConstOp = ConstOp
+ { const :: HugrValue
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (ConstOp node) where
-  toJSON (ConstOp {..}) = object ["parent" .= parent
-                                 ,"op" .= ("Const" :: Text)
-                                 ,"v" .= const
-                                 ]
+instance JSONParent ConstOp where
+  toJSONp (ConstOp {..}) parent = object ["parent" .= parent
+                                         ,"op" .= ("Const" :: Text)
+                                         ,"v" .= const
+                                         ]
 
 
 
-data InputNode node = InputNode
- { parent :: node
- , types  :: [HugrType]
+data InputNode = InputNode
+ { types  :: [HugrType]
  , metadata :: [(String, String)]
- } deriving (Eq, Functor, Show)
-
-instance Eq a => Ord (InputNode a) where
-  compare _ _ = EQ
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (InputNode node) where
-  toJSON (InputNode parent types metadata) = object ["parent" .= parent
-                                                    ,"op" .= ("Input" :: Text)
-                                                    ,"types" .= types
-                                                    ,"metadata" .= metadata
-                                                    ]
+instance JSONParent InputNode where
+  toJSONp (InputNode types metadata) parent = object ["parent" .= parent
+                                                     ,"op" .= ("Input" :: Text)
+                                                     ,"types" .= types
+                                                     ,"metadata" .= metadata
+                                                     ]
 
-data OutputNode node = OutputNode
- { parent :: node
- , types  :: [HugrType]
+data OutputNode = OutputNode
+ { types  :: [HugrType]
  , metadata :: [(String, String)]
- } deriving (Eq, Functor, Show)
-
-instance Eq a => Ord (OutputNode a) where
-  compare _ _ = EQ
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (OutputNode node) where
-  toJSON (OutputNode { .. }) = object ["parent" .= parent
-                                      ,"op" .= ("Output" :: Text)
-                                      ,"types" .= types
-                                      ,"metadata" .= metadata
-                                      ]
+instance JSONParent OutputNode where
+  toJSONp (OutputNode { .. }) parent = object ["parent" .= parent
+                                              ,"op" .= ("Output" :: Text)
+                                              ,"types" .= types
+                                              ,"metadata" .= metadata
+                                              ]
 
-data Conditional node = Conditional
- { parent :: node
- , sum_rows :: [[HugrType]]
+data Conditional = Conditional
+ { sum_rows :: [[HugrType]]
  , other_inputs :: [HugrType]
  , outputs :: [HugrType]
  , metadata :: [(String, String)]
- } deriving (Eq, Functor, Show)
-
-instance Eq a => Ord (Conditional a) where
-  compare _ _ = EQ
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (Conditional node) where
-  toJSON (Conditional { .. })
+instance JSONParent Conditional where
+  toJSONp (Conditional { .. }) parent
    = object ["op" .= ("Conditional" :: Text)
             ,"parent" .= parent
             ,"sum_rows" .= sum_rows
@@ -339,21 +332,17 @@ instance ToJSON node => ToJSON (Conditional node) where
             ,"metadata" .= metadata
             ]
 
-data Case node = Case
-  { parent :: node
-  , signature_ :: FunctionType
+data Case = Case
+  { signature_ :: FunctionType
   , metadata :: [(String, String)]
-  } deriving (Eq, Functor, Show)
+  } deriving (Eq, Show)
 
-instance Eq node => Ord (Case node) where
-  compare _ _ = EQ
-
-instance ToJSON node => ToJSON (Case node) where
-  toJSON (Case { .. }) = object ["op" .= ("Case" :: Text)
-                                ,"parent" .= parent
-                                ,"signature" .= signature_
-                                ,"metadata" .= metadata
-                                ]
+instance JSONParent Case where
+  toJSONp (Case { .. }) parent = object ["op" .= ("Case" :: Text)
+                                        ,"parent" .= parent
+                                        ,"signature" .= signature_
+                                        ,"metadata" .= metadata
+                                        ]
 
 {-
 data Const = Const
@@ -363,34 +352,26 @@ data Const = Const
  }
 -}
 
-data DFG node = DFG
- { parent :: node
- , signature_ :: FunctionType
+data DFG = DFG
+ { signature_ :: FunctionType
  , metadata :: [(String, String)]
- } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (DFG node) where
-  compare _ _ = EQ
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (DFG node) where
-  toJSON (DFG { .. }) = object ["op" .= ("DFG" :: Text)
-                               ,"parent" .= parent
-                               ,"signature" .= signature_
-                               ,"metadata" .= metadata
-                               ]
+instance JSONParent DFG where
+  toJSONp (DFG { .. }) parent = object ["op" .= ("DFG" :: Text)
+                                       ,"parent" .= parent
+                                       ,"signature" .= signature_
+                                       ,"metadata" .= metadata
+                                       ]
 
-data TagOp node = TagOp
- { parent :: node
- , tag :: Int
+data TagOp = TagOp
+ { tag :: Int
  , variants :: [[HugrType]]
  , metadata :: [(String, String)]
- } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (TagOp node) where
-  compare _ _ = EQ
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (TagOp node) where
-  toJSON (TagOp parent tag variants metadata)
+instance JSONParent TagOp where
+  toJSONp (TagOp tag variants metadata) parent
    = object ["parent" .= parent
             ,"op" .= ("Tag" :: Text)
             ,"tag" .= tag
@@ -398,41 +379,33 @@ instance ToJSON node => ToJSON (TagOp node) where
             ,"metadata" .= metadata
             ]
 
-data MakeTupleOp node = MakeTupleOp
- { parent :: node
- , tys :: [HugrType]
- } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (MakeTupleOp node) where
-  compare _ _ = EQ
+data MakeTupleOp = MakeTupleOp
+ { tys :: [HugrType]
+ } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (MakeTupleOp node) where
-  toJSON (MakeTupleOp parent tys)
+instance JSONParent MakeTupleOp where
+  toJSONp (MakeTupleOp tys) parent
    = object ["parent" .= parent
             ,"op" .= ("MakeTuple" :: Text)
             ,"tys" .= tys
             ]
 
-data CustomOp node = CustomOp
-  { parent :: node
-  , extension :: String
+data CustomOp = CustomOp
+  { extension :: String
   , op_name :: String
   , signature_ :: FunctionType
   , args :: [TypeArg]
-  } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (CustomOp node) where
-  compare _ _ = EQ
-
-instance ToJSON node => ToJSON (CustomOp node) where
-  toJSON (CustomOp { .. }) = object ["parent" .= parent
-                                    ,"op" .= ("CustomOp" :: Text)
-                                    ,"description" .= ("" :: Text)
-                                    ,"extension" .= pack extension
-                                    ,"args" .= args
-                                    ,"op_name" .= pack op_name
-                                    ,"signature" .= signature_
-                                    ]
+  } deriving (Eq, Show)
+
+instance JSONParent CustomOp where
+  toJSONp (CustomOp { .. }) parent = object ["parent" .= parent
+                                            ,"op" .= ("CustomOp" :: Text)
+                                            ,"description" .= ("" :: Text)
+                                            ,"extension" .= pack extension
+                                            ,"args" .= args
+                                            ,"op_name" .= pack op_name
+                                            ,"signature" .= signature_
+                                            ]
 
 -- In BRAT, we're not using the type parameter machinery of hugr for
 -- polymorphism, so calls can just take simple signatures.
@@ -442,16 +415,12 @@ instance ToJSON node => ToJSON (CustomOp node) where
 --
 -- TODO: Instead of using hugr type args, we should be using coercions for
 -- polymorphic function arguments.
-data CallOp node = CallOp
-  { parent :: node
-  , signature_ :: FunctionType
-  } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (CallOp node) where
-  compare _ _ = EQ
+data CallOp = CallOp
+  { signature_ :: FunctionType
+  } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (CallOp node) where
-  toJSON (CallOp parent signature_) =
+instance JSONParent CallOp where
+  toJSONp (CallOp signature_) parent =
     object ["parent" .= parent
            ,"op" .= ("Call" :: Text)
            ,"func_sig" .= PolyFuncType [] signature_
@@ -459,37 +428,38 @@ instance ToJSON node => ToJSON (CallOp node) where
            ,"instantiation" .= signature_
            ]
 
-intOp :: node -> String -> [HugrType] -> [HugrType] -> [TypeArg] -> CustomOp node
-intOp parent opName ins outs = CustomOp parent "arithmetic.int_ops" opName (FunctionType ins outs ["arithmetic.int_ops"])
+intOp :: String -> [HugrType] -> [HugrType] -> [TypeArg] -> CustomOp
+intOp opName ins outs = CustomOp "arithmetic.int_ops" opName (FunctionType ins outs ["arithmetic.int_ops"])
 
-binaryIntOp :: node -> String -> CustomOp node
-binaryIntOp parent name
- = intOp parent name [hugrInt, hugrInt] [hugrInt] [TANat intWidth]
+binaryIntOp :: String -> CustomOp
+binaryIntOp name
+ = intOp name [hugrInt, hugrInt] [hugrInt] [TANat intWidth]
 
-floatOp :: node -> String -> [HugrType] -> [HugrType] -> [TypeArg] -> CustomOp node
-floatOp parent opName ins outs = CustomOp parent "arithmetic.float_ops" opName (FunctionType ins outs ["arithmetic.float_ops"])
+floatOp :: String -> [HugrType] -> [HugrType] -> [TypeArg] -> CustomOp
+floatOp opName ins outs = CustomOp "arithmetic.float_ops" opName (FunctionType ins outs ["arithmetic.float_ops"])
 
-binaryFloatOp :: node -> String -> CustomOp node
-binaryFloatOp parent name = floatOp parent name [hugrFloat, hugrFloat] [hugrFloat] []
+binaryFloatOp :: String -> CustomOp
+binaryFloatOp name = floatOp name [hugrFloat, hugrFloat] [hugrFloat] []
 
-data CallIndirectOp node = CallIndirectOp
-  { parent :: node
-  , signature_ :: FunctionType
-  } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (CallIndirectOp node) where
-  compare _ _ = EQ
+data CallIndirectOp = CallIndirectOp
+  { signature_ :: FunctionType
+  } deriving (Eq, Show)
 
-instance ToJSON node => ToJSON (CallIndirectOp node) where
-  toJSON (CallIndirectOp parent signature_) = object ["parent" .= parent
-                                                     ,"signature" .= signature_
-                                                     ,"op" .= ("CallIndirect" :: Text)
-                                                     ]
+instance JSONParent CallIndirectOp where
+  toJSONp (CallIndirectOp signature_) parent = object ["parent" .= parent
+                                                      ,"signature" .= signature_
+                                                      ,"op" .= ("CallIndirect" :: Text)
+                                                      ]
 
-holeOp :: node -> Int -> FunctionType -> CustomOp node
-holeOp parent idx sig = CustomOp parent "BRAT" "Hole" sig
+holeOp :: Int -> FunctionType -> CustomOp
+holeOp idx sig = CustomOp "BRAT" "Hole" sig
                         [TANat idx, TAType (HTFunc (PolyFuncType [] sig))]
 
+isHole :: HugrOp -> Maybe (Int, FunctionType)
+isHole (OpCustom (CustomOp "BRAT" "Hole" sig args)) =
+  let [TANat idx, _] = args in Just (idx, sig) -- crash rather than return false for bad args
+isHole _ = Nothing
+
 -- TYPE ARGS:
 --  * A length-2 sequence comprising:
 --    * A sequence of types (the inputs of outerSig)
@@ -500,12 +470,11 @@ holeOp parent idx sig = CustomOp parent "BRAT" "Hole" sig
 --  * Many graphs with types given by innerSigs (to go in the holes)
 -- OUTPUT:
 --  * A single graph whose signature is the same as outerSig
-substOp :: node
-        -> {- outerSig :: -}FunctionType
+substOp :: {- outerSig :: -}FunctionType
         -> {- innerSigs :: -}[FunctionType]{- length n -}
-        -> CustomOp node
-substOp parent outerSig innerSigs
-  = CustomOp parent "BRAT" "Substitute" sig [toArg outerSig, TASequence (toArg <$> innerSigs)]
+        -> CustomOp
+substOp outerSig innerSigs
+  = CustomOp "BRAT" "Substitute" sig [toArg outerSig, TASequence (toArg <$> innerSigs)]
  where
   fnExts (FunctionType _ _ exts) = S.fromList exts
   combinedExts = S.toList $ foldr S.union (fnExts outerSig) (fnExts <$> innerSigs)
@@ -519,11 +488,10 @@ toFunc ty = HTFunc (PolyFuncType [] ty)
 toSeq :: [HugrType] -> TypeArg
 toSeq tys = TASequence (TAType <$> tys)
 
-partialOp :: node  -- Parent
-          -> FunctionType  -- Signature of the function that is partially evaluated
+partialOp :: FunctionType  -- Signature of the function that is partially evaluated
           -> Int  -- Number of arguments that are evaluated
-          -> CustomOp node
-partialOp parent funcSig numSupplied = CustomOp parent "BRAT" "Partial" sig args
+          -> CustomOp
+partialOp funcSig numSupplied = CustomOp "BRAT" "Partial" sig args
  where
   sig :: FunctionType
   sig = FunctionType
@@ -536,139 +504,95 @@ partialOp parent funcSig numSupplied = CustomOp parent "BRAT" "Partial" sig args
   otherInputs = drop numSupplied (input funcSig)
 
 
-data LoadConstantOp node = LoadConstantOp
-  { parent :: node
-  , datatype :: HugrType
-  } deriving (Eq, Functor, Show)
+data LoadConstantOp = LoadConstantOp
+  { datatype :: HugrType
+  } deriving (Eq, Show)
 
-instance Eq node => Ord (LoadConstantOp node) where
-  compare _ _ = EQ
+instance JSONParent LoadConstantOp where
+  toJSONp (LoadConstantOp {..}) parent = object ["parent" .= parent
+                                                ,"op" .= ("LoadConstant" :: Text)
+                                                ,"datatype" .= datatype
+                                                ]
 
-instance ToJSON node => ToJSON (LoadConstantOp node) where
-  toJSON (LoadConstantOp {..}) = object ["parent" .= parent
-                                        ,"op" .= ("LoadConstant" :: Text)
-                                        ,"datatype" .= datatype
-                                        ]
-
-data LoadFunctionOp node = LoadFunctionOp
-  { parent :: node
-  , func_sig :: PolyFuncType
+data LoadFunctionOp = LoadFunctionOp
+  { func_sig :: PolyFuncType
   , type_args :: [TypeArg]
   , signature :: FunctionType
-  } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (LoadFunctionOp node) where
-  compare _ _ = EQ
-
-instance ToJSON node => ToJSON (LoadFunctionOp node) where
-  toJSON (LoadFunctionOp {..}) = object ["parent" .= parent
-                                        ,"op" .= ("LoadFunction" :: Text)
-                                        ,"func_sig" .= func_sig
-                                        ,"type_args" .= type_args
-                                        ,"signature" .= signature
+  } deriving (Eq, Show)
+
+instance JSONParent LoadFunctionOp where
+  toJSONp (LoadFunctionOp {..}) parent = object ["parent" .= parent
+                                                ,"op" .= ("LoadFunction" :: Text)
+                                                ,"func_sig" .= func_sig
+                                                ,"type_args" .= type_args
+                                                ,"signature" .= signature
+                                                ]
+
+data NoopOp = NoopOp
+  { ty :: HugrType
+  } deriving (Eq, Show)
+
+instance JSONParent NoopOp where
+  toJSONp (NoopOp {..}) parent = object ["parent" .= parent
+                                        ,"op" .= ("Noop" :: Text)
+                                        ,"ty" .= ty
                                         ]
 
-data NoopOp node = NoopOp
-  { parent :: node
-  , ty :: HugrType
-  } deriving (Eq, Functor, Show)
-
-instance Eq node => Ord (NoopOp node) where
-  compare _ _ = EQ
-
-instance ToJSON node => ToJSON (NoopOp node) where
-  toJSON (NoopOp {..}) = object ["parent" .= parent
-                                ,"op" .= ("Noop" :: Text)
-                                ,"ty" .= ty
-                                ]
-
 -- In the order they must be printed in - roots, inputs, outputs
-data HugrOp node
+data HugrOp
   -- OpConditional should be compiled last so we can sort out its parent
-  = OpMod (ModuleOp node)
-  | OpIn (InputNode node)
-  | OpOut (OutputNode node)
+  = OpMod ModuleOp
+  | OpIn InputNode
+  | OpOut OutputNode
   -- the rest
-  | OpDefn (FuncDefn node)
-  | OpDFG (DFG node)
-  | OpConst (ConstOp node)
-  | OpConditional (Conditional node)
-  -- Make sure that the cases are printed out in the correct order
-  | OpCase (Int, Case node)
-  | OpTag (TagOp node)
-  | OpMakeTuple (MakeTupleOp node)
-  | OpCustom (CustomOp node)
-  | OpCall (CallOp node)
-  | OpCallIndirect (CallIndirectOp node)
-  | OpLoadConstant (LoadConstantOp node)
-  | OpLoadFunction (LoadFunctionOp node)
-  | OpNoop (NoopOp node)
- deriving (Eq, Functor, Ord, Show)
-
-addMetadata :: [(String, String)] -> HugrOp node -> HugrOp node
+  | OpDefn FuncDefn
+  | OpDFG DFG
+  | OpConst ConstOp
+  | OpConditional Conditional
+  | OpCase Case
+  | OpTag TagOp
+  | OpMakeTuple MakeTupleOp
+  | OpCustom CustomOp
+  | OpCall CallOp
+  | OpCallIndirect CallIndirectOp
+  | OpLoadConstant LoadConstantOp
+  | OpLoadFunction LoadFunctionOp
+  | OpNoop NoopOp
+ deriving (Eq, Show)
+
+addMetadata :: [(String, String)] -> HugrOp -> HugrOp
 addMetadata md (OpDFG (DFG { .. })) = OpDFG (DFG { metadata = metadata ++ md, .. })
-addMetadata md (OpCase (i, (Case { .. }))) = OpCase (i, (Case { metadata = metadata ++ md, .. }))
+addMetadata md (OpCase (Case { .. })) = OpCase (Case { metadata = metadata ++ md, .. })
 addMetadata md (OpIn (InputNode { .. })) = OpIn (InputNode { metadata = metadata ++ md, .. })
 addMetadata md (OpTag (TagOp { .. })) = OpTag (TagOp { metadata = metadata ++ md, .. })
 addMetadata md (OpDefn (FuncDefn { .. })) = OpDefn (FuncDefn { metadata = metadata ++ md, .. })
 addMetadata md (OpConditional (Conditional { .. })) = OpConditional (Conditional { metadata = metadata ++ md, .. })
 addMetadata _ op = op
 
-instance ToJSON node => ToJSON (HugrOp node) where
-  toJSON (OpMod op) = toJSON op
-  toJSON (OpDefn op) = toJSON op
-  toJSON (OpConst op) = toJSON op
-  toJSON (OpDFG op) = toJSON op
-  toJSON (OpIn op) = toJSON op
-  toJSON (OpOut op) = toJSON op
-  toJSON (OpCase (_, op)) = toJSON op
-  toJSON (OpConditional op) = toJSON op
-  toJSON (OpTag op) = toJSON op
-  toJSON (OpMakeTuple op) = toJSON op
-  toJSON (OpCustom op) = toJSON op
-  toJSON (OpCall op) = toJSON op
-  toJSON (OpCallIndirect op) = toJSON op
-  toJSON (OpLoadConstant op) = toJSON op
-  toJSON (OpLoadFunction op) = toJSON op
-  toJSON (OpNoop op) = toJSON op
-
-getParent :: HugrOp node -> node
-getParent (OpMod (ModuleOp { parent = parent })) = parent
-getParent (OpDefn (FuncDefn { parent = parent })) = parent
-getParent (OpConst (ConstOp { parent = parent })) = parent
-getParent (OpDFG (DFG { parent = parent })) = parent
-getParent (OpConditional (Conditional { parent = parent })) = parent
-getParent (OpCase (_, Case { parent = parent })) = parent
-getParent (OpIn (InputNode { parent = parent })) = parent
-getParent (OpOut (OutputNode { parent = parent })) = parent
-getParent (OpTag (TagOp { parent = parent })) = parent
-getParent (OpMakeTuple (MakeTupleOp { parent = parent })) = parent
-getParent (OpCustom (CustomOp { parent = parent })) = parent
-getParent (OpCall (CallOp { parent = parent })) = parent
-getParent (OpCallIndirect (CallIndirectOp { parent = parent })) = parent
-getParent (OpLoadConstant (LoadConstantOp { parent = parent })) = parent
-getParent (OpLoadFunction (LoadFunctionOp { parent = parent })) = parent
-getParent (OpNoop (NoopOp { parent = parent })) = parent
-
-data Hugr node = Hugr [HugrOp node] [(PortId node, PortId node)]
-  deriving (Eq, Functor, Show)
-
-instance ToJSON node => ToJSON (Hugr node) where
-  toJSON (Hugr ns es) = object ["version" .= ("v1" :: Text)
-                               ,"nodes" .= ns
-                               ,"edges" .= es
-                               ,"encoder" .= ("BRAT" :: Text)
-                               ]
-
-orderEdgeOffset :: Int
-orderEdgeOffset = -1
-
-data PortId node = Port
-  { nodeId :: node
-  , offset :: Int
-  }
- deriving (Eq, Functor, Show)
-
-instance ToJSON node => ToJSON (PortId node) where
-  toJSON (Port node offset) = toJSON (node, offset')
-    where offset' = if offset == orderEdgeOffset then Nothing else Just offset
+instance JSONParent HugrOp where
+  toJSONp (OpMod op) parent = toJSONp op parent
+  toJSONp (OpDefn op) parent = toJSONp op parent
+  toJSONp (OpConst op) parent = toJSONp op parent
+  toJSONp (OpDFG op) parent = toJSONp op parent
+  toJSONp (OpIn op) parent = toJSONp op parent
+  toJSONp (OpOut op) parent = toJSONp op parent
+  toJSONp (OpCase op) parent = toJSONp op parent
+  toJSONp (OpConditional op) parent = toJSONp op parent
+  toJSONp (OpTag op) parent = toJSONp op parent
+  toJSONp (OpMakeTuple op) parent = toJSONp op parent
+  toJSONp (OpCustom op) parent = toJSONp op parent
+  toJSONp (OpCall op) parent = toJSONp op parent
+  toJSONp (OpCallIndirect op) parent = toJSONp op parent
+  toJSONp (OpLoadConstant op) parent = toJSONp op parent
+  toJSONp (OpLoadFunction op) parent = toJSONp op parent
+  toJSONp (OpNoop op) parent = toJSONp op parent
+
+data Hugr node = Hugr ([(node, HugrOp)], [(PortId node, PortId node)]) deriving (Eq, Show)
+
+instance ToJSON (Hugr Int) where
+  toJSON (Hugr (nodes, edges)) = object
+    ["version" .= ("v1" :: Text)
+    ,"nodes" .= [toJSONp op (toJSON parent) | (parent, op) <- nodes]
+    ,"edges" .= edges
+    ,"encoder" .= ("BRAT" :: Text)
+    ]
diff --git a/brat/Data/HugrGraph.hs b/brat/Data/HugrGraph.hs
new file mode 100644
index 00000000..49b1883c
--- /dev/null
+++ b/brat/Data/HugrGraph.hs
@@ -0,0 +1,259 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Data.HugrGraph(NodeId,
+                      HugrGraph(root), -- do NOT export contents, keep abstract
+                      new, splitNamespace,
+                      freshNode,
+                      setFirstChildren,
+                      setOp, getParent, getOp,
+                      addEdge, addOrderEdge, edgeList,
+                      splice, inlineDFG,
+                      serialize, to_json
+                     ) where
+
+import Brat.Naming (Namespace, Name(..), fresh, split)
+import Bwd
+import Data.Hugr hiding (const)
+
+import qualified Data.ByteString.Lazy as BS
+import Data.Aeson (encode)
+
+import Control.Monad.State (State, execState, state, get, put, modify)
+import Data.Foldable (for_)
+import Data.Functor ((<&>))
+import Data.Bifunctor (first)
+import Data.Maybe (fromMaybe)
+import qualified Data.Map as M
+
+track = const id
+
+newtype NodeId = NodeId Name deriving (Eq, Ord, Show)
+
+data HugrGraph = HugrGraph {
+    root :: NodeId,
+    parents :: M.Map NodeId NodeId, -- definitive list of (valid) nodes, excluding root
+    first_children:: M.Map NodeId [NodeId],
+    nodes :: M.Map NodeId HugrOp,
+    edges_out :: M.Map NodeId [(Int, PortId NodeId)],
+    edges_in :: M.Map NodeId [(PortId NodeId, Int)],
+    nameSupply :: Namespace
+} deriving (Eq, Show) -- we probably want a better `show`
+
+splitNamespace :: String -> State HugrGraph Namespace
+splitNamespace n = state $ \hugr -> let (nsx, nsNew) = split n (nameSupply hugr)
+                                    in (nsx, hugr {nameSupply = nsNew})
+
+freshNode :: NodeId -> String -> State HugrGraph NodeId
+freshNode parent nam = state $ \hugr@(HugrGraph {root, parents, nameSupply}) ->
+  case M.lookup parent parents of
+    Nothing | parent /= root-> error "parent does not exist"
+    _ -> let (freshName, newSupply) = fresh nam nameSupply
+         in (NodeId freshName, hugr {
+              nameSupply = newSupply,
+              parents = M.alter (\Nothing -> Just parent) (NodeId freshName) parents
+            })
+
+setFirstChildren :: NodeId -> [NodeId] -> State HugrGraph ()
+setFirstChildren p cs = state $ \h -> let nch = M.alter (\Nothing -> Just cs) p (first_children h)
+                                      in ((), h {first_children = nch})
+
+setOp :: NodeId -> HugrOp -> State HugrGraph ()
+-- Insist the parent exists
+setOp name op = state $ \h@HugrGraph {parents, nodes} -> case M.lookup name parents of
+  Nothing -> error "name has no parent"
+  Just _ ->
+    -- alter + partial match is just to fail if key already present
+    ((), h { nodes = M.alter (\Nothing -> Just op) name nodes })
+
+new :: Namespace -> String -> HugrOp -> HugrGraph
+new ns nam op =
+  let (name, ns') = fresh nam ns
+      root = NodeId name
+  in HugrGraph {
+        root,
+        parents = M.empty,
+        first_children = M.empty,
+        nodes = M.singleton root op,
+        edges_in = M.empty,
+        edges_out = M.empty,
+        nameSupply = ns'
+      }
+
+addEdge :: (PortId NodeId, PortId NodeId) -> State HugrGraph ()
+addEdge (src@(Port s o), tgt@(Port t i)) = state $ \h@HugrGraph {..} ->
+  ((), ) $ case (M.lookup s nodes, M.lookup t nodes) of
+    (Just _, Just _) -> h {
+      edges_out = addToMap s (o, tgt) edges_out,
+      edges_in = addToMap t (src, i) edges_in
+    }
+    _ -> error "addEdge to/from node not present"
+ where
+  addToMap :: Ord k => k -> v -> M.Map k [v] -> M.Map k [v]
+  addToMap k v m = M.insert k (v:(fromMaybe [] $ M.lookup k m)) m
+
+addOrderEdge :: (NodeId, NodeId) -> State HugrGraph ()
+addOrderEdge (src, tgt) = addEdge (Port src orderEdgeOffset, Port tgt orderEdgeOffset)
+
+edgeList :: HugrGraph -> [(PortId NodeId, PortId NodeId)]
+edgeList (HugrGraph {edges_out}) = [(Port n off, tgt) | (n, vs) <- M.assocs edges_out
+                                                      , (off, tgt) <- vs
+                                   ]
+
+getParent :: HugrGraph -> NodeId -> NodeId
+getParent HugrGraph {parents} n = parents M.! n
+
+getOp :: HugrGraph -> NodeId -> HugrOp
+getOp HugrGraph {nodes} n = nodes M.! n
+
+--- Replaces the specified node of the first Hugr, with the second Hugr.
+splice :: HugrGraph -> NodeId -> HugrGraph -> HugrGraph
+splice host hole add = case (M.lookup hole (nodes host) >>= isHole) of
+  Just (_, sig) -> case M.lookup (root add) (nodes add) of
+    Just (OpDFG (DFG sig' _)) | sig == sig' -> {-inlineDFG hole-} host {
+        -- prefer host entry for parent of (`hole` == root of `add`)
+        parents = union (parents host) (M.mapKeys k $ M.map k $ parents add),
+        -- override host `nodes` for `hole` with new (DFG)
+        nodes = M.union (M.mapKeys k (nodes add)) (nodes host),
+        edges_in  = union (edges_in host)  $ M.fromList [(k tgt, [(Port (k srcNode) srcPort, tgtPort)
+                                                                 | (Port srcNode srcPort, tgtPort) <- in_edges ])
+                                                        | (tgt, in_edges ) <- M.assocs (edges_in add)],
+        edges_out = union (edges_out host) $ M.fromList [(k src, [(srcPort, Port (k tgtNode) tgtPort)
+                                                                 | (srcPort, Port tgtNode tgtPort) <- out_edges])
+                                                        | (src, out_edges) <- M.assocs (edges_out add)],
+        first_children = union (first_children host) (M.mapKeys k $ M.map (k <$>) $ first_children add)
+      }
+    other -> error $ "Expected DFG with sig " ++ show sig ++ "\nBut found: " ++ show other
+  other -> error $ "Expected a hole, found " ++ show other
+  where
+    prefixRoot :: NodeId -> NodeId
+    prefixRoot (NodeId (MkName ids)) = let NodeId (MkName rs) = hole in NodeId $ MkName (rs ++ ids)
+
+    keyMap :: M.Map NodeId NodeId -- translate `add` keys into `host` by prefixing with `hole`.
+    -- parent is definitive list of non-root nodes
+    keyMap = M.fromList $ (root add, hole):[(k, prefixRoot k) | k <- M.keys (parents add)]
+
+    union = M.unionWith (\_ _ -> error "keys not disjoint")
+    k = (keyMap M.!)
+
+inlineDFG :: NodeId -> State HugrGraph ()
+inlineDFG dfg = get >>= \h -> case M.lookup dfg (nodes h) of
+  (Just (OpDFG _)) -> do
+    let newp = (parents h) M.! dfg
+    let [inp, out] = (first_children h) M.! dfg
+    -- rewire edges
+    dfg_in_map <- takeInEdgeMap dfg
+    input_out_map <- takeOutEdges inp
+    for_ input_out_map $ \(outp, dest) -> addEdge (dfg_in_map M.! outp, dest)
+    dfg_out_map <- takeOutEdges dfg
+    output_in_map <- takeInEdgeMap out
+    for_ dfg_out_map $ \(outp, dest) -> addEdge (output_in_map M.! outp, dest)
+    -- remove dfg, inp, out; reparent children of dfg
+    let to_remove = [dfg, inp, out]
+    modify $ \h -> h {
+      first_children = M.delete dfg (first_children h), -- inp/out shouldn't have any children
+      nodes = foldl (flip M.delete) (nodes h) to_remove,
+      -- TODO this is O(size of hugr) reparenting. Either add a child map,
+      -- or combine with splicing so we only iterate through the inserted
+      -- hugr (which we do anyway) rather than the host.
+      parents = M.fromList [(n, if p==dfg then newp else p)
+                          | (n,p) <- M.assocs (parents h), not (elem n to_remove)]
+    }
+  other -> error $ "Expected DFG, found " ++ show other
+ where
+  takeInEdgeMap n = takeInEdges n <&> \es -> M.fromList [(p, src) | (src, p) <- es]
+
+takeInEdges :: NodeId -> State HugrGraph [(PortId NodeId, Int)]
+takeInEdges tgt = do
+  h <- get
+  let (removed_edges, edges_in') = first (fromMaybe []) $ M.updateLookupWithKey
+        (\_ _ -> Nothing) tgt (edges_in h)
+  let edges_out' = foldl removeFromOutMap (edges_out h) removed_edges
+  put h {edges_in=edges_in', edges_out=edges_out'}
+  pure removed_edges
+ where
+  removeFromOutMap :: M.Map NodeId [(Int, PortId NodeId)] -> (PortId NodeId, Int) -> M.Map NodeId [(Int, PortId NodeId)]
+  removeFromOutMap eos (Port src outport, inport) = M.alter (\(Just es) -> Just $ removeFromOutList es (outport, Port tgt inport)) src eos
+
+  removeFromOutList :: [(Int, PortId NodeId)] -> (Int, PortId NodeId) -> [(Int, PortId NodeId)]
+  removeFromOutList [] _ = error "Out-edge not found"
+  removeFromOutList (e:es) e' | e == e' = es
+  removeFromOutList ((outport, _):_) (outport', _) | outport == outport' = error "Wrong out-edge"
+  removeFromOutList (e:es) r = e:(removeFromOutList es r)
+
+takeOutEdges :: NodeId -> State HugrGraph [(Int, PortId NodeId)]
+takeOutEdges src = do
+  h <- get
+  let (removed_edges, edges_out') = first (fromMaybe []) $ M.updateLookupWithKey
+       (\_ _ -> Nothing) src (edges_out h)
+  let edges_in' = foldl removeFromInMap (edges_in h) removed_edges
+  put h {edges_in=edges_in', edges_out=edges_out'}
+  pure removed_edges
+ where
+  removeFromInMap :: M.Map NodeId [(PortId NodeId, Int)] -> (Int, PortId NodeId) -> M.Map NodeId [(PortId NodeId, Int)]
+  removeFromInMap eis (outport, Port tgt inport) = M.alter (\(Just es) -> Just $ removeFromInList es (Port src outport, inport)) tgt eis
+
+  removeFromInList:: [(PortId NodeId, Int)] -> (PortId NodeId, Int) -> [(PortId NodeId, Int)]
+  removeFromInList [] _ = error "In-edge not found"
+  removeFromInList (e:es) e' | e==e' = es
+  removeFromInList ((_, inport):_) (_,inport') | inport == inport' = error "Wrong in-edge"
+  removeFromInList (e:es) r = e:(removeFromInList es r)
+
+to_json :: HugrGraph -> BS.ByteString
+to_json = encode . serialize
+
+serialize :: HugrGraph -> Hugr Int
+serialize hugr = renameAndSort (execState (for_ orderEdges addOrderEdge) hugr)
+ where
+  orderEdges :: [(NodeId, NodeId)]
+  orderEdges =
+    -- Nonlocal edges (from a node to another which is a *descendant* of a sibling of the source)
+    -- require an extra order edge from the source to the sibling that is ancestor of the target
+    let interEdges = [(n1, n2) | (Port n1 _, Port n2 _) <- edgeList hugr,
+            (parentOf n1 /= parentOf n2),
+            requiresOrderEdge n1,
+            requiresOrderEdge n2] in
+    track ("interEdges: " ++ show interEdges) (walkUp <$> interEdges)
+
+  requiresOrderEdge :: NodeId -> Bool
+  requiresOrderEdge n = case getOp hugr n of
+    OpMod _ -> False
+    OpDefn _ -> False
+    OpConst _ -> False
+    _ -> True
+
+  parentOf = getParent hugr
+
+  -- Walk up the hierarchy from the tgt until we hit a node at the same level as src
+  walkUp :: (NodeId, NodeId) -> (NodeId, NodeId)
+  walkUp (src, tgt) | parentOf src == parentOf tgt = (src, tgt)
+  walkUp (_, tgt) | parentOf tgt == tgt = error "Tgt was not descendant of Src-parent"
+  walkUp (src, tgt) = walkUp (src, parentOf tgt)
+
+-- this should be local to renameAndSort but local `type` is not allowed
+type StackAndIndices = (Bwd (NodeId, HugrOp) -- node is index, this is (parent, op)
+                       , M.Map NodeId Int)
+
+renameAndSort :: HugrGraph -> Hugr Int
+renameAndSort hugr@(HugrGraph {root, first_children=fc, nodes, parents}) = Hugr (
+    (first transNode) <$> (fst nodeStackAndIndices) <>> [],
+    [(Port (transNode s) o, Port (transNode t) i) | (Port s o, Port t i) <- edgeList hugr]
+  ) where
+    first_children k = M.findWithDefault [] k fc
+    nodeStackAndIndices :: StackAndIndices
+    nodeStackAndIndices = let just_root = (B0 :< (root, nodes M.! root), M.singleton root 0)
+                              init = foldl addNode just_root (first_children root)
+                          in foldl addNode init (M.keys parents)
+
+    addNode :: StackAndIndices -> NodeId -> StackAndIndices
+    addNode ins n = case M.lookup n (snd ins) of
+      (Just _) -> ins
+      Nothing -> let
+        parent = parents M.! n -- guaranteed as root is always in `ins`
+        with_parent@(stack, indices) = addNode ins parent -- add parent first, will recurse up
+       in case M.lookup n indices of
+            Just _ -> with_parent -- self added by recursive call; we must be in parent's first_children 
+            Nothing -> let with_n = (stack :< (parent, nodes M.! n), M.insert n (M.size indices) indices)
+                       -- finally add first_children immediately after n
+                       in foldl addNode with_n (first_children n)
+
+    transNode :: NodeId -> Int
+    transNode = ((snd nodeStackAndIndices) M.!)
diff --git a/brat/app/Main.hs b/brat/app/Main.hs
index bac393b7..95a35ee3 100644
--- a/brat/app/Main.hs
+++ b/brat/app/Main.hs
@@ -1,4 +1,5 @@
 import Brat.Compiler
+import Brat.Machine (runInterpreter)
 
 import Control.Monad (when)
 import Options.Applicative
@@ -9,7 +10,8 @@ data Options = Opt {
   compile :: Bool,
   file    :: String,
   libs    :: String,
-  raw     :: Bool
+  raw     :: Bool,
+  runFunc :: String
 }
 
 compileFlag :: Parser Bool
@@ -23,8 +25,10 @@ dotOption = strOption (long "dot" <> value "" <> help "Write graph in Dot format
 
 libOption = strOption (long "lib" <> value "" <> help "Look in extra directories for libraries (delimited with ;)")
 
+runFuncOption = strOption (long "run" <> value "" <> help "Run function with interpreter (must take no arguments)")
+
 opts :: Parser Options
-opts = Opt <$> astFlag <*> dotOption <*> compileFlag <*> strArgument (metavar "FILE") <*> libOption <*> rawFlag
+opts = Opt <$> astFlag <*> dotOption <*> compileFlag <*> strArgument (metavar "FILE") <*> libOption <*> rawFlag <*> runFuncOption
 
 -- Parse a list of library directories delimited by a semicolon
 parseLibs :: String -> [String]
@@ -39,4 +43,6 @@ main = do
   when (ast || raw) $ printAST raw ast file
   let libDirs = parseLibs libs
   when (dot /= "") $ writeDot libDirs file dot
-  if compile then compileAndPrintFile libDirs file else printDeclsHoles libDirs file
+  if compile then compileAndPrintFile libDirs file
+  else if runFunc /= "" then runInterpreter libDirs file runFunc
+                        else printDeclsHoles libDirs file
diff --git a/brat/arith.brat b/brat/arith.brat
new file mode 100644
index 00000000..60eeeebc
--- /dev/null
+++ b/brat/arith.brat
@@ -0,0 +1,37 @@
+i :: Nat
+i = 3 + 4
+
+j :: Nat
+j = 7 - 2
+
+f :: Float
+f = 2.1 * 5.3
+
+g :: Float
+g = 7.2 - 3.9
+
+inc(Nat) -> Nat
+inc(x) = x + 1
+
+foo :: Nat
+foo = inc(inc(4) + inc(7))
+
+dec(Nat) -> Nat
+dec(0) = 0
+dec(succ(n)) = n
+
+goo :: Nat
+goo = dec(foo)
+
+length(X :: *, n :: #, Vec(X, n)) -> Nat
+length(_, n, _) = n
+
+hoo(n :: #, Vec(Nat, n + 1)) -> Nat
+hoo(succ(l), ls =, m ,= rs) = length(!, !, ls)
+hoo(n, _) = n
+
+ioo :: Nat
+ioo = hoo(2, [1,2,3])
+
+joo :: Vec(Nat, 3)
+joo = [1,2,3]
diff --git a/brat/brat.cabal b/brat/brat.cabal
index aded7927..bbb65255 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -44,11 +44,7 @@ common warning-flags
     -Wno-unused-do-bind
     -Wno-missing-signatures
     -Wno-noncanonical-monoid-instances
-    -Werror=unused-imports
-    -Werror=unused-matches
     -Werror=missing-methods
-    -Werror=unused-top-binds
-    -Werror=unused-local-binds
     -Werror=redundant-constraints
     -Werror=orphans
     -Werror=overlapping-patterns
@@ -78,6 +74,7 @@ library
                        Brat.Error,
                        Brat.Graph,
                        Brat.Load,
+                       Brat.Machine,
                        Brat.Parser,
                        Brat.Search,
                        Brat.Elaborator,
@@ -90,6 +87,7 @@ library
                        Bwd,
                        Control.Monad.Freer,
                        Data.Hugr,
+                       Data.HugrGraph,
                        Hasochism,
                        Util
 
@@ -165,6 +163,7 @@ test-suite tests
                        Test.Elaboration,
                        Test.Failure,
                        Test.Graph,
+                       Test.HugrGraph,
                        Test.Libs,
                        Test.Parsing,
                        Test.Naming,
@@ -174,7 +173,8 @@ test-suite tests
                        Test.TypeArith,
                        Test.Util
 
-  build-depends:       base <5,
+  build-depends:       aeson,
+                       base <5,
                        brat,
                        tasty,
                        tasty-hunit,
diff --git a/brat/test/Main.hs b/brat/test/Main.hs
index 2c67e0cb..f91033f6 100644
--- a/brat/test/Main.hs
+++ b/brat/test/Main.hs
@@ -7,6 +7,7 @@ import Test.Graph
 import Test.Compile.Hugr
 import Test.Elaboration
 import Test.Failure
+import Test.HugrGraph
 import Test.Libs
 import Test.Naming
 import Test.Parsing
@@ -64,6 +65,7 @@ main = do
   parsingTests <- getParsingTests
   compilationTests <- setupCompilationTests
   graphTests <- getGraphTests
+  spliceTests <- getSpliceTests
   let coroTests = testGroup "coroutine"
        [testCase "coroT1" $ assertChecking coroT1
        ,testCase "coroT2" $ assertCheckingFail "Typechecking blocked on" coroT2
@@ -82,4 +84,5 @@ main = do
                                 ,compilationTests
                                 ,typeArithTests
                                 ,coroTests
+                                ,spliceTests
                                 ]
diff --git a/brat/test/Test/Compile/Hugr.hs b/brat/test/Test/Compile/Hugr.hs
index 0f3d7bd9..485bae33 100644
--- a/brat/test/Test/Compile/Hugr.hs
+++ b/brat/test/Test/Compile/Hugr.hs
@@ -1,11 +1,14 @@
 module Test.Compile.Hugr where
 
+import Control.Monad (forM)
+import Data.HugrGraph (to_json)
 import Brat.Compiler (compileFile, CompilingHoles(..))
 import Test.Checking (expectedCheckingFails)
 import Test.Parsing (expectedParsingFails)
 import Test.Util (expectFailForPaths)
 
 import qualified Data.ByteString.Lazy as BS
+import qualified Data.Map as M
 import System.Directory (createDirectoryIfMissing)
 import System.FilePath
 import Test.Tasty
@@ -18,7 +21,7 @@ outputDir = prefix </> "output"
 
 -- examples that we expect to compile, but then to fail validation
 invalidExamples :: [FilePath]
-invalidExamples = map ((++ ".brat") . ("examples" </>))
+invalidExamples = (map ((++ ".brat") . ("examples" </>))
   ["adder"
   ,"app"
   ,"dollar_kind"
@@ -29,41 +32,43 @@ invalidExamples = map ((++ ".brat") . ("examples" </>))
   ,"infer_thunks2" -- Weird: Mismatch between caller and callee signatures in map call
   ,"repeated_app" -- missing coercions, https://github.com/quantinuum-dev/brat/issues/413
   ,"thunks"]
+  ) ++ ["test/compilation/closures.brat"] -- fails to compile but still spits out some JSON (not whole Hugr)
 
 -- examples that we expect not to compile.
 -- Note this does not include those with remaining holes; these are automatically skipped.
 nonCompilingExamples = expectedCheckingFails ++ expectedParsingFails ++
   map ((++ ".brat") . ("examples" </>))
-  ["fzbz"
-  ,"ising"
-  ,"let"
-  ,"patterns"
-  ,"qft"
-  ,"infer" -- problems with undoing pattern tests
-  ,"infer2" -- problems with undoing pattern tests
+  [--"fzbz" -- can compile just kernels
+  --,"ising" -- can compile just kernels
+  --,"let" -- can compile just kernels
+  --,"patterns" -- can compile just kernels
+  "qft"
+  --,"infer" -- problems with undoing pattern tests -- can compile just kernels
+  --,"infer2" -- problems with undoing pattern tests -- can compile just kernels
   ,"fanout" -- Contains Selectors
-  ,"vectorise" -- Generates MapFun nodes which aren't implemented yet
-  ,"vector_solve" -- Generates "Pow" nodes which aren't implemented yet
-  ,"batcher-merge-sort" -- Generates MapFun nodes which aren't implemented yet
+  --,"vectorise" -- Generates MapFun nodes which aren't implemented yet -- can compile just kernels
+  --,"vector_solve" -- Generates "Pow" nodes which aren't implemented yet -- can compile just kernels
+  --,"batcher-merge-sort" -- Generates MapFun nodes which aren't implemented yet -- can compile just kernels
   -- Victims of #13
-  ,"arith"
+  --,"arith" -- can compile just kernels
   ,"cqcconf"
   ,"imports"
-  ,"ising"
   ,"klet"
   ,"magic-state-distillation" -- also makes selectors
   ,"rus"
   ,"teleportation"
-  ,"vlup_covering"
+  --,"vlup_covering" -- can compile just kernels
   ]
 
 compileToOutput :: FilePath -> TestTree
 compileToOutput file = testCaseInfo (show file) $ compileFile [] file >>= \case
-    Right bs -> do
+    Right hs ->
       let outputExt = if file `elem` invalidExamples then "json.invalid" else "json"
-      let outFile = outputDir </> replaceExtension (takeFileName file) outputExt
-      BS.writeFile outFile bs
-      pure $ "Written to " ++ outFile ++ " pending validation"
+      in mconcat <$> (forM (M.toList hs) $ \(boxName, (hugr, splices)) -> do
+        -- ignore splices for now
+        let outFile = outputDir </> replaceExtension (takeFileName file) ((show boxName) ++ "." ++ outputExt)
+        BS.writeFile outFile (to_json hugr)
+        pure $ "Written to " ++ outFile ++ " pending validation\n")
     Left (CompilingHoles _) -> pure "Skipped as contains holes"
 
 setupCompilationTests :: IO TestTree
diff --git a/brat/test/Test/HugrGraph.hs b/brat/test/Test/HugrGraph.hs
new file mode 100644
index 00000000..b9c10580
--- /dev/null
+++ b/brat/test/Test/HugrGraph.hs
@@ -0,0 +1,75 @@
+module Test.HugrGraph(getSpliceTests) where
+
+import Brat.Naming as N
+import Data.HugrGraph as H
+import Data.Hugr
+
+import Control.Monad.State (State, execState, get, runState)
+import Data.Aeson (encode)
+import Data.Functor ((<&>))
+import Data.Maybe (isJust, isNothing)
+import Data.List (find)
+import qualified Data.ByteString.Lazy as BS
+import System.Directory (createDirectoryIfMissing)
+import System.FilePath
+import Test.Tasty
+import Test.Tasty.HUnit
+
+prefix = "test/hugr"
+outputDir = prefix </> "output"
+
+addNode :: String -> NodeId -> HugrOp -> State HugrGraph NodeId
+addNode nam parent op = do
+  name <- H.freshNode parent nam
+  H.setOp name op
+  pure name
+
+getSpliceTests :: IO TestTree
+getSpliceTests = do
+  createDirectoryIfMissing True outputDir
+  pure $ testGroup "splice" [testSplice False, testSplice True]
+
+testSplice :: Bool -> TestTree
+testSplice inline = testCaseInfo name $ do
+  let (h, holeId) = host
+  let outPrefix = outputDir </> name
+  BS.writeFile (outPrefix ++ "_host.json") (encode $ H.serialize h)
+  BS.writeFile (outPrefix ++ "_insertee.json") (encode $ H.serialize dfgHugr)
+  let spliced = H.splice h holeId dfgHugr
+  let resHugr@(Hugr (ns, _))  = H.serialize $ if inline
+        then execState (inlineDFG holeId) spliced else spliced
+  let outFile = outPrefix ++ "_result.json"
+  BS.writeFile outFile $ encode resHugr
+  assertBool "Should be no holes now" $ isNothing $ find (isJust . isHole) $ snd <$> ns
+  -- if inline, we should assert there's no DFG either
+  pure $ "Written to " ++ outFile ++ " pending validation"
+ where
+  name = if inline then "inline" else "noinline"
+  host :: (HugrGraph, NodeId)
+  host = swap $ flip runState (H.new N.root "root" rootDefn) $ do
+    root <- get <&> H.root
+    input <- addNode "inp" root (OpIn (InputNode tys []))
+    output <- addNode "out" root (OpOut (OutputNode tys []))
+    setFirstChildren root [input, output]
+    hole <- addNode "hole" root (OpCustom $ holeOp 0 tq_ty)
+    H.addEdge (Port input 0, Port hole 0)
+    H.addEdge (Port input 1, Port hole 1)
+    H.addEdge (Port hole 0, Port output 0)
+    H.addEdge (Port hole 1, Port output 1)
+    pure hole
+  dfgHugr :: HugrGraph
+  dfgHugr = flip execState (H.new N.root "root" rootDfg) $ do
+    root <- get <&> H.root
+    input <- addNode "inp" root (OpIn (InputNode tys []))
+    output <- addNode "out" root (OpOut (OutputNode tys []))
+    setFirstChildren root [input, output]
+    gate <- addNode "gate" root (OpCustom $ CustomOp "tket" "CX" tq_ty [])
+    H.addEdge (Port input 0, Port gate 0)
+    H.addEdge (Port input 1, Port gate 1)
+    H.addEdge (Port gate 0, Port output 0)
+    H.addEdge (Port gate 1, Port output 1)
+  swap (x,y) = (y,x)
+  tys = [HTQubit, HTQubit]
+  tq_ty = FunctionType tys tys bratExts
+  rootDefn = OpDefn $ FuncDefn "main" (PolyFuncType [] tq_ty) []
+  rootDfg = OpDFG $ DFG tq_ty []
diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph
index 06981276..3206ae5a 100644
--- a/brat/test/golden/graph/cons.brat.graph
+++ b/brat/test/golden/graph/cons.brat.graph
@@ -1,22 +1,26 @@
 Nodes:
+(check_defs_1_three_2_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (check_defs_1_three_2_$rhs_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (check_defs_1_three_2_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_three_2_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(check_defs_1_three_2_$rhs_check'Con_const_3,BratNode (Const 0) [] [("value",Int)])
+(check_defs_1_three_2_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
+(check_defs_1_three_2_$rhs_check'Con_const_4,BratNode (Const 0) [] [("value",Int)])
 (check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_two_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (check_defs_1_two_$rhs_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (check_defs_1_two_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_check'Con_4_nil_2,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_const_3,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_two_$rhs_check'Con_check'Con_4_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
-(check_defs_1_two_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
-(check_defs_1_two_$rhs_check'Con_const_3,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_two_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_nil_3,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_const_4,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_two_$rhs_check'Con_check'Con_5_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_two_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
+(check_defs_1_two_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
 (check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
 (check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
@@ -30,17 +34,21 @@ Nodes:
 (globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex check_defs_1_three_2_$rhs_check'Con_cons_2 0,Vec(Int, 3),In globals_decl_9_three 0)
-(Ex check_defs_1_three_2_$rhs_check'Con_const_3 0,Int,In check_defs_1_three_2_$rhs_check'Con_cons_2 0)
+(Ex check_defs_1_three_2_$rhs_check'Con__2 0,[],In check_defs_1_three_2_$rhs_check'Con_$!_pat2val 0)
+(Ex check_defs_1_three_2_$rhs_check'Con_cons_3 0,Vec(Int, 3),In globals_decl_9_three 0)
+(Ex check_defs_1_three_2_$rhs_check'Con_const_4 0,Int,In check_defs_1_three_2_$rhs_check'Con_cons_3 0)
 (Ex check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_three_2_$rhs_check'Con_$!_numpat2val_1 0)
 (Ex check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 1)
-(Ex check_defs_1_two_$rhs_check'Con_check'Con_4_check'Con_4_nil_2 0,Vec(Int, 0),In check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2 0,Vec(Int, 1),In check_defs_1_two_$rhs_check'Con_cons_2 1)
-(Ex check_defs_1_two_$rhs_check'Con_check'Con_4_const_3 0,Int,In check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex check_defs_1_two_$rhs_check'Con_check'Con_4_typeEqsTail_1_buildConst_1 0,Nat,In check_defs_1_two_$rhs_check'Con_check'Con_4_$!_numpat2val_1 0)
-(Ex check_defs_1_two_$rhs_check'Con_cons_2 0,Vec(Int, 2),In globals_decl_4_two 0)
-(Ex check_defs_1_two_$rhs_check'Con_const_3 0,Int,In check_defs_1_two_$rhs_check'Con_cons_2 0)
+(Ex check_defs_1_two_$rhs_check'Con__2 0,[],In check_defs_1_two_$rhs_check'Con_$!_pat2val 0)
+(Ex check_defs_1_two_$rhs_check'Con_check'Con_5__2 0,[],In check_defs_1_two_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5__2 0,[],In check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_nil_3 0,Vec(Int, 0),In check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3 0,Vec(Int, 1),In check_defs_1_two_$rhs_check'Con_cons_3 1)
+(Ex check_defs_1_two_$rhs_check'Con_check'Con_5_const_4 0,Int,In check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex check_defs_1_two_$rhs_check'Con_check'Con_5_typeEqsTail_1_buildConst_1 0,Nat,In check_defs_1_two_$rhs_check'Con_check'Con_5_$!_numpat2val_1 0)
+(Ex check_defs_1_two_$rhs_check'Con_cons_3 0,Vec(Int, 2),In globals_decl_4_two 0)
+(Ex check_defs_1_two_$rhs_check'Con_const_4 0,Int,In check_defs_1_two_$rhs_check'Con_cons_3 0)
 (Ex check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_two_$rhs_check'Con_$!_numpat2val_1 0)
 (Ex check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 1)
@@ -50,4 +58,4 @@ Wires:
 (Ex globals_Vec_6 0,[],In globals___kca_three_5 0)
 (Ex globals_const_3 0,Nat,In globals_Vec_1 1)
 (Ex globals_const_8 0,Nat,In globals_Vec_6 1)
-(Ex globals_decl_4_two 0,Vec(Int, 2),In check_defs_1_three_2_$rhs_check'Con_cons_2 1)
+(Ex globals_decl_4_two 0,Vec(Int, 2),In check_defs_1_three_2_$rhs_check'Con_cons_3 1)
diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph
index e918270f..0c180fb5 100644
--- a/brat/test/golden/graph/kernel.brat.graph
+++ b/brat/test/golden/graph/kernel.brat.graph
@@ -2,21 +2,25 @@ Nodes:
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] [])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2,BratNode (Dummy $) [] [("dummy",[])])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2,KernelNode (Constructor nil) [] [("value",Vec(Qubit, 0))])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_cons_2,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 0))] [("value",Vec(Qubit, 1))])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_cons_2,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 1))] [("value",Vec(Qubit, 2))])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
-(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 2))] [("value",Vec(Qubit, 3))])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5__2,BratNode (Dummy $) [] [("dummy",[])])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy $) [] [("dummy",[])])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_check'Con_5__2,BratNode (Dummy $) [] [("dummy",[])])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3,KernelNode (Constructor nil) [] [("value",Vec(Qubit, 0))])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_cons_3,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 0))] [("value",Vec(Qubit, 1))])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_cons_3,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 1))] [("value",Vec(Qubit, 2))])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 2))] [("value",Vec(Qubit, 3))])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
@@ -36,20 +40,24 @@ Nodes:
 (globals_decl_9_id3,BratNode Id [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })] [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
 
 Wires:
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2 0,Vec(Qubit, 0),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_cons_2 1)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_cons_2 0,Vec(Qubit, 1),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_cons_2 1)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_typeEqsTail_1_buildConst_1 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_$!_numpat2val_1 0)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_cons_2 0,Vec(Qubit, 2),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2 1)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_$!_numpat2val_1 0)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 0)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 1)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2 0,Vec(Qubit, 3),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2 0,[],In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5__2 0,[],In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5__2 0,[],In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_check'Con_5__2 0,[],In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3 0,Vec(Qubit, 0),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_cons_3 1)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_cons_3 0,Vec(Qubit, 1),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_cons_3 1)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_typeEqsTail_1_buildConst_1 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_$!_numpat2val_1 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_cons_3 0,Vec(Qubit, 2),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3 1)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_numpat2val_1 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 1)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3 0,Vec(Qubit, 3),In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0)
 (Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1 0)
 (Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1 1)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2 0)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 1,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_cons_2 0)
-(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 2,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_cons_2 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 1,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_cons_3 0)
+(Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 2,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_cons_3 0)
 (Ex check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0,Vec(Qubit, 3),In check_defs_1_id3_$rhs_check'Th_thunk/out_1 0)
 (Ex check_defs_1_id3_$rhs_check'Th_thunk/in 0,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0)
 (Ex check_defs_1_id3_$rhs_check'Th_thunk/in 1,Qubit,In check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 1)
diff --git a/brat/test/golden/graph/list.brat.graph b/brat/test/golden/graph/list.brat.graph
index fc6e7300..d5928b6e 100644
--- a/brat/test/golden/graph/list.brat.graph
+++ b/brat/test/golden/graph/list.brat.graph
@@ -1,26 +1,34 @@
 Nodes:
+(check_defs_1_xs_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (check_defs_1_xs_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2,BratNode (Constructor nil) [] [("value",List(Int))])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3,BratNode (Const 3) [] [("value",Int)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_xs_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(check_defs_1_xs_$rhs_check'Con_const_3,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3,BratNode (Constructor nil) [] [("value",List(Int))])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4,BratNode (Const 3) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_List_1,BratNode (Constructor List) [("listValue",[])] [("value",[])])
 (globals_decl_3_xs,BratNode Id [("a1",List(Int))] [("a1",List(Int))])
 
 Wires:
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2 0,List(Int),In check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0,List(Int),In check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0,List(Int),In check_defs_1_xs_$rhs_check'Con_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex check_defs_1_xs_$rhs_check'Con_cons_2 0,List(Int),In globals_decl_3_xs 0)
-(Ex check_defs_1_xs_$rhs_check'Con_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_cons_2 0)
+(Ex check_defs_1_xs_$rhs_check'Con__2 0,[],In check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3 0,List(Int),In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0,List(Int),In check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0,List(Int),In check_defs_1_xs_$rhs_check'Con_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex check_defs_1_xs_$rhs_check'Con_cons_3 0,List(Int),In globals_decl_3_xs 0)
+(Ex check_defs_1_xs_$rhs_check'Con_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_cons_3 0)
 (Ex globals_Int_2 0,[],In globals_List_1 0)
 (Ex globals_List_1 0,[],In globals___kca_xs 0)
diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph
index 88e697ab..dc69464d 100644
--- a/brat/test/golden/graph/pair.brat.graph
+++ b/brat/test/golden/graph/pair.brat.graph
@@ -1,13 +1,17 @@
 Nodes:
+(check_defs_1_xs_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (check_defs_1_xs_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
 (check_defs_1_xs_$rhs_check'Con_$!_pat2val_1,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val_1,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_3_true_1,BratNode (Constructor true) [] [("value",Bool)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_nil_1,BratNode (Constructor nil) [] [("value",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Bool),("tail",[])] [("value",[Bool])])
-(check_defs_1_xs_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",[Bool])] [("value",[Int,Bool])])
-(check_defs_1_xs_$rhs_check'Con_const_3,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val_1,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_4_true_1,BratNode (Constructor true) [] [("value",Bool)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_nil_1,BratNode (Constructor nil) [] [("value",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Bool),("tail",[])] [("value",[Bool])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1__1,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",[Bool])] [("value",[Int,Bool])])
+(check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_typeEqsTail_1__1,BratNode (Dummy *) [] [("dummy",[])])
 (globals_Bool_4,BratNode (Constructor Bool) [] [("value",[])])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_cons_1,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])])
@@ -16,11 +20,15 @@ Nodes:
 (globals_nil_5,BratNode (Constructor nil) [] [("value",[])])
 
 Wires:
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_3_true_1 0,Bool,In check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_nil_1 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0,[Bool],In check_defs_1_xs_$rhs_check'Con_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_cons_2 0,[Int,Bool],In globals_decl_6_xs 0)
-(Ex check_defs_1_xs_$rhs_check'Con_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_cons_2 0)
+(Ex check_defs_1_xs_$rhs_check'Con__2 0,[],In check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_4_true_1 0,Bool,In check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_nil_1 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0,[Bool],In check_defs_1_xs_$rhs_check'Con_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1__1 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val_1 0)
+(Ex check_defs_1_xs_$rhs_check'Con_cons_3 0,[Int,Bool],In globals_decl_6_xs 0)
+(Ex check_defs_1_xs_$rhs_check'Con_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_cons_3 0)
+(Ex check_defs_1_xs_$rhs_check'Con_typeEqsTail_1__1 0,[],In check_defs_1_xs_$rhs_check'Con_$!_pat2val_1 0)
 (Ex globals_Bool_4 0,[],In globals_cons_3 0)
 (Ex globals_Int_2 0,[],In globals_cons_1 0)
 (Ex globals_cons_1 0,[],In globals___kca_xs 0)
diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph
index 63d51b0b..07c8f981 100644
--- a/brat/test/golden/graph/vec.brat.graph
+++ b/brat/test/golden/graph/vec.brat.graph
@@ -1,22 +1,26 @@
 Nodes:
+(check_defs_1_xs_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (check_defs_1_xs_$rhs_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (check_defs_1_xs_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
-(check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
-(check_defs_1_xs_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(check_defs_1_xs_$rhs_check'Con_const_3,BratNode (Const 0) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
+(check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_xs_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
+(check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 0) [] [("value",Int)])
 (check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
@@ -26,17 +30,21 @@ Nodes:
 (globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2 0,Vec(Int, 0),In check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0,Vec(Int, 1),In check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_typeEqsTail_1_buildConst_1 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_numpat2val_1 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0,Vec(Int, 2),In check_defs_1_xs_$rhs_check'Con_cons_2 1)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_numpat2val_1 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 0)
-(Ex check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 1)
-(Ex check_defs_1_xs_$rhs_check'Con_cons_2 0,Vec(Int, 3),In globals_decl_4_xs 0)
-(Ex check_defs_1_xs_$rhs_check'Con_const_3 0,Int,In check_defs_1_xs_$rhs_check'Con_cons_2 0)
+(Ex check_defs_1_xs_$rhs_check'Con__2 0,[],In check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2 0,[],In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3 0,Vec(Int, 0),In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0,Vec(Int, 1),In check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_typeEqsTail_1_buildConst_1 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_numpat2val_1 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0,Vec(Int, 2),In check_defs_1_xs_$rhs_check'Con_cons_3 1)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_numpat2val_1 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 0)
+(Ex check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 1)
+(Ex check_defs_1_xs_$rhs_check'Con_cons_3 0,Vec(Int, 3),In globals_decl_4_xs 0)
+(Ex check_defs_1_xs_$rhs_check'Con_const_4 0,Int,In check_defs_1_xs_$rhs_check'Con_cons_3 0)
 (Ex check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In check_defs_1_xs_$rhs_check'Con_$!_numpat2val_1 0)
 (Ex check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 1)
diff --git a/brat/tools/validate.sh b/brat/tools/validate.sh
index 2a4342a0..e8f234d5 100755
--- a/brat/tools/validate.sh
+++ b/brat/tools/validate.sh
@@ -12,20 +12,22 @@ declare -a FAILED_TEST_MSGS
 UNEXPECTED_PASSES=
 NUM_FAILURES=0
 
-for json in $(find test/compilation/output -maxdepth 1 -name "*.json"); do
-    echo Validating "$json"
-    RESULT=$(cat "$json" | hugr_validator 2>&1)
-    if [ $? -ne 0 ]; then
-        FAILED_TEST_NAMES[NUM_FAILURES]=$json
-        FAILED_TEST_MSGS[NUM_FAILURES]=$RESULT
-        NUM_FAILURES=$((NUM_FAILURES + 1))
-    fi
-done
+for dir in test/compilation/output test/hugr/output; do
+    for json in $(find $dir -maxdepth 1 -name "*.json"); do
+        echo Validating "$json"
+        RESULT=$(cat "$json" | hugr_validator 2>&1)
+        if [ $? -ne 0 ]; then
+            FAILED_TEST_NAMES[NUM_FAILURES]=$json
+            FAILED_TEST_MSGS[NUM_FAILURES]=$RESULT
+            NUM_FAILURES=$((NUM_FAILURES + 1))
+        fi
+    done
 
-for invalid_json in $(find test/compilation/output -maxdepth 1 -name "*.json.invalid"); do
-    if (hugr_validator < $invalid_json 2>/dev/null > /dev/null); then
-        UNEXPECTED_PASSES="$UNEXPECTED_PASSES $invalid_json"
-    fi
+    for invalid_json in $(find test/compilation/output -maxdepth 1 -name "*.json.invalid"); do
+        if (hugr_validator < $invalid_json 2>/dev/null > /dev/null); then
+            UNEXPECTED_PASSES="$UNEXPECTED_PASSES $invalid_json"
+        fi
+    done
 done
 
 RED='\033[0;31m'