From bc95f09828313007792c1fbc3545573fbac99b57 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Feb 2015 12:56:52 -0800
Subject: [PATCH] feat(frontends/lean/decl_cmds): allow user to specify
 unfold-c hint

---
 src/frontends/lean/decl_cmds.cpp   | 10 ++++++++++
 src/frontends/lean/token_table.cpp |  2 +-
 src/frontends/lean/tokens.cpp      |  4 ++++
 src/frontends/lean/tokens.h        |  1 +
 4 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 43e5b17ed..efe5f78b9 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -279,6 +279,7 @@ struct decl_attributes {
     bool               m_is_class;
     bool               m_has_multiple_instances;
     optional<unsigned> m_priority;
+    optional<unsigned> m_unfold_c_hint;
 
     decl_attributes(bool def_only = true):m_priority() {
         m_def_only               = def_only;
@@ -347,6 +348,13 @@ struct decl_attributes {
                 m_priority = *it;
                 if (!m_is_instance)
                     throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]'", pos);
+            } else if (p.curr_is_token(get_unfold_c_tk())) {
+                p.next();
+                unsigned r = p.parse_small_nat();
+                if (r == 0)
+                    throw parser_error("invalid '[unfold-c]' attribute, value must be greater than 0", pos);
+                m_unfold_c_hint = r - 1;
+                p.check_token_next(get_rbracket_tk(), "invalid 'unfold-c', ']' expected");
             } else {
                 break;
             }
@@ -374,6 +382,8 @@ struct decl_attributes {
             env = add_class(env, d, persistent);
         if (m_has_multiple_instances)
             env = mark_multiple_instances(env, d, persistent);
+        if (m_unfold_c_hint)
+            env = add_unfold_c_hint(env, d, m_unfold_c_hint, persistent);
         return env;
     }
 };
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 68dea0c80..3d5d4c698 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
-         "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[priority", "print", "end", "namespace", "section", "prelude",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index ee3a4416a..056e3e9a4 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -94,6 +94,7 @@ static name * g_variables    = nullptr;
 static name * g_opaque       = nullptr;
 static name * g_instance     = nullptr;
 static name * g_priority     = nullptr;
+static name * g_unfold_c     = nullptr;
 static name * g_coercion     = nullptr;
 static name * g_reducible    = nullptr;
 static name * g_irreducible  = nullptr;
@@ -208,6 +209,7 @@ void initialize_tokens() {
     g_variables    = new name("variables");
     g_instance     = new name("[instance]");
     g_priority     = new name("[priority");
+    g_unfold_c     = new name("[unfold-c");
     g_coercion     = new name("[coercion]");
     g_reducible    = new name("[reducible]");
     g_irreducible  = new name("[irreducible]");
@@ -265,6 +267,7 @@ void finalize_tokens() {
     delete g_variable;
     delete g_instance;
     delete g_priority;
+    delete g_unfold_c;
     delete g_coercion;
     delete g_reducible;
     delete g_irreducible;
@@ -437,6 +440,7 @@ name const & get_variables_tk() { return *g_variables; }
 name const & get_opaque_tk() { return *g_opaque; }
 name const & get_instance_tk() { return *g_instance; }
 name const & get_priority_tk() { return *g_priority; }
+name const & get_unfold_c_tk() { return *g_unfold_c; }
 name const & get_coercion_tk() { return *g_coercion; }
 name const & get_reducible_tk() { return *g_reducible; }
 name const & get_irreducible_tk() { return *g_irreducible; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 7976798ef..70e25e8ba 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -96,6 +96,7 @@ name const & get_variables_tk();
 name const & get_opaque_tk();
 name const & get_instance_tk();
 name const & get_priority_tk();
+name const & get_unfold_c_tk();
 name const & get_coercion_tk();
 name const & get_reducible_tk();
 name const & get_irreducible_tk();