From 7cc31835e40fb783d34529a39f6388e73cb86cd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 31 Jan 2017 18:01:54 -0800 Subject: [PATCH] refactor(library/init/meta/fun_info): cleanup fun_info API --- library/init/meta/fun_info.lean | 30 +++-------------- src/library/tactic/fun_info_tactics.cpp | 45 +++++++++++-------------- tests/lean/run/fun_info1.lean | 6 ++-- tests/lean/run/opt_param_cc.lean | 6 ++-- 4 files changed, 30 insertions(+), 57 deletions(-) diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean index 371aa58d33..e92dfdb028 100644 --- a/library/init/meta/fun_info.lean +++ b/library/init/meta/fun_info.lean @@ -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 diff --git a/src/library/tactic/fun_info_tactics.cpp b/src/library/tactic/fun_info_tactics.cpp index 29ca572080..34a0a63757 100644 --- a/src/library/tactic/fun_info_tactics.cpp +++ b/src/library/tactic/fun_info_tactics.cpp @@ -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 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() { diff --git a/tests/lean/run/fun_info1.lean b/tests/lean/run/fun_info1.lean index b7162f19f7..f670a1927d 100644 --- a/tests/lean/run/fun_info1.lean +++ b/tests/lean/run/fun_info1.lean @@ -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 diff --git a/tests/lean/run/opt_param_cc.lean b/tests/lean/run/opt_param_cc.lean index 036f642b7b..1d1596b92b 100644 --- a/tests/lean/run/opt_param_cc.lean +++ b/tests/lean/run/opt_param_cc.lean @@ -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