    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Calling external processes
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module System.Process where

    open import Level using (Level)
    open import Data.List.Base using (List)
    open import Data.Product.Base using (_×_; proj₁)
    open import Data.String.Base using (String)
    open import Data.Unit.Polymorphic using (⊤)
    open import Foreign.Haskell.Coerce
    open import IO.Base

    open import System.Exit
    import System.Process.Primitive as Prim

    private
      variable
        ℓ : Level

    callCommand : String → IO {ℓ} ⊤
    callCommand cmd = lift′ (Prim.callCommand cmd)

    system : String → IO ExitCode
    system cmd = lift (Prim.system cmd)

    callProcess : String → List String → IO {ℓ} ⊤
    callProcess exe args = lift′ (Prim.callProcess exe args)

    readProcess
        : String       -- Filename of the executable
        → List String  -- any arguments
        → String       -- standard input
        → IO String    -- stdout
    readProcess exe args stdin = lift (Prim.readProcess exe args stdin)

    readProcessWithExitCode
        : String                           -- Filename of the executable
        → List String                      -- any arguments
        → String                           -- standard input
        → IO (ExitCode × String × String)  -- exitcode, stdout, stderr
    readProcessWithExitCode exe args stdin =
      lift (coerce Prim.readProcessWithExitCode exe args stdin)

    callProcessWithExitCode : String → List String → IO ExitCode
    callProcessWithExitCode exe args = proj₁ <$> readProcessWithExitCode exe args ""