From 9863755ae10daf144d1b00e2f54b7327405a30cb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Feb 2017 09:17:18 -0800
Subject: [PATCH] feat(shell/lean,library/smt): fix SMT2 frontend

---
 library/smt/arith.lean   | 17 +++++++++++++++++
 library/smt/array.lean   | 29 +++++++++++++++++++++++++++++
 library/smt/default.lean |  6 ++++++
 library/smt/prove.lean   | 15 +++++++++++++++
 src/shell/lean.cpp       | 38 +++++++++++++++++++-------------------
 5 files changed, 86 insertions(+), 19 deletions(-)
 create mode 100644 library/smt/arith.lean
 create mode 100644 library/smt/array.lean
 create mode 100644 library/smt/default.lean
 create mode 100644 library/smt/prove.lean

diff --git a/library/smt/arith.lean b/library/smt/arith.lean
new file mode 100644
index 0000000000..1abc311e11
--- /dev/null
+++ b/library/smt/arith.lean
@@ -0,0 +1,17 @@
+-- TODO(Leo): remove after we port reals to new stdlib
+-- Arithmetic
+constants (real : Type)
+
+constants (real_has_zero : has_zero real)
+constants (real_has_one : has_one real)
+constants (real_has_add : has_add real)
+constants (real_has_mul : has_mul real)
+constants (real_has_sub : has_sub real)
+constants (real_has_neg : has_neg real)
+constants (real_has_div : has_div real)
+constants (real_has_lt : has_lt real)
+constants (real_has_le : has_le real)
+
+attribute [instance] real_has_zero real_has_one real_has_add real_has_mul real_has_sub real_has_neg real_has_div real_has_le real_has_lt
+
+constants (real.of_int : int → real) (real.to_int : real → int) (real.is_int : real → Prop)
diff --git a/library/smt/array.lean b/library/smt/array.lean
new file mode 100644
index 0000000000..36c8f7ca85
--- /dev/null
+++ b/library/smt/array.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+namespace smt
+def array (α β : Type) := α → β
+
+variables {α β : Type}
+open tactic
+
+def select (a : array α β) (i : α) : β :=
+a i
+
+lemma arrayext (a₁ a₂ : array α β) : (∀ i, select a₁ i = select a₂ i) → a₁ = a₂ :=
+funext
+
+variable [decidable_eq α]
+
+def store (a : array α β) (i : α) (v : β) : array α β :=
+λ j, if j = i then v else select a j
+
+@[simp] lemma select_store (a : array α β) (i : α) (v : β) : select (store a i v) i = v :=
+by unfold smt.store smt.select; dsimp; rewrite if_pos; reflexivity
+
+@[simp] lemma select_store_ne (a : array α β) (i j : α) (v : β) : j ≠ i → select (store a i v) j = select a j :=
+by intros; unfold smt.store smt.select; dsimp; rewrite if_neg; assumption
+
+end smt
diff --git a/library/smt/default.lean b/library/smt/default.lean
new file mode 100644
index 0000000000..b8b2afb7bd
--- /dev/null
+++ b/library/smt/default.lean
@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+import smt.arith smt.array smt.prove
diff --git a/library/smt/prove.lean b/library/smt/prove.lean
new file mode 100644
index 0000000000..04501e2d19
--- /dev/null
+++ b/library/smt/prove.lean
@@ -0,0 +1,15 @@
+namespace smt
+open tactic
+
+private meta def collect_props : list expr → tactic (list expr)
+| []        := return []
+| (H :: Hs) := do
+  Eqs   ← collect_props Hs,
+  Htype ← infer_type H >>= whnf,
+  return $ if Htype = expr.prop then (H :: Eqs) else Eqs
+
+meta def prove : tactic unit :=
+do local_context >>= collect_props >>= revert_lst,
+   simp
+
+end smt
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 31e3bb76af..d397d299c8 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -398,25 +398,6 @@ int main(int argc, char ** argv) {
 
     io_state ios(opts, lean::mk_pretty_formatter_factory());
 
-    if (smt2) {
-        // Note: the smt2 flag may override other flags
-        bool ok = true;
-        for (int i = optind; i < argc; i++) {
-            try {
-                if (doc) throw lean::exception("leandoc does not support .smt2 files");
-                ok = ::lean::smt2::parse_commands(env, ios, argv[i]);
-            } catch (lean::exception & ex) {
-                ok = false;
-                type_context tc(env, ios.get_options());
-                simple_pos_info_provider pp(argv[i]);
-                lean::message_builder(&pp, std::make_shared<type_context>(env, ios.get_options()),
-                                      env, ios, argv[i], pos_info(1, 1), lean::ERROR)
-                        .set_exception(ex).report();
-            }
-        }
-        return ok ? 0 : 1;
-    }
-
 #if defined(LEAN_JSON)
     if (opts.get_bool("server")) {
         /* Disable assertion violation dialog:
@@ -447,6 +428,25 @@ int main(int argc, char ** argv) {
     scoped_message_buffer scope_msg_buf(msg_buf.get());
     scope_message_context scope_msg_ctx(message_bucket_id { "_global", 1 });
 
+    if (smt2) {
+        // Note: the smt2 flag may override other flags
+        bool ok = true;
+        for (int i = optind; i < argc; i++) {
+            try {
+                if (doc) throw lean::exception("leandoc does not support .smt2 files");
+                ok = ::lean::smt2::parse_commands(env, ios, argv[i]);
+            } catch (lean::exception & ex) {
+                ok = false;
+                type_context tc(env, ios.get_options());
+                simple_pos_info_provider pp(argv[i]);
+                lean::message_builder(&pp, std::make_shared<type_context>(env, ios.get_options()),
+                                      env, ios, argv[i], pos_info(1, 1), lean::ERROR)
+                        .set_exception(ex).report();
+            }
+        }
+        return ok ? 0 : 1;
+    }
+
     try {
         std::vector<std::string> args(argv + optind, argv + argc);
         if (recursive) {