From 8e4560a866ceac2edf56d288e19cad39b3d4c7fc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Dec 2013 13:21:36 -0800
Subject: [PATCH] feat(frontends/lean/parser): protect imported modules from
 Lua definitions and macros in the file importing the module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp       |  3 ++-
 tests/lean/macro.lean               | 11 +++++++++++
 tests/lean/macro.lean.expected.out  |  5 +++++
 tests/lean/module.lean              |  2 ++
 tests/lean/module.lean.expected.out |  3 +++
 5 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/macro.lean
 create mode 100644 tests/lean/macro.lean.expected.out
 create mode 100644 tests/lean/module.lean
 create mode 100644 tests/lean/module.lean.expected.out

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index eb5fb4692..aea843cca 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2346,7 +2346,8 @@ class parser::imp {
             return;
         }
         try {
-            parser import_parser(m_env, m_io_state, in, m_script_state, true /* use exceptions */, false /* not interactive */);
+            script_state state; // Empty state object for the imported module
+            parser import_parser(m_env, m_io_state, in, &state, true /* use exceptions */, false /* not interactive */);
             import_parser();
         } catch (interrupted &) {
             throw;
diff --git a/tests/lean/macro.lean b/tests/lean/macro.lean
new file mode 100644
index 000000000..fa7434d91
--- /dev/null
+++ b/tests/lean/macro.lean
@@ -0,0 +1,11 @@
+(**
+macro("IdMacro",
+      { macro_arg.Expr },
+      function (env, e)
+         return e
+      end
+)
+**)
+
+Show IdMacro 10.
+Import "module.lean"
diff --git a/tests/lean/macro.lean.expected.out b/tests/lean/macro.lean.expected.out
new file mode 100644
index 000000000..62a807e22
--- /dev/null
+++ b/tests/lean/macro.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+10
+Error (line: 2, pos: 5) unknown identifier 'IdMacro'
+Error (line: 11, pos: 0) failed to import file './module.lean'
diff --git a/tests/lean/module.lean b/tests/lean/module.lean
new file mode 100644
index 000000000..7b10352c0
--- /dev/null
+++ b/tests/lean/module.lean
@@ -0,0 +1,2 @@
+(* The following command should fail because the IdMacro is not defined *)
+Show IdMacro 20.
\ No newline at end of file
diff --git a/tests/lean/module.lean.expected.out b/tests/lean/module.lean.expected.out
new file mode 100644
index 000000000..2607ee6d7
--- /dev/null
+++ b/tests/lean/module.lean.expected.out
@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+Error (line: 2, pos: 5) unknown identifier 'IdMacro'