------------------------------------------------------------------------
-- 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