feat(library/tactic): add "check_expr" tactic

closes #486

hott/init/tactic.hlean

@@ -65,6 +65,7 @@ opaque definition refine     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
 -- Relaxed version of exact that does not enforce goal type
 opaque definition rexact     (e : expr)   : tactic := builtin
+opaque definition check_expr (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 
 inductive expr_list : Type :=

library/init/tactic.lean

@@ -65,6 +65,7 @@ opaque definition refine     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
 -- Relaxed version of exact that does not enforce goal type
 opaque definition rexact     (e : expr)   : tactic := builtin
+opaque definition check_expr (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 
 inductive expr_list : Type :=

src/emacs/lean-syntax.el

@@ -133,7 +133,7 @@
                 "apply" "fapply" "rename" "intro" "intros" "all_goals" "fold"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                 "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
-                "unfold" "change"))
+                "unfold" "change" "check_expr"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types

src/library/constants.cpp

@@ -73,6 +73,7 @@ name const * g_tactic_beta = nullptr;
 name const * g_tactic_builtin = nullptr;
 name const * g_tactic_cases = nullptr;
 name const * g_tactic_change = nullptr;
+name const * g_tactic_check_expr = nullptr;
 name const * g_tactic_clear = nullptr;
 name const * g_tactic_clears = nullptr;
 name const * g_tactic_determ = nullptr;
@@ -189,6 +190,7 @@ void initialize_constants() {
     g_tactic_builtin = new name{"tactic", "builtin"};
     g_tactic_cases = new name{"tactic", "cases"};
     g_tactic_change = new name{"tactic", "change"};
+    g_tactic_check_expr = new name{"tactic", "check_expr"};
     g_tactic_clear = new name{"tactic", "clear"};
     g_tactic_clears = new name{"tactic", "clears"};
     g_tactic_determ = new name{"tactic", "determ"};
@@ -306,6 +308,7 @@ void finalize_constants() {
     delete g_tactic_builtin;
     delete g_tactic_cases;
     delete g_tactic_change;
+    delete g_tactic_check_expr;
     delete g_tactic_clear;
     delete g_tactic_clears;
     delete g_tactic_determ;
@@ -422,6 +425,7 @@ name const & get_tactic_beta_name() { return *g_tactic_beta; }
 name const & get_tactic_builtin_name() { return *g_tactic_builtin; }
 name const & get_tactic_cases_name() { return *g_tactic_cases; }
 name const & get_tactic_change_name() { return *g_tactic_change; }
+name const & get_tactic_check_expr_name() { return *g_tactic_check_expr; }
 name const & get_tactic_clear_name() { return *g_tactic_clear; }
 name const & get_tactic_clears_name() { return *g_tactic_clears; }
 name const & get_tactic_determ_name() { return *g_tactic_determ; }

src/library/constants.h

@@ -75,6 +75,7 @@ name const & get_tactic_beta_name();
 name const & get_tactic_builtin_name();
 name const & get_tactic_cases_name();
 name const & get_tactic_change_name();
+name const & get_tactic_check_expr_name();
 name const & get_tactic_clear_name();
 name const & get_tactic_clears_name();
 name const & get_tactic_determ_name();

src/library/constants.txt

@@ -68,6 +68,7 @@ tactic.beta
 tactic.builtin
 tactic.cases
 tactic.change
+tactic.check_expr
 tactic.clear
 tactic.clears
 tactic.determ

src/library/tactic/CMakeLists.txt

@@ -4,6 +4,6 @@ exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp
 inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp
 assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp
 rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp
-change_tactic.cpp)
+change_tactic.cpp check_expr_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/check_expr_tactic.cpp

@@ -0,0 +1,52 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "library/constants.h"
+#include "library/reducible.h"
+#include "library/flycheck.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+tactic check_expr_tactic(elaborate_fn const & elab, expr const & e,
+                         std::string const & fname, pair<unsigned, unsigned> const & pos) {
+    return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
+            goals const & gs = s.get_goals();
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
+                return none_proof_state();
+            }
+            goal const & g      = head(gs);
+            name_generator ngen = s.get_ngen();
+            expr new_e = elab(g, ngen.mk_child(), e, none_expr(), false).first;
+            auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+            expr new_t = tc->infer(new_e).first;
+            auto out = regular(env, ios);
+            flycheck_information info(out);
+            if (info.enabled()) {
+                out << fname << ":" << pos.first << ":" << pos.second << ": information: ";
+                out << "check result:\n";
+            }
+            out << new_e << " : " << new_t << endl;
+            return some_proof_state(s);
+        });
+}
+
+void initialize_check_expr_tactic() {
+    register_tac(get_tactic_check_expr_name(),
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+                     check_tactic_expr(app_arg(e), "invalid 'check_expr' tactic, invalid argument");
+                     expr arg = get_tactic_expr_expr(app_arg(e));
+                     if (p) {
+                         if (auto it = p->get_pos_info(e))
+                             return check_expr_tactic(fn, arg, std::string(p->get_file_name()), *it);
+                     }
+                     return check_expr_tactic(fn, arg, "<unknown file>", mk_pair(0, 0));
+                 });
+}
+void finalize_check_expr_tactic() {
+}
+}

src/library/tactic/check_expr_tactic.h

@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2015 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 {
+void initialize_check_expr_tactic();
+void finalize_check_expr_tactic();
+}

src/library/tactic/init_module.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/tactic/class_instance_synth.h"
 #include "library/tactic/rewrite_tactic.h"
 #include "library/tactic/change_tactic.h"
+#include "library/tactic/check_expr_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -43,9 +44,11 @@ void initialize_tactic_module() {
     initialize_class_instance_elaborator();
     initialize_rewrite_tactic();
     initialize_change_tactic();
+    initialize_check_expr_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_check_expr_tactic();
     finalize_change_tactic();
     finalize_rewrite_tactic();
     finalize_class_instance_elaborator();

tests/lean/check_expr.lean

@@ -0,0 +1,8 @@
+import data.list
+open sigma list
+
+theorem foo (A : Type) (l : list A): A → A → list A :=
+begin
+  intros [a, b],
+  check_expr (a::l),
+end

tests/lean/check_expr.lean.expected.out

@@ -0,0 +1,10 @@
+a :: l : list A
+check_expr.lean:8:0: error: 1 unsolved subgoal
+A : Type,
+l : list A,
+a b : A
+⊢ list A
+check_expr.lean:8:0: error: failed to add declaration 'foo' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (l : …),
+    ?M_1