From f8e5753a134979438b2780ea53ff36abe9af855a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Aug 2016 16:15:12 -0700 Subject: [PATCH] feat(library/type_context, library/tactic): add eta-expansion method and tactic --- library/init/meta/tactic.lean | 1 + src/library/tactic/tactic_state.cpp | 11 +++++++++++ src/library/type_context.cpp | 25 +++++++++++++++++++++++++ src/library/type_context.h | 2 ++ tests/lean/eta_tac.lean | 13 +++++++++++++ tests/lean/eta_tac.lean.expected.out | 4 ++++ 6 files changed, 56 insertions(+) create mode 100644 tests/lean/eta_tac.lean create mode 100644 tests/lean/eta_tac.lean.expected.out diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index d7c949b3da..f5d441b592 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -220,6 +220,7 @@ meta_constant rename : name → name → tactic unit meta_constant clear : expr → tactic unit meta_constant revert_lst : list expr → tactic nat meta_constant whnf_core : transparency → expr → tactic expr +meta_constant eta_expand : expr → tactic expr meta_constant unify_core : transparency → expr → expr → tactic unit /- Infer the type of the given expression. Remark: transparency does not affect type inference -/ diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 2c97b4c275..53ee8800ec 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -309,6 +309,16 @@ vm_obj tactic_whnf_core(vm_obj const & t, vm_obj const & e, vm_obj const & s0) { } } +vm_obj tactic_eta_expand(vm_obj const & e, vm_obj const & s0) { + tactic_state const & s = to_tactic_state(s0); + type_context ctx = mk_type_context_for(s); + try { + return mk_tactic_success(to_obj(ctx.eta_expand(to_expr(e))), s); + } catch (exception & ex) { + return mk_tactic_exception(ex, s); + } +} + vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) { tactic_state const & s = to_tactic_state(s0); type_context ctx = mk_type_context_for(s); @@ -492,6 +502,7 @@ void initialize_tactic_state() { 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_core"}), tactic_whnf_core); + DECLARE_VM_BUILTIN(name({"tactic", "eta_expand"}), tactic_eta_expand); DECLARE_VM_BUILTIN(name({"tactic", "is_class"}), tactic_is_class); DECLARE_VM_BUILTIN(name({"tactic", "mk_instance"}), tactic_mk_instance); DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}), tactic_unify_core); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 2e29916344..9b342d252e 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2529,6 +2529,31 @@ optional type_context::mk_subsingleton_instance(expr const & type) { return r; } +/* ------------- + Auxiliary + ------------- */ + +expr type_context::eta_expand(expr const & e) { + tmp_locals locals(*this); + expr it = e; + while (is_lambda(it)) { + expr d = instantiate_rev(binding_domain(it), locals.as_buffer().size(), locals.as_buffer().data()); + locals.push_local(binding_name(it), d, binding_info(it)); + it = binding_body(it); + } + it = instantiate_rev(it, locals.as_buffer().size(), locals.as_buffer().data()); + expr it_type = relaxed_whnf(infer(it)); + if (!is_pi(it_type)) return e; + buffer extra_args; + while (is_pi(it_type)) { + expr arg = locals.push_local_from_binding(it_type); + extra_args.push_back(arg); + it_type = relaxed_whnf(instantiate(binding_body(it_type), arg)); + } + expr r = mk_app(it, extra_args); + return locals.mk_lambda(r); +} + tmp_type_context::tmp_type_context(type_context & tctx, unsigned num_umeta, unsigned num_emeta): m_tctx(tctx) { m_tmp_uassignment.resize(num_umeta, none_level()); m_tmp_eassignment.resize(num_emeta, none_expr()); diff --git a/src/library/type_context.h b/src/library/type_context.h index 1e04f75ff2..793515085e 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -265,6 +265,8 @@ public: transparency_mode mode() const { return m_transparency_mode; } unsigned mode_idx() const { return static_cast(mode()); } + expr eta_expand(expr const & e); + struct transparency_scope : public flet { transparency_scope(type_context & ctx, transparency_mode m): flet(ctx.m_transparency_mode, m) { diff --git a/tests/lean/eta_tac.lean b/tests/lean/eta_tac.lean new file mode 100644 index 0000000000..449e7f8446 --- /dev/null +++ b/tests/lean/eta_tac.lean @@ -0,0 +1,13 @@ +open tactic + +set_option pp.binder_types true +set_option pp.implicit true +set_option pp.notation false + +example (a : nat) : true := +by do + mk_const `add >>= eta_expand >>= trace, + mk_const `nat.succ >>= eta_expand >>= trace, + to_expr `(add a) >>= eta_expand >>= trace, + to_expr `(λ x : nat, add x) >>= eta_expand >>= trace, + constructor diff --git a/tests/lean/eta_tac.lean.expected.out b/tests/lean/eta_tac.lean.expected.out new file mode 100644 index 0000000000..a2cb3e98b2 --- /dev/null +++ b/tests/lean/eta_tac.lean.expected.out @@ -0,0 +1,4 @@ +λ {A : Type} [_inst_1 : has_add A] (a a_1 : A), @add A _inst_1 a a_1 +λ (a : nat), nat.succ a +λ (a_1 : nat), @add nat nat_has_add a a_1 +λ (x a : nat), @add nat nat_has_add x a