acbcadb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unrelated misc golf.

Mostly about using util methods like `fromMaybe` & friends. Also, not sure why there was `forkOS` instead of `forkIO`.

commitacbcadbbdd45739630644c00187f3dad00c637a6 authorLeif Warner <abimelech@gmail.com> dateFri 4 Dec 2015, 21:36 (11 years ago) parentbf4bdcc

3 files changed+10−23

compare with master

unifiedsplit

src/IRTS/System.hs+3−7 src/Idris/ProofSearch.hs+1−2 src/Idris/REPL.hs+6−14

src/IRTS/System.hs+3−7

@@ -21,10 +21,7 @@ getCC :: IO String

2121getCC = fromMaybe "gcc" <$> environment "IDRIS_CC"

2222

2323getEnvFlags :: IO [String]

24−getEnvFlags = do flags <- environment "IDRIS_CFLAGS"

25− case flags of

26− Nothing -> return $ []

27− Just s -> return $ splitOn " " s

24+getEnvFlags = maybe [] (splitOn " ") <$> environment "IDRIS_CFLAGS"

2825

2926mvnCommand :: String

3027#ifdef mingw32_HOST_OS

@@ -37,9 +34,8 @@ getMvn :: IO String

3734getMvn = fromMaybe mvnCommand <$> environment "IDRIS_MVN"

3835

3936environment :: String -> IO (Maybe String)

40−environment x = catchIO (do e <- getEnv x

41− return (Just e))

42− (\_ -> return Nothing)

37+environment x = catchIO (Just <$> getEnv x)

38+ (\_ -> return Nothing)

4339

4440getTargetDir :: IO String

4541getTargetDir = environment "TARGET" >>= maybe getDataDir return

src/Idris/ProofSearch.hs+1−2

@@ -478,8 +478,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

478478 return (num + 1)

479479 _ -> return 0

480480

481− solven 0 = return ()

482− solven n = do solve; solven (n - 1)

481+ solven n = replicateM_ n solve

483482

484483 resolve n depth

485484 | depth == 0 = fail $ "Can't resolve type class"

src/Idris/REPL.hs+6−14

@@ -126,10 +126,8 @@ repl orig mods efile

126126 do ms <- H.catch (lift $ processInput input orig mods efile)

127127 (ctrlC (return (Just mods)))

128128 case ms of

129− Just mods -> let efile' = case mods of

130− [] -> efile

131− (e:_) -> e in

132− repl orig mods efile'

129+ Just mods -> let efile' = fromMaybe efile (listToMaybe mods)

130+ in repl orig mods efile'

133131 Nothing -> return ()

134132-- ctrlC)

135133-- ctrlC

@@ -154,15 +152,13 @@ repl orig mods efile

154152

155153-- | Run the REPL server

156154startServer :: PortID -> IState -> [FilePath] -> Idris ()

157−startServer port orig fn_in = do tid <- runIO $ forkOS (serverLoop port)

155+startServer port orig fn_in = do tid <- runIO $ forkIO (serverLoop port)

158156 return ()

159157 where serverLoop port = withSocketsDo $

160158 do sock <- listenOnLocalhost port

161159 loop fn orig { idris_colourRepl = False } sock

162160

163− fn = case fn_in of

164− (f:_) -> f

165− _ -> ""

161+ fn = fromMaybe "" (listToMaybe fn_in)

166162

167163 loop fn ist sock

168164 = do (h,_,_) <- accept sock

@@ -276,9 +272,7 @@ idemode h orig mods

276272 i <- getIState

277273 putIState $ i { idris_outputmode = (IdeMode id h) }

278274 idrisCatch -- to report correct id back!

279− (do let fn = case mods of

280− (f:_) -> f

281− _ -> ""

275+ (do let fn = fromMaybe "" (listToMaybe mods)

282276 case IdeMode.sexpToCommand sexp of

283277 Just cmd -> runIdeModeCommand h id orig fn mods cmd

284278 Nothing -> iPrintError "did not understand" )

@@ -683,9 +677,7 @@ processInput cmd orig inputs efile

683677 = do i <- getIState

684678 let opts = idris_options i

685679 let quiet = opt_quiet opts

686− let fn = case inputs of

687− (f:_) -> f

688− _ -> ""

680+ let fn = fromMaybe "" (listToMaybe inputs)

689681 c <- colourise

690682 case parseCmd i "(input)" cmd of

691683 Failure err -> do iputStrLn $ show (fixColour c err)