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

refactor(library/init/meta/tactic): implement num_goals in Lean

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-17 16:18:15 -07:00
parent ee888e9872
commit ded1fe74c5
2 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -74,8 +74,6 @@ meta_constant unify_core : expr → expr → transparency → tactic bool
meta_constant get_local : name → tactic expr
/- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/
meta_constant local_context : tactic (list expr)
/- Return the number of goals that need to be solved -/
meta_constant num_goals : tactic nat
/- Helper tactic for creating simple applications where some arguments are inferred using
type inference.
@ -166,6 +164,11 @@ do { ctx ← local_context,
meta_definition dsimp : tactic unit :=
target >>= defeq_simp >>= change
/- Return the number of goals that need to be solved -/
meta_definition num_goals : tactic nat :=
do gs ← get_goals,
return (length gs)
/- We have to provide the instance argument `[has_mod nat]` because
mod for nat was not defined yet -/
meta_definition rotate_right (n : nat) [has_mod nat] : tactic unit :=

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

@ -341,10 +341,6 @@ vm_obj tactic_local_context(vm_obj const & s0) {
return mk_tactic_success(to_obj(to_list(r)), s);
}
vm_obj tactic_num_goals(vm_obj const & s) {
return mk_tactic_success(mk_vm_nat(length(to_tactic_state(s).goals())), to_tactic_state(s));
}
vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & s) {
/* TODO(Leo): invoke elaborator */
return mk_tactic_success(qe, to_tactic_state(s));
@ -414,7 +410,6 @@ void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}), tactic_unify_core);
DECLARE_VM_BUILTIN(name({"tactic", "get_local"}), tactic_get_local);
DECLARE_VM_BUILTIN(name({"tactic", "local_context"}), tactic_local_context);
DECLARE_VM_BUILTIN(name({"tactic", "num_goals"}), tactic_num_goals);
DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}), tactic_to_expr);
DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp"}), tactic_defeq_simp);
DECLARE_VM_BUILTIN(name({"tactic", "rotate_left"}), tactic_rotate_left);