Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[refactor] combine checkInputs/Outputs and use for(M) #42

Merged
merged 11 commits into from
Nov 1, 2024
63 changes: 29 additions & 34 deletions brat/Brat/Checker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,10 @@ module Brat.Checker (checkBody
,tensor
) where

import Control.Arrow (first)
import Control.Exception (assert)
import Control.Monad (foldM, zipWithM)
import Control.Monad (foldM, forM, zipWithM)
import Control.Monad.Freer
import Data.Bifunctor (second)
import Data.Bifunctor (first, second)
import Data.Functor (($>), (<&>))
import Data.List ((\\))
import Data.List.NonEmpty (NonEmpty(..))
Expand Down Expand Up @@ -124,45 +123,41 @@ checkWire Kerny (WC fc tm) outputs (dangling, ot) (hungry, ut) = localFC fc $ do
else typeEq (show tm) (Dollar []) ut ot
wire (dangling, ot, hungry)

checkInputs :: (CheckConstraints m KVerb, ?my :: Modey m)
checkIO :: forall m d k exp act . (CheckConstraints m k, ?my :: Modey m)
=> WC (Term d k)
-> [(NamedPort exp, BinderType m)]
-> [(NamedPort act, BinderType m)]
-> ((NamedPort exp, BinderType m) -> (NamedPort act, BinderType m) -> Checking ())
-> String
-> Checking [(NamedPort exp, BinderType m)] -- left(overs/unders)
checkIO tm@(WC fc _) exps acts wireFn errMsg = modily ?my $ do
let (rows, rest) = zipSuffixes exps acts
localFC fc $ forM rows $ \(e:|exps, a:|acts) ->
wrapError (addRowContext (showRow $ e:exps) (showRow $ a:acts)) $ wireFn e a
throwLeft $ first (\(b:|bs) -> TypeErr $ errMsg ++ showRow (b:bs) ++ " for " ++ show tm) rest
where
addRowContext :: String -> String -> Error -> Error
addRowContext exp act = \case
(Err fc (TypeMismatch tm _ _)) -> Err fc $ TypeMismatch tm exp act
e -> e
zipSuffixes :: [a] -> [b] -> ([(NonEmpty a, NonEmpty b)], Either (NonEmpty b) [a])
zipSuffixes as [] = ([], Right as)
zipSuffixes [] (b:bs) = ([], Left (b:|bs)) -- indicates error
zipSuffixes (a:as) (b:bs) = first ((a:|as,b:|bs):) $ zipSuffixes as bs

checkInputs :: forall m d . (CheckConstraints m KVerb, ?my :: Modey m)
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Of course if we got rid of the extensive existing type signatures for checkInputs and checkOutputs then the line count here would look much better ;-). (Each of checkInputs and checkOutputs is used twice though so I don't think inlining is a good idea)

=> WC (Term d KVerb)
-> [(Src, BinderType m)] -- Expected
-> [(Tgt, BinderType m)] -- Actual
-> Checking [(Src, BinderType m)]
checkInputs _ overs [] = pure overs
checkInputs tm@(WC fc _) (o:overs) (u:unders) = localFC fc $ do
wrapError (addRowContext ?my (o:overs) (u:unders)) $ checkWire ?my tm False o u
checkInputs tm overs unders
where
addRowContext :: Show (BinderType m)
=> Modey m
-> [(Src, BinderType m)] -- Expected
-> [(Tgt, BinderType m)] -- Actual
-> Error -> Error
addRowContext _ as bs (Err fc (TypeMismatch tm _ _))
= Err fc $ TypeMismatch tm (showRow as) (showRow bs)
addRowContext _ _ _ e = e
checkInputs tm [] unders = typeErr $ "No overs but unders: " ++ showRow unders ++ " for " ++ show tm

checkOutputs :: (CheckConstraints m k, ?my :: Modey m)
checkInputs tm overs unders = checkIO tm overs unders (checkWire ?my tm False) "No overs but unders: "

checkOutputs :: forall m k . (CheckConstraints m k, ?my :: Modey m)
=> WC (Term Syn k)
-> [(Tgt, BinderType m)] -- Expected
-> [(Src, BinderType m)] -- Actual
-> Checking [(Tgt, BinderType m)]
checkOutputs _ unders [] = pure unders
checkOutputs tm@(WC fc _) (u:unders) (o:overs) = localFC fc $ do
wrapError (addRowContext ?my (u:unders) (o:overs)) $ checkWire ?my tm True o u
checkOutputs tm unders overs
where
addRowContext :: Show (BinderType m)
=> Modey m
-> [(Tgt, BinderType m)] -- Expected
-> [(Src, BinderType m)] -- Actual
-> Error -> Error
addRowContext _ as bs (Err fc (TypeMismatch tm _ _))
= Err fc $ TypeMismatch tm (showRow as) (showRow bs)
addRowContext _ _ _ e = e
checkOutputs tm [] overs = typeErr $ "No unders but overs: " ++ showRow overs ++ " for " ++ show tm
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
Expand Down
Loading