如何在Idris中調用子進程？

Question

Idris標準庫（或第三方庫）中是否有一個模塊允許其他程序執行？我在考慮Python的模塊subprocess和Haskell的System.Process。

理想情況下，我想以編程方式與進程交互（寫入其標準輸入，從標準輸出讀取等）。

Answer 1

有一個system : String -> IO Int函數，它接受一個shell命令，運行它並返回它的退出代碼。你需要import System使用它：

import System 

main : IO() 
main = do 
    exitCode <- system "echo HelloWorld!" 
    putStrLn $ "Exit code: " ++ show exitCode 

    exitCode <- system "echo HelloWorld!; false" 
    putStrLn $ "Exit code: " ++ show exitCode 

在我的系統下面的輸出上面的代碼的結果：

HelloWorld! 
Exit code: 0 
HelloWorld! 
Exit code: 256 

我希望它在第二返回1代替256案件。至少這是echo $?顯示的內容。

---

另一個版本可以製成基礎上Effects庫，該庫在this教程描述：

import Effects 
import Effect.System 
import Effect.StdIO 

execAndPrint : (cmd : String) -> Eff() [STDIO, SYSTEM] 
execAndPrint cmd = do 
    exitCode <- system cmd 
    putStrLn $ "Exit code: " ++ show exitCode 

script : Eff() [STDIO, SYSTEM] 
script = do 
    execAndPrint "echo HelloWorld!" 
    execAndPrint "sh -c \"echo HelloWorld!; exit 1\"" 

main : IO() 
main = run script 

在這裏我們需要解釋伊德里斯它所需要的Effects包：

idris -p effects <filename.idr> 

---

我不知道任何Idris libr ary，可讓您輕鬆使用子進程的stdin/stdout。作爲一種解決方法，我們可以使用C的管道工具，利用其功能，這些功能在Idris標準庫中都具有綁定功能。 讓我來告訴我們如何可以，例如，從子進程的標準輸出讀取（請記住，這是一個簡單的代碼片段，其中最基本的錯誤處理）：

import System 

-- read the contents of a file 
readFileH : (fileHandle : File) -> IO String 
readFileH h = loop "" 
    where 
    loop acc = do 
     if !(fEOF h) then pure acc 
     else do 
     Right l <- fGetLine h | Left err => pure acc 
     loop (acC++ l) 

execAndReadOutput : (cmd : String) -> IO String 
execAndReadOutput cmd = do 
    Right fh <- popen cmd Read | Left err => pure "" 
    contents <- readFileH fh 
    pclose fh 
    pure contents 

main : IO() 
main = do 
    out <- (execAndReadOutput "echo \"Captured output\"") 
    putStrLn "Here is what we got:" 
    putStr out 

當你運行程序，你應該看到

Here is what we got: 
Captured output