From 2b5f19677dad8c8218aeb7e2a3feb9ee6fc6c1ca Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 7 Jan 2019 17:02:15 +0100
Subject: [PATCH] feat(frontends/lean/vm_elaborator): elaborate `#check`

---
 library/init/lean/elaborator.lean    | 12 ++++++++++-
 library/init/lean/expander.lean      |  2 ++
 src/frontends/lean/vm_elaborator.cpp | 30 ++++++++++++++++++++++++++++
 3 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 2c89ec300b..79524dd2a5 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -428,6 +428,8 @@ do -- build and register parser
        pure (symbol a.val : term_parser)
      | _ := throw "register_notation_parser: unreachable",
      ptrans ← match r.transition with
+     | some (transition.view.binder b) :=
+       pure $ some $ term.binder_ident.parser
      | some (transition.view.binders b) :=
        pure $ some $ term.binders.parser
      | some (transition.view.arg {action := none, ..}) :=
@@ -597,6 +599,13 @@ def attribute.elaborate : elaborator :=
   let ids := expr.mk_capp `_ $ attr.ids.map $ λ id, expr.const (mangle_ident id) [],
   old_elab_command stx $ expr.mdata mdata $ expr.app attrs ids
 
+def check.elaborate : elaborator :=
+λ stx, do
+  let v := view check stx,
+  let mdata := kvmap.set_name {} `command `#check,
+  e ← to_pexpr v.term,
+  old_elab_command stx $ expr.mdata mdata e
+
 def open.elaborate : elaborator :=
 λ stx, do
   let v := view «open» stx,
@@ -681,7 +690,8 @@ def elaborators : rbmap name coelaborator (<) := rbmap.from_list [
   (declaration.name, declaration.elaborate),
   (attribute.name, attribute.elaborate),
   (open.name, open.elaborate),
-  (export.name, export.elaborate)
+  (export.name, export.elaborate),
+  (check.name, check.elaborate)
 ] _
 
 def resolve_global : name → elaborator_m (list name)
diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 1bdf3dd38f..0f76ad7a57 100644
--- a/library/init/lean/expander.lean
+++ b/library/init/lean/expander.lean
@@ -114,6 +114,8 @@ def mk_notation_transformer (nota : notation_macro) : transformer :=
       | notation_symbol.view.quoted {symbol := some a ..} := pop_stx_arg
       | _ := error stx "mk_notation_transformer: unreachable",
       match r.transition with
+      | some (transition.view.binder b) :=
+        do { stx_arg ← pop_stx_arg, modify $ λ st, {st with scoped := some $ binders.view.extended {leading_ids := [view binder_ident.parser stx_arg]}} }
       | some (transition.view.binders b) :=
         do { stx_arg ← pop_stx_arg, modify $ λ st, {st with scoped := some $ view term.binders.parser stx_arg} }
       | some (transition.view.arg {action := none, id := id}) :=
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index 95c6d0275b..abe485974c 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -10,6 +10,7 @@ Lean interface to the old elaborator/elaboration parts of the parser
 #include <string>
 #include <iostream>
 #include "util/timeit.h"
+#include "library/locals.h"
 #include "library/trace.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_string.h"
@@ -54,6 +55,32 @@ cmd_meta to_cmd_meta(environment const & env, expr const & e) {
     return m;
 }
 
+void elab_check_cmd(parser & p, expr const & cmd) {
+    // TODO(Sebastian)
+    // transient_cmd_scope cmd_scope(p);
+    expr e = mdata_expr(cmd);
+    bool check_unassigend = false;
+    names ls;
+    metavar_context mctx;
+    e = resolve_names(p.env(), p.mk_local_context_adapter().lctx(), e);
+    std::tie(e, ls) = p.elaborate("_check", mctx, e, check_unassigend);
+    names new_ls = to_names(collect_univ_params(e));
+    type_context_old tc(p.env());
+    expr type = tc.infer(e);
+    if (is_synthetic_sorry(e) && (is_synthetic_sorry(type) || is_metavar(type))) {
+        // do not show useless type-checking results such as ?? : ?M_1
+        return;
+    }
+    auto out              = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION);
+    formatter fmt         = out.get_formatter();
+    unsigned indent       = get_pp_indent(p.get_options());
+    format e_fmt    = fmt(e);
+    format type_fmt = fmt(type);
+    format r = group(e_fmt + space() + colon() + nest(indent, line() + type_fmt));
+    out.set_caption("check result") << r;
+    out.report();
+}
+
 void elab_constant_cmd(parser & p, expr const & cmd) {
     buffer<expr> args, ls;
     get_app_args(mdata_expr(cmd), args);
@@ -73,6 +100,9 @@ void elaborate_command(parser & p, expr const & cmd) {
         if (*cmd_name == "attribute") {
             p.set_env(elab_attribute_cmd(p.env(), cmd));
             return;
+        } else if (*cmd_name == "#check") {
+            elab_check_cmd(p, cmd);
+            return;
         } else if (*cmd_name == "constant") {
             elab_constant_cmd(p, cmd);
             return;