From 593f1f2ebd2835cd411db2837ad4dda60809855b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Feb 2014 20:47:39 -0800
Subject: [PATCH] fix(frontends/lean): allow user set constants defined in
 other namespaces as opaque

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser_cmds.cpp  | 14 +++++++++++---
 tests/lean/opaque.lean              | 18 ++++++++++++++++++
 tests/lean/opaque.lean.expected.out |  8 ++++++++
 3 files changed, 37 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/opaque.lean
 create mode 100644 tests/lean/opaque.lean.expected.out

diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index 0bc40f14a..31f94254e 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -547,6 +547,7 @@ void parser_imp::parse_set_option() {
 /** Parse 'SetOpaque' [id] [true/false] */
 void parser_imp::parse_set_opaque() {
     next();
+    auto p = pos();
     name id;
     if (curr() == scanner::token::Exists) {
         id = "exists";
@@ -555,13 +556,20 @@ void parser_imp::parse_set_opaque() {
         id = curr_name();
     }
     next();
-    name full_id = mk_full_name(id);
+    expr d = get_name_ref(id, p, false);
+    name real_id;
+    if (is_constant(d))
+        real_id = const_name(d);
+    else if (is_value(d))
+        real_id = to_value(d).get_name();
+    else
+        throw parser_error(sstream() << "invalid set opaque, identifier '" << id << "' cannot be set opaque", p);
     auto val_pos = pos();
     name val = check_identifier_next("invalid opaque flag, true/false expected");
     if (val == "true")
-        m_env->set_opaque(full_id, true);
+        m_env->set_opaque(real_id, true);
     else if (val == "false")
-        m_env->set_opaque(full_id, false);
+        m_env->set_opaque(real_id, false);
     else
         throw parser_error("invalid opaque flag, true/false expected", val_pos);
 }
diff --git a/tests/lean/opaque.lean b/tests/lean/opaque.lean
new file mode 100644
index 000000000..fa7da92c9
--- /dev/null
+++ b/tests/lean/opaque.lean
@@ -0,0 +1,18 @@
+import macros
+import pair
+import subtype
+import optional
+using subtype
+using optional
+
+namespace sum
+
+set_opaque optional false
+set_opaque subtype false
+set_opaque some false
+set_opaque optional::none false
+set_opaque rep false
+set_opaque subtype::abst false
+set_opaque optional_pred false
+
+end
diff --git a/tests/lean/opaque.lean.expected.out b/tests/lean/opaque.lean.expected.out
new file mode 100644
index 000000000..9f16b35a4
--- /dev/null
+++ b/tests/lean/opaque.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Imported 'pair'
+  Imported 'subtype'
+  Imported 'optional'
+  Using: subtype
+  Using: optional