From 60b1862ccfedf78eac3c8ec684a9a8af673f1b23 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 22 Nov 2024 11:41:54 +0000 Subject: [PATCH 1/3] checkBody: common-up two makeBox's, the hard way --- brat/Brat/Checker.hs | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index c855e6ad..7001aa8d 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -709,20 +709,18 @@ 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 +checkBody fnName body cty = do + (tm, checkFn) <- case body of + NoLhs tm -> pure (tm, checkConnectorsUsed (fcOf tm, fcOf tm) (show tm)) + Clauses (c :| cs) -> do + fc <- req AskFC 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") + pure $ (WC fc tm, checkConnectorsUsed (bimap fcOf fcOf c) (show tm)) + Undefined -> err (InternalError "Checking undefined clause") + ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do + (((), ()), leftovers) <- check tm conns + checkFn conns leftovers + pure src where checkConnectorsUsed _ _ _ ([], []) = pure () checkConnectorsUsed (_, tmFC) tm (_, unders) ([], rightUnders) = localFC tmFC $ From 9316c67d0f9476a5a06f4d8a48537c5d5c0bc48a Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 22 Nov 2024 11:44:56 +0000 Subject: [PATCH 2/3] Clauses case includes new FC in show'd term, common up more --- brat/Brat/Checker.hs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 7001aa8d..c5381230 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -710,16 +710,15 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m) -> CTy m Z -- Function type -> Checking Src checkBody fnName body cty = do - (tm, checkFn) <- case body of - NoLhs tm -> pure (tm, checkConnectorsUsed (fcOf tm, fcOf tm) (show tm)) + (tm, fcs) <- case body of + NoLhs tm -> pure (tm, (fcOf tm, fcOf tm)) Clauses (c :| cs) -> do fc <- req AskFC - let tm = Lambda c cs - pure $ (WC fc tm, checkConnectorsUsed (bimap fcOf fcOf c) (show tm)) + pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c)) Undefined -> err (InternalError "Checking undefined clause") ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do (((), ()), leftovers) <- check tm conns - checkFn conns leftovers + checkConnectorsUsed fcs (show tm) conns leftovers pure src where checkConnectorsUsed _ _ _ ([], []) = pure () From db0ef97b7c62bbd2479b404ecd7eb6449dce5eb5 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Fri, 22 Nov 2024 11:49:38 +0000 Subject: [PATCH 3/3] ...and inline singly-used checkConnectorsUsed --- brat/Brat/Checker.hs | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index c5381230..0e213fc2 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -710,23 +710,22 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m) -> CTy m Z -- Function type -> Checking Src checkBody fnName body cty = do - (tm, fcs) <- case body of + (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 -> do + ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do (((), ()), leftovers) <- check tm conns - checkConnectorsUsed fcs (show tm) conns leftovers + 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 - 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") -- 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