[refactor] pull1Port: use partition from Data.List

brat/Brat/Checker/Helpers.hs

@@ -39,6 +39,7 @@
 import Control.Monad.Freer (req)
 import Data.Bifunctor
 import Data.Foldable (foldrM)
+import Data.List (partition)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 import qualified Data.Map as M
 import Prelude hiding (last)
@@ -121,13 +122,10 @@
   pull1Port :: PortName
             -> [(a, ty)]
             -> Checking ((a, ty), [(a, ty)])
-  pull1Port p [] = fail $ "Port not found: " ++ p ++ " in " ++ showFn types
-  pull1Port p (x@(a,_):xs)
-   | p == toPort a
-   = if p `elem` (toPort . fst <$> xs)
-     then err (AmbiguousPortPull p (showFn (x:xs)))
-     else pure (x, xs)
-   | otherwise = second (x:) <$> pull1Port p xs
+  pull1Port p available = case partition ((== p) . toPort . fst) available of
+      ([], _) -> err $ BadPortPull $ "Port not found: " ++ p ++ " in " ++ showFn available
+      ([found], remaining) -> pure (found, remaining)
+      (_, _) -> err $ AmbiguousPortPull p (showFn available)
 
 ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking ()
 ensureEmpty _ [] = pure ()
@@ -310,7 +308,7 @@
     pure src
 
   mkMono :: Monotone (VVar Z) -> Checking Src
   mkMono (Linear (VPar (ExEnd e))) = pure (NamedPort e "mono")
   mkMono (Full sm) = do
     (_, [], [(twoSrc,_)], _) <- next "2" (Const (Num 2)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
     (_, [(lhs,_),(rhs,_)], [(powSrc,_)], _) <- next "2^" (ArithNode Pow) (S0, Some (Zy :* S0))
@@ -337,7 +335,7 @@
             -> (Src, CTy m Z) -- The input to this level of mapfun
             -> Checking (Src, CTy m Z)
   mkMapFun (lenSrc, len) (valSrc, cty) = do
     let weak1 = changeVar (Thinning (ThDrop ThNull))
     vecFun <- vectorisedFun len my cty
     (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right (VFun my' cty))], _) <-
       next "MapFun" MapFun (S0, Some (Zy :* S0))