From 8ad05de5ca9b0d398c329ae2081b8b5afddb831a Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 12:28:04 +0000 Subject: [PATCH] Revert "drive-by: Give everything created with anext a label" This reverts commit c8cb33fd94d7aec243871bd1206db76b32c7d286. --- brat/Brat/Checker.hs | 4 ++-- brat/Brat/Checker/Helpers.hs | 12 ++++++------ brat/test/golden/error/remaining_hopes.brat.golden | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 40983c9b..4f56f1ba 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -486,7 +486,7 @@ check' (Simple tm) ((), (hungry, ty):unders) = do case (?my, ty, tm) of -- The only SimpleType that checks against a kind is a Nat (Braty, Left Nat, Num n) -> do - (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0)) + (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0) let val = VNum (nConstant (fromIntegral n)) defineSrc dangling val @@ -497,7 +497,7 @@ check' (Simple tm) ((), (hungry, ty):unders) = do _ -> do let vty = biType @m ty throwLeft $ simpleCheck ?my vty tm - (_, _, [(dangling, _)], _) <- anext @m "const" (Const tm) (S0,Some (Zy :* S0)) + (_, _, [(dangling, _)], _) <- anext @m "" (Const tm) (S0,Some (Zy :* S0)) R0 (RPr ("value", vty) R0) wire (dangling, vty, hungry) pure (((), ()), ((), unders)) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 882a787c..b6812e79 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -250,7 +250,7 @@ getThunks _ [] = pure ([], [], []) getThunks Braty row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case (src, VFun Braty (ss :->> ts)) -> do (node, unders, overs, _) <- let ?my = Braty in - anext "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts + anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Braty rest pure (node:nodes, unders <> unders', overs <> overs') -- These shouldn't happen @@ -258,7 +258,7 @@ getThunks Braty row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) v -> typeErr $ "Force called on non-thunk: " ++ show v getThunks Kerny row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case (src, VFun Kerny (ss :->> ts)) -> do - (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts + (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Kerny rest pure (node:nodes, unders <> unders', overs <> overs') (_, VFun _ _) -> err $ ExpectedThunk (showMode Kerny) (showRow row) @@ -267,7 +267,7 @@ getThunks Braty ((src, Left (Star args)):rest) = do (node, unders, overs) <- case bwdStack (B0 <>< args) of Some (_ :* stk) -> do let (ri,ro) = kindArgRows stk - (node, unders, overs, _) <- next "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro + (node, unders, overs, _) <- next "" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro pure (node, unders, overs) (nodes, unders', overs') <- getThunks Braty rest pure (node:nodes, unders <> unders', overs <> overs') @@ -344,7 +344,7 @@ vectorise (src, ty) = do let weak1 = changeVar (Thinning (ThDrop ThNull)) vecFun <- vectorisedFun len my cty (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <- - next "MapFun" MapFun (S0, Some (Zy :* S0)) + next "" MapFun (S0, Some (Zy :* S0)) (REx ("len", Nat) (RPr ("value", weak1 ty) R0)) (RPr ("vector", weak1 vecFun) R0) defineTgt lenTgt (VNum len) @@ -499,10 +499,10 @@ runArith _ _ _ = Nothing buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src) buildArithOp op = do - (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next (show op) (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) + (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next "" (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) pure ((lhs, rhs), out) buildConst :: SimpleTerm -> Val Z -> Checking Src buildConst tm ty = do - (_, _, [(out,_)], _) <- next "const" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) + (_, _, [(out,_)], _) <- next "" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) pure out diff --git a/brat/test/golden/error/remaining_hopes.brat.golden b/brat/test/golden/error/remaining_hopes.brat.golden index 80d15436..49009d3a 100644 --- a/brat/test/golden/error/remaining_hopes.brat.golden +++ b/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_1_Eval 0 + In checking_check_defs_1_g_1_ 0