acbcadb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unrelated misc golf.

acbcadbLeif Warner11 years ago

src/IRTS/System.hs+3−7

compare with master

unifiedsplit

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

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

23getEnvFlags :: IO [String]

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

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

25− case flags of

26− Nothing -> return $ []

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

29mvnCommand :: String

26mvnCommand :: String

30#ifdef mingw32_HOST_OS

27#ifdef mingw32_HOST_OS

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

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

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

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

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

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

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

41− return (Just e))

42− (\_ -> return Nothing)

38+ (\_ -> return Nothing)

44getTargetDir :: IO String

40getTargetDir :: IO String

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

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

src/Idris/ProofSearch.hs+1−2

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

478 return (num + 1)

479 _ -> return 0

480

481− solven 0 = return ()

481+ solven n = replicateM_ n solve

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

483

482

484 resolve n depth

483 resolve n depth

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

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

src/Idris/REPL.hs+6−14

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

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

127 (ctrlC (return (Just mods)))

128 case ms of

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

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

130− [] -> efile

131− (e:_) -> e in

132− repl orig mods efile'

130+ in repl orig mods efile'

133 Nothing -> return ()

131 Nothing -> return ()

134-- ctrlC)

132-- ctrlC)

135-- ctrlC

133-- ctrlC

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

154

152

155-- | Run the REPL server

153-- | Run the REPL server

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

154startServer :: 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)

158 return ()

156 return ()

159 where serverLoop port = withSocketsDo $

157 where serverLoop port = withSocketsDo $

160 do sock <- listenOnLocalhost port

158 do sock <- listenOnLocalhost port

161 loop fn orig { idris_colourRepl = False } sock

159 loop fn orig { idris_colourRepl = False } sock

162

160

163− fn = case fn_in of

161+ fn = fromMaybe "" (listToMaybe fn_in)

164− (f:_) -> f

165− _ -> ""

166

162

167 loop fn ist sock

163 loop fn ist sock

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

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

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

276 i <- getIState

272 i <- getIState

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

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

278 idrisCatch -- to report correct id back!

274 idrisCatch -- to report correct id back!

279− (do let fn = case mods of

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

280− (f:_) -> f

281− _ -> ""

282 case IdeMode.sexpToCommand sexp of

276 case IdeMode.sexpToCommand sexp of

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

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

284 Nothing -> iPrintError "did not understand" )

278 Nothing -> iPrintError "did not understand" )

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

683 = do i <- getIState

677 = do i <- getIState

684 let opts = idris_options i

678 let opts = idris_options i

685 let quiet = opt_quiet opts

679 let quiet = opt_quiet opts

686− let fn = case inputs of

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

687− (f:_) -> f

688− _ -> ""

689 c <- colourise

681 c <- colourise

690 case parseCmd i "(input)" cmd of

682 case parseCmd i "(input)" cmd of

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

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