Skip to content

Commit

Permalink
[refactor] Common-up in checkBody (#57)
Browse files Browse the repository at this point in the history
  • Loading branch information
acl-cqc authored Nov 25, 2024
1 parent 86f94de commit e539073
Showing 1 changed file with 17 additions and 21 deletions.
38 changes: 17 additions & 21 deletions brat/Brat/Checker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -709,27 +709,23 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
-> FunBody Term UVerb
-> CTy m Z -- Function type
-> Checking Src
checkBody fnName body cty = case body of
NoLhs tm -> do
((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do
(((), ()), leftovers) <- check tm conns
checkConnectorsUsed (fcOf tm, fcOf tm) (show tm) conns leftovers
pure src
Clauses (c :| cs) -> do
fc <- req AskFC
((box, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do
let tm = Lambda c cs
(((), ()), leftovers) <- check (WC fc tm) conns
checkConnectorsUsed (bimap fcOf fcOf c) (show tm) conns leftovers
pure box
Undefined -> err (InternalError "Checking undefined clause")
where
checkConnectorsUsed _ _ _ ([], []) = pure ()
checkConnectorsUsed (_, tmFC) tm (_, unders) ([], rightUnders) = localFC tmFC $
let numUsed = length unders - length rightUnders in
err (TypeMismatch tm (showRow unders) (showRow (take numUsed unders)))
checkConnectorsUsed (absFC, _) _ _ (rightOvers, _) = localFC absFC $
typeErr ("Inputs " ++ showRow rightOvers ++ " weren't used")
checkBody fnName body cty = do
(tm, (absFC, tmFC)) <- case body of
NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
Clauses (c :| cs) -> do
fc <- req AskFC
pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c))
Undefined -> err (InternalError "Checking undefined clause")
((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do
(((), ()), leftovers) <- check tm conns
case leftovers of
([], []) -> pure ()
([], rightUnders) -> localFC tmFC $
let numUsed = length unders - length rightUnders
in err (TypeMismatch (show tm) (showRow unders) (showRow (take numUsed unders)))
(rightOvers, _) -> localFC absFC $
typeErr ("Inputs " ++ showRow rightOvers ++ " weren't used")
pure src

-- Constructs row from a list of ends and types. Uses standardize to ensure that dependency is
-- detected. Fills in the first bot ends from a stack. The stack grows every time we go under
Expand Down

0 comments on commit e539073

Please sign in to comment.