Fix: namespacing in Load.hs

brat/Brat/Checker.hs

@@ -20,7 +20,6 @@ import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
-import qualified Data.Set as S
 import Data.Traversable (for)
 import Data.Type.Equality ((:~:)(..), testEquality)
 import Prelude hiding (filter)
@@ -59,15 +58,10 @@ standardise k val = eval S0 val >>= (\case
   (_, val) -> pure val) . (k,)
 
 mergeEnvs :: [Env a] -> Checking (Env a)
-mergeEnvs = foldM combineDisjointEnvs M.empty
- where
-  combineDisjointEnvs :: M.Map QualName v -> M.Map QualName v -> Checking (M.Map QualName v)
-  combineDisjointEnvs l r =
-    let commonKeys = S.intersection (M.keysSet l) (M.keysSet r)
-    in if S.null commonKeys
-       then pure $ M.union l r
-       else typeErr ("Variable(s) defined twice: " ++
-    intercalate "," (map show $ S.toList commonKeys))
+mergeEnvs es = throwLeft $ first fmterr $ foldM combineDisjointEnvs M.empty es
+  where
+    fmterr :: [QualName] -> ErrorMsg
+    fmterr names = TypeErr $ "Variable(s) defined twice: " ++ intercalate "," (map show names)
 
 
 singletonEnv :: (?my :: Modey m) => String -> (Src, BinderType m) -> Checking (Env (EnvData m))

brat/Brat/Checker/Types.hs

@@ -5,6 +5,7 @@ module Brat.Checker.Types (Overs, Unders
                           ,ChkConnectors, SynConnectors
                           ,Mode(..), Modey(..)
                           ,Env, VEnv, KEnv, EnvData
+                          ,combineDisjointEnvs
                           ,IsSkolem(..), Store(..), EndType(..)
                           ,emptyEnv
                           ,TypedHole(..), HoleTag(..), HoleData(..)
@@ -22,6 +23,7 @@ import Hasochism (N(..))
 
 import Data.Kind (Type)
 import qualified Data.Map as M
+import qualified Data.Set as S
 
 -- Inputs against which a term is checked
 type family Overs (m :: Mode) (k :: Kind) :: Type where
@@ -61,6 +63,14 @@ type KEnv = Env (EnvData Kernel)
 emptyEnv :: Env a
 emptyEnv = M.empty
 
+-- Left == error == list of the QualNames that were multiply defined
+combineDisjointEnvs :: Env e -> Env e -> Either [QualName] (Env e)
+combineDisjointEnvs l r =
+  let commonKeys = S.intersection (M.keysSet l) (M.keysSet r)
+  in if S.null commonKeys
+      then pure $ M.union l r
+      else Left $ S.toList commonKeys
+
 data HoleTag :: Mode -> Kind -> Type where
   NBHole :: HoleTag Brat Noun
   NKHole :: HoleTag Kernel Noun

brat/Brat/Compile/Hugr.hs

@@ -126,6 +126,10 @@ addNode nam (parent, op) = do
   setOp name (addMetadata [("id", show name)] op)
   pure name
 
+filePrefix :: [String] -> Name -> Maybe Name
+filePrefix prefixes (MkName (("checking",_):_filename:ns)) =
+  hasPrefix (["globals"]++prefixes) (MkName ns)
+
 runCheckingInCompile :: Free CheckingSig t -> Compile t
 runCheckingInCompile (Ret t) = pure t
 runCheckingInCompile (Req (ELup e) k) = do
@@ -314,7 +318,7 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
   -- If we only care about the node for typechecking, then drop it and return `Nothing`.
   -- Otherwise, NodeId of compiled node, and list of Hugr in-edges (source and target-port)
   compileNode :: Compile (Maybe (NodeId, [(PortId NodeId, Int)]))
-  compileNode = case (hasPrefix ["checking", "globals", "decl"] name) of
+  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).
@@ -364,7 +368,7 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
       ins <- compilePorts ins
       outs <- compilePorts outs
       let sig = FunctionType ins outs bratExts
-      case hasPrefix ["checking", "globals", "prim"] outNode of
+      case filePrefix ["prim"] outNode of
         -- If we're evaling a Prim, we add it directly into the kernel graph
         Just suffix -> do
           (ns, _) <- gets bratGraph
@@ -407,13 +411,13 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
       outs <- compilePorts outs
       (ns, _) <- gets bratGraph
       decls <- gets decls
-      case hasPrefix ["checking", "globals", "prim"] outNode of
+      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 hasPrefix ["checking", "globals"] outNode of
+        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 ++ ")")
@@ -449,7 +453,7 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
 
     Target -> error "Target found outside of compileBox"
 
-    Id | Nothing <- hasPrefix ["checking", "globals", "decl"] name -> default_edges <$> do
+    Id | Nothing <- filePrefix ["decl"] name -> default_edges <$> do
       -- not a top-level decl, just compile it as an Id (TLDs handled in compileNode)
       let [(_,ty)] = ins -- fail if more than one input
       addNode "Id" (parent, OpNoop (NoopOp (compileType ty)))
@@ -854,7 +858,7 @@ compileModule venv moduleNode = do
   decls = do -- in list monad, no Compile here
             (fnName, wires) <- M.toList venv
             let (Ex idNode _) = end (fst $ head wires) -- would be better to check same for all rather than just head
-            case hasPrefix ["checking","globals","decl"] idNode of
+            case filePrefix ["decl"] idNode of
               Just _ -> pure (fnName, idNode) -- assume all ports are 0,1,2...
               Nothing -> []
 

brat/Brat/Load.hs

@@ -7,7 +7,7 @@ module Brat.Load (loadFilename
 import Brat.Checker
 import Brat.Checker.Helpers (ensureEmpty, next, showMode, wire)
 import Brat.Checker.Monad
-import Brat.Checker.Types (Store, TypedHole, VEnv, initStore)
+import Brat.Checker.Types (Store, TypedHole, initStore, VEnv)
 import Brat.Elaborator (elabEnv)
 import Brat.Error
 import Brat.FC hiding (end)
@@ -213,11 +213,13 @@ loadFiles ns (cwd :| extraDirs) fname contents = do
       pure (deps ++ [main])
     Nothing -> throwError (SrcErr "" $ dumbErr (InternalError "Empty dependency graph"))
   -- keep VEnv as we fold but discard holes, graph and captures except from the last file in the list
-  liftEither $ foldM
-    (\(venv, decls, _, defs, _, _) -> loadStmtsWithEnv ns (venv, decls, defs))
-    emptyMod
-    allStmts'
+  liftEither $ fst <$> foldM loadStmtsSplitNS (emptyMod, ns) allStmts'
   where
+    loadStmtsSplitNS :: (VMod, Namespace) -> (FilePath, Prefix, FEnv, String) -> Either SrcErr (VMod, Namespace)
+    loadStmtsSplitNS ((venv,decls,_,store,_,_), ns) file@(fname, _, _, _) =
+      let (subns, ns') = split (takeBaseName fname) ns
+      in (, ns') <$> loadStmtsWithEnv subns (venv,decls,store) file
+
     -- builds a map from Import to (index in which discovered, module)
     depGraph :: M.Map Import (Int, FlatMod) -- input map to which to add
              -> Import -> String

brat/test/Test/Compile/Hugr.hs

@@ -19,16 +19,16 @@ outputDir = prefix </> "output"
 -- examples that we expect to compile, but then to fail validation
 invalidExamples :: [FilePath]
 invalidExamples = (map ((++ ".brat") . ("examples" </>))
-  ["adder"
-  ,"app"
+  ["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" -- missing coercions, https://github.com/quantinuum-dev/brat/issues/413
-  ,"thunks"]
+  --,"repeated_app" -- not checking yet, but will be missing coercions, https://github.com/quantinuum-dev/brat/issues/413
+  ]
   ) ++ ["test/compilation/closures.brat"] -- fails to compile but still spits out some JSON (not whole Hugr)
 
 -- examples that we expect not to compile.

brat/test/golden/error/badvec3.brat.golden

@@ -2,5 +2,5 @@ Error in test/golden/error/badvec3.brat on line 2:
 v3 = cons(1, nil)
      ^^^^^^^^^^^^
 
-  Unification error: Couldn't force 1 + VPar In checking_check_defs_1_v3_$rhs_check'Con_$!_numpat2val_1 0 to be 0
+  Unification error: Couldn't force 1 + VPar In checking_badvec3_check_defs_1_v3_$rhs_check'Con_$!_numpat2val_1 0 to be 0
 

brat/test/golden/error/fanin-dynamic-length.brat.golden

@@ -2,5 +2,5 @@ Error in test/golden/error/fanin-dynamic-length.brat on line 2:
 f(n) = { [\/] }
          ^^^^
 
-  Type error: Can't fanout a Vec with non-constant length: VPar Ex checking_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 0
+  Type error: Can't fanout a Vec with non-constant length: VPar Ex checking_fanin-dynamic-length_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 0
 

brat/test/golden/error/fanout-dynamic-length.brat.golden

@@ -2,5 +2,5 @@ Error in test/golden/error/fanout-dynamic-length.brat on line 2:
 f(n) = { [/\] }
          ^^^^
 
-  Type error: Can't fanout a Vec with non-constant length: VPar Ex checking_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 0
+  Type error: Can't fanout a Vec with non-constant length: VPar Ex checking_fanout-dynamic-length_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 0
 

brat/test/golden/error/kbadvec3.brat.golden

@@ -2,5 +2,5 @@ Error in test/golden/error/kbadvec3.brat on line 2:
 constNil = { b => cons(1, nil) }
                   ^^^^^^^^^^^^
 
-  Unification error: Couldn't force 1 + VPar In checking_check_defs_1_constNil_$rhs_check'Th_LambdaChk_7_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1 0 to be 0
+  Unification error: Couldn't force 1 + VPar In checking_kbadvec3_check_defs_1_constNil_$rhs_check'Th_LambdaChk_7_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1 0 to be 0
 

brat/test/golden/error/remaining-nat-hopes.brat.golden

@@ -3,6 +3,6 @@ bad = let _ = read([]) in show(!)
                               ^^^
 
   Expected to work out values for these holes:
-    In checking_check_defs_1_bad_5_$rhs_$!_3 0
+    In checking_remaining-nat-hopes_check_defs_1_bad_5_$rhs_$!_3 0
 
 

brat/test/golden/error/remaining_hopes.brat.golden

@@ -3,6 +3,6 @@ g = f(!)
      ^^^
 
   Expected to work out values for these holes:
-    In checking_check_defs_1_g_3_$rhs_$!_1 0
+    In checking_remaining_hopes_check_defs_1_g_3_$rhs_$!_1 0
 
 

brat/test/golden/error/vec_length.brat.golden

@@ -2,5 +2,5 @@ Error in test/golden/error/vec_length.brat on line 2:
 f(_, _, xs) = xs
               ^^
 
-  Unification error: Can't make Ex checking_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 1 = 1 + VPar Ex checking_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 1
+  Unification error: Can't make Ex checking_vec_length_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 1 = 1 + VPar Ex checking_vec_length_check_defs_1_f_LambdaChk_7_checkClauses_1_lambda.0_rhs/in_1 1
 

brat/test/golden/error/vectorise1.brat.golden

@@ -2,7 +2,7 @@ Error in test/golden/error/vectorise1.brat on line 2:
 bad1(n) = (n of (1, 2.0)), (n of 3)
                            ^^^^^^^^
 
-  Type error: Got: Vector of length VPar Ex checking_check_defs_1_bad1_$lhs_3_lambda_fake_source 0
+  Type error: Got: Vector of length VPar Ex checking_vectorise1_check_defs_1_bad1_$lhs_3_lambda_fake_source 0
 Expected: empty row
 
 

brat/test/golden/error/vectorise3.brat.golden

@@ -3,5 +3,5 @@ f(_, _, n, f, xs) = (n of f)(xs)
                     ^^^^^^^^^^^^
 
   Type error: Expected function 「n」 of f() to consume all of its arguments (「xs」)
- but found leftovers: (b1 :: Vec(VApp VPar Ex checking_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_check_defs_1_f_$lhs_3_lambda_fake_source 2))
+ but found leftovers: (b1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2))
 

brat/test/golden/graph/addN.brat.graph

@@ -1,35 +1,35 @@
 Nodes:
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in,BratNode Source [] [("inp",Int)])
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/out_1,BratNode Target [("out",Int)] [])
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (inp :: Int) -> (out :: Int) })])
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval,BratNode (Eval (Ex globals_prim_8_add 0)) [("a",Int),("b",Int)] [("c",Int)])
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/in_1,BratNode Source [] [("n",Int)])
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2,BratNode Target [("out",Int)] [])
-(check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/in_1 check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (n :: Int) -> (out :: Int) })])
-(check_defs_1_addN_LambdaChk_9_lambda,BratNode (PatternMatch ((TestMatchData Braty (MatchSequence {matchInputs = [(NamedPort {end = Ex check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "inp"},Int)], matchTests = [], matchOutputs = [(NamedPort {end = Ex check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "inp"},Int)]}),check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("inp",Int)] [("out",Int)])
-(check_defs_1_addN_addN.box/in,BratNode Source [] [("inp",Int)])
-(check_defs_1_addN_addN.box/out_1,BratNode Target [("out",Int)] [])
-(check_defs_1_addN_addN.box_thunk_2,BratNode (Box check_defs_1_addN_addN.box/in check_defs_1_addN_addN.box/out_1) [] [("thunk",{ (inp :: Int) -> (out :: Int) })])
-(globals_Int_1,BratNode (Constructor Int) [] [("value",[])])
-(globals_Int_5,BratNode (Constructor Int) [] [("value",[])])
-(globals_Int_6,BratNode (Constructor Int) [] [("value",[])])
-(globals_Int_7,BratNode (Constructor Int) [] [("value",[])])
-(globals_Int_11,BratNode (Constructor Int) [] [("value",[])])
-(globals_Int_12,BratNode (Constructor Int) [] [("value",[])])
-(globals_decl_13_addN,BratNode Id [("thunk",{ (inp :: Int) -> (out :: Int) })] [("thunk",{ (inp :: Int) -> (out :: Int) })])
-(globals_prim_2_N,BratNode (Prim ("","N")) [] [("value",Int)])
-(globals_prim_8_add,BratNode (Prim ("","add")) [] [("thunk",{ (a :: Int), (b :: Int) -> (c :: Int) })])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in,BratNode Source [] [("inp",Int)])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/out_1,BratNode Target [("out",Int)] [])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (inp :: Int) -> (out :: Int) })])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval,BratNode (Eval (Ex addN.brat_globals_prim_8_add 0)) [("a",Int),("b",Int)] [("c",Int)])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/in_1,BratNode Source [] [("n",Int)])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2,BratNode Target [("out",Int)] [])
+(addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/in_1 addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (n :: Int) -> (out :: Int) })])
+(addN.brat_check_defs_1_addN_LambdaChk_9_lambda,BratNode (PatternMatch ((TestMatchData Braty (MatchSequence {matchInputs = [(NamedPort {end = Ex addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "inp"},Int)], matchTests = [], matchOutputs = [(NamedPort {end = Ex addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "inp"},Int)]}),addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("inp",Int)] [("out",Int)])
+(addN.brat_check_defs_1_addN_addN.box/in,BratNode Source [] [("inp",Int)])
+(addN.brat_check_defs_1_addN_addN.box/out_1,BratNode Target [("out",Int)] [])
+(addN.brat_check_defs_1_addN_addN.box_thunk_2,BratNode (Box addN.brat_check_defs_1_addN_addN.box/in addN.brat_check_defs_1_addN_addN.box/out_1) [] [("thunk",{ (inp :: Int) -> (out :: Int) })])
+(addN.brat_globals_Int_1,BratNode (Constructor Int) [] [("value",[])])
+(addN.brat_globals_Int_5,BratNode (Constructor Int) [] [("value",[])])
+(addN.brat_globals_Int_6,BratNode (Constructor Int) [] [("value",[])])
+(addN.brat_globals_Int_7,BratNode (Constructor Int) [] [("value",[])])
+(addN.brat_globals_Int_11,BratNode (Constructor Int) [] [("value",[])])
+(addN.brat_globals_Int_12,BratNode (Constructor Int) [] [("value",[])])
+(addN.brat_globals_decl_13_addN,BratNode Id [("thunk",{ (inp :: Int) -> (out :: Int) })] [("thunk",{ (inp :: Int) -> (out :: Int) })])
+(addN.brat_globals_prim_2_N,BratNode (Prim ("","N")) [] [("value",Int)])
+(addN.brat_globals_prim_8_add,BratNode (Prim ("","add")) [] [("thunk",{ (a :: Int), (b :: Int) -> (c :: Int) })])
 
 Wires:
-(Ex check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0,Int,In check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2 0)
-(Ex check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/in_1 0,Int,In check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0)
-(Ex check_defs_1_addN_LambdaChk_9_lambda 0,Int,In check_defs_1_addN_addN.box/out_1 0)
-(Ex check_defs_1_addN_addN.box/in 0,Int,In check_defs_1_addN_LambdaChk_9_lambda 0)
-(Ex check_defs_1_addN_addN.box_thunk_2 0,{ (inp :: Int) -> (out :: Int) },In globals_decl_13_addN 0)
-(Ex globals_Int_1 0,[],In globals___kcr_N 0)
-(Ex globals_Int_11 0,[],In globals___kcc_10 0)
-(Ex globals_Int_12 0,[],In globals___kcc_10 1)
-(Ex globals_Int_5 0,[],In globals___kcc_4 0)
-(Ex globals_Int_6 0,[],In globals___kcc_4 1)
-(Ex globals_Int_7 0,[],In globals___kcc_4 2)
-(Ex globals_prim_2_N 0,Int,In check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 1)
+(Ex addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0,Int,In addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2 0)
+(Ex addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/in_1 0,Int,In addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0)
+(Ex addN.brat_check_defs_1_addN_LambdaChk_9_lambda 0,Int,In addN.brat_check_defs_1_addN_addN.box/out_1 0)
+(Ex addN.brat_check_defs_1_addN_addN.box/in 0,Int,In addN.brat_check_defs_1_addN_LambdaChk_9_lambda 0)
+(Ex addN.brat_check_defs_1_addN_addN.box_thunk_2 0,{ (inp :: Int) -> (out :: Int) },In addN.brat_globals_decl_13_addN 0)
+(Ex addN.brat_globals_Int_1 0,[],In addN.brat_globals___kcr_N 0)
+(Ex addN.brat_globals_Int_11 0,[],In addN.brat_globals___kcc_10 0)
+(Ex addN.brat_globals_Int_12 0,[],In addN.brat_globals___kcc_10 1)
+(Ex addN.brat_globals_Int_5 0,[],In addN.brat_globals___kcc_4 0)
+(Ex addN.brat_globals_Int_6 0,[],In addN.brat_globals___kcc_4 1)
+(Ex addN.brat_globals_Int_7 0,[],In addN.brat_globals___kcc_4 2)
+(Ex addN.brat_globals_prim_2_N 0,Int,In addN.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 1)