feat: give all next calls a label (#61)

And other drive-by fixes pulled out from #59

---------

Co-authored-by: Alan Lawrence <[email protected]>

brat/Brat/Checker.hs

@@ -722,9 +722,9 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
 checkBody fnName body cty = do
   (tm, (absFC, tmFC)) <- case body of
     NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
-    Clauses (c :| cs) -> do
+    Clauses (c@(abs, tm) :| cs) -> do
       fc <- req AskFC
-      pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c))
+      pure (WC fc (Lambda c cs), (fcOf abs, fcOf tm))
     Undefined -> err (InternalError "Checking undefined clause")
   ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do
     (((), ()), leftovers) <- check tm conns
@@ -799,7 +799,7 @@ kindCheck ((hungry, k@(TypeFor m [])):unders) (Con c arg) = req (TLup (m, c)) >>
         -- the thing we *do* define kindOut as
 
         (_, argUnders, [(kindOut,_)], (_ :<< _va, _)) <-
-          next "" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0)
+          next "kc_alias" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0)
         -- arg is a juxtaposition
         (args, emptyUnders) <- kindCheck (second (\(Left k) -> k) <$> argUnders) (unWC arg)
         ensureEmpty "alias args" emptyUnders
@@ -869,7 +869,7 @@ kindCheck unders (Emb (WC fc (Var v))) = localFC fc $ vlup v >>= f unders
   f _ (x:_) = err $ InternalError $ "Kindchecking a row which contains " ++ show x
 -- TODO: Add other operations on numbers
 kindCheck ((hungry, Nat):unders) (Simple (Num n)) | n >= 0 = do
-  (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0)
+  (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0)
   let value = VNum (nConstant (fromIntegral n))
   defineTgt hungry value
   defineSrc dangling value

brat/Brat/Checker/Helpers.hs

@@ -20,7 +20,7 @@ module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig
                             ,evalSrcRow, evalTgtRow
                             )-} where
 
-import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, err, typeErr, kindArgRows)
+import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, err, typeErr, kindArgRows, defineEnd)
 import Brat.Checker.Types
 import Brat.Error (ErrorMsg(..))
 import Brat.Eval (eval, EvMode(..), kindType)
@@ -250,14 +250,14 @@ getThunks :: Modey m
 getThunks _ [] = pure ([], [], [])
 getThunks Braty ((src, Right ty):rest) = do
   ty <- eval S0 ty
-  (src, (ss :->> ts)) <- vectorise Braty (src, ty)
+  (src, ss :->> ts) <- vectorise Braty (src, ty)
   (node, unders, overs, _) <- let ?my = Braty in
                                 anext "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts
   (nodes, unders', overs') <- getThunks Braty rest
   pure (node:nodes, unders <> unders', overs <> overs')
 getThunks Kerny ((src, Right ty):rest) = do
   ty <- eval S0 ty
-  (src, (ss :->> ts)) <- vectorise Kerny (src,ty)
+  (src, ss :->> ts) <- vectorise Kerny (src,ty)
   (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts
   (nodes, unders', overs') <- getThunks Kerny rest
   pure (node:nodes, unders <> unders', overs <> overs')
@@ -380,10 +380,10 @@ valueToBinder Braty = Right
 valueToBinder Kerny = id
 
 defineSrc :: Src -> Val Z -> Checking ()
-defineSrc src v = req (Define (ExEnd (end src)) v)
+defineSrc src = defineEnd (ExEnd (end src))
 
 defineTgt :: Tgt -> Val Z -> Checking ()
-defineTgt tgt v = req (Define (InEnd (end tgt)) v)
+defineTgt tgt = defineEnd (InEnd (end tgt))
 
 declareSrc :: Src -> Modey m -> BinderType m -> Checking ()
 declareSrc src my ty = req (Declare (ExEnd (end src)) my ty)

brat/Brat/Checker/Monad.hs

@@ -315,3 +315,6 @@ localNS ns (Req (Fresh str) k) = let (name, root) = fresh str ns in
 localNS ns (Req (SplitNS str) k) = let (subSpace, newRoot) = split str ns in
                                       localNS newRoot (k subSpace)
 localNS ns (Req c k) = Req c (localNS ns . k)
+
+defineEnd :: End -> Val Z -> Checking ()
+defineEnd e v = req (Define e v)

brat/Brat/Checker/SolvePatterns.hs

@@ -139,13 +139,18 @@ solveConstructor :: EvMode m
                              )
 solveConstructor my src (c, abs) ty p = do
   (CArgs pats _ patRo argRo, (tycon, tyargs)) <- lookupConstructor my c ty
+  -- Create a row of hypothetical kinds which contextualise the arguments to the
+  -- constructor.
+  -- These need to be Tgts because we don't know how to compute them dynamically
   (_, _, _, stuff) <- next "type_args" Hypo (S0, Some (Zy :* S0)) patRo R0
   (node, _, patArgWires, _) <- let ?my = my in anext "val_args" Hypo stuff R0 argRo
   trackM ("Constructor " ++ show c ++ "; type " ++ show ty)
   case snd stuff of
     Some (_ :* patEnds) -> do
       trackM (show pats)
       trackM (show patEnds)
+      -- Match the patterns for `c` against the ends of the Hypo node, to
+      -- produce the terms that we're interested in
       let (lhss, leftovers) = patVals pats (stkList patEnds)
       unless (null leftovers) $ error "There's a bug in the constructor table"
       tyArgKinds <- tlup (Brat, tycon)
@@ -186,10 +191,12 @@ unify l k r = do
       --       the whole `Problem`.
       (l, r, _) -> err . UnificationError $ "Can't unify " ++ show l ++ " with " ++ show r
 
+-- Solve a metavariable statically - don't do anything dynamic
+-- Once a metavariable is solved, we expect to not see it again in a normal form.
 instantiateMeta :: End -> Val Z -> Checking ()
 instantiateMeta e val = do
   throwLeft (doesntOccur e val)
-  req (Define e val)
+  defineEnd e val
 
 
 -- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding
@@ -225,6 +232,9 @@ doesntOccurRo _ _ R0 = pure ()
 doesntOccurRo my e (RPr (_, ty) ro) = doesntOccur e ty *> doesntOccurRo my e ro
 doesntOccurRo Braty e (REx _ ro) = doesntOccurRo Braty e ro
 
+-- Need to keep track of which way we're solving - which side is known/unknown
+-- Things which are dynamically unknown must be Tgts - information flows from Srcs
+-- ...But we don't need to do any wiring here, right?
 unifyNum :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
 unifyNum (NumValue lup lgro) (NumValue rup rgro)
   | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro)
@@ -334,6 +344,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
     req $ Define (ExEnd out) (VNum (nPlus 1 (nVar (VPar (toEnd pred)))))
     pure (nVar (VPar (toEnd pred)))
 
+-- The variable must be a non-zero nat!!
 patVal :: ValPat -> [End] -> (Val Z, [End])
 -- Nat variables will only be found in a `NumPat`, not a `ValPat`
 patVal VPVar (e:es) = (VApp (VPar e) B0, es)

brat/Brat/Checker/Types.hs

@@ -9,6 +9,7 @@ module Brat.Checker.Types (Overs, Unders
                           ,emptyEnv
                           ,TypedHole(..), HoleTag(..), HoleData(..)
                           ,initStore
+                          ,kindForMode
                           ) where
 
 import Brat.Checker.Quantity
@@ -111,3 +112,7 @@ initStore = Store M.empty M.empty
 
 instance Semigroup Store where
   (Store ks vs) <> (Store ks' vs') = Store (ks <> ks') (vs <> vs')
+
+kindForMode :: Modey m -> TypeKind
+kindForMode Braty = Star []
+kindForMode Kerny = Dollar []

brat/Brat/Eval.hs

@@ -15,7 +15,7 @@ module Brat.Eval (EvMode(..)
                  ) where
 
 import Brat.Checker.Monad
-import Brat.Checker.Types (EndType(..))
+import Brat.Checker.Types (EndType(..), kindForMode)
 import Brat.Error (ErrorMsg(..))
 import Brat.QualName (plain)
 import Brat.Syntax.Value
@@ -275,9 +275,7 @@ eqRowTest :: Modey m
                                        ))
 eqRowTest _ _ lvkz (stk0, R0) (stk1, R0) = pure $ Right (Some lvkz, stk0, stk1)
 eqRowTest m tm lvkz (stk0, RPr (_, ty0) r0) (stk1, RPr (_, ty1) r1) = do
-  let k = case m of
-        Braty -> Star []
-        Kerny -> Dollar []
+  let k = kindForMode m
   ty0 <- sem stk0 ty0
   ty1 <- sem stk1 ty1
   eqWorker tm lvkz k ty0 ty1 >>= \case

brat/Brat/Load.hs

@@ -115,7 +115,7 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do
 
 loadAlias :: TypeAlias -> Checking (QualName, Alias)
 loadAlias (TypeAlias fc name args body) = localFC fc $ do
-  (_, [(hhungry, Left k)], _, _) <- next "" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0
+  (_, [(hhungry, Left k)], _, _) <- next "load_alias" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0
   let abs = WC fc $ foldr ((:||:) . APat . Bind . fst) AEmpty args
   ([v], unders) <- kindCheck [(hhungry, k)] $ Th (WC fc (Lambda (abs, WC fc body) []))
   ensureEmpty "loadAlias unders" unders

brat/Brat/Syntax/Value.hs

@@ -51,6 +51,8 @@ data Inx :: N -> Type where
   VZ :: Inx (S n)
   VS :: Inx n -> Inx (S n)
 
+deriving instance Eq (Inx n)
+
 instance Show (Inx n) where
   show = show . toNat
    where
@@ -144,7 +146,7 @@ deriving instance Show (VVar n)
 
 instance Eq (VVar n) where
   (VPar e0) == (VPar e1) = e0 == e1
-  (VInx _) == (VInx _) = error "tried to compare VInxs"
+  (VInx i) == (VInx i') = i == i'
   _ == _ = False
 
 -- More syntactic, called "Term" elsewhere in literature (not in BRAT)

brat/test/golden/graph/cons.brat.graph

@@ -6,12 +6,12 @@ Nodes:
 (check_defs_1_two_const_1,BratNode (Const 1) [] [("value",Int)])
 (check_defs_1_two_const_3,BratNode (Const 2) [] [("value",Int)])
 (check_defs_1_two_nil_4,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
-(globals__3,BratNode (Const 2) [] [("value",Nat)])
-(globals__8,BratNode (Const 3) [] [("value",Nat)])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_Int_7,BratNode (Constructor Int) [] [("value",[])])
 (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
 (globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
+(globals_const_3,BratNode (Const 2) [] [("value",Nat)])
+(globals_const_8,BratNode (Const 3) [] [("value",Nat)])
 (globals_decl_4_two,BratNode Id [("a1",Vec(Int, 2))] [("a1",Vec(Int, 2))])
 (globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
@@ -27,6 +27,6 @@ Wires:
 (Ex globals_Int_7 0,[],In globals_Vec_6 0)
 (Ex globals_Vec_1 0,[],In globals___kca_two 0)
 (Ex globals_Vec_6 0,[],In globals___kca_three_5 0)
-(Ex globals__3 0,Nat,In globals_Vec_1 1)
-(Ex globals__8 0,Nat,In globals_Vec_6 1)
+(Ex globals_const_3 0,Nat,In globals_Vec_1 1)
+(Ex globals_const_8 0,Nat,In globals_Vec_6 1)
 (Ex globals_decl_4_two 0,Vec(Int, 2),In check_defs_1_three_1_cons 1)

brat/test/golden/graph/kernel.brat.graph

@@ -13,12 +13,12 @@ Nodes:
 (check_defs_1_id3_thunk/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
 (check_defs_1_id3_thunk/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] [])
 (check_defs_1_id3_thunk_thunk_2,BratNode (Box (fromList []) check_defs_1_id3_thunk/in check_defs_1_id3_thunk/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
-(globals__8,BratNode (Const 3) [] [("value",Nat)])
 (globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Qubit_7,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
+(globals_const_8,BratNode (Const 3) [] [("value",Nat)])
 (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:
@@ -39,4 +39,4 @@ Wires:
 (Ex globals_Qubit_4 0,[],In globals___kcr__1 2)
 (Ex globals_Qubit_7 0,[],In globals_Vec_6 0)
 (Ex globals_Vec_6 0,[],In globals___kcr__5 0)
-(Ex globals__8 0,Nat,In globals_Vec_6 1)
+(Ex globals_const_8 0,Nat,In globals_Vec_6 1)

brat/test/golden/graph/vec.brat.graph

@@ -6,9 +6,9 @@ Nodes:
 (check_defs_1_xs_const_3,BratNode (Const 1) [] [("value",Int)])
 (check_defs_1_xs_const_5,BratNode (Const 2) [] [("value",Int)])
 (check_defs_1_xs_nil_6,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
-(globals__3,BratNode (Const 3) [] [("value",Nat)])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
+(globals_const_3,BratNode (Const 3) [] [("value",Nat)])
 (globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
@@ -21,4 +21,4 @@ Wires:
 (Ex check_defs_1_xs_nil_6 0,Vec(Int, 0),In check_defs_1_xs_cons_4 1)
 (Ex globals_Int_2 0,[],In globals_Vec_1 0)
 (Ex globals_Vec_1 0,[],In globals___kca_xs 0)
-(Ex globals__3 0,Nat,In globals_Vec_1 1)
+(Ex globals_const_3 0,Nat,In globals_Vec_1 1)