Merge branch 'agda5000' of https://github.com/agda/agda-stdlib into agda5000

Conflicts:
	.travis.yml

Author: andreasabel

.travis.yml

@@ -112,6 +112,9 @@ matrix:
         # setting up travis-specific scripts and files
         - cp travis/* .
 
+        # create a suitable Agda `executables` file for examples in README using `Reflection.External`
+        - echo -e "/usr/bin/expr\n" ~/.agda/executables
+
       before_script:
         - export AGDA_OPTIONS="-Werror"
         - export RTS_OPTIONS="+RTS -M3.5G -H3.5G -A128M -RTS"

CHANGELOG.md

@@ -6,6 +6,9 @@ The library has been tested using Agda 2.6.2
 Highlights
 ----------
 
+* New module for making system calls during type checking, `Reflection.External`,
+  which re-exports `Agda.Builtin.Reflection.External`.
+
 Bug-fixes
 ---------
 
@@ -52,6 +55,12 @@ Deprecated names
 New modules
 -----------
 
+* New module for making system calls during type checking:
+  ```agda
+  Reflection.External
+  ```
+  which re-exports and augments the contents of `Agda.Builtin.Reflection.External`.
+
 * Added `Reflection.Traversal` for generic de Bruijn-aware traversals of reflected terms.
 * Added `Reflection.DeBruijn` with weakening, strengthening and free variable operations
   on reflected terms.

README/Reflection/External.agda

@@ -0,0 +1,60 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- How to use reflection to call external functions.
+--
+-- IMPORTANT: In order for this file to type-check you will need to add
+-- a line `/usr/bin/expr` to your `~/.agda/executables` file. See the
+-- section on Reflection in the Agda user manual for more details.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --allow-exec #-}
+
+module README.Reflection.External where
+
+open import Data.List.Base using ([]; _∷_)
+open import Data.String.Base using (String; _++_)
+open import Relation.Binary.PropositionalEquality
+
+-- All the commands needed to make an external system call are included
+-- in `Reflection.External`.
+
+open import Reflection.External
+  using (CmdSpec; runCmd)
+
+-- The most important one is `CmdSpec` ("command specification")
+-- which allows ones to specify the external command being called, its
+-- arguments and the contents of stdin.
+
+-- Here we define a simple command spec that takes two numbers and
+-- uses the Unix `expr` command to add the two together.
+
+add : String → String → CmdSpec
+add x y = record
+  { name  = "expr"
+  ; args  = x ∷ "+" ∷ y  ∷ []
+  ; input = ""
+  }
+
+-- The command can then be run using the `runCmd` macro. If no error
+-- occured then by default the macro returns the result of `stdout`.
+-- Otherwise the macro will terminate with a type error.
+
+test : runCmd (add "1" "2") ≡ "3\n"
+test = refl
+
+-- If you are running a command that you know might be ill-formed
+-- and result in an error then can use `unsafeRunCmd` instead that
+-- returns a `Result` object containing the exit code and the contents
+-- of both `stdout` and `stderr`.
+
+open import Reflection.External
+  using (unsafeRunCmd; result; exitFailure)
+
+error = "/usr/bin/expr: non-integer argument\n"
+
+test2 : unsafeRunCmd (add "a" "b") ≡ result (exitFailure 2) "" error
+test2 = refl
+
+-- For a more advanced use-case where SMT solvers are invoked from
+-- Agda, see Schmitty (https://github.com/wenkokke/schmitty)

src/Reflection/External.agda

@@ -0,0 +1,123 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Support for system calls as part of reflection
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --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 using (_×_; _,_)
+open import Data.String.Base as String using (String; _++_)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Unit.Base using (⊤; tt)
+open import Function 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)
+  return $ 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) ∷ [])
+      return $ 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