From 6ea7bb3ea43b4f93aaccdf7ebc96f0917b03b3be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 4 Jul 2014 18:33:46 -0700
Subject: [PATCH] feat(frontends/lean/builtin_exprs): add 'including'
 expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/emacs/lean-mode.el               |  2 +-
 src/frontends/lean/builtin_exprs.cpp | 28 ++++++++++++++++++++++++++++
 src/frontends/lean/token_table.cpp   |  2 +-
 3 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 6734720cb..a1abe4f6b 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -24,7 +24,7 @@
 (define-generic-mode
     'lean-mode     ;; name of the mode to create
   '("--")          ;; comments start with
-  '("import" "abbreviation" "definition" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords
+  '("import" "abbreviation" "definition" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords
   '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 401cefbe4..5f7677503 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/sstream.h"
 #include "kernel/abstract.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
@@ -288,6 +289,32 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
     return p.save_pos(mk_explicit(e), pos);
 }
 
+static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    buffer<expr> locals;
+    while (!p.curr_is_token(g_comma)) {
+        auto pos = p.pos();
+        name id  = p.check_id_next("invalid 'including', identifier expected");
+        if (auto it = p.get_local(id)) {
+            locals.push_back(*it);
+        } else {
+            throw parser_error(sstream() << "invalid 'including', '" << id << "' is not a local declaraton", pos);
+        }
+    }
+    p.next();
+    parser::local_scope scope(p);
+    buffer<expr> new_locals;
+    for (auto old_l : locals) {
+        binder_info bi = local_info(old_l);
+        bi = bi.update_contextual(true);
+        expr new_l     = p.save_pos(mk_local(local_pp_name(old_l), mlocal_type(old_l), bi), pos);
+        p.add_local(new_l);
+        new_locals.push_back(new_l);
+    }
+    expr r = p.rec_save_pos(Fun(new_locals, p.parse_expr()), pos);
+    r = p.rec_save_pos(mk_app(r, locals), pos);
+    return r;
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -307,6 +334,7 @@ parse_table init_nud_table() {
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
+    r = r.add({transition("including", mk_ext_action(parse_including_expr))}, x0);
     return r;
 }
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index fc76c2504..89172ae7b 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -59,7 +59,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"!", 0}, {"with", 0},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec},
+         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec}, {"including", 0},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",