From 75145c29efeccb86151daedd7838ce8e425c8f05 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 25 Jul 2016 09:27:14 -0700 Subject: [PATCH] refactor(library/smt): move smt files from algebra --- library/init/classical.lean | 2 ++ library/init/logic.lean | 3 ++ library/{algebra/smt2.lean => smt/arith.lean} | 17 ---------- library/smt/default.lean | 6 ++++ library/smt/prove.lean | 5 +++ src/frontends/smt2/elaborator.cpp | 30 +++++------------ src/frontends/smt2/parser.cpp | 7 ++-- src/library/constants.cpp | 32 ++++++++++++------- src/library/constants.h | 8 +++-- src/library/constants.txt | 8 +++-- 10 files changed, 56 insertions(+), 62 deletions(-) rename library/{algebra/smt2.lean => smt/arith.lean} (72%) create mode 100644 library/smt/default.lean create mode 100644 library/smt/prove.lean diff --git a/library/init/classical.lean b/library/init/classical.lean index d62820fce0..323f5833c2 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -179,6 +179,8 @@ inhabited_of_nonempty noncomputable definition prop_decidable [instance] [priority 0] (a : Prop) : decidable a := arbitrary (decidable a) +noncomputable definition type_decidable_eq [instance] [priority 0] (A : Type) : decidable_eq A := _ + noncomputable definition type_decidable (A : Type) : sum A (A → false) := match prop_decidable (nonempty A) with | tt Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp)) diff --git a/library/init/logic.lean b/library/init/logic.lean index 083e801f6f..ac94ff42ba 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -288,6 +288,9 @@ assume not_em : ¬(a ∨ ¬a), theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl +/- xor -/ +definition xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a) + /- iff -/ definition iff (a b : Prop) := (a → b) ∧ (b → a) diff --git a/library/algebra/smt2.lean b/library/smt/arith.lean similarity index 72% rename from library/algebra/smt2.lean rename to library/smt/arith.lean index e70ebd39bc..7a2eaf8e44 100644 --- a/library/algebra/smt2.lean +++ b/library/smt/arith.lean @@ -1,8 +1,4 @@ import algebra.ordered_field -import data.map - --- Core -constants (xor : Prop → Prop → Prop) -- Arithmetic constants (int real : Type.{1}) @@ -32,16 +28,3 @@ 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) - --- Arrays --- Note: we don't use map because of the [option] in the return type -universe variables l₁ l₂ -constant (array : Type.{l₁} → Type.{l₂} → Type.{max 1 l₁ l₂}) -namespace array -constant (select : Π (A B : Type), A → array A B → B) -constant (store : Π (A : Type) (B : Type), A → B → array A B → array A B) -end array - -namespace tactic -meta_definition smt2 : tactic unit := trace_state >> now -end tactic 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..dd7eedf6a2 --- /dev/null +++ b/library/smt/prove.lean @@ -0,0 +1,5 @@ +namespace smt +open tactic + +meta_definition prove : tactic unit := trace_state >> now +end smt diff --git a/src/frontends/smt2/elaborator.cpp b/src/frontends/smt2/elaborator.cpp index 397f898fa1..5d839b31f0 100644 --- a/src/frontends/smt2/elaborator.cpp +++ b/src/frontends/smt2/elaborator.cpp @@ -171,37 +171,23 @@ private: expr elaborate_select(buffer & args) { lean_assert(is_constant(args[0]) && const_name(args[0]) == get_select_name()); - // Have: select - // Want: array.select.{1 1} X Y x A expr ty = m_tctx.infer(args[1]); buffer array_args; expr array = get_app_args(ty, array_args); - lean_assert(is_constant(array) && const_name(array) == get_array_name()); - buffer new_args; - new_args.push_back(mk_constant(get_array_select_name(), {l1(), l1()})); - new_args.push_back(array_args[0]); - new_args.push_back(array_args[1]); - new_args.push_back(args[2]); - new_args.push_back(args[1]); - return mk_app(new_args); + lean_assert(is_constant(array) && const_name(array) == get_smt_array_name()); + args[0] = mk_app(mk_constant(get_smt_select_name(), {l1(), l1()}), array_args[0], array_args[1]); + return mk_app(args); } expr elaborate_store(buffer & args) { lean_assert(is_constant(args[0]) && const_name(args[0]) == get_store_name()); - // Have: store - // Want: array.store.{1 1} X Y x y A expr ty = m_tctx.infer(args[1]); buffer array_args; expr array = get_app_args(ty, array_args); - lean_assert(is_constant(array) && const_name(array) == get_array_name()); - buffer new_args; - new_args.push_back(mk_constant(get_array_store_name(), {l1(), l1()})); - new_args.push_back(array_args[0]); - new_args.push_back(array_args[1]); - new_args.push_back(args[2]); - new_args.push_back(args[3]); - new_args.push_back(args[1]); - return mk_app(new_args); + lean_assert(is_constant(array) && const_name(array) == get_smt_array_name()); + expr dec_eq = mk_app(mk_constant(get_classical_type_decidable_eq_name(), {l1()}), array_args[0]); + args[0] = mk_app(mk_constant(get_smt_store_name(), {l1(), l1()}), array_args[0], array_args[1], dec_eq); + return mk_app(args); } expr elaborate_arith(buffer & args, arith_app_info const & info) { @@ -313,7 +299,7 @@ void initialize_elaborator() { {"not", mk_constant(get_not_name())}, {"Int", mk_constant(get_int_name())}, {"Real", mk_constant(get_real_name())}, - {"Array", mk_constant(get_array_name(), {l1(), l1()})}, + {"Array", mk_constant(get_smt_array_name(), {l1(), l1()})}, {"to_real", mk_constant(get_real_of_int_name())}, {"to_int", mk_constant(get_real_to_int_name())}, {"is_int", mk_constant(get_real_is_int_name())} diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp index f3282e14e2..9166a4405f 100644 --- a/src/frontends/smt2/parser.cpp +++ b/src/frontends/smt2/parser.cpp @@ -43,7 +43,6 @@ namespace lean { namespace smt2 { static name * g_smt2_unique_prefix; -static name * g_smt2_tactic; static char const * g_token_use_locals = ":use_locals"; @@ -478,7 +477,7 @@ private: metavar_context mctx; expr goal_mvar = mctx.mk_metavar_decl(lctx(), mk_constant(get_false_name())); vm_obj s = to_obj(tactic_state(env(), ios().get_options(), mctx, list(goal_mvar), goal_mvar)); - vm_obj result = get_tactic_vm_state(env()).invoke(*g_smt2_tactic, s); + vm_obj result = get_tactic_vm_state(env()).invoke(get_smt_prove_name(), s); if (optional s_new = is_tactic_success(result)) { mctx = s_new->mctx(); expr proof = mctx.instantiate_mvars(goal_mvar); @@ -643,7 +642,7 @@ public: optional k; olean_files.push_back(module_name(k, name("init"))); - olean_files.push_back(module_name(k, name({"algebra", "smt2"}))); + olean_files.push_back(module_name(k, name("smt"))); unsigned num_threads = 0; bool keep_imported_theorems = false; @@ -670,12 +669,10 @@ public: void initialize_parser() { g_smt2_unique_prefix = new name(name::mk_internal_unique_name()); // TODO(dhs): write a theorem prover and call that instead - g_smt2_tactic = new name({"tactic", "smt2"}); } void finalize_parser() { delete g_smt2_unique_prefix; - delete g_smt2_tactic; } // Entry point diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 1bc980f082..970adc94ec 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -15,9 +15,6 @@ name const * g_and = nullptr; name const * g_and_elim_left = nullptr; name const * g_and_elim_right = nullptr; name const * g_and_intro = nullptr; -name const * g_array = nullptr; -name const * g_array_select = nullptr; -name const * g_array_store = nullptr; name const * g_bit0 = nullptr; name const * g_bit1 = nullptr; name const * g_bool = nullptr; @@ -31,6 +28,7 @@ name const * g_char = nullptr; name const * g_char_of_nat = nullptr; name const * g_classical = nullptr; name const * g_classical_prop_decidable = nullptr; +name const * g_classical_type_decidable_eq = nullptr; name const * g_combinator_K = nullptr; name const * g_comm_ring = nullptr; name const * g_comm_semiring = nullptr; @@ -284,6 +282,10 @@ name const * g_select = nullptr; name const * g_semiring = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; +name const * g_smt_array = nullptr; +name const * g_smt_select = nullptr; +name const * g_smt_store = nullptr; +name const * g_smt_prove = nullptr; name const * g_sorry = nullptr; name const * g_store = nullptr; name const * g_string = nullptr; @@ -330,9 +332,6 @@ void initialize_constants() { g_and_elim_left = new name{"and", "elim_left"}; g_and_elim_right = new name{"and", "elim_right"}; g_and_intro = new name{"and", "intro"}; - g_array = new name{"array"}; - g_array_select = new name{"array", "select"}; - g_array_store = new name{"array", "store"}; g_bit0 = new name{"bit0"}; g_bit1 = new name{"bit1"}; g_bool = new name{"bool"}; @@ -346,6 +345,7 @@ void initialize_constants() { g_char_of_nat = new name{"char", "of_nat"}; g_classical = new name{"classical"}; g_classical_prop_decidable = new name{"classical", "prop_decidable"}; + g_classical_type_decidable_eq = new name{"classical", "type_decidable_eq"}; g_combinator_K = new name{"combinator", "K"}; g_comm_ring = new name{"comm_ring"}; g_comm_semiring = new name{"comm_semiring"}; @@ -599,6 +599,10 @@ void initialize_constants() { g_semiring = new name{"semiring"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; + g_smt_array = new name{"smt", "array"}; + g_smt_select = new name{"smt", "select"}; + g_smt_store = new name{"smt", "store"}; + g_smt_prove = new name{"smt", "prove"}; g_sorry = new name{"sorry"}; g_store = new name{"store"}; g_string = new name{"string"}; @@ -646,9 +650,6 @@ void finalize_constants() { delete g_and_elim_left; delete g_and_elim_right; delete g_and_intro; - delete g_array; - delete g_array_select; - delete g_array_store; delete g_bit0; delete g_bit1; delete g_bool; @@ -662,6 +663,7 @@ void finalize_constants() { delete g_char_of_nat; delete g_classical; delete g_classical_prop_decidable; + delete g_classical_type_decidable_eq; delete g_combinator_K; delete g_comm_ring; delete g_comm_semiring; @@ -915,6 +917,10 @@ void finalize_constants() { delete g_semiring; delete g_sigma; delete g_sigma_mk; + delete g_smt_array; + delete g_smt_select; + delete g_smt_store; + delete g_smt_prove; delete g_sorry; delete g_store; delete g_string; @@ -961,9 +967,6 @@ name const & get_and_name() { return *g_and; } name const & get_and_elim_left_name() { return *g_and_elim_left; } name const & get_and_elim_right_name() { return *g_and_elim_right; } name const & get_and_intro_name() { return *g_and_intro; } -name const & get_array_name() { return *g_array; } -name const & get_array_select_name() { return *g_array_select; } -name const & get_array_store_name() { return *g_array_store; } name const & get_bit0_name() { return *g_bit0; } name const & get_bit1_name() { return *g_bit1; } name const & get_bool_name() { return *g_bool; } @@ -977,6 +980,7 @@ name const & get_char_name() { return *g_char; } name const & get_char_of_nat_name() { return *g_char_of_nat; } name const & get_classical_name() { return *g_classical; } name const & get_classical_prop_decidable_name() { return *g_classical_prop_decidable; } +name const & get_classical_type_decidable_eq_name() { return *g_classical_type_decidable_eq; } name const & get_combinator_K_name() { return *g_combinator_K; } name const & get_comm_ring_name() { return *g_comm_ring; } name const & get_comm_semiring_name() { return *g_comm_semiring; } @@ -1230,6 +1234,10 @@ name const & get_select_name() { return *g_select; } name const & get_semiring_name() { return *g_semiring; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } +name const & get_smt_array_name() { return *g_smt_array; } +name const & get_smt_select_name() { return *g_smt_select; } +name const & get_smt_store_name() { return *g_smt_store; } +name const & get_smt_prove_name() { return *g_smt_prove; } name const & get_sorry_name() { return *g_sorry; } name const & get_store_name() { return *g_store; } name const & get_string_name() { return *g_string; } diff --git a/src/library/constants.h b/src/library/constants.h index bf1af4fbc4..54f93109df 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -17,9 +17,6 @@ name const & get_and_name(); name const & get_and_elim_left_name(); name const & get_and_elim_right_name(); name const & get_and_intro_name(); -name const & get_array_name(); -name const & get_array_select_name(); -name const & get_array_store_name(); name const & get_bit0_name(); name const & get_bit1_name(); name const & get_bool_name(); @@ -33,6 +30,7 @@ name const & get_char_name(); name const & get_char_of_nat_name(); name const & get_classical_name(); name const & get_classical_prop_decidable_name(); +name const & get_classical_type_decidable_eq_name(); name const & get_combinator_K_name(); name const & get_comm_ring_name(); name const & get_comm_semiring_name(); @@ -286,6 +284,10 @@ name const & get_select_name(); name const & get_semiring_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); +name const & get_smt_array_name(); +name const & get_smt_select_name(); +name const & get_smt_store_name(); +name const & get_smt_prove_name(); name const & get_sorry_name(); name const & get_store_name(); name const & get_string_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 0f0a4385c3..d8faadb7fe 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -10,9 +10,6 @@ and and.elim_left and.elim_right and.intro -array -array.select -array.store bit0 bit1 bool @@ -26,6 +23,7 @@ char char.of_nat classical classical.prop_decidable +classical.type_decidable_eq combinator.K comm_ring comm_semiring @@ -279,6 +277,10 @@ select semiring sigma sigma.mk +smt.array +smt.select +smt.store +smt.prove sorry store string