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

chore(library/init/meta/tactic): define focus_aux using is_assigned

Browse source
This commit is contained in:
Leonardo de Moura 2017-07-21 02:32:08 -07:00
parent 94ecc3292f
commit af80c2890d
3 changed files with 32 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/meta/coinductive_predicates.lean
View file

@ -69,9 +69,6 @@ meta def add_theorem_by (n : name) (ls : list name) (type : expr) (tac : tactic
add_decl $ mk_theorem n ls type body,
return $ const n $ ls.map param
meta def is_assigned (m : expr): tactic bool :=
((get_assignment m >> return ff) <|> return tt)
meta def mk_exists_lst (args : list expr) (inner : expr) : tactic expr :=
args.mfoldr (λarg i:expr, do
t ← infer_type arg,
@ -405,7 +402,7 @@ meta def add_coinductive_predicate
func_intros.mmap' (λ⟨n, pp_n, t⟩, solve1 $ do
bs ← intros,
ms ← apply_core ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) {new_goals := new_goals.all},
params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, is_assigned m),
params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, bnot <$> is_assigned m),
params.mmap' (λ⟨n, m, d⟩, mono d (fs.map prod.snd) <|>
fail format! "failed to prove montonoicity of {n+1}. parameter of intro-rule {pp_n}")))),

37
library/init/meta/tactic.lean
View file

@ -385,6 +385,9 @@ meta constant get_univ_assignment : level → tactic level
/-- Return the value assigned to the given meta-variable.
Fail if argument is not a meta-variable or if it is not assigned. -/
meta constant get_assignment : expr → tactic expr
/-- Return the value assigned to the given meta-variable.
Fail if argument is not a meta-variable. -/
meta constant is_assigned : expr → tactic bool
meta constant mk_fresh_name : tactic name
/-- Return a hash code for expr that ignores inst_implicit arguments,
and proofs. -/
@ -728,16 +731,16 @@ do gs ← get_goals,
meta def solve (ts : list (tactic unit)) : tactic unit :=
first $ map solve1 ts
private meta def focus_aux : list (tactic unit) → list expr → list expr → tactic unit
private meta def focus_aux : list (tactic unit) → list expr → list expr → tactic unit
| [] [] rs := set_goals rs
| (t::ts) [] rs := fail "focus tactic failed, insufficient number of goals"
| tts (g::gs) rs :=
do set_goals [g],
_::_ ← get_goals | focus_aux tts gs rs,
t::ts ← pure tts | fail "focus tactic failed, insufficient number of tactics",
t,
rs' ← get_goals,
focus_aux ts gs (rs ++ rs')
mcond (is_assigned g) (focus_aux tts gs rs) $
do set_goals [g],
t::ts ← pure tts | fail "focus tactic failed, insufficient number of tactics",
t,
rs' ← get_goals,
focus_aux ts gs (rs ++ rs')
/-- `focus [t_1, ..., t_n]` applies t_i to the i-th goal. Fails if the number of goals is not n. -/
meta def focus (ts : list (tactic unit)) : tactic unit :=
@ -758,11 +761,11 @@ do g::gs ← get_goals,
private meta def all_goals_core (tac : tactic unit) : list expr → list expr → tactic unit
| [] ac := set_goals ac
| (g :: gs) ac :=
do set_goals [g],
_::_ ← get_goals | all_goals_core gs ac,
tac,
new_gs ← get_goals,
all_goals_core gs (ac ++ new_gs)
mcond (is_assigned g) (all_goals_core gs ac) $
do set_goals [g],
tac,
new_gs ← get_goals,
all_goals_core gs (ac ++ new_gs)
/-- Apply the given tactic to all goals. -/
meta def all_goals (tac : tactic unit) : tactic unit :=
@ -772,11 +775,11 @@ do gs ← get_goals,
private meta def any_goals_core (tac : tactic unit) : list expr → list expr → bool → tactic unit
| [] ac progress := guard progress >> set_goals ac
| (g :: gs) ac progress :=
do set_goals [g],
_::_ ← get_goals | any_goals_core gs ac progress,
succeeded ← try_core tac,
new_gs ← get_goals,
any_goals_core gs (ac ++ new_gs) (succeeded.is_some || progress)
mcond (is_assigned g) (any_goals_core gs ac progress) $
do set_goals [g],
succeeded ← try_core tac,
new_gs ← get_goals,
any_goals_core gs (ac ++ new_gs) (succeeded.is_some || progress)
/-- Apply the given tactic to any goal where it succeeds. The tactic succeeds only if
tac succeeds for at least one goal. -/

12
src/library/tactic/tactic_state.cpp
View file

@ -601,7 +601,7 @@ vm_obj tactic_get_assignment(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
metavar_context mctx = s.mctx();
if (!is_metavar(to_expr(e))) {
return tactic::mk_exception("get_assignment tactic failed, argument is not an universe metavariable", s);
return tactic::mk_exception("get_assignment tactic failed, argument is not a metavariable", s);
} else if (auto r = mctx.get_assignment(to_expr(e))) {
return tactic::mk_success(to_obj(*r), s);
} else {
@ -609,6 +609,15 @@ vm_obj tactic_get_assignment(vm_obj const & e, vm_obj const & s0) {
}
}
vm_obj tactic_is_assigned(vm_obj const & g, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
if (!is_metavar(to_expr(g))) {
return tactic::mk_exception("is_assigned tactic failed, argument is not a metavariable", s);
} else {
return tactic::mk_success(mk_vm_bool(s.mctx().is_assigned(to_expr(g))), s);
}
}
vm_obj tactic_state_get_options(vm_obj const & s) {
return to_obj(tactic::to_state(s).get_options());
}
@ -881,6 +890,7 @@ void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic_state", "set_options"}), tactic_state_set_options);
DECLARE_VM_BUILTIN(name({"tactic", "target"}), tactic_target);
DECLARE_VM_BUILTIN(name({"tactic", "result"}), tactic_result);
DECLARE_VM_BUILTIN(name({"tactic", "is_assigned"}), tactic_is_assigned);
DECLARE_VM_BUILTIN(name({"tactic", "format_result"}), tactic_format_result);
DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}), tactic_infer_type);
DECLARE_VM_BUILTIN(name({"tactic", "whnf"}), tactic_whnf);