    ------------------------------------------------------------------------
    -- 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))
                  }
    #-}