From d8caa294b5adbd6b46e148343fc812b2f6298b7a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 11:02:01 -0700
Subject: [PATCH] fix(frontends/lean/parser): configuration options defined in
 a context are transient, fixes #162

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_cmds.cpp |  3 ++-
 src/frontends/lean/parser.cpp       | 11 ++++++++++-
 src/frontends/lean/parser.h         |  4 +++-
 tests/lean/ctxopt.lean              |  9 +++++++++
 tests/lean/ctxopt.lean.expected.out |  2 ++
 5 files changed, 26 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/ctxopt.lean
 create mode 100644 tests/lean/ctxopt.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3627171f0..6612fece9 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -76,7 +76,8 @@ environment context_cmd(parser & p) {
     name n;
     if (p.curr_is_identifier())
         n = p.check_atomic_id_next("invalid context, atomic identifier expected");
-    p.push_local_scope();
+    bool save_options = true;
+    p.push_local_scope(save_options);
     return push_scope(p.env(), p.ios(), scope_kind::Context, n);
 }
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9152fc87a..378c30c53 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -389,14 +389,23 @@ expr parser::mk_app(std::initializer_list<expr> const & args, pos_info const & p
     return r;
 }
 
-void parser::push_local_scope() {
+void parser::push_local_scope(bool save_options) {
     m_local_level_decls.push();
     m_local_decls.push();
+    if (save_options)
+        m_options_stack.push_back(optional<options>(m_ios.get_options()));
+    else
+        m_options_stack.push_back(optional<options>());
 }
 
 void parser::pop_local_scope() {
     m_local_level_decls.pop();
     m_local_decls.pop();
+    if (auto const & it = m_options_stack.back()) {
+        m_ios.set_options(*it);
+        updt_options();
+    }
+    m_options_stack.pop_back();
 }
 
 void parser::add_local_level(name const & n, level const & l) {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 7c3157ae6..be4a5602b 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -61,6 +61,7 @@ struct snapshot {
 typedef std::vector<snapshot> snapshot_vector;
 
 class parser {
+    typedef std::vector<optional<options>> options_stack;
     environment             m_env;
     io_state                m_ios;
     name_generator          m_ngen;
@@ -72,6 +73,7 @@ class parser {
     scanner::token_kind     m_curr;
     local_level_decls       m_local_level_decls;
     local_expr_decls        m_local_decls;
+    options_stack           m_options_stack;
     pos_info                m_last_cmd_pos;
     pos_info                m_last_script_pos;
     unsigned                m_next_tag_idx;
@@ -162,7 +164,7 @@ class parser {
     friend environment context_cmd(parser & p);
     friend environment end_scoped_cmd(parser & p);
 
-    void push_local_scope();
+    void push_local_scope(bool save_options = false);
     void pop_local_scope();
 
     void save_snapshot();
diff --git a/tests/lean/ctxopt.lean b/tests/lean/ctxopt.lean
new file mode 100644
index 000000000..af96a7f26
--- /dev/null
+++ b/tests/lean/ctxopt.lean
@@ -0,0 +1,9 @@
+import logic
+definition id {A : Type} (a : A) := a
+
+context
+  set_option pp.implicit true
+  check id true
+end
+
+check id true
diff --git a/tests/lean/ctxopt.lean.expected.out b/tests/lean/ctxopt.lean.expected.out
new file mode 100644
index 000000000..d75e4dd64
--- /dev/null
+++ b/tests/lean/ctxopt.lean.expected.out
@@ -0,0 +1,2 @@
+@id Prop true : Prop
+id true : Prop