From 4560413a92fa471e14f92aeac3c427595800e4c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Jun 2014 11:35:12 -0700
Subject: [PATCH] feat(frontends/lean): add '[fact]' modifier for 'have'
 expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_exprs.cpp | 16 +++++++++++++---
 src/frontends/lean/token_table.cpp   |  2 +-
 tests/lean/run/have1.lean            |  8 ++++++++
 tests/lean/run/have2.lean            |  8 ++++++++
 4 files changed, 30 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/have1.lean
 create mode 100644 tests/lean/run/have2.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 5e734ba46..22531ef72 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -19,6 +19,7 @@ static name g_in("in");
 static name g_colon(":");
 static name g_assign(":=");
 static name g_comma(",");
+static name g_fact("[fact]");
 static name g_from("from");
 static name g_using("using");
 static name g_by("by");
@@ -143,9 +144,18 @@ static expr parse_proof(parser & p, expr const & prop) {
     }
 }
 
+static void parse_have_modifiers(parser & p, bool & is_fact) {
+    if (p.curr_is_token(g_fact)) {
+        p.next();
+        is_fact = true;
+    }
+}
+
 static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
-    auto id_pos = p.pos();
-    name id     = p.check_id_next("invalid 'have' declaration, identifier expected");
+    auto id_pos  = p.pos();
+    bool is_fact = false;
+    name id      = p.check_id_next("invalid 'have' declaration, identifier expected");
+    parse_have_modifiers(p, is_fact);
     expr prop;
     if (p.curr_is_token(g_colon)) {
         p.next();
@@ -158,7 +168,7 @@ static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos)
     p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
     parser::local_scope scope(p);
     expr l = p.save_pos(mk_local(id, prop), pos);
-    binder_info bi = mk_contextual_info(false);
+    binder_info bi = mk_contextual_info(is_fact);
     p.add_local(l, bi);
     expr body  = abstract(p.parse_expr(), l);
     // remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables.
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 6c9e41c09..11df05cda 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -62,7 +62,7 @@ token_table init_token_table() {
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]",
-                               "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation",
+                               "variables", "{variables}", "[variables]", "[private]", "[inline]", "[fact]", "abbreviation",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "set_option",
diff --git a/tests/lean/run/have1.lean b/tests/lean/run/have1.lean
new file mode 100644
index 000000000..549d66e6d
--- /dev/null
+++ b/tests/lean/run/have1.lean
@@ -0,0 +1,8 @@
+abbreviation Bool : Type.{1} := Type.{0}
+variables a b c : Bool
+axiom Ha : a
+axiom Hb : b
+axiom Hc : c
+check have H1 : a, from Ha,
+      have H2 : a, using H1, from H1,
+      H2
\ No newline at end of file
diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean
new file mode 100644
index 000000000..8afd796d9
--- /dev/null
+++ b/tests/lean/run/have2.lean
@@ -0,0 +1,8 @@
+abbreviation Bool : Type.{1} := Type.{0}
+variables a b c : Bool
+axiom Ha : a
+axiom Hb : b
+axiom Hc : c
+check have H1 [fact] : a, from Ha,
+      have H2 : a, from H1,
+      H2
\ No newline at end of file