max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/smt): move smt files from algebra

Browse source
This commit is contained in:
Daniel Selsam 2016-07-25 09:27:14 -07:00 • committed by Leonardo de Moura
parent e946ebc8fc
commit 75145c29ef
10 changed files with 56 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/classical.lean
View file

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

3
library/init/logic.lean
View file

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

17
library/algebra/smt2.lean → library/smt/arith.lean
View file

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

6
library/smt/default.lean Normal file
View file

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

5
library/smt/prove.lean Normal file
View file

@ -0,0 +1,5 @@
namespace smt
open tactic
meta_definition prove : tactic unit := trace_state >> now
end smt

30
src/frontends/smt2/elaborator.cpp
View file

@ -171,37 +171,23 @@ private:
expr elaborate_select(buffer<expr> & args) {
lean_assert(is_constant(args[0]) && const_name(args[0]) == get_select_name());
// Have: select <A : Array X Y> <x : X>
// Want: array.select.{1 1} X Y x A
expr ty = m_tctx.infer(args[1]);
buffer<expr> array_args;
expr array = get_app_args(ty, array_args);
lean_assert(is_constant(array) && const_name(array) == get_array_name());
buffer<expr> 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<expr> & args) {
lean_assert(is_constant(args[0]) && const_name(args[0]) == get_store_name());
// Have: store <A : Array X Y> <x : X> <y : Y>
// Want: array.store.{1 1} X Y x y A
expr ty = m_tctx.infer(args[1]);
buffer<expr> array_args;
expr array = get_app_args(ty, array_args);
lean_assert(is_constant(array) && const_name(array) == get_array_name());
buffer<expr> 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<expr> & 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())}

7
src/frontends/smt2/parser.cpp
View file

@ -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<expr>(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<tactic_state> s_new = is_tactic_success(result)) {
mctx = s_new->mctx();
expr proof = mctx.instantiate_mvars(goal_mvar);
@ -643,7 +642,7 @@ public:
optional<unsigned> 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

32
src/library/constants.cpp
View file

@ -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; }

8
src/library/constants.h
View file

@ -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();

8
src/library/constants.txt
View file

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