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

feat(library/init/meta/smt): add intros variants for smt_tactic

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-13 16:13:19 -08:00
parent a6ef7f52a9
commit 05d86e49ca
3 changed files with 53 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/meta/smt/interactive.lean
View file

@ -28,8 +28,9 @@ open interactive.types
meta def itactic : Type :=
smt_tactic unit
meta def intros : smt_tactic unit :=
smt_tactic.intros
meta def intros : raw_ident_list → smt_tactic unit
| [] := smt_tactic.intros
| hs := smt_tactic.intro_lst hs
/--
Try to close main goal by using equalities implied by the congruence

17
library/init/meta/smt/smt_tactic.lean
View file

@ -98,9 +98,9 @@ meta instance : alternative smt_tactic :=
namespace smt_tactic
open tactic (transparency)
/-- (intros_core fresh_names), if fresh_names is tt, then create fresh names for new hypotheses.
Otherwise, it just uses the given names. -/
meta constant intros_core : bool → smt_tactic unit
meta constant intros : smt_tactic unit
meta constant intron : nat → smt_tactic unit
meta constant intro_lst : list name → smt_tactic unit
/--
Try to close main goal by using equalities implied by the congruence
closure module.
@ -150,9 +150,6 @@ meta def add_ematch_eqn_lemmas_for_core (md : transparency) (n : name) : smt_ta
do hs ← mk_ematch_eqn_lemmas_for_core md n,
add_lemmas hs
meta def intros : smt_tactic unit :=
intros_core tt
meta def ematch : smt_tactic unit :=
ematch_core (λ _, tt)
@ -265,19 +262,19 @@ do (ss, ts) ← get_goals,
/-- Add a new goal for t, and the hypothesis (h : t) in the current goal. -/
meta def assert (h : name) (t : expr) : smt_tactic unit :=
tactic.assert_core h t >> swap >> intros_core ff >> swap >> try close
tactic.assert_core h t >> swap >> intros >> swap >> try close
/-- Add the hypothesis (h : t) in the current goal if v has type t. -/
meta def assertv (h : name) (t : expr) (v : expr) : smt_tactic unit :=
tactic.assertv_core h t v >> intros_core ff >> return ()
tactic.assertv_core h t v >> intros >> return ()
/-- Add a new goal for t, and the hypothesis (h : t := ?M) in the current goal. -/
meta def define (h : name) (t : expr) : smt_tactic unit :=
tactic.define_core h t >> swap >> intros_core ff >> swap >> try close
tactic.define_core h t >> swap >> intros >> swap >> try close
/-- Add the hypothesis (h : t := v) in the current goal if v has type t. -/
meta def definev (h : name) (t : expr) (v : expr) : smt_tactic unit :=
tactic.definev_core h t v >> intros_core ff >> return ()
tactic.definev_core h t v >> intros >> return ()
/-- Add (h : t := pr) to the current goal -/
meta def pose (h : name) (pr : expr) : smt_tactic unit :=

47
src/library/tactic/smt/smt_state.cpp
View file

@ -721,7 +721,42 @@ vm_obj smt_tactic_close(vm_obj const & ss, vm_obj const & _ts) {
return mk_tactic_exception("smt_tactic.close failed", ts);
}
vm_obj smt_tactic_intros_core(vm_obj const & use_unused_names, vm_obj const & ss, vm_obj const & _ts) {
vm_obj smt_tactic_intros_core(list<name> const & ids, optional<unsigned> const & num, vm_obj const & ss, tactic_state ts) {
if (is_nil(ss))
return mk_smt_state_empty_exception(ts);
LEAN_TACTIC_TRY;
smt_goal new_sgoal = to_smt_goal(head(ss));
vm_obj r = preprocess(ts, new_sgoal.get_pre_config());
if (is_tactic_result_exception(r)) return r;
ts = to_tactic_state(get_tactic_result_state(r));
metavar_context mctx = ts.mctx();
defeq_can_state dcs = ts.dcs();
expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()),
dcs, new_sgoal, true, num, ids);
tactic_state new_ts = set_mctx_goals_dcs(ts, mctx, cons(new_mvar, tail(ts.goals())), dcs);
vm_obj new_ss = mk_vm_cons(to_obj(new_sgoal), tail(ss));
return mk_smt_tactic_success(new_ss, new_ts);
LEAN_TACTIC_CATCH(ts);
}
vm_obj smt_tactic_intros(vm_obj const & ss, vm_obj const & ts) {
return smt_tactic_intros_core(list<name>(), optional<unsigned>(), ss, to_tactic_state(ts));
}
vm_obj smt_tactic_intron(vm_obj const & n, vm_obj const & ss, vm_obj const & ts) {
return smt_tactic_intros_core(list<name>(), optional<unsigned>(force_to_unsigned(n)), ss, to_tactic_state(ts));
}
vm_obj smt_tactic_intro_lst(vm_obj const & _ids, vm_obj const & ss, vm_obj const & ts) {
list<name> const & ids = to_list_name(_ids);
return smt_tactic_intros_core(list<name>(ids), optional<unsigned>(length(ids)), ss, to_tactic_state(ts));
}
vm_obj smt_tactic_intros_core(vm_obj const & _ids, vm_obj const & ss, vm_obj const & _ts) {
tactic_state ts = to_tactic_state(_ts);
if (is_nil(ss))
return mk_smt_state_empty_exception(ts);
@ -735,9 +770,11 @@ vm_obj smt_tactic_intros_core(vm_obj const & use_unused_names, vm_obj const & ss
metavar_context mctx = ts.mctx();
defeq_can_state dcs = ts.dcs();
list<name> ids;
list<name> ids = to_list_name(_ids);
optional<unsigned> n;
if (ids) n = length(ids);
expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()),
dcs, new_sgoal, to_bool(use_unused_names), optional<unsigned>(), ids);
dcs, new_sgoal, true, n, ids);
tactic_state new_ts = set_mctx_goals_dcs(ts, mctx, cons(new_mvar, tail(ts.goals())), dcs);
vm_obj new_ss = mk_vm_cons(to_obj(new_sgoal), tail(ss));
@ -918,7 +955,9 @@ void initialize_smt_state() {
DECLARE_VM_BUILTIN(name({"smt_state", "classical"}), smt_state_classical);
DECLARE_VM_BUILTIN("tactic_to_smt_tactic", tactic_to_smt_tactic);
DECLARE_VM_BUILTIN(name({"smt_tactic", "close"}), smt_tactic_close);
DECLARE_VM_BUILTIN(name({"smt_tactic", "intros_core"}), smt_tactic_intros_core);
DECLARE_VM_BUILTIN(name({"smt_tactic", "intros"}), smt_tactic_intros);
DECLARE_VM_BUILTIN(name({"smt_tactic", "intron"}), smt_tactic_intron);
DECLARE_VM_BUILTIN(name({"smt_tactic", "intro_lst"}), smt_tactic_intro_lst);
DECLARE_VM_BUILTIN(name({"smt_tactic", "ematch_core"}), smt_tactic_ematch_core);
DECLARE_VM_BUILTIN(name({"smt_tactic", "ematch_using"}), smt_tactic_ematch_using);
DECLARE_VM_BUILTIN(name({"smt_tactic", "to_cc_state"}), smt_tactic_to_cc_state);