------------------------------------------------------------------------
-- The Agda standard library
--
-- Support for system calls as part of reflection
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.External where
import Agda.Builtin.Reflection.External as Builtin
open import Data.Nat.Base using (ℕ; suc; zero; NonZero)
open import Data.List.Base using (List; _∷_; [])
open import Data.Product.Base using (_×_; _,_)
open import Data.String.Base as String using (String; _++_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Unit.Base using (⊤; tt)
open import Function.Base using (case_of_; _$_; _∘_)
open import Reflection hiding (name)
-- Type aliases for the various strings.
CmdName = String
StdIn = String
StdErr = String
StdOut = String
-- Representation for exit codes, assuming 0 is consistently used to
-- indicate success across platforms.
data ExitCode : Set where
exitSuccess : ExitCode
exitFailure : (n : ℕ) {n≢0 : NonZero n} → ExitCode
-- Specification for a command.
record CmdSpec : Set where
constructor cmdSpec
field
name : CmdName -- ^ Executable name (see ~/.agda/executables)
args : List String -- ^ Command-line arguments for executable
input : StdIn -- ^ Contents of standard input
-- Result of running a command.
record Result : Set where
constructor result
field
exitCode : ExitCode -- ^ Exit code returned by the process
output : StdOut -- ^ Contents of standard output
error : StdErr -- ^ Contents of standard error
-- Convert a natural number to an exit code.
toExitCode : ℕ → ExitCode
toExitCode zero = exitSuccess
toExitCode (suc n) = exitFailure (suc n)
-- Quote an exit code as an Agda term.
quoteExitCode : ExitCode → Term
quoteExitCode exitSuccess =
con (quote exitSuccess) []
quoteExitCode (exitFailure n) =
con (quote exitFailure) (vArg (lit (nat n)) ∷ hArg (con (quote tt) []) ∷ [])
-- Quote a result as an Agda term.
quoteResult : Result → Term
quoteResult (result exitCode output error) =
con (quote result) $ vArg (quoteExitCode exitCode)
∷ vArg (lit (string output))
∷ vArg (lit (string error))
∷ []
-- Run command from specification and return the full result.
--
-- NOTE: If the command fails, this macro still succeeds, and returns the
-- full result, including exit code and the contents of stderr.
--
unsafeRunCmdTC : CmdSpec → TC Result
unsafeRunCmdTC c = do
(exitCode , (stdOut , stdErr))
← Builtin.execTC (CmdSpec.name c) (CmdSpec.args c) (CmdSpec.input c)
pure $ result (toExitCode exitCode) stdOut stdErr
macro
unsafeRunCmd : CmdSpec → Term → TC ⊤
unsafeRunCmd c hole = unsafeRunCmdTC c >>= unify hole ∘ quoteResult
-- Show a command for the user.
showCmdSpec : CmdSpec → String
showCmdSpec c = String.unwords $ CmdSpec.name c ∷ CmdSpec.args c
private
-- Helper function for throwing an error from reflection.
userError : ∀ {a} {A : Set a} → CmdSpec → StdOut × StdErr → TC A
userError c (stdout , stderr) = typeError (strErr errMsg ∷ [])
where
errMsg : String
errMsg = String.unlines
$ ("Error while running command '" ++ showCmdSpec c ++ "'")
∷ ("Input:\n" ++ CmdSpec.input c)
∷ ("Output:\n" ++ stdout)
∷ ("Error:\n" ++ stderr)
∷ []
-- Run command from specification. If the command succeeds, it returns the
-- contents of stdout. Otherwise, it throws a type error with the contents
-- of stderr.
runCmdTC : CmdSpec → TC StdOut
runCmdTC c = do
r ← unsafeRunCmdTC c
let debugPrefix = ("user." ++ CmdSpec.name c)
case Result.exitCode r of λ
{ exitSuccess → do
debugPrint (debugPrefix ++ ".stderr") 10 (strErr (Result.error r) ∷ [])
pure $ Result.output r
; (exitFailure n) → do
userError c (Result.output r , Result.error r)
}
macro
runCmd : CmdSpec → Term → TC ⊤
runCmd c hole = runCmdTC c >>= unify hole ∘ lit ∘ string
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