From e22eb3543cdced4488fdaab60fb6d1775a569258 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Oct 2014 23:18:49 -0700 Subject: [PATCH] feat(library/tactic): add whnf tactic, closes #270 --- library/tools/tactic.lean | 1 + src/emacs/lean-syntax.el | 2 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/elaborate.cpp | 20 +++++++++++++ src/library/tactic/elaborate.h | 2 ++ src/library/tactic/init_module.cpp | 3 ++ src/library/tactic/whnf_tactic.cpp | 43 +++++++++++++++++++++++++++ src/library/tactic/whnf_tactic.h | 14 +++++++++ tests/lean/whnf_tac.lean | 11 +++++++ tests/lean/whnf_tac.lean.expected.out | 4 +++ 10 files changed, 100 insertions(+), 2 deletions(-) create mode 100644 src/library/tactic/whnf_tactic.cpp create mode 100644 src/library/tactic/whnf_tactic.h create mode 100644 tests/lean/whnf_tac.lean create mode 100644 tests/lean/whnf_tac.lean.expected.out diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 032e9beb7..efb017063 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -37,6 +37,7 @@ opaque definition fail : tactic := builtin opaque definition id : tactic := builtin opaque definition beta : tactic := builtin opaque definition info : tactic := builtin +opaque definition whnf : tactic := builtin -- This is just a trick to embed expressions into tactics. -- The nested expressions are "raw". They tactic should diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 078ac5864..ecc2546d7 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -119,7 +119,7 @@ ;; tactics (,(rx (not (any "\.")) word-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros" - "generalize" "back" "beta" "done" "exact" "repeat") + "generalize" "back" "beta" "done" "exact" "repeat" "whnf") word-end) . 'font-lock-constant-face) ;; Types diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index fc26b122c..b5ceecfc0 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp -exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp +exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp whnf_tactic.cpp expr_to_tactic.cpp util.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 059f01dcb..b33d2b1df 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -9,6 +9,26 @@ Author: Leonardo de Moura #include "library/tactic/elaborate.h" namespace lean { +bool solve_constraints(environment const & env, io_state const & ios, proof_state & ps, constraint_seq const & cs) { + if (!cs) + return true; + unifier_config cfg(ios.get_options()); + buffer cs_buffer; + cs.linearize(cs_buffer); + to_buffer(ps.get_postponed(), cs_buffer); + name_generator ngen = ps.get_ngen(); + substitution subst = ps.get_subst(); + unify_result_seq rseq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen.mk_child(), subst, cfg); + if (auto p = rseq.pull()) { + substitution new_subst = p->first.first; + constraints new_postponed = p->first.second; + ps = proof_state(ps.get_goals(), new_subst, ngen, new_postponed); + return true; + } else { + return false; + } +} + optional elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state & s, expr const & e, optional const & expected_type) { name_generator ngen = s.get_ngen(); diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index c2507ff70..1ed8c7452 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -8,6 +8,8 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { +bool solve_constraints(environment const & env, io_state const & ios, proof_state & ps, constraint_seq const & cs); + /** \brief Function for elaborating expressions nested in tactics. Some tactics contain nested expression (aka pre-terms) that need to be elaborated. */ diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 5f99d4e38..125478689 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/tactic/exact_tactic.h" #include "library/tactic/unfold_tactic.h" #include "library/tactic/generalize_tactic.h" +#include "library/tactic/whnf_tactic.h" namespace lean { void initialize_tactic_module() { @@ -27,9 +28,11 @@ void initialize_tactic_module() { initialize_exact_tactic(); initialize_unfold_tactic(); initialize_generalize_tactic(); + initialize_whnf_tactic(); } void finalize_tactic_module() { + finalize_whnf_tactic(); finalize_generalize_tactic(); finalize_unfold_tactic(); finalize_exact_tactic(); diff --git a/src/library/tactic/whnf_tactic.cpp b/src/library/tactic/whnf_tactic.cpp new file mode 100644 index 000000000..18c9e9c63 --- /dev/null +++ b/src/library/tactic/whnf_tactic.cpp @@ -0,0 +1,43 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/reducible.h" +#include "library/tactic/expr_to_tactic.h" +#include "library/tactic/elaborate.h" +#include "library/tactic/whnf_tactic.h" + +namespace lean { +tactic whnf_tactic(bool relax_main_opaque) { + return tactic01([=](environment const & env, io_state const & ios, proof_state const & ps) { + goals const & gs = ps.get_goals(); + if (empty(gs)) + return none_proof_state(); + name_generator ngen = ps.get_ngen(); + auto tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque); + goal g = head(gs); + goals tail_gs = tail(gs); + expr type = g.get_type(); + auto t_cs = tc->whnf(type); + goals new_gs(goal(g.get_meta(), t_cs.first), tail_gs); + proof_state new_ps(ps, new_gs, ngen); + if (solve_constraints(env, ios, new_ps, t_cs.second)) { + return some_proof_state(new_ps); + } else { + return none_proof_state(); + } + }); +} + +void initialize_whnf_tactic() { + register_tac(name({"tactic", "whnf"}), + [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) { + return whnf_tactic(); + }); +} + +void finalize_whnf_tactic() { +} +} diff --git a/src/library/tactic/whnf_tactic.h b/src/library/tactic/whnf_tactic.h new file mode 100644 index 000000000..263783370 --- /dev/null +++ b/src/library/tactic/whnf_tactic.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/tactic.h" + +namespace lean { +tactic whnf_tactic(bool relax_main_opaque = true); +void initialize_whnf_tactic(); +void finalize_whnf_tactic(); +} diff --git a/tests/lean/whnf_tac.lean b/tests/lean/whnf_tac.lean new file mode 100644 index 000000000..bbaa1be3d --- /dev/null +++ b/tests/lean/whnf_tac.lean @@ -0,0 +1,11 @@ +import logic + +definition id {A : Type} (a : A) := a + +theorem tst (a : Prop) : a → id a := +begin + intro Ha, + whnf, + state, + apply Ha +end diff --git a/tests/lean/whnf_tac.lean.expected.out b/tests/lean/whnf_tac.lean.expected.out new file mode 100644 index 000000000..634499047 --- /dev/null +++ b/tests/lean/whnf_tac.lean.expected.out @@ -0,0 +1,4 @@ +whnf_tac.lean:9:2: proof state +a : Prop, +Ha : a +⊢ a