feat(library/vm/process): add basic process support

.clang-format

@@ -0,0 +1,5 @@
+---
+
+BreakBeforeBraces: 'Attach'
+
+IndentWidth: 4

library/system/io.lean

@@ -1,9 +1,10 @@
 /-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
 -/
 import data.buffer
+import system.process
 
 inductive io.error
 | other     : string → io.error
@@ -16,9 +17,8 @@ structure io.terminal (m : Type → Type → Type) :=
 inductive io.mode
 | read | write | read_write | append
 
-structure io.file_system (m : Type → Type → Type) :=
+structure io.file_system (handle : Type) (m : Type → Type → Type) :=
 /- Remark: in Haskell, they also provide  (Maybe TextEncoding) and  NewlineMode -/
-(handle         : Type)
 (read_file      : string → bool → m io.error char_buffer)
 (mk_file_handle : string → io.mode → bool → m io.error handle)
 (is_eof         : handle → m io.error bool)
@@ -36,8 +36,12 @@ class io.interface :=
 (monad    : Π e, monad (m e))
 (catch    : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α)
 (fail     : Π e α, e → m e α)
+-- Primitive Types
+(handle   : Type)
+-- Interface Extensions
 (term     : io.terminal m)
-(fs       : io.file_system m)
+(fs       : io.file_system handle m)
+(process  : io.process io.error handle m)
 
 variable [io.interface]
 
@@ -74,7 +78,7 @@ def print_ln {α} [has_to_string α] (s : α) : io unit :=
 print s >> put_str "\n"
 
 def handle : Type :=
-interface.fs.handle
+interface.handle
 
 def mk_file_handle (s : string) (m : mode) (bin : bool := ff) : io handle :=
 interface.fs.mk_file_handle s m bin
@@ -137,4 +141,23 @@ format.print_using (to_fmt a) o
 meta definition pp {α : Type} [has_to_format α] (a : α) : io unit :=
 format.print (to_fmt a)
 
+/-- Run the external process named by `cmd`, supplied with the arguments `args`.
+
+    The process will run to completion with its output captured by a pipe, and
+    read into `string` which is then returned.
+-/
+def io.cmd [io.interface] (cmd : string) (args : list string) : io string :=
+do let proc : process := {
+    cmd := cmd,
+    args := args,
+    stdout := process.stdio.piped
+  },
+  child ← interface.process^.spawn proc,
+  let inh := child^.stdin,
+  let outh := child^.stdout,
+  let errh := child^.stderr,
+  buf ← io.fs.read outh 1024,
+  return buf^.to_string
+
+/-- Lift a monadic `io` action into the `tactic` monad. -/
 meta constant tactic.run_io {α : Type} : (Π ioi : io.interface, @io ioi α) → tactic α

library/system/process.lean

@@ -0,0 +1,25 @@
+import init.data.list.basic
+
+inductive process.stdio
+| piped
+| inherit
+| null
+
+structure process :=
+(cmd : string)
+/- Add an argument to pass to the process. -/
+(args : list string)
+/- Configuration for the process's stdin handle. -/
+(stdin := stdio.inherit)
+/- Configuration for the process's stdout handle. -/
+(stdout := stdio.inherit)
+/- Configuration for the process's stderr handle. -/
+(stderr := stdio.inherit)
+
+structure process.child (handle : Type) :=
+(stdin : handle)
+(stdout : handle)
+(stderr : handle)
+
+structure io.process (err : Type) (handle : Type) (m : Type → Type → Type) :=
+(spawn : process → m err (process.child handle))

library/tools/smt2/builder.lean

@@ -0,0 +1,48 @@
+import .syntax
+
+@[reducible] def smt2.builder (α : Type) := state (list smt2.cmd) α
+
+meta def smt2.builder.to_format {α : Type} (build : smt2.builder α) : format :=
+format.join $ list.map to_fmt $ (build [])^.snd
+
+meta instance (α : Type) : has_to_format (smt2.builder α) :=
+⟨ smt2.builder.to_format ⟩
+
+namespace smt2
+
+namespace builder
+
+def add_command (c : cmd) : builder unit := do
+cs ← state.read,
+state.write (c :: cs)
+
+def echo (msg : string) : builder unit :=
+add_command (cmd.echo msg)
+
+def check_sat : builder unit :=
+add_command cmd.check_sat
+
+def pop (n : nat) : builder unit :=
+add_command $ cmd.pop n
+
+def push (n : nat) : builder unit :=
+add_command $ cmd.push n
+
+def scope {α} (level : nat) (action : builder α) : builder α :=
+do push level,
+   res ← action,
+   pop level,
+   return res
+
+def reset : builder unit :=
+add_command cmd.reset
+
+def exit' : builder unit :=
+add_command cmd.exit_cmd
+
+def declare_const (sym : string) (s : sort) : builder unit :=
+add_command $ cmd.declare_const sym s
+
+end builder
+
+end smt2

library/tools/smt2/default.lean

@@ -0,0 +1,37 @@
+import system.io
+import system.process
+import .solvers.z3
+import .syntax
+import .builder
+
+meta def smt2 [io.interface] (build : smt2.builder unit) : io string :=
+do z3 ← z3_instance.start,
+   io.put_str (to_string $ to_fmt build),
+   res ← z3^.raw (to_string $ to_fmt build),
+   io.put_str res,
+   return res
+
+open tactic
+open smt2
+open smt2.builder
+
+meta def reflect_prop (e : expr) : tactic (builder unit) :=
+do p ← is_prop e,
+   if p
+   then do
+       trace e,
+       n ← mk_fresh_name,
+       return $ declare_const (to_string n) "Bool"
+   else return (return ())
+
+meta def reflect_context : tactic (builder unit) :=
+do ls ← local_context,
+   bs ← monad.mapm reflect_prop ls,
+   return $ list.foldl (λ (a b : builder unit), a >> b) (return ()) bs
+
+meta def reflect : tactic unit :=
+do tgt ← target,
+   b ← reflect_context,
+   str ← run_io (λ ioi, @smt2 ioi b),
+   tactic.trace str,
+   return ()

library/tools/smt2/solvers/z3.lean

@@ -0,0 +1,30 @@
+import system.io
+import system.process
+import data.buffer
+
+open process
+
+structure z3_instance [io.interface] : Type :=
+  (process : child io.handle)
+
+def spawn [ioi : io.interface] : process → io (child io.handle) :=
+io.interface.process^.spawn
+
+def z3_instance.start  [io.interface] : io z3_instance :=
+do let proc : process := {
+       cmd := "z3",
+       args := ["-smt2", "-in"],
+       stdin := stdio.piped,
+       stdout := stdio.piped
+    },
+    z3_instance.mk <$> spawn proc
+
+def z3_instance.raw [io.interface] (z3 : z3_instance) (cmd : string) : io string :=
+do let z3_stdin := z3^.process^.stdin,
+   let z3_stdout := z3^.process^.stdout,
+   let cs := cmd^.reverse^.to_buffer,
+   io.fs.write z3_stdin cs,
+   io.fs.close z3_stdin,
+   -- need read all
+   res ← io.fs.read z3_stdout 1024,
+   return res^.to_string

library/tools/smt2/syntax.lean

@@ -0,0 +1,87 @@
+namespace smt2
+
+@[reducible] def symbol : Type := string
+@[reducible] def identifier : Type := string
+
+inductive special_constant : Type
+| number : int → special_constant
+| string : string → special_constant
+
+inductive sort : Type
+| id : identifier → sort
+| apply : identifier → list sort → sort
+
+instance : has_coe string sort :=
+⟨ fun str, sort.id str ⟩
+
+meta def sort.to_format : sort → format
+| (sort.id i) := to_fmt i
+| (sort.apply _ _) := "NYI"
+
+meta instance sort_has_to_fmt : has_to_format sort :=
+⟨ sort.to_format ⟩
+
+inductive attr : Type
+
+inductive qualified_name : Type
+| id : identifier → qualified_name
+| qual_id : identifier → sort → qualified_name
+
+inductive term : Type
+| qual_id : qualified_name → term
+| const : special_constant → term
+| apply : qualified_name → list term → term
+| letb : list (name × term) → term → term
+| forallq : list (symbol × sort) → term → term
+| existsq : list (symbol × sort) → term → term
+| annotate : term → list attr → term
+
+inductive fun_def : Type
+inductive info_flag : Type
+inductive keyword : Type
+inductive option : Type
+
+inductive cmd : Type
+| assert_cmd : term → cmd
+| check_sat : cmd
+| check_sat_assuming : term → cmd -- not complete
+| declare_const : symbol → sort → cmd
+| declare_fun : symbol → list sort → cmd
+| declare_sort : symbol → nat → cmd
+| define_fun : fun_def → cmd
+| define_fun_rec : fun_def → cmd
+| define_funs_rec : cmd -- not complete
+| define_sort : symbol → list symbol → sort → cmd
+| echo : string → cmd
+| exit_cmd : cmd
+| get_assertions : cmd
+| get_assignment : cmd
+| get_info : info_flag → cmd
+| get_model : cmd
+| get_option : keyword → cmd
+| get_proof : cmd
+| get_unsat_assumtpions : cmd
+| get_unsat_core : cmd
+| get_value : cmd -- not complete
+| pop : nat → cmd
+| push : nat → cmd
+| reset : cmd
+| reset_assertions : cmd
+| set_info : attr → cmd
+| set_logic : symbol → cmd
+| set_opt : option → cmd
+
+open cmd
+
+meta def string_lit (s : string) : format :=
+format.bracket "\"" "\"" (to_fmt s)
+
+meta def cmd.to_format : cmd → format
+| (echo msg) := "(echo " ++ string_lit msg ++ ")\n"
+| (declare_const sym srt) := "(declare-const " ++ sym ++ " " ++ to_fmt srt ++ ")"
+| _ := "NYI"
+
+meta instance : has_to_format cmd :=
+⟨ cmd.to_format ⟩
+
+end smt2

src/library/CMakeLists.txt

@@ -19,4 +19,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   mt_task_queue.cpp st_task_queue.cpp
   library_task_builder.cpp
   messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
-  documentation.cpp check.cpp arith_instance.cpp parray.cpp)
+  documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp
+  pipe.cpp handle.cpp)

src/library/handle.cpp

@@ -0,0 +1,77 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author:  Leonardo de Moura & Jared Roesch
+*/
+#include <string>
+#include <fstream>
+#include <iostream>
+#include <iomanip>
+#include <utility>
+#include <stdio.h>
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#include <windows.h>
+#include <tchar.h>
+#include <strsafe.h>
+#else
+#include <sys/wait.h>
+#include <unistd.h>
+#endif
+
+#include "library/process.h"
+#include "library/handle.h"
+#include "util/buffer.h"
+#include "library/pipe.h"
+
+
+namespace lean {
+
+void handle::write(buffer<char> & buf) {
+    auto sz = buf.size();
+    if (fwrite(buf.data(), 1, sz, m_file) != sz) {
+        std::cout << "write_error: " << errno << std::endl;
+        clearerr(m_file);
+        throw handle_exception("write failed");
+    }
+}
+
+void handle::flush() {
+    if (fflush(m_file) != 0) {
+        clearerr(m_file);
+        throw handle_exception("flush failed");
+    }
+}
+
+handle::~handle() {
+    if (m_file && m_file != stdin &&
+        m_file != stderr && m_file != stdout) {
+        fclose(m_file);
+    }
+}
+
+bool handle::is_stdin() {
+    return m_file == stdin;
+}
+
+bool handle::is_stdout() {
+    return m_file == stdout;
+}
+
+bool handle::is_stderr() {
+    return m_file == stderr;
+}
+
+void handle::close() {
+    if (fclose(m_file) == 0) {
+        m_file = nullptr;
+    } else {
+        clearerr(m_file);
+        throw handle_exception("close failed");
+    }
+}
+
+bool handle::is_closed() { return !m_file; }
+
+}