------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive System.Process simple bindings to Haskell functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module System.Process.Primitive where
open import Level using (Level)
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Foreign.Haskell using (Pair)
open import IO.Primitive.Core using (IO)
open import System.Exit.Primitive using (ExitCode)
postulate
callCommand : String → IO ⊤
system : String → IO ExitCode
callProcess : String → List String → IO ⊤
readProcess
: String -- Filename of the executable
→ List String -- any arguments
→ String -- standard input
→ IO String -- stdout
readProcessWithExitCode
: String -- Filename of the executable
→ List String -- any arguments
→ String -- standard input
→ IO (Pair ExitCode (Pair String String)) -- exitcode, stdout, stderr
{-# FOREIGN GHC import System.Process #-}
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# FOREIGN GHC import MAlonzo.Code.System.Exit.Primitive #-}
{-# COMPILE GHC callCommand = \ cmd -> callCommand (T.unpack cmd) #-}
{-# COMPILE GHC system = \ cmd -> fmap fromExitCode (system (T.unpack cmd)) #-}
{-# COMPILE GHC callProcess = \ exe -> callProcess (T.unpack exe) . map T.unpack #-}
{-# COMPILE GHC readProcess = \ exe args -> fmap T.pack . readProcess (T.unpack exe) (map T.unpack args) . T.unpack #-}
{-# COMPILE GHC readProcessWithExitCode = \ exe args stdin ->
do { (ex, out, err) <- readProcessWithExitCode (T.unpack exe) (map T.unpack args) (T.unpack stdin)
; pure (fromExitCode ex, (T.pack out, T.pack err))
}
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4