From 05d86e49cacd4c94fc39216e367d47eff79eaac0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Jan 2017 16:13:19 -0800 Subject: [PATCH] feat(library/init/meta/smt): add intros variants for smt_tactic --- library/init/meta/smt/interactive.lean | 5 +-- library/init/meta/smt/smt_tactic.lean | 17 ++++------ src/library/tactic/smt/smt_state.cpp | 47 +++++++++++++++++++++++--- 3 files changed, 53 insertions(+), 16 deletions(-) diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 3ead19fa07..458141d38c 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -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 diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean index dab5d1cda7..4c8a2c8a17 100644 --- a/library/init/meta/smt/smt_tactic.lean +++ b/library/init/meta/smt/smt_tactic.lean @@ -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 := diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 2a30782e7b..0e4719517e 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -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 const & ids, optional 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(), optional(), 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(), optional(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 const & ids = to_list_name(_ids); + return smt_tactic_intros_core(list(ids), optional(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 ids; + list ids = to_list_name(_ids); + optional 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(), 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);