mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
[ refactor ] lift partitionEithers to toplevel
This commit is contained in:
parent
b19a8e0a2c
commit
e277054fda
@ -23,6 +23,8 @@ import Data.StringMap
|
||||
import System.Directory
|
||||
import System.File
|
||||
|
||||
import Utils.Either
|
||||
|
||||
%default covering
|
||||
|
||||
record ModTree where
|
||||
@ -162,7 +164,7 @@ buildMod loc num len mod
|
||||
-- We'd expect any errors in nsToPath to have been caught by now
|
||||
-- since the imports have been built! But we still have to check.
|
||||
depFilesE <- traverse (nsToPath loc) (imports mod)
|
||||
let (ferrs, depFiles) = getEithers depFilesE
|
||||
let (ferrs, depFiles) = partitionEithers depFilesE
|
||||
ttcTime <- catch (do t <- fnameModified mttc
|
||||
pure (Just t))
|
||||
(\err => pure Nothing)
|
||||
@ -193,16 +195,6 @@ buildMod loc num len mod
|
||||
else do emitWarnings
|
||||
traverse_ emitError ferrs
|
||||
pure ferrs
|
||||
where
|
||||
getEithers : List (Either a b) -> (List a, List b)
|
||||
getEithers [] = ([], [])
|
||||
getEithers (Left x :: es)
|
||||
= let (ls, rs) = getEithers es in
|
||||
(x :: ls, rs)
|
||||
getEithers (Right y :: es)
|
||||
= let (ls, rs) = getEithers es in
|
||||
(ls, y :: rs)
|
||||
|
||||
|
||||
buildMods : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
|
@ -5,3 +5,13 @@ module Utils.Either
|
||||
export
|
||||
mapError : (a -> c) -> Either a b -> Either c b
|
||||
mapError f e = either (Left . f) (Right . id) e
|
||||
|
||||
export
|
||||
partitionEithers : List (Either a b) -> (List a, List b)
|
||||
partitionEithers [] = ([], [])
|
||||
partitionEithers (Left x :: es)
|
||||
= let (ls, rs) = partitionEithers es in
|
||||
(x :: ls, rs)
|
||||
partitionEithers (Right y :: es)
|
||||
= let (ls, rs) = partitionEithers es in
|
||||
(ls, y :: rs)
|
||||
|
Loading…
Reference in New Issue
Block a user