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

refactor(library/init/meta/fun_info): cleanup fun_info API

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-31 18:01:54 -08:00
parent 49a0d13c50
commit 7cc31835e4
4 changed files with 30 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
library/init/meta/fun_info.lean
View file

@ -86,13 +86,10 @@ meta instance : has_to_format subsingleton_info :=
has_to_format.mk subsingleton_info_to_format
namespace tactic
meta constant get_fun_info_core : transparency → expr → tactic fun_info
/- (get_fun_info fn n) return information assuming the function has only n arguments.
The tactic fail if n > length (params (get_fun_info fn)) -/
meta constant get_fun_info_n_core : transparency → expr → nat → tactic fun_info
meta constant get_subsingleton_info_core : transparency → expr → tactic (list subsingleton_info)
meta constant get_subsingleton_info_n_core : transparency → expr → nat → tactic (list subsingleton_info)
/-- If nargs is not none, then return information assuming the function has only nargs arguments. -/
meta constant get_fun_info (f : expr) (nargs : option nat := none) (md := semireducible) : tactic fun_info
meta constant get_subsingleton_info (f : expr) (nargs : option nat := none) (md := semireducible) : tactic (list subsingleton_info)
/- (get_spec_subsingleton_info t) return subsingleton parameter
information for the function application t of the form
@ -109,24 +106,7 @@ meta constant get_subsingleton_info_n_core : transparency → expr → nat → t
The second argument is marked as subsingleton only because the resulting information
is taking into account the first argument. -/
meta constant get_spec_subsingleton_info_core : transparency → expr → tactic (list subsingleton_info)
meta constant get_spec_prefix_size_core : transparency → expr → nat → tactic nat
meta constant get_spec_subsingleton_info (t : expr) (md := semireducible) : tactic (list subsingleton_info)
meta constant get_spec_prefix_size (t : expr) (nargs : nat) (md := semireducible) : tactic nat
meta def get_fun_info : expr → tactic fun_info :=
get_fun_info_core semireducible
meta def get_fun_info_n : expr → nat → tactic fun_info :=
get_fun_info_n_core semireducible
meta def get_subsingleton_info : expr → tactic (list subsingleton_info) :=
get_subsingleton_info_core semireducible
meta def get_subsingleton_info_n : expr → nat → tactic (list subsingleton_info) :=
get_subsingleton_info_n_core semireducible
meta def get_spec_subsingleton_info : expr → tactic (list subsingleton_info) :=
get_spec_subsingleton_info_core semireducible
meta def get_spec_prefix_size : expr → nat → tactic nat :=
get_spec_prefix_size_core semireducible
end tactic

45
src/library/tactic/fun_info_tactics.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "library/vm/vm_list.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_option.h"
#include "library/tactic/tactic_state.h"
namespace lean {
@ -59,42 +60,36 @@ static vm_obj mk_result(list<ss_param_info> const & info, vm_obj const & s) {
return mk_tactic_success(to_obj(info), to_tactic_state(s));
}
vm_obj tactic_get_fun_info(vm_obj const & m, vm_obj const & fn, vm_obj const & s) {
vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) {
TRY;
type_context ctx = mk_type_context_for(s, m);
return mk_result(get_fun_info(ctx, to_expr(fn)), s);
if (is_none(n)) {
return mk_result(get_fun_info(ctx, to_expr(fn)), s);
} else {
return mk_result(get_fun_info(ctx, to_expr(fn), force_to_unsigned(get_some_value(n), 0)), s);
}
CATCH;
}
vm_obj tactic_get_fun_info_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
vm_obj tactic_get_subsingleton_info(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) {
TRY;
type_context ctx = mk_type_context_for(s, m);
return mk_result(get_fun_info(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
if (is_none(n)) {
return mk_result(get_subsingleton_info(ctx, to_expr(fn)), s);
} else {
return mk_result(get_subsingleton_info(ctx, to_expr(fn), force_to_unsigned(get_some_value(n), 0)), s);
}
CATCH;
}
vm_obj tactic_get_subsingleton_info(vm_obj const & m, vm_obj const & fn, vm_obj const & s) {
TRY;
type_context ctx = mk_type_context_for(s, m);
return mk_result(get_subsingleton_info(ctx, to_expr(fn)), s);
CATCH;
}
vm_obj tactic_get_subsingleton_info_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
TRY;
type_context ctx = mk_type_context_for(s, m);
return mk_result(get_subsingleton_info(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
CATCH;
}
vm_obj tactic_get_spec_subsingleton_info(vm_obj const & m, vm_obj const & app, vm_obj const & s) {
vm_obj tactic_get_spec_subsingleton_info(vm_obj const & app, vm_obj const & m, vm_obj const & s) {
TRY;
type_context ctx = mk_type_context_for(s, m);
return mk_result(get_specialized_subsingleton_info(ctx, to_expr(app)), s);
CATCH;
}
vm_obj tactic_get_spec_prefix_size(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) {
TRY;
type_context ctx = mk_type_context_for(s, m);
return mk_tactic_success(mk_vm_nat(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))),
@ -103,12 +98,10 @@ vm_obj tactic_get_spec_prefix_size(vm_obj const & m, vm_obj const & fn, vm_obj c
}
void initialize_fun_info_tactics() {
DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info_core"}), tactic_get_fun_info);
DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info_n_core"}), tactic_get_fun_info_n);
DECLARE_VM_BUILTIN(name({"tactic", "get_subsingleton_info_core"}), tactic_get_subsingleton_info);
DECLARE_VM_BUILTIN(name({"tactic", "get_subsingleton_info_n_core"}), tactic_get_subsingleton_info_n);
DECLARE_VM_BUILTIN(name({"tactic", "get_spec_subsingleton_info_core"}), tactic_get_spec_subsingleton_info);
DECLARE_VM_BUILTIN(name({"tactic", "get_spec_prefix_size_core"}), tactic_get_spec_prefix_size);
DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info"}), tactic_get_fun_info);
DECLARE_VM_BUILTIN(name({"tactic", "get_subsingleton_info"}), tactic_get_subsingleton_info);
DECLARE_VM_BUILTIN(name({"tactic", "get_spec_subsingleton_info"}), tactic_get_spec_subsingleton_info);
DECLARE_VM_BUILTIN(name({"tactic", "get_spec_prefix_size"}), tactic_get_spec_prefix_size);
}
void finalize_fun_info_tactics() {

6
tests/lean/run/fun_info1.lean
View file

@ -10,9 +10,9 @@ by do
get_spec_subsingleton_info lhs >>= trace,
trace "-----------",
trace "ite information:",
mk_const `ite >>= get_fun_info >>= trace,
c ← mk_const `ite, get_fun_info c >>= trace,
trace "eq.rec information:",
mk_const `eq.rec >>= get_fun_info >>= trace,
c ← mk_const `eq.rec, get_fun_info c >>= trace,
trace "and.intro information:",
mk_const `and.intro >>= get_fun_info >>= trace,
c ← mk_const `and.intro, get_fun_info c >>= trace,
mk_const `trivial >>= exact

6
tests/lean/run/opt_param_cc.lean
View file

@ -17,9 +17,9 @@ end
open tactic
run_command mk_const `f >>= get_fun_info >>= trace
run_command mk_const `eq >>= get_fun_info >>= trace
run_command mk_const `id >>= get_fun_info >>= trace
run_command do c ← mk_const `f, get_fun_info c >>= trace
run_command do c ← mk_const `eq, get_fun_info c >>= trace
run_command do c ← mk_const `id, get_fun_info c >>= trace
set_option trace.congr_lemma true
set_option trace.app_builder true