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/Compile/Hugr.hs b/brat/Brat/Compile/Hugr.hs
index 3f9c05df..ec0e7d2d 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, makeIO, makeCS, CompilationState(..), addEdge, addNode, Container(..), onHugr) where
 
 import Brat.Constructors.Patterns (pattern CFalse, pattern CTrue)
-import Brat.Checker.Monad (track, trackM, CheckingSig(..), CaptureSets)
+import Brat.Checker.Monad (track, trackM, CheckingSig(..))
 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 hiding (root)
+import Brat.Naming
 import Brat.QualName
 import Brat.Syntax.Port
 import Brat.Syntax.Common
@@ -29,15 +29,11 @@ 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 (sortBy)
+import Data.Functor ((<&>))
 import qualified Data.Map as M
 import Data.Maybe (catMaybes, fromJust)
-import Data.Ord (comparing)
 import Data.Traversable (for)
 import Control.Monad.State
 import Data.List.NonEmpty (NonEmpty, nonEmpty)
@@ -52,7 +48,6 @@ 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
  , hugr :: HugrGraph NodeId
  , compiled :: M.Map Name NodeId  -- Mapping from Brat nodes to Hugr nodes
@@ -60,14 +55,8 @@ data CompilationState = CompilationState
  -- 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)
  }
 
 type Compile = State CompilationState
@@ -81,25 +70,18 @@ data Container = Ctr {
   output :: NodeId
 }
 
-makeCS :: (Graph, Namespace, CaptureSets, Store) -> HugrGraph NodeId -> CompilationState
-makeCS (g, ns, cs, store) hugr =
+makeCS :: (Graph, Namespace, Store) -> HugrGraph NodeId -> CompilationState
+makeCS (g, ns, store) hugr =
   CompilationState
     { bratGraph = g
     , nameSupply = ns
-    , capSets = cs
     , hugr = hugr
     , 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) })
-
 freshNode :: String -> NodeId -> Compile NodeId
 freshNode name parent = do
   s <- get
@@ -110,7 +92,7 @@ freshNode name parent = do
 makeIO :: String -> NodeId -> Compile Container
 makeIO name parent = do
   input <- freshNode (name ++ "_Input") parent
-  output <- freshNode (name ++ "_Input") parent
+  output <- freshNode (name ++ "_Output") parent
   onHugr $ H.setFirstChildren parent [input, output]
   pure $ Ctr {parent, input, output}
 
@@ -126,6 +108,16 @@ addNode nam (parent, op) = do
   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
+  put (st { holes = (holes st) :< (h, outPort)})
+  pure h
+
 filePrefix :: [String] -> Name -> Maybe Name
 filePrefix prefixes (MkName (("checking",_):_filename:ns)) =
   hasPrefix (["globals"]++prefixes) (MkName ns)
@@ -203,33 +195,6 @@ compileConst parent tm ty = do
   addEdge (Port constId 0, Port loadId 0)
   pure loadId
 
-compileArithNode :: NodeId -> ArithOp -> Val Z -> Compile NodeId
-compileArithNode parent op TNat  = addNode (show op ++ "_Nat") (parent, OpCustom $ case op of
-  Add -> binaryIntOp "iadd"
-  Sub -> binaryIntOp "isub"
-  Mul-> binaryIntOp "imul"
-  Div -> intOp "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") (parent, OpCustom $ case op of
-  Add -> binaryIntOp "iadd"
-  Sub -> binaryIntOp "isub"
-  Mul-> binaryIntOp "imul"
-  Div -> intOp "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") (parent, OpCustom $ case op of
-  Add -> binaryFloatOp "fadd"
-  Sub -> binaryFloatOp "fsub"
-  Mul-> binaryFloatOp "fmul"
-  Div-> binaryFloatOp "fdiv"
-  Pow -> error "TODO: Pow"  -- Not defined in extension
- )
-compileArithNode _ _ ty = error $ "compileArithNode: Unexpected type " ++ show ty
-
-dumpJSON :: Compile BS.ByteString
-dumpJSON = gets hugr <&> (encode . H.serialize)
-
 compileClauses :: NodeId -> [TypedPort] -> NonEmpty (TestMatchData m, Name) -> Compile [TypedPort]
 compileClauses parent ins ((matchData, rhs) :| clauses) = do
   (ns, _) <- gets bratGraph
@@ -319,36 +284,13 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
   -- Otherwise, NodeId of compiled node, and list of Hugr in-edges (source and target-port)
   compileNode :: Compile (Maybe (NodeId, [(PortId NodeId, Int)]))
   compileNode = case (filePrefix ["decl"] name) of
-    Just _ -> 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
-      hTys <- in_edges name <&> (map (compileType . snd . fst) . sortBy (comparing snd))
-
-      decls <- gets decls
-      let (funcDef, extra_call) = decls M.! name
-      nod <- if extra_call
-            then addNode ("direct_call(" ++ show funcDef ++ ")")
-                          (parent, OpCall (CallOp (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 ++ ")")
-                (parent, OpLoadFunction (LoadFunctionOp 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)])
+    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 thing ins outs) -> compileNode' thing ins outs
+        (BratNode _ _ _) -> error "Can't compile classical Brat"
         (KernelNode thing ins outs) -> compileNode' thing ins outs
       case nod_edge_info of
         Nothing -> pure Nothing
@@ -359,12 +301,12 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
   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
@@ -377,77 +319,8 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
               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) (parent, OpCustom (holeOp 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 $
-       \Ctr{parent, input, output} -> do
-        setOp input (OpIn (InputNode inputTys [("source", "Prim")]))
-        let ins = zip (Port input <$> [0..]) inputTys
-        outs <- addNodeWithInputs n (parent, OpCustom (CustomOp ext op boxFunTy [])) ins outputTys
-        setOp output (OpOut (OutputNode outputTys [("source", "Prim")]))
-        for_ (zip (fst <$> outs) (Port output <$> [0..])) addEdge
-        pure ()
-      pure $ default_edges loadConst
-
-    -- Check if the node has prefix "globals", hence should be a direct call
-    Eval tgt@(Ex outNode _) -> do
-      ins <- compilePorts ins
-      outs <- compilePorts outs
-      (ns, _) <- gets bratGraph
-      decls <- gets decls
-      case filePrefix ["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) (parent, OpCustom (CustomOp ext op (FunctionType ins outs [ext]) []))
-          x -> error $ "Expected a Prim node but got " ++ show x
-        Nothing -> case filePrefix [] 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 ++ ")")
-                                    (parent, OpCall (CallOp (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)
-          _ -> getOutPort parent tgt >>= \case
-            Just funcPort@(Port calleeId _) -> do
-              callerId <- addNode ("indirect_call(" ++ show calleeId ++ ")")
-                                  (parent, OpCallIndirect (CallIndirectOp (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, [(funcPort, 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 (show name) (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
+
+        Nothing -> addHole parent sig outPort
 
     Source -> error "Source found outside of compileBox"
       
@@ -474,14 +347,7 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
       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" (parent, OpCustom (CustomOp "BRAT" "Replicate" sig [TAType elemTy]))
     x -> error $ show x ++ " should have been compiled outside of compileNode"
 
 compileConstructor :: NodeId -> QualName -> QualName -> FunctionType -> Compile NodeId
@@ -510,92 +376,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]) -> (Container -> Compile a) -> Compile (TypedPort, a)
-compileConstDfg parent desc (inTys, outTys) contents = do
-  let funTy = FunctionType inTys outTys bratExts
-  -- First, we fork off a new namespace
-  st <- get
-  let (nsx,ns') = split desc (nameSupply st)
-  put (st {nameSupply = ns'})
-  -- And pass that namespace into nested monad that compiles the DFG
-  let boxdesc = "Box_" ++ desc
-  let (h, nsx') = runState (H.new boxdesc (OpDFG $ DFG funTy [])) nsx
-  let (a, compState) = runState (makeIO boxdesc (root h) >>= contents)
-                                (makeCS (bratGraph st, nsx' ,capSets st, store st) h)
-  let nestedHugr = H.serialize (hugr compState)
-  let ht = HTFunc $ PolyFuncType [] funTy
-
-  constNode <- addNode ("ConstTemplate_" ++ desc) (parent, OpConst (ConstOp (HVFunction nestedHugr)))
-  lcPort <- head <$> addNodeWithInputs ("LoadTemplate_" ++ desc) (parent, OpLoadConstant (LoadConstantOp 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) $
-   -- ideally would name the Input "LiftedCapturedInputs"
-   \Ctr {parent, input = src_id, output} -> do
-    setOp src_id (OpIn (InputNode 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
-    compileTarget parent output tgt
-
-  -- Finally, we add a `Partial` node to supply the captured params.
-  partialNode <- addNode "Partial" (parent, OpCustom $ partialOp 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 -> String -> (Name, Name) -> CTy Kernel Z -> Compile TypedPort
-compileKernBox parent desc src_tgt 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" ++ desc) boxInnerSig $ \ctr -> do
-    compileBox ctr src_tgt
-    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 kernel_src) ins outs) = ns M.! splice
-    ins <- compilePorts ins
-    outs <- compilePorts outs
-    kernel_src <- getOutPort parent kernel_src <&> fromJust
-    pure (kernel_src, 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_" ++ desc) (parent, OpCustom (substOp (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
@@ -798,95 +578,27 @@ undoPrimTest parent inPorts outTy (PrimLitTest tm) = do
   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 -> NodeId
-              -> Compile ()
-compileModule venv moduleNode = do
-  -- 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
-    ctr@Ctr {parent=defNode} <- freshNodeWithIO (show fnName ++ "_def") moduleNode
-    setOp defNode (OpDefn $ FuncDefn (show fnName) funTy [])
-    registerFuncDef idNode (defNode, extra_call)
-    pure (body ctr)
-    )
-  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, Container -> 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, [(NodeId, OutPort)])
+compileKernel (nsp, store, g@(ns, _)) desc name = (hgr, holelist) where
+  (src_tgt, outs) = case ns M.! 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, flip 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, \Ctr {parent, input, output} -> do
-              setOp input (OpIn (InputNode [] [("source", "analyseDecl")]))
-              setOp output (OpOut (OutputNode [thunkTy] [("source", "analyseDecl")]))
-              wire <- compileKernBox parent (show input) (src, tgt) cty
-              addEdge (fst wire, Port output 0))
-          _ -> 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))
-
-  -- 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 filePrefix ["decl"] idNode of
-              Just _ -> pure (fnName, idNode) -- assume all ports are 0,1,2...
-              Nothing -> []
-
-  funcReturning :: [HugrType] -> PolyFuncType
-  funcReturning outs = PolyFuncType [] (FunctionType [] outs bratExts)
-
-compileNoun :: [HugrType] -> [OutPort] -> Container -> Compile ()
-compileNoun outs srcPorts Ctr {parent, input, output} = do
-  setOp input (OpIn (InputNode [] [("source", "compileNoun")]))
-  setOp output (OpOut (OutputNode 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 =
-  let (hugr, ns') = runState (H.new "module" (OpMod ModuleOp)) ns
-  in evalState
-    (trackM "compileFunctions" *>
-     compileModule venv (root hugr) *>
-     trackM "dumpJSON" *>
-     dumpJSON
-    )
-    (makeCS (g, ns', capSets, store) hugr)
+    (BratNode (Box src tgt) [] outs) -> ((src, tgt), outs)
+    nt -> error $ "Can only compile Box nodes, not " ++ show nt ++ " (for " ++ show name ++ ")"
+  cty = case outs of
+    [(_, VFun Kerny cty)] -> cty
+  (startHugr, nsp') = runState (H.new desc (OpDFG $ DFG (FunctionType hInTys hOutTys bratExts) [])) nsp
+  (hgr, holelist) = flip evalState (makeCS (g, nsp', store) startHugr) $ do
+    ctr <- makeIO desc (H.getRoot 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 e1bd3534..9b031ac5 100644
--- a/brat/Brat/Compiler.hs
+++ b/brat/Brat/Compiler.hs
@@ -3,16 +3,21 @@ module Brat.Compiler (printAST
                      ,writeDot
                      ,compileFile
                      ,compileAndPrintFile
+                     ,compileToGraph
                      ,CompilingHoles(..)
                      ) where
 
-import Brat.Checker.Types (TypedHole)
+import Brat.Checker.Types (TypedHole, Modey(Kerny), VEnv)
 import Brat.Compile.Hugr
 import Brat.Dot (toDotString)
 import Brat.Elaborator
 import Brat.Error
+import Brat.Graph(Graph, Node(BratNode), NodeType(Box, Id))
 import Brat.Load
-import Brat.Naming (root, split)
+import Brat.Naming (Namespace, root, split, Name)
+import Brat.QualName (QualName)
+import Brat.Syntax.Port (NamedPort(..), OutPort(..), InPort(..))
+import Brat.Syntax.Value (Val(VFun))
 
 import Control.Exception (evaluate)
 import Control.Monad (forM, when)
@@ -20,6 +25,8 @@ import Control.Monad.Except
 import Data.List (intercalate)
 import qualified Data.Map as M
 import qualified Data.ByteString.Lazy as BS
+import Data.Foldable (for_)
+import Data.HugrGraph (HugrGraph, NodeId, to_json)
 import System.Exit (die)
 
 printDeclsHoles :: [FilePath] -> String -> IO ()
@@ -74,18 +81,43 @@ instance Show CompilingHoles where
   show (CompilingHoles hs) = unlines $
     "Can't compile file with remaining holes": fmap (("  " ++) . show) hs
 
-compileFile :: [FilePath] -> String -> IO (Either CompilingHoles BS.ByteString)
-compileFile libDirs file = do
+compileToGraph :: [FilePath] -> String -> IO (Namespace, VMod)
+compileToGraph libDirs file = do
   let (checkRoot, newRoot) = split "checking" root
   env <- runExceptT $ loadFilename checkRoot libDirs file
-  (declEnv, holes, defs, outerGraph, capSets) <- eitherIO env
+  (newRoot,) <$> eitherIO env
+
+-- Map from box name to (compiled hugr, list of hole nodes in it)
+type CompilationResult = M.Map Name (HugrGraph NodeId, [NodeId])
+
+compileFile :: [FilePath] -> String -> IO (Either CompilingHoles CompilationResult)
+compileFile libDirs file = do
+  (newRoot, (declEnv, holes, st, outerGraph, _)) <- compileToGraph libDirs file
   let venv = M.map fst declEnv
   case holes of
-    [] -> Right <$> evaluate -- turns 'error' into IO 'die'
-                    (compile defs newRoot outerGraph capSets venv)
+    [] -> let box_decls = (M.keys declEnv) >>= (findBoxes venv outerGraph)
+          in Right <$> (evaluate -- turns 'error' into IO 'die'
+            $ M.fromList [(n, let (hugr, holes) = compileKernel (newRoot, st, outerGraph) "root" n
+                               in (hugr, map fst holes))
+                         | n <- box_decls])
     hs -> pure $ Left (CompilingHoles hs)
+ where
+  findBoxes :: VEnv -> Graph -> QualName -> [Name]
+  findBoxes venv (ns, es) name = case M.lookup name venv of
+        Nothing -> error $ (show name) ++ ".... not found in VEnv"
+        Just vals -> vals >>= \(NamedPort (Ex n _) _, _) -> case M.lookup n ns of
+            Just (BratNode Id _ _) ->
+               [src | (Ex src 0, _, In tgt _) <- es, tgt == n, isKernelBox src ns]
+            _ -> []
+  isKernelBox :: Name -> M.Map Name Node -> Bool
+  isKernelBox name ns
+    | Just (BratNode (Box _ _ ) [] [(_, VFun Kerny _cty)]) <- M.lookup name ns = True
+    | otherwise = False
 
 compileAndPrintFile :: [FilePath] -> String -> IO ()
 compileAndPrintFile libDirs file = compileFile libDirs file >>= \case
-  Right bs -> BS.putStr bs
+  Right hs -> for_ (M.toList hs) $ \(n, (hugr, splices)) -> do
+    putStrLn $ "Compiled box: " ++ show n
+    BS.putStr (to_json hugr)
+    putStrLn $ "With splices: " ++ show splices
   Left err -> die (show err)
diff --git a/brat/Brat/Constructors/Patterns.hs b/brat/Brat/Constructors/Patterns.hs
index 1388d159..4fd6fac1 100644
--- a/brat/Brat/Constructors/Patterns.hs
+++ b/brat/Brat/Constructors/Patterns.hs
@@ -2,10 +2,11 @@ module Brat.Constructors.Patterns where
 
 import Brat.QualName
 
-pattern CSucc, CDoub, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
+pattern CSucc, CDoub, CFull, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
         CConcatEqEven, CConcatEqOdd, CRiffle :: QualName
 pattern CSucc = PrefixName [] "succ"
 pattern CDoub = PrefixName [] "doub"
+pattern CFull = PrefixName [] "full"
 pattern CNil = PrefixName [] "nil"
 pattern CSome = PrefixName [] "some"
 pattern CNone = PrefixName [] "none"
diff --git a/brat/Brat/Graph.hs b/brat/Brat/Graph.hs
index 62c4619b..1de73e12 100644
--- a/brat/Brat/Graph.hs
+++ b/brat/Brat/Graph.hs
@@ -51,6 +51,8 @@ data NodeType :: Mode -> Type where
   ArithNode :: ArithOp -> NodeType Brat
   Replicate :: NodeType Brat
   MapFun :: NodeType a
+  -- The thing that gets plugged into type hopes when we solve them
+  Dummy :: TypeKind -> NodeType Brat
 
 deriving instance Show (NodeType a)
 
@@ -110,9 +112,6 @@ toGraph (ns, ws) = G.graphFromEdges adj
           )
         | (name, node) <- M.toList ns]
 
-wiresFrom :: Name -> Graph -> [Wire]
-wiresFrom src (_, ws) = [ w | w@(Ex a _, _, _) <- ws, a == src ]
-
 lookupNode :: Name -> Graph -> Maybe Node
 lookupNode name (ns, _) = M.lookup name ns
 
@@ -121,3 +120,10 @@ wireStart (Ex x _, _, _) = x
 
 wireEnd :: Wire -> Name
 wireEnd (_, _, In x _) = x
+
+-- These are horribly inefficient until we use a better structure for graph edges
+wiresFrom :: Name -> Graph -> [Wire]
+wiresFrom src (_, ws) = [ w | w@(Ex a _, _, _) <- ws, a == src ]
+
+wiresTo :: Name -> Graph -> [Wire]
+wiresTo tgt (_, ws) = [ w | w@(_, _, In a _) <- ws, a == tgt ]
diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
index c1a6ea4c..bb495407 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..45037279
--- /dev/null
+++ b/brat/Brat/Machine.hs
@@ -0,0 +1,437 @@
+module Brat.Machine (runInterpreter) where
+
+import Brat.Checker.Monad (CaptureSets)
+import Brat.Checker.Types (Store, initStore)
+import Brat.Compiler (compileToGraph)
+import Brat.Compile.Hugr
+import Brat.Constructors.Patterns
+import Brat.Naming (Name, Namespace, split)
+import Brat.Graph (Graph, NodeType (..), Node (BratNode), wiresTo, MatchSequence (..), PrimTest (..), TestMatchData (..), emptyGraph)
+import Brat.QualName (QualName(..), plain)
+import Brat.Syntax.Simple (SimpleTerm(..))
+import Brat.Syntax.Common
+import Brat.Syntax.Value
+
+import Data.Hugr
+import qualified Data.HugrGraph as HG
+import Hasochism
+
+import Control.Monad.State (execState, gets, evalState)
+import qualified Data.Text.Lazy as T
+import Data.Maybe (fromMaybe, fromJust, isNothing)
+import Data.List (uncons)
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Bwd
+import Util (zipSameLength)
+
+type GraphInfo = (Graph, Store, Namespace, CaptureSets)
+
+runInterpreter :: [FilePath] -> String -> String -> IO (Either T.Text (HG.HugrGraph HG.NodeId))
+runInterpreter libDirs file runFunc = do
+    (root, (declEnv, _, st, outerGraph, capSets)) <- compileToGraph libDirs file
+    let venv = M.map fst declEnv
+    --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.
+    pure $ case outTask of
+      Finished [(KernelV hugr)] -> Right hugr
+      _ -> Left $ T.pack $ show outTask
+
+data Frame where
+    BratValues :: EvalEnv -> Frame
+    -- In process of evaluating a list of OutPorts: (values computed, ports still needed)
+    -- (excluding the one that's in process of being evaluated)
+    EvalPorts :: Bwd Value -> [OutPort] -> Frame
+    -- We're waiting for a task to deliver us all of the inputs for this node,
+    -- goal is to deliver the single requested OutPort (after evaluating the node)
+    AwaitNodeInputs :: OutPort -> Frame
+    -- Waiting for a task to deliver us all of the outputs for a node,
+    -- goal is to deliver the single requested OutPort.
+    SelectFromNodeOutputs :: 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 -> [(HG.NodeId, OutPort)] -> Frame
+    -- Remaining thunks with their inputs, and rows output by prior thunks
+    VectorisedFuncs :: [(BratThunk, [Value])] -> Bwd [Value] -> Frame
+
+divider = replicate 78 '-'
+
+instance Show Frame where
+  show f = unlines $
+   [""
+   ,divider
+   ] ++ showFrame f
+
+showFrame :: Frame -> [String]
+showFrame (BratValues env) = ["BratValues", show env]
+showFrame (EvalPorts vz ports) = ["EvalPorts", show vz, "<-- You are here -->", show ports]
+showFrame (AwaitNodeInputs out) = ["AwaitNodeInputs", show out ++ "<-- You are here"]
+showFrame (SelectFromNodeOutputs out) = ["SelectFromNodeOutputs", show out]
+showFrame (CallWith vz) = ["CallWith", show vz]
+showFrame (ReturnTo fz) = "ReturnTo" : (("> " ++) <$> showFrames fz)
+showFrame (Alternatives matches vz) = ["Alternatives", show matches, show vz]
+showFrame (PerformMatchTests tests srcs node) = ["PerformMatchTests", show tests, show srcs, show node] -- TODO
+showFrame (DoSplices hg src hugrs) = ["DoSplices", show hg, show src, show hugrs]
+showFrame (VectorisedFuncs ths outs) = ["VectorisedFuncs", "remaining " ++ show (length ths) ++ " thunks", show outs]
+showFrames :: Bwd Frame -> [String]
+showFrames = foldMap (\f -> divider : showFrame f)
+
+data Task where
+    Suspend :: [Frame] -> Task -> Task
+    -- A single Outport value is ready; searches for EvalPorts or DoSplices to use it.
+    Use :: Value -> Task
+    -- Finished computing a list of values (all outputs of one node);
+    -- searches for SelectFromNodeOutputs to use one, or is final result (of runInterpreter or ReturnTo).
+    Finished :: [Value] -> Task
+    -- Try the next clause in an Alternatives
+    TryNextMatch :: Task
+    -- No clause in an Alternatives matched
+    NoMatch :: Task
+    StuckOnNode :: Name -> Node -> Task
+  deriving Show
+
+lookupOutport :: Bwd Frame -> OutPort -> Maybe Value
+lookupOutport B0 _ = Nothing
+-- TODO: Might we need to look beyond the most local cache?
+-- Believe "CaptureSets" are computed to ensure we don't need to.
+lookupOutport (_ :< BratValues env) p = M.lookup p env
+--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) = evalPort g (fz :< EvalPorts valz ps) p
+evalPorts g fz valz [] = run g fz (Finished (valz <>> []))
+
+-- Evaluates a port (or retrieves value from cache)
+evalPort :: GraphInfo -> Bwd Frame -> OutPort -> Task
+evalPort gi fz p@(Ex name _) = case lookupOutport fz p of
+    Just v -> run gi fz (Use v)
+    Nothing -> evalNodeInputs gi (fz :< AwaitNodeInputs p) name
+
+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 -> [(HG.NodeId, OutPort)] -> Task
+evalSplices gi fz hugr [] = run gi fz (Finished [KernelV hugr])
+evalSplices gi fz hugr ((nid, outport):rest) =
+    evalPort gi (fz :< DoSplices hugr nid rest) outport
+
+runVectorisedThunks :: GraphInfo -> Bwd Frame -> [(BratThunk, [Value])] -> Bwd [Value] -> Task
+runVectorisedThunks gi fz [] outs = run gi fz (Finished $ transposeRows2V $ outs <>> [])
+ where
+  -- outs accumulates a [Value] from each thunk, being a row.
+  -- assemble corresponding elements from each row into a VecV,
+  -- being that element of the output row of the vectorised thunk.
+  transposeRows2V :: [[Value]] -> [Value]
+  transposeRows2V rows = let rows' = map uncons rows
+    in if all isNothing rows'
+       then []
+       else let (hds, tls) = unzip (map fromJust rows') in (VecV hds) : (transposeRows2V tls)
+runVectorisedThunks gi fz ((th, inputs):ths) outs =
+    runThunk gi (fz :< VectorisedFuncs ths outs) th inputs
+
+run :: GraphInfo -> Bwd Frame -> Task -> Task
+--run g fz t | trace ("RUN: " ++ show fz ++ "\n" ++ show t) False = undefined
+
+runThunk :: GraphInfo -> Bwd Frame -> BratThunk -> [Value] -> Task
+runThunk gi fz (BratClosure env src tgt) inputs =
+    let env_with_args = foldr (uncurry M.insert) env [(Ex src off, val) | (off, val) <- zip [0..] inputs]
+    in evalNodeInputs gi (fz :< (BratValues env_with_args)) tgt
+runThunk (g,st,ns,cs) fz (BratPrim ext op _cty) inputs
+ | (hugrNS,newRoot) <- split "hugr" ns, Just outs <- runPrim hugrNS (ext,op) inputs = run (g,st,newRoot,cs) fz (Finished outs)
+runThunk gi fz (VectorisedThunks ths) inputs =
+  runVectorisedThunks gi fz (fromJust $ zipSameLength ths $ transposeV2Rows inputs) B0
+ where
+  -- inputs to the vectorised thunk are a row of vectors;
+  -- we run thunk#1 on the row formed from element#1 of each vector, and so on.
+  transposeV2Rows :: [Value] -> [[Value]]
+  transposeV2Rows vs
+    | all isEmptyVecV vs = []
+    | otherwise = let (hds, tls) = unzip $ map (\(VecV (hd:tl)) -> (hd, VecV tl)) vs in hds : (transposeV2Rows tls)
+  isEmptyVecV :: Value -> Bool
+  isEmptyVecV (VecV []) = True
+  isEmptyVecV _ = False
+
+-- Evaluate a node given its inputs (graph edges, excluding e.g. func to Eval)
+evalNode :: GraphInfo -> Bwd Frame -> Name -> [Value] -> Task
+evalNode gi@(g@(nodes, _), st, root, cs) fz 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) _ _) -> evalPort gi (fz :< CallWith ins) func
+  (BratNode (Box _ _) [] [(_, 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 _) _ _) -> run gi fz (Finished [DummyV])
+  (BratNode (Prim (ext, op)) [] [(_, VFun Braty cty)]) -> run gi fz (Finished [ThunkV (BratPrim ext op cty)])
+  (BratNode (Selector stor) _ _) -> case (stor, ins) of
+      (PrefixName [] "cons", [VecV (x:xs)]) -> run gi fz (Finished [x, VecV xs])
+  (BratNode Replicate _ _) -> case ins of
+    [IntV n, elem] -> run gi fz (Finished [(VecV (replicate n elem))])
+  (BratNode MapFun _ _) -> case ins of
+    -- We have a vector (or vec of vecs, n-dimensions) of functions
+    [IntV len, VecV funs] -> run gi fz (Finished [dig len funs])
+  nw -> run gi fz (StuckOnNode n nw)
+ where
+   -- Assuming a tree of VecV's whose leaf values are ThunkV's,
+   -- Convert the bottom level of VecV's to VectorisedFuncs.
+   -- We assume the tree is of uniform height (and arity at each *level*,
+   -- perhaps varying between levels), this should be guaranteed by the checker.
+   -- (TODO: consider encoding the expected levels/arities in the MapFun?)
+  dig :: Int -> [Value] -> Value
+  dig n vals
+   | Just vecs <- mapM getVecs vals = VecV vecs
+   | Just ths <- mapM getThunks vals
+   , n == length vals = ThunkV (VectorisedThunks ths)
+   where
+    getVecs :: Value -> Maybe Value
+    getVecs (VecV x) = Just (dig n x)
+    getVecs _ = Nothing
+
+    getThunks :: Value -> Maybe BratThunk
+    getThunks (ThunkV th) = Just th
+    getThunks _ = Nothing
+
+
+-- 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' = execState (HG.splice_prepend nid sub_hugr) hugr
+    in evalSplices gi fz hugr' rest
+run gi (fz :< CallWith inputs) (Use (ThunkV th)) = runThunk gi (B0 :< ReturnTo fz) th inputs
+
+---- Finished (list of values)
+run gi (fz :< AwaitNodeInputs req@(Ex name _)) (Finished inputs) =
+    evalNode gi (fz :< SelectFromNodeOutputs req) name inputs
+run gi (fz :< SelectFromNodeOutputs (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 evalPort gi (fz :< CallWith vals) $ Ex box 0
+
+-- Next element of VectorisedFuncs
+run gi (fz :< VectorisedFuncs th_inps outs) (Finished vals) =
+  runVectorisedThunks gi fz th_inps (outs :< vals)
+
+run gi (fz :< BratValues _) t = run gi fz t
+run _ B0 t = t
+run gi fz t = run gi fz (Suspend [] t)
+
+runPrim :: Namespace -> (String, String) -> [Value] -> Maybe [Value]
+runPrim _ ("arith","i2f") [IntV v] = Just [FloatV (fromIntegral v)]
+runPrim ns ("tket", op) [FloatV th] | op `elem` ["CRx", "CRy", "CRz"] = Just [KernelV (makeParametrisedGateHugr ns op th 2)]
+runPrim _ _ _ = Nothing
+
+makeParametrisedGateHugr :: Namespace -> {- Op name: -} String -> {- angle arg: -} Double -> Int -> HG.HugrGraph HG.NodeId
+makeParametrisedGateHugr ns op th nqubits =
+  let (ns', newRoot) = split "" ns in
+   hugr $ flip execState (makeCS (emptyGraph, newRoot, initStore) (dfgHugr ns')) $ do
+     parent <- gets (HG.getRoot . hugr)
+     Ctr {parent,input,output} <- makeIO "" parent
+     onHugr $ HG.setOp input (OpIn (InputNode [HTQubit, HTQubit] []))
+     onHugr $ HG.setOp output (OpOut (OutputNode [HTQubit, HTQubit] []))
+     -- TODO: Make this a rotation (using hvRotation) when we use the actual TKET
+     -- ops, we're just targeting dummy ops in the BRAT extension for the sake of
+     -- getting things going until hugr is updated.
+     constTh <- addNode "k_th" (parent, OpConst (ConstOp (hvFloat th)))
+     th <- addNode "th" (parent, OpLoadConstant (LoadConstantOp hugrFloat))
+     gate <- addNode "gate" (parent, addMetadata [("Our","Gate")] $ OpCustom gateOp)
+     addEdge (Port input 0, Port gate 0)
+     addEdge (Port input 1, Port gate 1)
+     addEdge (Port constTh 0, Port th 0)
+     addEdge (Port th 0, Port gate 2)
+     addEdge (Port gate 0, Port output 0)
+     addEdge (Port gate 1, Port output 1)
+ where
+  dfgHugr :: Namespace -> HG.HugrGraph HG.NodeId
+  dfgHugr = evalState (HG.new "" (OpDFG (DFG signature [])))
+
+  signature = FunctionType
+   { input = [HTQubit | _ <- [1..nqubits]]
+   , output = [HTQubit | _ <- [1..nqubits]]
+   , extensions = bratExts
+   }
+
+  gateOp = CustomOp
+   { extension = "BRAT" -- TODO: Make this "tket.quantum"
+   , op_name = op
+   , signature_ = FunctionType
+                  { input = [HTQubit | _ <- [1..nqubits]]
+                             ++ [hugrFloat] -- TODO: Make this hugrRotation
+                  , output = [HTQubit | _ <- [1..nqubits]]
+                  , extensions = bratExts
+                  }
+   , args = []
+   }
+
+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 CFull [IntV n] = IntV ((2 ^ n) - 1)
+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 (Text s) = StringV s
+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 CSnoc (VecV vs@(_:_)) = Just [VecV (init vs), last vs]
+testCtor CList CNil (VecV []) = Just []
+testCtor CList 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 [_] = 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 HG.NodeId)
+  | DummyV
+  | StringV String
+
+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)
+  | VectorisedThunks [BratThunk] -- result of MapFun
+
+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 (VectorisedThunks ths)) = "<vectorized thunk of " ++ show (length ths) ++ ">"
+  show (ThunkV _) = "<thunk>"
+  show (KernelV k) = "Kernel (" ++ show k ++ ")"
+  show DummyV = "Dummy"
+  show (StringV str) = show str
+
+type EvalEnv = M.Map OutPort Value
diff --git a/brat/Data/Hugr.hs b/brat/Data/Hugr.hs
index 6ea8b202..5f9d617e 100644
--- a/brat/Data/Hugr.hs
+++ b/brat/Data/Hugr.hs
@@ -66,6 +66,9 @@ sumOfRows ty = error $ show ty ++ " isn't a sum of row tuples"
 compileSumOfRows :: SumOfRows -> HugrType
 compileSumOfRows (SoR rows) = HTSum (SG (GeneralSum rows))
 
+hugrRotation :: HugrType
+hugrRotation = HTOpaque "tket.rotation" "rotation" [] TBCopy
+
 -- Depends on HugrValue (via TypeArg in HTOpaque)
 data HugrType
   = HTQubit
@@ -231,6 +234,8 @@ hvFloat x = HVExtension ["arithmetic.float_types"] hugrFloat
             (CC "ConstF64" (KeyMap.singleton "value" x))
 hvInt x = HVExtension ["arithmetic.int_types"] hugrInt
           (CC "ConstInt" (KeyMap.insert "log_width" 6 (KeyMap.singleton "value" x)))
+hvRotation rad = HVExtension ["tket.rotation"] hugrRotation
+                 (CC "ConstRotation" (KeyMap.singleton "half_turns" (rad / pi)))
 
 valFromSimple :: SimpleTerm -> HugrValue
 valFromSimple (Num x) = hvInt x
diff --git a/brat/Data/HugrGraph.hs b/brat/Data/HugrGraph.hs
index 8c5dfe89..5c76f531 100644
--- a/brat/Data/HugrGraph.hs
+++ b/brat/Data/HugrGraph.hs
@@ -1,19 +1,23 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Data.HugrGraph(NodeId,
-                      HugrGraph(root), -- do NOT export contents, keep abstract
+                      HugrGraph, -- do NOT export contents, keep abstract
                       new,
                       freshNode,
+                      getRoot, getNodes,
                       setFirstChildren,
                       setOp, getParent, getOp,
                       addEdge, addOrderEdge,
-                      serialize,
-                      splice, splice_new, splice_prepend, inlineDFG
+                      splice, splice_new, splice_prepend, inlineDFG,
+                      serialize, to_json
                      ) where
 
 import Brat.Naming (Namespace, Name(..), fresh)
 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 (foldl', for_)
 import Data.Functor ((<&>))
@@ -25,6 +29,12 @@ track = const id
 
 newtype NodeId = NodeId Name deriving (Eq, Ord, Show)
 
+getRoot :: HugrGraph n -> n
+getRoot HugrGraph {root} = root
+
+getNodes :: HugrGraph n -> [n]
+getNodes HugrGraph {parents, root} = root:(M.keys parents)
+
 data HugrGraph n = HugrGraph {
     root :: n,
     parents :: M.Map n n, -- definitive list of (valid) nodes, excluding root
@@ -73,12 +83,14 @@ new nam op = state $ \ns ->
 
 addEdge :: Ord n =>(PortId n, PortId n) -> State (HugrGraph n) ()
 addEdge (src@(Port s o), tgt@(Port t i)) = state $ \h@HugrGraph {..} ->
-  ((), ) $ case (M.lookup s nodes, M.lookup t nodes) of
+  ((), ) $ case (M.lookup s parents, M.lookup t parents) of
     (Just _, Just _) -> h {
       edges_out = addToMap s (o, tgt) edges_out id,
       edges_in = addToMap t (src, i) edges_in no_other_inedge
     }
-    _ -> error "addEdge to/from node not present"
+    (Nothing, Just _) -> error $ "addEdge source not present"
+    (Just _, Nothing) -> error $ "addEdge Target not present"
+    _ -> error $ "addEdge nodes not present"
  where
   addToMap :: Ord k => k -> v -> M.Map k [v] -> ([v] -> [v]) -> M.Map k [v]
   addToMap k v m chk = M.alter (Just . (v:) . maybe [] chk) k m
@@ -157,7 +169,7 @@ splice_prepend hole add = splice hole add (keyMap M.!)
 splice_new :: forall n. (Ord n, Show n) => NodeId -> HugrGraph n -> State (HugrGraph NodeId, Namespace) ()
 splice_new hole add = modify $ \(host, ns) ->
   let
-   (ns_out, keyMap) = foldr newMapping (ns, M.empty) (M.keys (parents add)) 
+   (ns_out, keyMap) = foldr newMapping (ns, M.empty) (M.keys (parents add))
    newMapping :: n -> (Namespace, M.Map n NodeId) -> (Namespace, M.Map n NodeId)
    newMapping n (ns, km) = let (nn, ns') = fresh (show n) ns in (ns', M.insert n (NodeId nn) km)
    host_out = execState (splice hole add (keyMap M.!)) host
@@ -228,6 +240,9 @@ takeOutEdges src = do
   removeFromInList ((_, inport):_) (_,inport') | inport == inport' = error "Wrong in-edge"
   removeFromInList (e:es) r = e:(removeFromInList es r)
 
+to_json :: HugrGraph NodeId -> BS.ByteString
+to_json = encode . serialize
+
 serialize :: forall n. (Ord n, Show n) => HugrGraph n -> Hugr Int
 serialize hugr = renameAndSort (execState (for_ orderEdges addOrderEdge) hugr)
  where
@@ -269,7 +284,7 @@ renameAndSort hugr@(HugrGraph {root, first_children=fc, nodes, parents}) = Hugr
     nodeStackAndIndices :: StackAndIndices n
     nodeStackAndIndices = let just_root = (B0 :< (root, nodes M.! root), M.singleton root 0)
                           in foldl' addNode just_root (first_children root ++ M.keys parents)
-    
+
     addNode :: StackAndIndices n -> n -> StackAndIndices n
     addNode ins n = case M.lookup n (snd ins) of
       (Just _) -> ins
@@ -277,7 +292,7 @@ renameAndSort hugr@(HugrGraph {root, first_children=fc, nodes, parents}) = Hugr
         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 
+            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)
diff --git a/brat/app/Main.hs b/brat/app/Main.hs
index bac393b7..3acaa413 100644
--- a/brat/app/Main.hs
+++ b/brat/app/Main.hs
@@ -1,15 +1,23 @@
 import Brat.Compiler
+import Brat.Machine (runInterpreter)
 
+import qualified Data.ByteString.Lazy as BS (putStr)
+import Data.HugrGraph (to_json)
+
+import Data.Text.Lazy.IO (putStr)
 import Control.Monad (when)
 import Options.Applicative
 
+import Prelude hiding (putStr)
+
 data Options = Opt {
   ast     :: Bool,
   dot     :: String,
   compile :: Bool,
   file    :: String,
   libs    :: String,
-  raw     :: Bool
+  raw     :: Bool,
+  runFunc :: String
 }
 
 compileFlag :: Parser Bool
@@ -23,8 +31,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 +49,10 @@ 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 printDeclsHoles libDirs file
+  else do
+    result <- runInterpreter libDirs file runFunc
+    case result of
+      Right hugr -> BS.putStr (to_json hugr)
+      Left s -> putStr s
diff --git a/brat/brat.cabal b/brat/brat.cabal
index 0cdef59b..f237c89e 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -78,6 +78,7 @@ library
                        Brat.Error,
                        Brat.Graph,
                        Brat.Load,
+                       Brat.Machine,
                        Brat.Parser,
                        Brat.Search,
                        Brat.Elaborator,
@@ -164,11 +165,11 @@ test-suite tests
                        Test.Checking,
                        Test.Compile.Hugr,
                        Test.Elaboration,
+                       Test.Examples,
                        Test.Failure,
                        Test.Graph,
                        Test.HugrGraph,
                        Test.Libs,
-                       Test.Parsing,
                        Test.Naming,
                        Test.Search,
                        Test.Substitution,
diff --git a/brat/examples/adder.brat b/brat/examples/adder.brat
index fc834e4b..ce1ca32a 100644
--- a/brat/examples/adder.brat
+++ b/brat/examples/adder.brat
@@ -49,7 +49,7 @@ fastAdder(n :: #, Vec(Bool, 2^n), Vec(Bool, 2^n), carryIn :: Bool) -> carryOut :
 fastAdder(0, [x], [y], b) = let c, z = fullAdder(x, y, b) in c, [z]
 fastAdder(succ(n), xsh =,= xsl, ysh =,= ysl, b) =
   fastAdder(n, xsh, ysh, true), fastAdder(n, xsh, ysh, false), fastAdder(n, xsl, ysl, b) |>
-  (d1, zsh1, d0, zsh0, c, zsl => if(Bool, c, d1, d0), if(Vec(Bool, succ(full(n))), c, zsh1, zsh0) =,= zsl)
+  (d1, zsh1, d0, zsh0, c, zsl => if(Bool, c, d1, d0), if(!, c, zsh1, zsh0) =,= zsl)
 
 chop(n :: #, Vec(Bool, 2 * n)) -> Vec(Bool, n), Vec(Bool, n)
 chop(n, hi =,= lo) = hi, lo
diff --git a/brat/examples/app.brat b/brat/examples/app.brat
index aa2f64ac..4652034a 100644
--- a/brat/examples/app.brat
+++ b/brat/examples/app.brat
@@ -4,3 +4,16 @@ if(_, false, _, else) = else()
 
 test(Bool) -> Nat
 test(b) = if(Nat, b, { => 4 }, { => 12 })
+
+--!exec [4]
+t :: Nat
+t = test(true)
+
+--This is an 'xfail' as the expected value is clearly/deliberately wrong
+--!exec-xfail [11]
+f :: Nat
+f = test(false)
+
+--!exec [12]
+f' :: Nat
+f' = f
\ No newline at end of file
diff --git a/brat/examples/arith.brat b/brat/examples/arith.brat
index bc190c17..fab2675f 100644
--- a/brat/examples/arith.brat
+++ b/brat/examples/arith.brat
@@ -22,3 +22,48 @@ unary_minus(x) = x + -3.0
 
 unary_minus2(Int) -> Int
 unary_minus2(x) = -2-x
+
+--!exec [7]
+i :: Nat
+i = 3 + 4
+
+--!exec [-9]
+j :: Int
+j = unary_minus2(7)
+
+--!exec [11.13]
+f :: Float
+f = 2.1 * 5.3
+
+--!exec [3.3000000000000003]
+g :: Float
+g = 7.2 - 3.9
+
+inc(Nat) -> Nat
+inc(x) = x + 1
+
+--!exec [14]
+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
+
+--!exec [1]
+ioo :: Nat
+ioo = hoo(2, [1,2,3])
+
+--!exec [[1,2,3]]
+joo :: Vec(Nat, 3)
+joo = [1,2,3]
diff --git a/brat/examples/batcher-merge-sort.brat b/brat/examples/batcher-merge-sort.brat
index f7ec0a63..35385275 100644
--- a/brat/examples/batcher-merge-sort.brat
+++ b/brat/examples/batcher-merge-sort.brat
@@ -26,6 +26,7 @@ merge(succ(n), xs0 =%= xs1, ys0 =%= ys1)
 -- or even:
 -- = merge(n, xs0, ys0) =%= merge(n, xs1, ys1) |>
 --   (zs => fixOffBy1(n, zs))
+-- but the elaborator doesn't synthesize the type of the list before fixOffBy1
 
 
 -- Example of how to write with vectorising `of`
@@ -33,3 +34,16 @@ fixOffBy1(n :: #, Vec(Nat, 2^(n + 1))) -> Vec(Nat, 2^(n + 1))
 fixOffBy1(n, lo ,- (mid0 =%= mid1) -, hi) =
   let mid0', mid1' = (full(n) of cas)(mid0, mid1)
   in  lo ,- (mid0' =%= mid1') -, hi
+
+
+--!exec [[1,2,3,4]]
+test_fix1 :: Vec(Nat, 4)
+test_fix1 = fixOffBy1(1, [1,3,2,4])
+
+--!exec [[2,3,4,5,6,7,8,9,10,11,12,15,16,16,18,19]]
+test_merge :: Vec(Nat, 16)
+test_merge = merge(3, [2,5,7,8,9,15,16,19], [3, 4, 6, 10, 11, 12, 16, 18])
+
+--!exec [[1,5,5,7,9,11,13,15]]
+test_sort :: Vec(Nat, 8)
+test_sort =sort(3, [13,5,11,5,9,15,1,7])
diff --git a/brat/examples/brace-sections.brat b/brat/examples/brace-sections.brat
index 6723c7b6..94e77c4f 100644
--- a/brat/examples/brace-sections.brat
+++ b/brat/examples/brace-sections.brat
@@ -1,4 +1,5 @@
-ext "" add(x :: Int, y :: Int) -> (z :: Int)
+add(x :: Int, y :: Int) -> (z :: Int)
+add(x,y) = x + y
 
 be5 :: { -> Int }
 be5 = { => 5 }
@@ -15,6 +16,10 @@ id = { _ }
 use5 :: { Int -> Int }
 use5 = { _ |> (id,be5); add }
 
+--!exec [9]
+test_use5 :: Int
+test_use5 = use5(4)
+
 add5 :: { Int -> Int }
 add5 = {add(_, 5)}
    --> { '0 => add('0, 5) }
@@ -35,8 +40,10 @@ swap = { snd:_,_ }
 -- be5' :: Int
 -- be5' = be5() --> 5
 
+--!exec [6]
 add5' :: Int
-add5' = add5(1) --> 6
+add5' = add5(1)
 
+--!exec [3]
 add__' :: Int
-add__' = add__(1,2) --> 3
+add__' = add__(1,2)
diff --git a/brat/examples/cons.brat b/brat/examples/cons.brat
index 036bf4ec..a9a10289 100644
--- a/brat/examples/cons.brat
+++ b/brat/examples/cons.brat
@@ -1,4 +1,5 @@
-ext "" add(Int, Int) -> Int
+add(Int, Int) -> Int
+add(x, y) = x + y
 
 copy(Int) -> Int, Int
 copy(x) = x, x
@@ -20,6 +21,7 @@ three :: Int
 three = add(twoThings)
 
 -- Is equivalent to:
+--!exec [3]
 three' :: Int
 three' = let x, y = twoThings in add(x, y)
 
@@ -34,8 +36,9 @@ uncons(cons(x, xs)) = x, xs
 
 -- However, on the right hand side, something that represents the right number
 -- of values can be used as the argument to a cons
-dup(Int) -> List(Int)
-dup(n) = cons(uncons([1,2,3]))
+--!exec [[1,2,3]]
+dup :: List(Int)
+dup = cons(uncons([1,2,3]))
 
 -- Just like a regular function application:
 pair(Int, Int) -> [Int, Int]
diff --git a/brat/examples/fanout.brat b/brat/examples/fanout.brat
index 40bd6477..cbde9b16 100644
--- a/brat/examples/fanout.brat
+++ b/brat/examples/fanout.brat
@@ -1,8 +1,14 @@
+--!xfail-compilation
 open import lib.kernel (CX)
 
 fanout(Vec(Nat, 3)) -> Nat, Nat, Nat
 fanout = { [/\] }
 
+-- note a single Vec output would be [[3,5,7]]
+--!exec [3,5,7]
+test_fanout :: Nat, Nat, Nat
+test_fanout = fanout([3,5,7])
+
 swap(X :: $, Y :: $) -> { X, Y -o Y, X }
 swap(_, _) = { x, y => y, x }
 
diff --git a/brat/examples/hea.brat b/brat/examples/hea.brat
index 22d80e66..36768518 100644
--- a/brat/examples/hea.brat
+++ b/brat/examples/hea.brat
@@ -1,10 +1,11 @@
+--!xfail-checking
 -- Playing with representing a hardware-efficient ansatz
 
 -- Expectation:
 --  - this file parses and typechecks
 
 -- Reality:
---  - the parser is struggling with variables being plugged into the end of vectors
+--  - kernel compilation doesn't find `numNodes` or `Operator`
 
 open import lib.kernel
 
diff --git a/brat/examples/infer.brat b/brat/examples/infer.brat
index f1eaf0bf..b6ec5a2e 100644
--- a/brat/examples/infer.brat
+++ b/brat/examples/infer.brat
@@ -6,48 +6,28 @@ mapVec(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n)
 mapVec(_, _, _, _, []) = []
 mapVec(_, _, f, _, x ,- xs) = f(x) ,- mapVec(!, !, f, !, xs)
 
---map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y)
---map(_, _, _, []) = []
---map(_, _, f, x ,- xs) = f(x) ,- map(!, !, f, xs)
+-- This is needed as a temporary workaround for https://github.com/Quantinuum/brat/issues/109
+inc(Nat) -> Nat
+inc(x) = x + 1
 
---mapVec(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n)
---mapVec(_, _, _, _, []) = []
---mapVec(_, _, f, n, x ,- xs) = f(x) ,- mapVec(!, !, f, !, xs)
+--!exec [[5,7,9]]
+test_mapVec :: Vec(Nat, 3)
+test_mapVec = mapVec(!,!, inc, !, [4,6,8])
 
---length(X :: *, n :: #, Vec(X, n)) -> (m :: #)
---length(_, n, []) = n
---length(_, n, x ,- xs) = n
-
--- The "succ" still being required in both of these cases is https://github.com/CQCL/brat/issues/35
+length(X :: *, n :: #, Vec(X, n)) -> (m :: #)
+length(_, n, []) = n
+length(_, n, x ,- xs) = n
 
 -- While map above can infer the holes from the other arguments,
 -- here we need to infer the holes (arguments) from the results:
--- repeat(X :: *, n :: #, x :: X) -> Vec(X, n)
--- repeat(_, 0, _) = []
--- repeat(_, succ(_), x) = x ,- repeat(!, !, x) -- X can be inferred from x but n cannot
---
--- mapFirst(X :: *, Y :: *, { X -> Y}, n :: #, Vec(X, n)) -> Vec(Y, n)
--- mapFirst(_, _, _, _, []) = []
--- mapFirst(_, _, f, succ(_), x ,- _) = repeat(!, !, f(x)) -- first ! (X) is second _ (Y)
---
--- isfull(n :: #) -> Bool
--- isfull(succ(doub(n))) = isfull(n)
--- isfull(0) = true
--- isfull(_) = false
---
--- hasfulllen(n :: #, Vec(Bool, n)) -> Bool
--- hasfulllen(n, x ,- (xs =,= ys)) = hasfulllen(!, xs)
--- hasfulllen(_, []) = true
--- hasfulllen(_, _) = false
---
--- eatsfull(n :: #, xs :: Vec(Bool, full(n))) -> Nat
--- eatsfull(n, _) = n
--- mkftwo :: Nat
--- mkftwo = eatsfull(!, [false,false,false])
---
--- eatsodd(n :: #, xs :: Vec(Bool, succ(doub(n)))) -> Nat
--- eatsodd(n, _) = n
--- mkotwo' :: Nat
--- mkotwo' = eatsodd(2, [false,false,false,false,false])
--- mkotwo :: Nat
--- mkotwo = eatsodd(!, [false,false,false,false,false])
+repeat(X :: *, n :: #, x :: X) -> Vec(X, n)
+repeat(_, 0, _) = []
+repeat(_, succ(_), x) = x ,- repeat(!, !, x) -- X can be inferred from x but n cannot
+
+mapFirst(X :: *, Y :: *, { X -> Y}, n :: #, Vec(X, n)) -> Vec(Y, n)
+mapFirst(_, _, _, _, []) = []
+mapFirst(_, _, f, succ(_), x ,- _) = repeat(!, !, f(x)) -- first ! (X) is second _ (Y)
+
+--!exec [[5,5,5,5,5]]
+test_mapFirst :: Vec(Nat, 5)
+test_mapFirst = mapFirst(!, !, inc, !, [4,6,7,8,9])
diff --git a/brat/examples/infer2.brat b/brat/examples/infer2.brat
index 421e2eb7..f743f682 100644
--- a/brat/examples/infer2.brat
+++ b/brat/examples/infer2.brat
@@ -1,33 +1,39 @@
--- The "succ" still being required in both of these cases is https://github.com/CQCL/brat/issues/35
-
--- While some cases can infer the holes from the other arguments,
--- here we need to infer the holes (arguments) from the results:
-repeat(X :: *, n :: #, x :: X) -> Vec(X, n)
-repeat(_, 0, _) = []
-repeat(_, succ(_), x) = x ,- repeat(!, !, x) -- X can be inferred from x but n cannot
-
-mapFirst(X :: *, Y :: *, { X -> Y}, n :: #, Vec(X, n)) -> Vec(Y, n)
-mapFirst(_, _, _, _, []) = []
-mapFirst(_, _, f, succ(_), x ,- _) = repeat(!, !, f(x)) -- first ! (X) is second _ (Y)
-
 isfull(n :: #) -> Bool
 isfull(succ(doub(n))) = isfull(n)
 isfull(0) = true
 isfull(_) = false
 
+-- https://github.com/Quantinuum/brat/issues/112
+--!exec-xfail [True]
+is3full :: Bool
+is3full = isfull(3)
+
+-- https://github.com/Quantinuum/brat/issues/112
+--!exec-xfail [True]
+is15full :: Bool
+is15full = isfull(15)
+
+--!exec [False]
+is5full :: Bool
+is5full = isfull(5)
+
 hasfulllen(n :: #, Vec(Bool, n)) -> Bool
 hasfulllen(n, x ,- (xs =,= ys)) = hasfulllen(!, xs)
 hasfulllen(_, []) = true
 hasfulllen(_, _) = false
 
-eatsfull(n :: #, xs :: Vec(Bool, full(n))) -> Nat
-eatsfull(n, _) = n
-mkftwo :: Nat
-mkftwo = eatsfull(!, [false,false,false])
+--!exec [True]
+hasfulllen3 :: Bool
+hasfulllen3 = hasfulllen(!, [false, false, false])
 
 eatsodd(n :: #, xs :: Vec(Bool, succ(doub(n)))) -> Nat
 eatsodd(n, _) = n
+
+--!exec [2]
 mkotwo' :: Nat
 mkotwo' = eatsodd(2, [false,false,false,false,false])
+
+-- https://github.com/Quantinuum/brat/issues/111
+--!exec-xfail [2]
 mkotwo :: Nat
 mkotwo = eatsodd(!, [false,false,false,false,false])
diff --git a/brat/examples/infer_thunks.brat b/brat/examples/infer_thunks.brat
index 1030efc5..c553e841 100644
--- a/brat/examples/infer_thunks.brat
+++ b/brat/examples/infer_thunks.brat
@@ -1,4 +1,4 @@
-ext "to_float" to_float(i :: Int) -> Float
+ext "arith.i2f" to_float(i :: Int) -> Float
 
 id(X :: *, X) -> X
 id(_, x) = x
@@ -7,5 +7,6 @@ map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y)
 map(_, _, _, []) = []
 map(X, Y, f, x ,- xs) = f(x) ,- map(X, Y, f, xs)
 
+--!exec [[5.0]]
 test :: List(Float)
 test = map(!, !, {f => f(5)}, [to_float])
diff --git a/brat/examples/infer_thunks2.brat b/brat/examples/infer_thunks2.brat
index d9006b1a..654af54a 100644
--- a/brat/examples/infer_thunks2.brat
+++ b/brat/examples/infer_thunks2.brat
@@ -1,4 +1,4 @@
-ext "to_float" to_float(i :: Int) -> Float
+ext "arith.i2f" to_float(i :: Int) -> Float
 
 id(X :: *, X) -> X
 id(_, x) = x
@@ -7,5 +7,6 @@ map(X :: *, Y :: *, List(X), { X -> Y }) -> List(Y)
 map(_, _, [], _) = []
 map(X, Y, x ,- xs, f) = f(x) ,- map(X, Y, xs, f)
 
+--!exec [[5.0]]
 test :: List(Float)
 test = map(!, !, [to_float], {f => f(5)})
diff --git a/brat/examples/karlheinz.brat b/brat/examples/karlheinz.brat
index f4a9fbf1..52aff05f 100644
--- a/brat/examples/karlheinz.brat
+++ b/brat/examples/karlheinz.brat
@@ -1,3 +1,4 @@
+--!xfail-checking
 -- This file contains type signatures for various operations laid out in the
 -- "Types for Composite Experiments" Confluence page
 
diff --git a/brat/examples/karlheinz_alias.brat b/brat/examples/karlheinz_alias.brat
deleted file mode 100644
index bb3f07dd..00000000
--- a/brat/examples/karlheinz_alias.brat
+++ /dev/null
@@ -1,20 +0,0 @@
--- This is a subset of the karlheinz.brat test file
-
--- Expectation:
---  - The type of the input to exp expands to
---       `{ Vec Qubit 2 -o Vec Bool 2 }`
---  - The type of the input to execute expands to
---       `{Vec Qubit 2 -o Vec Bool 1}`
-
--- Reality:
---  - Type checking fails, as currently arguments to type aliases must all be of kind '*' (these are '#')
-
-type Dist = List(Bool)
-type KCirc(q, b) = { Vec(Qubit, q) -o Vec(Bool, b) }
-type PCirc(q) = { Vec(Qubit, q) -o Vec(Bool, q) }
-
-exp(PCirc(2)) -> Dist
-exp = ?exp
-
-execute(KCirc(2, 1)) -> Dist
-execute = ?a
diff --git a/brat/examples/kernel.brat b/brat/examples/kernel.brat
index 4897e84e..0d894fed 100644
--- a/brat/examples/kernel.brat
+++ b/brat/examples/kernel.brat
@@ -9,8 +9,12 @@ H = ?und
 Rz(th :: Float)-> {a::Qubit -o b::Qubit}
 Rz = ?rz
 
-pba(Float)-> {c :: Qubit,d::Qubit -o c::Qubit,d::Qubit}
+pba(Float) -> {c :: Qubit,d::Qubit -o c::Qubit,d::Qubit}
 pba = th => { x, y => (lib.kernel.H, |)(x, y) }
 
+--!exec-hugr
+test_pba(Qubit, Qubit) -o Qubit, Qubit
+test_pba = pba(0.314)
+
 th :: {Bool -> Bool}
 th = ?th
diff --git a/brat/examples/klet.brat b/brat/examples/klet.brat
index efacae76..251817bb 100644
--- a/brat/examples/klet.brat
+++ b/brat/examples/klet.brat
@@ -1,3 +1,4 @@
+--!xfail-compilation
 import lib.kernel
 
 id ::  { Qubit -o Qubit }
diff --git a/brat/examples/magic-state-distillation.brat b/brat/examples/magic-state-distillation.brat
index 069551c0..1029aa28 100644
--- a/brat/examples/magic-state-distillation.brat
+++ b/brat/examples/magic-state-distillation.brat
@@ -1,3 +1,4 @@
+--!xfail-compilation
 open import lib.functional
 open import lib.kernel
 open import lib.math
diff --git a/brat/examples/map.brat b/brat/examples/map.brat
deleted file mode 100644
index db7b558d..00000000
--- a/brat/examples/map.brat
+++ /dev/null
@@ -1,3 +0,0 @@
-map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y)
-map(_, _, _, []) = []
-map(_, _, f, x ,- xs) = f(x) ,- map(!, !, f, xs)
diff --git a/brat/examples/nested-abstractors.brat b/brat/examples/nested-abstractors.brat
index 199de4bb..422f69b2 100644
--- a/brat/examples/nested-abstractors.brat
+++ b/brat/examples/nested-abstractors.brat
@@ -1,3 +1,4 @@
+--!xfail-checking
 -- We expect that these examples should typecheck, but the machinery for dealing
 -- with nested rows is severly underdeveloped.
 
diff --git a/brat/examples/qft.brat b/brat/examples/qft.brat
index 99bf0a31..641bfb0f 100644
--- a/brat/examples/qft.brat
+++ b/brat/examples/qft.brat
@@ -29,3 +29,7 @@ qft(succ(n)) = {
     |, qft(n);
     recons(n)
 }
+
+--!exec-hugr
+test_qft(Vec(Qubit, 5)) -o Vec(Qubit, 5)
+test_qft = qft(5)
diff --git a/brat/examples/repeated_app.brat b/brat/examples/repeated_app.brat
index d0ba0aca..ab519079 100644
--- a/brat/examples/repeated_app.brat
+++ b/brat/examples/repeated_app.brat
@@ -1,3 +1,4 @@
+--!xfail-checking
 id(X::*) -> { X -> X }
 id(_) = {x => x}
 
diff --git a/brat/examples/thin.brat b/brat/examples/thin.brat
index 94ff57b9..92c99e46 100644
--- a/brat/examples/thin.brat
+++ b/brat/examples/thin.brat
@@ -1,3 +1,4 @@
+--!xfail-parsing
 -- Experiments with selecting out of vectors with first class selections
 -- This feature has fallen by the wayside, so expect this to fail
 
diff --git a/brat/examples/vectorise.brat b/brat/examples/vectorise.brat
index 2d8be07e..efa421aa 100644
--- a/brat/examples/vectorise.brat
+++ b/brat/examples/vectorise.brat
@@ -15,6 +15,10 @@ zip(X, Y, n, xs, ys) =
  xs, ys |>
  (n of ({[_,_]} :: { X, Y -> [X,Y] }))
 
+--!exec [[["yes",True],["no",False],["true",True],["false",False]]]
+test_zip :: Vec([String, Bool], 4)
+test_zip = zip(!, !, !, ["yes","no","true","false"], [true,false,true,false])
+
 mkPair(X :: *, Y :: *) -> { X, Y -> [X, Y] }
 mkPair(_, _) = { x, y => [x,y] }
 
@@ -30,6 +34,15 @@ rank2(X :: *, Y :: *, Z :: *,
 --rank2(_, _, _, n, m, fstArgs, sndArgs, f) = fstArgs, sndArgs |> m of n of f
 rank2(_, _, _, n, m, fstArgs, sndArgs, f) = (m of n of f)(fstArgs, sndArgs)
 
+leq(Nat, Nat) -> Bool
+leq(0, _) = true
+leq(_, 0) = false
+leq(succ(l), succ(n)) = leq(l, n)
+
+--!exec [[[True,False,True],[True,False,True]]]
+test_rank2 :: Vec(Vec(Bool, 3), 2)
+test_rank2 = rank2(!, !, !, !, !, [[1, 2, 3], [4, 5, 6]], [[2, 1, 3], [5, 4, 6]], leq)
+
 f(X :: *, n :: #, Vec(X, n)) -> Vec(X, 2 * n)
 f(X, 0, []) = []
 f(X, succ(n), x ,- xs) = x ,- x ,- f(X, n, xs)
@@ -54,3 +67,14 @@ juxt = 42 of 1, 42 of true
 
 notTooGreedy(Vec(Nat, 42)) -> Vec(Nat, 42), Vec(Nat, 42)
 notTooGreedy(xs) = 42 of 0, xs
+
+addN(Nat) -> { Nat -> Nat }
+addN(n) = { x => x + n }
+
+adders(n :: #) -> Vec({ Nat -> Nat }, n)
+adders(0) = []
+adders(succ(n)) = adders(n) -, addN(succ(n))
+
+--!exec [[1,2,3,4,5]]
+test_adders :: Vec(Nat, 5)
+test_adders = adders(5)(5 of 0)
diff --git a/brat/stack.yaml b/brat/stack.yaml
index e91924ad..4b390fa7 100644
--- a/brat/stack.yaml
+++ b/brat/stack.yaml
@@ -7,3 +7,4 @@ packages:
 
 extra-deps:
 - partial-order-0.2.0.0@sha256:a0d6ddc9ebcfa965a5cbcff1d06d46a79d44ea5a0335c583c2a51bcb41334487,2275
+- tasty-1.5@sha256:8da3f47fff790714f7d676692f1207aac156b41f705c55f14d1d8147a751264b,2787
diff --git a/brat/test/Main.hs b/brat/test/Main.hs
index f91033f6..3e0fda2b 100644
--- a/brat/test/Main.hs
+++ b/brat/test/Main.hs
@@ -2,15 +2,13 @@ import Test.Tasty  (testGroup)
 import Test.Tasty.Silver.Interactive (defaultMain)
 
 import Test.Abstractor
-import Test.Checking
+import Test.Examples
 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
 import Test.Search
 import Test.Substitution
 import Test.Syntax.Let
@@ -24,7 +22,7 @@ import Brat.QualName
 import Brat.Error
 import Control.Monad.Freer
 import qualified Data.Set as S
-import Debug.Trace
+--import Debug.Trace
 import Test.Util
 import Test.Tasty.HUnit (testCase)
 
@@ -38,7 +36,7 @@ coroT1 = do
           Nothing -> defineEnd "test" e (VCon (PrefixName [] "nil") [])
       )
   mkYield "coroT1" (S.singleton e) >> pure ()
-  traceM "Yield continued"
+  --traceM "Yield continued"
   v <- req $ ELup e
   case v of
     Just _ -> pure ()
@@ -61,9 +59,7 @@ coroT2 = do
 
 main = do
   failureTests  <- getFailureTests
-  checkingTests <- getCheckingTests
-  parsingTests <- getParsingTests
-  compilationTests <- setupCompilationTests
+  examplesTests <- getExamplesTests
   graphTests <- getGraphTests
   spliceTests <- getSpliceTests
   let coroTests = testGroup "coroutine"
@@ -72,16 +68,14 @@ main = do
        ]
   defaultMain $ testGroup "All" [graphTests
                                 ,failureTests
-                                ,checkingTests
+                                ,examplesTests
                                 ,letTests
                                 ,libDirTests
                                 ,nameTests
-                                ,parsingTests
                                 ,searchTests
                                 ,elaborationTests
                                 ,substitutionTests
                                 ,abstractorTests
-                                ,compilationTests
                                 ,typeArithTests
                                 ,coroTests
                                 ,spliceTests
diff --git a/brat/test/Test/Checking.hs b/brat/test/Test/Checking.hs
index d76fd07c..ddd7e77f 100644
--- a/brat/test/Test/Checking.hs
+++ b/brat/test/Test/Checking.hs
@@ -1,33 +1,17 @@
-module Test.Checking (parseAndCheck, getCheckingTests, expectedCheckingFails) where
+module Test.Checking (parseAndCheck, parseAndCheckNamed) where
 
 import Brat.Load
 import Brat.Naming (root)
-import Test.Parsing (expectedParsingFails)
-import Test.Util (expectFailForPaths)
 
 import Control.Monad.Except
-import System.FilePath
 import Test.Tasty
 import Test.Tasty.HUnit
-import Test.Tasty.Silver
-
-expectedCheckingFails = map ("examples" </>) ["nested-abstractors.brat"
-                                             ,"karlheinz.brat"
-                                             ,"karlheinz_alias.brat"
-                                             ,"hea.brat"
-                                             -- https://github.com/Quantinuum/brat/issues/92
-                                             ,"repeated_app.brat"
-                                             ,"adder.brat"
-                                             ]
-
-parseAndCheckXF :: [FilePath] -> [TestTree]
-parseAndCheckXF = expectFailForPaths (expectedParsingFails ++ expectedCheckingFails) (parseAndCheck [])
-
-getCheckingTests :: IO TestTree
-getCheckingTests = testGroup "checking" . parseAndCheckXF <$> findByExtension [".brat"] "examples"
 
 parseAndCheck :: [FilePath] -> FilePath -> TestTree
-parseAndCheck libDirs file = testCase (show file) $ do
+parseAndCheck libDirs file = parseAndCheckNamed (show file) libDirs file
+
+parseAndCheckNamed :: String -> [FilePath] -> FilePath -> TestTree
+parseAndCheckNamed name libDirs file = testCase name $ do
   env <- runExceptT $ loadFilename root libDirs file
   case env of
     Left err -> assertFailure (show err)
diff --git a/brat/test/Test/Compile/Hugr.hs b/brat/test/Test/Compile/Hugr.hs
index 842ec42f..1551f85c 100644
--- a/brat/test/Test/Compile/Hugr.hs
+++ b/brat/test/Test/Compile/Hugr.hs
@@ -1,76 +1,35 @@
-module Test.Compile.Hugr where
-
-import Brat.Compiler (compileFile, CompilingHoles(..))
-import Test.Checking (expectedCheckingFails)
-import Test.Parsing (expectedParsingFails)
-import Test.Util (expectFailForPaths)
+module Test.Compile.Hugr (compileToOutput, getHoles) where
 
+import Control.Monad (forM)
+import qualified Data.Map as M
 import qualified Data.ByteString as BS
 import System.Directory (createDirectoryIfMissing)
 import System.FilePath
 import Test.Tasty
 import Test.Tasty.HUnit
-import Test.Tasty.Silver
+
+import Data.Hugr (isHole)
+import Data.HugrGraph (to_json, getOp, HugrGraph, getNodes)
+import Data.List (sort)
+import Data.Maybe (isJust)
+import Brat.Compiler (compileFile, CompilingHoles(..))
 
 prefix = "test/compilation"
-examplesPrefix = "examples"
 outputDir = prefix </> "output"
 
--- examples that we expect to compile, but then to fail validation
-invalidExamples :: [FilePath]
-invalidExamples = (map ((++ ".brat") . ("examples" </>))
-  ["app"
-  --,"adder" -- not even checking yet
-  ,"dollar_kind"
-  ,"portpulling"
-  ,"eatsfull" -- Compiling hopes #96
-  ,"map" -- Compiling hopes #96
-  ,"infer_thunks" -- Weird: Mismatch between caller and callee signatures in map call
-  ,"infer_thunks2" -- Weird: Mismatch between caller and callee signatures in map call
-  --,"repeated_app" -- not checking yet, but will be missing coercions, https://github.com/quantinuum-dev/brat/issues/413
-  ]
-  )
-
--- 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"
-  ,"let"
-  ,"patterns"
-  ,"qft"
-  ,"infer" -- problems with undoing pattern tests
-  ,"infer2" -- problems with undoing pattern tests
-  ,"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
-  -- Victims of #13
-  ,"arith"
-  ,"klet"
-  ,"magic-state-distillation" -- also makes selectors
-  ]
-
--- This is https://github.com/Quantinuum/brat/issues/101
-nonCompilingTests = ["test/compilation/closures.brat"]
-
-compileToOutput :: FilePath -> TestTree
-compileToOutput file = testCaseInfo (show file) $ compileFile [] file >>= \case
-    Right hugr_bytes -> do
-          let outputExt = if file `elem` invalidExamples then "json.invalid" else "json"
-          let outFile = outputDir </> replaceExtension (takeFileName file) outputExt
-          -- lots of fun with lazy and even strict bytestrings
-          -- returning many bytes before evaluation has completed
-          BS.writeFile outFile $! (BS.toStrict hugr_bytes)
-          pure $ "Written to " ++ outFile ++ " pending validation\n"
-    Left (CompilingHoles _) -> pure "Skipped as contains holes"
-
-setupCompilationTests :: IO TestTree
-setupCompilationTests = do
-  tests <- findByExtension [".brat"] prefix
-  examples <- findByExtension [".brat"] examplesPrefix
-  createDirectoryIfMissing False outputDir
-  let compileTests = expectFailForPaths nonCompilingTests compileToOutput tests
-  let examplesTests = testGroup "examples" $ expectFailForPaths nonCompilingExamples compileToOutput examples
-
-  pure $ testGroup "compilation" (examplesTests:compileTests)
+compileToOutput :: String -> FilePath -> TestTree
+compileToOutput name file = testCaseInfo name $ do
+    createDirectoryIfMissing False outputDir
+    compileFile [] file >>= \case
+        Right hs -> mconcat <$> (forM (M.toList hs) $ \(boxName, (hugr, holes)) -> do
+            sort (getHoles hugr) @?= sort holes
+            -- ignore splices for now
+            let outFile = outputDir </> replaceExtension (takeFileName file) ((show boxName) ++ ".json")
+            -- lots of fun with lazy and even strict bytestrings
+            -- returning many bytes before evaluation has completed
+            BS.writeFile outFile $! (BS.toStrict $ to_json hugr)
+            pure $ "Written to " ++ outFile ++ " pending validation\n")
+        Left (CompilingHoles _) -> pure "Skipped as contains holes"
+
+getHoles :: Ord a => HugrGraph a -> [a]
+getHoles hg = [n | n <- getNodes hg, isJust (isHole $ getOp hg n)]
\ No newline at end of file
diff --git a/brat/test/Test/Examples.hs b/brat/test/Test/Examples.hs
new file mode 100644
index 00000000..41c547ff
--- /dev/null
+++ b/brat/test/Test/Examples.hs
@@ -0,0 +1,87 @@
+module Test.Examples (getExamplesTests) where
+
+import Test.Checking (parseAndCheckNamed)
+import Test.Compile.Hugr (compileToOutput, getHoles)
+import Brat.Load (parseFile)
+import Brat.Machine (runInterpreter)
+import Data.HugrGraph (to_json)
+
+import qualified Data.ByteString as BS
+import Data.Char (isAlphaNum)
+import Data.Functor ((<&>))
+import Data.List (isPrefixOf)
+import qualified Data.Text.Lazy as T
+import Data.Maybe (fromJust)
+import System.Directory (createDirectoryIfMissing)
+import System.FilePath
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.Silver
+import Test.Tasty.ExpectedFailure
+
+--import Debug.Trace
+
+outputDir :: FilePath
+outputDir = "test" </> "examples"
+
+execTestPrefix :: T.Text
+execTestPrefix = T.pack "--!exec"
+
+interpreterOutputPrefix :: String
+interpreterOutputPrefix = "Finished "
+
+getExamplesTests :: IO TestTree
+getExamplesTests =  do
+  paths <- findByExtension [".brat"] "examples"
+  testGroup "examples" <$> mapM mkTest paths
+ where
+  mkTest :: FilePath -> IO TestTree
+  mkTest path = readFile path <&> \cts ->
+    let parseTest = testCase "parsing" $ do
+          case parseFile path cts of
+            Left err -> assertFailure (show err)
+            Right _ -> return () -- OK
+        checkTest = parseAndCheckNamed "checking" [] path
+    in if isPrefixOf "--!xfail-parsing" cts then
+         testGroup (show path) [expectFail parseTest]
+       else if isPrefixOf "--!xfail-checking" cts then
+         testGroup (show path) [parseTest, expectFail checkTest]
+       else
+        let interpreterTests = T.breakOnAll execTestPrefix (T.pack cts) <&> \(_, start) ->
+              let (testLine, newlineDefn) = T.breakOn (T.pack "\n") start
+                  -- this repeats/roughly duplicates the logic for "identifiers" in the parser
+                  func_name = T.unpack $ T.takeWhile (\c -> isAlphaNum c || c == '_' || c == '\'') (T.drop 1 newlineDefn)
+                  -- testLine begins with execTestPrefix, then either
+                  -- " " and the expected result
+                  -- "-xfail " and the (un-)expected result
+                  -- "-hugr\n" (checks no splices, outputs hugr for validation)
+                  restLine = fromJust $ T.stripPrefix execTestPrefix testLine
+              in if (T.pack "-hugr") == restLine then testCaseInfo func_name $ do
+                let outFile = outputDir </> dropExtension (takeFileName path) ++ "_" ++ func_name <.> "json"
+                -- this completely recompiles the file for each test, which is pretty bad
+                hugr <- runInterpreter [] path func_name >>= \case
+                  Left s -> assertFailure $ "Expected hugr, got " ++ T.unpack s
+                  Right hugr -> pure hugr
+                getHoles hugr @?= []
+                -- output the hugr for validation
+                createDirectoryIfMissing False outputDir
+                BS.writeFile outFile $! (BS.toStrict $ to_json hugr)
+                pure $ "Written hugr to " ++ outFile ++ " pending validation"
+              else
+                let (is_xfail, eOut) = case T.stripPrefix (T.pack "-xfail ") restLine of
+                      Just out -> (True, out)
+                      Nothing | Just out <- T.stripPrefix (T.pack " ") restLine -> (False, out)
+                              | otherwise -> error $ "Invalid exec test line: " ++ T.unpack testLine
+                    expectedOutput = interpreterOutputPrefix ++ T.unpack (T.strip eOut)
+                in (if is_xfail then expectFail else id) $ testCase func_name $ do
+                  -- this completely recompiles the file for each test, which is pretty bad
+                  runInterpreter [] path func_name >>= \case
+                    Left t -> T.unpack t @?= expectedOutput
+                    Right _ -> assertFailure $ "Expected output: '" ++ expectedOutput ++ "' but got a hugr!"
+            compileTest = compileToOutput "compilation" path
+            checkAndCompile = if isPrefixOf "--!xfail-compilation" cts
+              then [checkTest, expectFail compileTest] else [compileTest]
+        in case interpreterTests of
+          [] -> testGroup (show path) checkAndCompile
+          intTests -> sequentialTestGroup path AllSucceed
+              (checkAndCompile ++ [testGroup "execution" intTests])
diff --git a/brat/test/Test/HugrGraph.hs b/brat/test/Test/HugrGraph.hs
index a9d93953..7e4ef08e 100644
--- a/brat/test/Test/HugrGraph.hs
+++ b/brat/test/Test/HugrGraph.hs
@@ -49,7 +49,7 @@ testSplice inline prepend = testCaseInfo name $ do
   name = (if inline then "inline" else "noinline") ++ (if prepend then "_prepend" else "_new")
   host :: (NodeId, (HugrGraph NodeId, Namespace))
   host = flip runState (runState (H.new "root" rootDefn) N.root) $ do
-    root <- get <&> H.root . fst
+    root <- get <&> H.getRoot . fst
     input <- addNode "inp" root (OpIn (InputNode tys []))
     output <- addNode "out" root (OpOut (OutputNode tys []))
     jh $setFirstChildren root [input, output]
@@ -63,7 +63,7 @@ testSplice inline prepend = testCaseInfo name $ do
   dfgHugr =
    let (initHugr, ns) = runState (H.new "root" rootDfg) N.root
    in fst $ flip execState (initHugr, ns) $ do
-    root <- get <&> H.root . fst
+    root <- get <&> H.getRoot . fst
     input <- addNode "inp" root (OpIn (InputNode tys []))
     output <- addNode "out" root (OpOut (OutputNode tys []))
     jh $ setFirstChildren root [input, output]
diff --git a/brat/test/Test/Parsing.hs b/brat/test/Test/Parsing.hs
deleted file mode 100644
index efe6afc8..00000000
--- a/brat/test/Test/Parsing.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-module Test.Parsing (getParsingTests, expectedParsingFails) where
-
-import Brat.Load
-
-import System.FilePath
-import Test.Tasty
-import Test.Tasty.HUnit
-import Test.Tasty.Silver
-import Test.Util (expectFailForPaths)
-
-testParse :: FilePath -> TestTree
-testParse file = testCase (show file) $ do
-  cts <- readFile file
-  case parseFile file cts of
-    Left err -> assertFailure (show err)
-    Right _ -> return () -- OK
-
-expectedParsingFails = ["examples" </> "thin.brat"]
-
-parseXF = expectFailForPaths expectedParsingFails testParse
-
-getParsingTests :: IO TestTree
-getParsingTests = testGroup "parsing" . parseXF <$> findByExtension [".brat"] "examples"
diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph
index ef921c7b..7dc26783 100644
--- a/brat/test/golden/graph/cons.brat.graph
+++ b/brat/test/golden/graph/cons.brat.graph
@@ -1,22 +1,26 @@
 Nodes:
+(cons.brat_check_defs_1_three_2_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(cons.brat_check_defs_1_three_2_$rhs_check'Con_const_3,BratNode (Const 0) [] [("value",Int)])
+(cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
+(cons.brat_check_defs_1_three_2_$rhs_check'Con_const_4,BratNode (Const 0) [] [("value",Int)])
 (cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
+(cons.brat_check_defs_1_two_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (cons.brat_check_defs_1_two_$rhs_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (cons.brat_check_defs_1_two_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_check'Con_4_nil_2,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
-(cons.brat_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))])
-(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_const_3,BratNode (Const 2) [] [("value",Int)])
-(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
-(cons.brat_check_defs_1_two_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
-(cons.brat_check_defs_1_two_$rhs_check'Con_const_3,BratNode (Const 1) [] [("value",Int)])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_nil_3,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(cons.brat_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))])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_const_4,BratNode (Const 2) [] [("value",Int)])
+(cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
+(cons.brat_check_defs_1_two_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
+(cons.brat_check_defs_1_two_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
 (cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
 (cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
@@ -30,17 +34,21 @@ Nodes:
 (cons.brat_globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_2 0,Vec(Int, 3),In cons.brat_globals_decl_9_three 0)
-(Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_const_3 0,Int,In cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_2 0)
+(Ex cons.brat_check_defs_1_three_2_$rhs_check'Con__2 0,[],In cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_pat2val 0)
+(Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_3 0,Vec(Int, 3),In cons.brat_globals_decl_9_three 0)
+(Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_const_4 0,Int,In cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_3 0)
 (Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_numpat2val_1 0)
 (Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In cons.brat_check_defs_1_three_2_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 1)
-(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_check'Con_4_nil_2 0,Vec(Int, 0),In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2 0,Vec(Int, 1),In cons.brat_check_defs_1_two_$rhs_check'Con_cons_2 1)
-(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_const_3 0,Int,In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_typeEqsTail_1_buildConst_1 0,Nat,In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_4_$!_numpat2val_1 0)
-(Ex cons.brat_check_defs_1_two_$rhs_check'Con_cons_2 0,Vec(Int, 2),In cons.brat_globals_decl_4_two 0)
-(Ex cons.brat_check_defs_1_two_$rhs_check'Con_const_3 0,Int,In cons.brat_check_defs_1_two_$rhs_check'Con_cons_2 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con__2 0,[],In cons.brat_check_defs_1_two_$rhs_check'Con_$!_pat2val 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5__2 0,[],In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5__2 0,[],In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_check'Con_5_nil_3 0,Vec(Int, 0),In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3 0,Vec(Int, 1),In cons.brat_check_defs_1_two_$rhs_check'Con_cons_3 1)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_const_4 0,Int,In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_typeEqsTail_1_buildConst_1 0,Nat,In cons.brat_check_defs_1_two_$rhs_check'Con_check'Con_5_$!_numpat2val_1 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_cons_3 0,Vec(Int, 2),In cons.brat_globals_decl_4_two 0)
+(Ex cons.brat_check_defs_1_two_$rhs_check'Con_const_4 0,Int,In cons.brat_check_defs_1_two_$rhs_check'Con_cons_3 0)
 (Ex cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In cons.brat_check_defs_1_two_$rhs_check'Con_$!_numpat2val_1 0)
 (Ex cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In cons.brat_check_defs_1_two_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 1)
@@ -50,4 +58,4 @@ Wires:
 (Ex cons.brat_globals_Vec_6 0,[],In cons.brat_globals___kca_three_5 0)
 (Ex cons.brat_globals_const_3 0,Nat,In cons.brat_globals_Vec_1 1)
 (Ex cons.brat_globals_const_8 0,Nat,In cons.brat_globals_Vec_6 1)
-(Ex cons.brat_globals_decl_4_two 0,Vec(Int, 2),In cons.brat_check_defs_1_three_2_$rhs_check'Con_cons_2 1)
+(Ex cons.brat_globals_decl_4_two 0,Vec(Int, 2),In cons.brat_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 e71d4ba0..130eb5b5 100644
--- a/brat/test/golden/graph/kernel.brat.graph
+++ b/brat/test/golden/graph/kernel.brat.graph
@@ -2,21 +2,25 @@ Nodes:
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] [])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_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)) })])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2,BratNode (Dummy $) [] [("dummy",[])])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(kernel.brat_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)])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(kernel.brat_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 [("",[])] [("",[])])
-(kernel.brat_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))])
-(kernel.brat_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))])
-(kernel.brat_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)])
-(kernel.brat_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))])
-(kernel.brat_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)])
-(kernel.brat_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)])
-(kernel.brat_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)])
-(kernel.brat_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))])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5__2,BratNode (Dummy $) [] [("dummy",[])])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(kernel.brat_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",[])])
+(kernel.brat_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)])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(kernel.brat_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",[])])
+(kernel.brat_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 [("",[])] [("",[])])
+(kernel.brat_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))])
+(kernel.brat_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))])
+(kernel.brat_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)])
+(kernel.brat_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))])
+(kernel.brat_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)])
+(kernel.brat_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)])
+(kernel.brat_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)])
+(kernel.brat_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))])
 (kernel.brat_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)])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (kernel.brat_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:
 (kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_cons_2 1)
-(Ex kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2 1)
-(Ex kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_$!_numpat2val_1 0)
-(Ex kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2 0,Vec(Qubit, 3),In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0)
+(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2 0,[],In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val 0)
+(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5__2 0,[],In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_pat2val 0)
+(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5__2 0,[],In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_cons_3 1)
+(Ex kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3 1)
+(Ex kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_$!_numpat2val_1 0)
+(Ex kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3 0,Vec(Qubit, 3),In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1 0)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_Add_1 1)
-(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_2 0)
-(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 1,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_4_cons_2 0)
-(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 2,Qubit,In kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_cons_3 0)
+(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 1,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_check'Con_5_cons_3 0)
+(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 2,Qubit,In kernel.brat_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 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0,Vec(Qubit, 3),In kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1 0)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 0,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 1,Qubit,In kernel.brat_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 825abd27..5b7fb356 100644
--- a/brat/test/golden/graph/list.brat.graph
+++ b/brat/test/golden/graph/list.brat.graph
@@ -1,26 +1,34 @@
 Nodes:
+(list.brat_check_defs_1_xs_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (list.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2,BratNode (Constructor nil) [] [("value",List(Int))])
-(list.brat_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))])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3,BratNode (Const 3) [] [("value",Int)])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3,BratNode (Const 2) [] [("value",Int)])
-(list.brat_check_defs_1_xs_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(list.brat_check_defs_1_xs_$rhs_check'Con_const_3,BratNode (Const 1) [] [("value",Int)])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3,BratNode (Constructor nil) [] [("value",List(Int))])
+(list.brat_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))])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4,BratNode (Const 3) [] [("value",Int)])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4,BratNode (Const 2) [] [("value",Int)])
+(list.brat_check_defs_1_xs_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(list.brat_check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
 (list.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (list.brat_globals_List_1,BratNode (Constructor List) [("listValue",[])] [("value",[])])
 (list.brat_globals_decl_3_xs,BratNode Id [("a1",List(Int))] [("a1",List(Int))])
 
 Wires:
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2 0,List(Int),In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 1)
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0,List(Int),In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3 0,Int,In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0)
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0,List(Int),In list.brat_check_defs_1_xs_$rhs_check'Con_cons_2 1)
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3 0,Int,In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_cons_2 0,List(Int),In list.brat_globals_decl_3_xs 0)
-(Ex list.brat_check_defs_1_xs_$rhs_check'Con_const_3 0,Int,In list.brat_check_defs_1_xs_$rhs_check'Con_cons_2 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3 0,List(Int),In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 1)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0,List(Int),In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4 0,Int,In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0,List(Int),In list.brat_check_defs_1_xs_$rhs_check'Con_cons_3 1)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4 0,Int,In list.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_cons_3 0,List(Int),In list.brat_globals_decl_3_xs 0)
+(Ex list.brat_check_defs_1_xs_$rhs_check'Con_const_4 0,Int,In list.brat_check_defs_1_xs_$rhs_check'Con_cons_3 0)
 (Ex list.brat_globals_Int_2 0,[],In list.brat_globals_List_1 0)
 (Ex list.brat_globals_List_1 0,[],In list.brat_globals___kca_xs 0)
diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph
index 1d06715a..7ac1db68 100644
--- a/brat/test/golden/graph/pair.brat.graph
+++ b/brat/test/golden/graph/pair.brat.graph
@@ -1,13 +1,17 @@
 Nodes:
+(pair.brat_check_defs_1_xs_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (pair.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
 (pair.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val_1,BratNode Id [("",[])] [("",[])])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val_1,BratNode Id [("",[])] [("",[])])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_3_true_1,BratNode (Constructor true) [] [("value",Bool)])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_nil_1,BratNode (Constructor nil) [] [("value",[])])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2,BratNode (Constructor cons) [("head",Bool),("tail",[])] [("value",[Bool])])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",[Bool])] [("value",[Int,Bool])])
-(pair.brat_check_defs_1_xs_$rhs_check'Con_const_3,BratNode (Const 1) [] [("value",Int)])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val_1,BratNode Id [("",[])] [("",[])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_4_true_1,BratNode (Constructor true) [] [("value",Bool)])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_nil_1,BratNode (Constructor nil) [] [("value",[])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3,BratNode (Constructor cons) [("head",Bool),("tail",[])] [("value",[Bool])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1__1,BratNode (Dummy *) [] [("dummy",[])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",[Bool])] [("value",[Int,Bool])])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
+(pair.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1__1,BratNode (Dummy *) [] [("dummy",[])])
 (pair.brat_globals_Bool_4,BratNode (Constructor Bool) [] [("value",[])])
 (pair.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (pair.brat_globals_cons_1,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])])
@@ -16,11 +20,15 @@ Nodes:
 (pair.brat_globals_nil_5,BratNode (Constructor nil) [] [("value",[])])
 
 Wires:
-(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_3_true_1 0,Bool,In pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_nil_1 0,[],In pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0,[Bool],In pair.brat_check_defs_1_xs_$rhs_check'Con_cons_2 1)
-(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_cons_2 0,[Int,Bool],In pair.brat_globals_decl_6_xs 0)
-(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_const_3 0,Int,In pair.brat_check_defs_1_xs_$rhs_check'Con_cons_2 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In pair.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5__2 0,[],In pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_4_true_1 0,Bool,In pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_nil_1 0,[],In pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0,[Bool],In pair.brat_check_defs_1_xs_$rhs_check'Con_cons_3 1)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1__1 0,[],In pair.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val_1 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_cons_3 0,[Int,Bool],In pair.brat_globals_decl_6_xs 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_const_4 0,Int,In pair.brat_check_defs_1_xs_$rhs_check'Con_cons_3 0)
+(Ex pair.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1__1 0,[],In pair.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val_1 0)
 (Ex pair.brat_globals_Bool_4 0,[],In pair.brat_globals_cons_3 0)
 (Ex pair.brat_globals_Int_2 0,[],In pair.brat_globals_cons_1 0)
 (Ex pair.brat_globals_cons_1 0,[],In pair.brat_globals___kca_xs 0)
diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph
index 47ae2434..301605ea 100644
--- a/brat/test/golden/graph/vec.brat.graph
+++ b/brat/test/golden/graph/vec.brat.graph
@@ -1,22 +1,26 @@
 Nodes:
+(vec.brat_check_defs_1_xs_$rhs_check'Con__2,BratNode (Dummy *) [] [("dummy",[])])
 (vec.brat_check_defs_1_xs_$rhs_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (vec.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_$!_pat2val,BratNode Id [("",[])] [("",[])])
-(vec.brat_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))])
-(vec.brat_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))])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3,BratNode (Const 2) [] [("value",Int)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
-(vec.brat_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))])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3,BratNode (Const 1) [] [("value",Int)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(vec.brat_check_defs_1_xs_$rhs_check'Con_const_3,BratNode (Const 0) [] [("value",Int)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2,BratNode (Dummy *) [] [("dummy",[])])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val,BratNode Id [("",[])] [("",[])])
+(vec.brat_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))])
+(vec.brat_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))])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4,BratNode (Const 2) [] [("value",Int)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_typeEqsTail_1_buildConst_1,BratNode (Const 0) [] [("value",Nat)])
+(vec.brat_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))])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4,BratNode (Const 1) [] [("value",Int)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst,BratNode (Const 1) [] [("value",Nat)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_cons_3,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
+(vec.brat_check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 0) [] [("value",Int)])
 (vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
 (vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
@@ -26,17 +30,21 @@ Nodes:
 (vec.brat_globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_check'Con_4_nil_2 0,Vec(Int, 0),In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 1)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0,Vec(Int, 1),In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 1)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_const_3 0,Int,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_cons_2 0)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_typeEqsTail_1_buildConst_1 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_check'Con_4_$!_numpat2val_1 0)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0,Vec(Int, 2),In vec.brat_check_defs_1_xs_$rhs_check'Con_cons_2 1)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_const_3 0,Int,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_cons_2 0)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_$!_numpat2val_1 0)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 0)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_4_typeEqsTail_1_$!_1_Add_1 1)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_cons_2 0,Vec(Int, 3),In vec.brat_globals_decl_4_xs 0)
-(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_const_3 0,Int,In vec.brat_check_defs_1_xs_$rhs_check'Con_cons_2 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_pat2val 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_$!_pat2val 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_check'Con_5_nil_3 0,Vec(Int, 0),In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 1)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0,Vec(Int, 1),In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 1)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_const_4 0,Int,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_cons_3 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_typeEqsTail_1_buildConst_1 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_check'Con_5_$!_numpat2val_1 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0,Vec(Int, 2),In vec.brat_check_defs_1_xs_$rhs_check'Con_cons_3 1)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_const_4 0,Int,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_cons_3 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_$!_numpat2val_1 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_check'Con_5_typeEqsTail_1_$!_1_Add_1 1)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_cons_3 0,Vec(Int, 3),In vec.brat_globals_decl_4_xs 0)
+(Ex vec.brat_check_defs_1_xs_$rhs_check'Con_const_4 0,Int,In vec.brat_check_defs_1_xs_$rhs_check'Con_cons_3 0)
 (Ex vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_$!_numpat2val_1 0)
 (Ex vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst 0,Nat,In vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_Add_1 0)
 (Ex vec.brat_check_defs_1_xs_$rhs_check'Con_typeEqsTail_1_$!_1_buildConst_2 0,Nat,In vec.brat_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 e8f234d5..7a9d414a 100755
--- a/brat/tools/validate.sh
+++ b/brat/tools/validate.sh
@@ -12,7 +12,7 @@ declare -a FAILED_TEST_MSGS
 UNEXPECTED_PASSES=
 NUM_FAILURES=0
 
-for dir in test/compilation/output test/hugr/output; do
+for dir in test/compilation/output test/examples test/hugr/output; do
     for json in $(find $dir -maxdepth 1 -name "*.json"); do
         echo Validating "$json"
         RESULT=$(cat "$json" | hugr_validator 2>&1)
@@ -22,12 +22,12 @@ for dir in test/compilation/output test/hugr/output; do
             NUM_FAILURES=$((NUM_FAILURES + 1))
         fi
     done
+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
-    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
 done
 
 RED='\033[0;31m'
diff --git a/hugr_extension/src/defs.rs b/hugr_extension/src/defs.rs
index f1683a70..2e849eb6 100644
--- a/hugr_extension/src/defs.rs
+++ b/hugr_extension/src/defs.rs
@@ -4,12 +4,13 @@ use crate::{closure_type, ctor::BratCtor};
 use enum_iterator::Sequence;
 use hugr::{
     extension::{
-        prelude::USIZE_T,
+        prelude::{QB_T, USIZE_T},
         simple_op::{MakeOpDef, OpLoadError},
         ExtensionId, OpDef, SignatureError, SignatureFromArgs, SignatureFunc,
     },
     ops::NamedOp,
     std_extensions::arithmetic::int_types::INT_TYPES,
+    std_extensions::arithmetic::float_types::FLOAT64_TYPE,
     std_extensions::collections::list_type,
     types::{
         type_param::TypeParam, FuncValueType, PolyFuncTypeRV, Signature, Type,
@@ -42,6 +43,9 @@ pub enum BratOpDef {
     PrimCtorTest(BratCtor),
     Lluf,
     Replicate,
+    CRx,
+    CRy,
+    CRz,
 }
 
 impl NamedOp for BratOpDef {
@@ -58,6 +62,9 @@ impl NamedOp for BratOpDef {
             PrimCtorTest(ctor) => format_smolstr!("PrimCtorTest::{}", ctor.name()),
             Lluf => "Lluf".into(),
             Replicate => "Replicate".into(),
+            CRx => "CRx".into(),
+            CRy => "CRy".into(),
+            CRz => "CRz".into(),
         }
     }
 }
@@ -78,6 +85,9 @@ impl FromStr for BratOpDef {
             ["PrimCtorTest", ctor] => Ok(BratOpDef::PrimCtorTest(BratCtor::from_str(ctor)?)),
             ["Lluf"] => Ok(BratOpDef::Lluf),
             ["Replicate"] => Ok(BratOpDef::Replicate),
+            ["CRx"] => Ok(BratOpDef::CRx),
+            ["CRy"] => Ok(BratOpDef::CRy),
+            ["CRz"] => Ok(BratOpDef::CRz),
             _ => Err(ParseError::VariantNotFound),
         }
     }
@@ -150,7 +160,10 @@ impl MakeOpDef for BratOpDef {
                     vec![list_type(Type::new_var_use(0, TypeBound::Copyable))],
                 ),
             )
-            .into(),
+                .into(),
+            CRx => Signature::new(vec![QB_T, QB_T, FLOAT64_TYPE], vec![QB_T, QB_T]).into(),
+            CRy => Signature::new(vec![QB_T, QB_T, FLOAT64_TYPE], vec![QB_T, QB_T]).into(),
+            CRz => Signature::new(vec![QB_T, QB_T, FLOAT64_TYPE], vec![QB_T, QB_T]).into(),
         }
     }
 
diff --git a/hugr_extension/src/lib.rs b/hugr_extension/src/lib.rs
index fc2a549b..42c9d5b3 100644
--- a/hugr_extension/src/lib.rs
+++ b/hugr_extension/src/lib.rs
@@ -9,7 +9,7 @@ use hugr::{
         simple_op::{MakeOpDef, MakeRegisteredOp},
         ExtensionId, ExtensionRegistry, ExtensionSet, TypeDefBound,
     },
-    std_extensions::{arithmetic::int_types, collections},
+    std_extensions::{arithmetic::{float_types,int_types}, collections},
     types::{type_param::TypeParam, CustomType, Type, TypeArg, TypeBound, TypeName, TypeRV},
     Extension,
 };
@@ -49,6 +49,7 @@ lazy_static! {
     pub static ref BRAT_OPS_REGISTRY: ExtensionRegistry  = ExtensionRegistry::try_new([
         prelude::PRELUDE.to_owned(),
         int_types::EXTENSION.to_owned(),
+        float_types::EXTENSION.to_owned(),
         collections::EXTENSION.to_owned(),
         EXTENSION.to_owned(),
     ])
diff --git a/hugr_extension/src/ops.rs b/hugr_extension/src/ops.rs
index ee1159dc..5d2dc3a8 100644
--- a/hugr_extension/src/ops.rs
+++ b/hugr_extension/src/ops.rs
@@ -46,6 +46,9 @@ pub enum BratOp {
     // The inverse operation of "full" on Nats
     Lluf,
     Replicate(TypeArg),
+    CRx,
+    CRy,
+    CRz,
 }
 
 impl NamedOp for BratOp {
@@ -62,6 +65,10 @@ impl NamedOp for BratOp {
             PrimCtorTest { ctor, .. } => format_smolstr!("PrimCtorTest::{}", ctor.name()),
             Lluf => "Lluf".into(),
             Replicate(_) => "Replicate".into(),
+
+            CRx => "CRx".into(),
+            CRy => "CRy".into(),
+            CRz => "CRz".into(),
         }
     }
 }
@@ -142,6 +149,9 @@ impl MakeExtensionOp for BratOp {
             }),
             BratOpDef::Lluf => Ok(BratOp::Lluf),
             BratOpDef::Replicate => Ok(BratOp::Replicate(ext_op.args()[0].clone())),
+            BratOpDef::CRx => Ok(BratOp::CRx),
+            BratOpDef::CRy => Ok(BratOp::CRy),
+            BratOpDef::CRz => Ok(BratOp::CRz),
         }
     }
 
@@ -181,6 +191,9 @@ impl MakeExtensionOp for BratOp {
             BratOp::PrimCtorTest { args, .. } => args.clone(),
             BratOp::Lluf => vec![],
             BratOp::Replicate(arg) => vec![arg.clone()],
+            BratOp::CRx => vec![],
+            BratOp::CRy => vec![],
+            BratOp::CRz => vec![],
         }
     }
 }