Skip to content

Commit

Permalink
[trivial+refactor] Make checkThunk local (#50)
Browse files Browse the repository at this point in the history
Used in only one place, so more readable to bring things closer together.
  • Loading branch information
acl-cqc authored Nov 6, 2024
1 parent 8a4ff4f commit c699cda
Showing 1 changed file with 18 additions and 18 deletions.
36 changes: 18 additions & 18 deletions brat/Brat/Checker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -159,24 +159,6 @@ checkOutputs :: forall m k . (CheckConstraints m k, ?my :: Modey m)
-> Checking [(Tgt, BinderType m)]
checkOutputs tm unders overs = checkIO tm unders overs (flip $ checkWire ?my tm True) "No unders but overs: "

checkThunk :: (CheckConstraints m UVerb, EvMode m)
=> Modey m
-> String
-> CTy m Z
-> WC (Term Chk UVerb)
-> Checking Src
checkThunk m name cty tm = do
((dangling, _), ()) <- let ?my = m in makeBox name cty $
\(thOvers, thUnders) -> do
(((), ()), leftovers) <- check tm (thOvers, thUnders)
case leftovers of
([], []) -> pure ()
([], unders) -> err (ThunkLeftUnders (showRow unders))
-- If there are leftovers and leftunders, complain about the leftovers
-- Until we can report multiple errors!
(overs, _) -> err (ThunkLeftOvers (showRow overs))
pure dangling

check :: (CheckConstraints m k
,EvMode m
,TensorOutputs (Outputs m d)
Expand Down Expand Up @@ -315,6 +297,24 @@ check' (Th tm) ((), u@(hungry, ty):unders) = case (?my, ty) of
_ -> err . ExpectedThunk "" $ showRow (u:unders)
pure (((), ()), ((), unders))
(Kerny, _) -> err . ThunkInKernel $ show (Th tm)
where
checkThunk :: forall m. (CheckConstraints m UVerb, EvMode m)
=> Modey m
-> String
-> CTy m Z
-> WC (Term Chk UVerb)
-> Checking Src
checkThunk m name cty tm = do
((dangling, _), ()) <- let ?my = m in makeBox name cty $
\(thOvers, thUnders) -> do
(((), ()), leftovers) <- check tm (thOvers, thUnders)
case leftovers of
([], []) -> pure ()
([], unders) -> err (ThunkLeftUnders (showRow unders))
-- If there are leftovers and leftunders, complain about the leftovers
-- Until we can report multiple errors!
(overs, _) -> err (ThunkLeftOvers (showRow overs))
pure dangling
check' (TypedTh t) ((), ()) = case ?my of
-- the thunk itself must be Braty
Kerny -> err . ThunkInKernel $ show (TypedTh t)
Expand Down

0 comments on commit c699cda

Please sign in to comment.