Skip to content

Commit

Permalink
Revert "drive-by: Give everything created with anext a label"
Browse files Browse the repository at this point in the history
This reverts commit c8cb33f.
  • Loading branch information
croyzor committed Nov 27, 2024
1 parent 541f35a commit 8ad05de
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 9 deletions.
4 changes: 2 additions & 2 deletions brat/Brat/Checker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))
Expand Down
12 changes: 6 additions & 6 deletions brat/Brat/Checker/Helpers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -250,15 +250,15 @@ 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
(_, VFun _ _) -> err $ ExpectedThunk (showMode Braty) (showRow row)
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)
Expand All @@ -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')
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion brat/test/golden/error/remaining_hopes.brat.golden
Original file line number Diff line number Diff line change
Expand Up @@ -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


0 comments on commit 8ad05de

Please sign in to comment.