fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored

src/frontends/lean/parser.cpp

@@ -97,7 +97,7 @@ parser::parser(environment const & env, io_state const & ios,
         m_local_decls        = s->m_eds;
         m_variables          = s->m_vars;
         m_include_vars       = s->m_include_vars;
-        m_options_stack     = s->m_options_stack;
+        m_parser_scope_stack = s->m_parser_scope_stack;
     }
     m_num_threads = num_threads;
     m_no_undef_id_error = false;
@@ -405,21 +405,25 @@ expr parser::mk_app(std::initializer_list<expr> const & args, pos_info const & p
 void parser::push_local_scope(bool save_options) {
     m_local_level_decls.push();
     m_local_decls.push();
+    optional<options> opts;
     if (save_options)
-        m_options_stack = cons(optional<options>(m_ios.get_options()), m_options_stack);
+        opts = m_ios.get_options();
-    else
+    m_parser_scope_stack = cons(parser_scope_stack_elem(opts, m_variables, m_include_vars),
-        m_options_stack = cons(optional<options>(), m_options_stack);
+                                m_parser_scope_stack);
 }
 
 void parser::pop_local_scope() {
     m_local_level_decls.pop();
     m_local_decls.pop();
-    lean_assert(!is_nil(m_options_stack));
+    lean_assert(!is_nil(m_parser_scope_stack));
-    if (auto const & it = head(m_options_stack)) {
+    auto s = head(m_parser_scope_stack);
-        m_ios.set_options(*it);
+    if (s.m_options) {
+        m_ios.set_options(*s.m_options);
         updt_options();
     }
-    m_options_stack = tail(m_options_stack);
+    m_variables          = s.m_variables;
+    m_include_vars       = s.m_include_vars;
+    m_parser_scope_stack = tail(m_parser_scope_stack);
 }
 
 void parser::add_local_level(name const & n, level const & l) {
@@ -1360,7 +1364,7 @@ void parser::save_snapshot() {
         return;
     if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
         m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_variables, m_include_vars,
-                                              m_options_stack, m_ios.get_options(), m_scanner.get_line()));
+                                              m_ios.get_options(), m_parser_scope_stack, m_scanner.get_line()));
 }
 
 void parser::save_pre_info_data() {

src/frontends/lean/parser.h

@@ -43,9 +43,18 @@ struct parser_error : public exception {
 struct interrupt_parser {};
 typedef local_decls<expr>       local_expr_decls;
 typedef local_decls<level>      local_level_decls;
-typedef list<optional<options>> options_stack;
 typedef environment             local_environment;
 
+/** \brief Extra data needed to be saved when we execute parser::push_local_scope */
+struct parser_scope_stack_elem {
+    optional<options>  m_options;
+    name_set           m_variables;
+    name_set           m_include_vars;
+    parser_scope_stack_elem(optional<options> const & o, name_set const & vs, name_set const & ivs):
+        m_options(o), m_variables(vs), m_include_vars(ivs) {}
+};
+typedef list<parser_scope_stack_elem> parser_scope_stack;
+
 /** \brief Snapshot of the state of the Lean parser */
 struct snapshot {
     environment        m_env;
@@ -53,16 +62,16 @@ struct snapshot {
     local_expr_decls   m_eds;
     name_set           m_vars; // subset of m_eds that is tagged as section variables
     name_set           m_include_vars; // subset of m_eds that must be includes
-    options_stack     m_options_stack;
     options            m_options;
+    parser_scope_stack m_parser_scope_stack;
     unsigned           m_line;
     snapshot():m_line(0) {}
     snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {}
     snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds,
-             name_set const & vars, name_set const & includes, options_stack const & os, options const & opts,
+             name_set const & vars, name_set const & includes, options const & opts,
-             unsigned line):
+             parser_scope_stack const & pss, unsigned line):
         m_env(env), m_lds(lds), m_eds(eds), m_vars(vars), m_include_vars(includes),
-        m_options_stack(os), m_options(opts), m_line(line) {}
+        m_options(opts), m_parser_scope_stack(pss), m_line(line) {}
 };
 
 typedef std::vector<snapshot> snapshot_vector;
@@ -81,7 +90,7 @@ class parser {
     local_expr_decls        m_local_decls;
     name_set                m_variables; // subset of m_local_decls that is marked as variables
     name_set                m_include_vars; // subset of m_local_decls that is marked as include
-    options_stack           m_options_stack;
+    parser_scope_stack      m_parser_scope_stack;
     pos_info                m_last_cmd_pos;
     pos_info                m_last_script_pos;
     unsigned                m_next_tag_idx;

tests/lean/run/group3.lean

@@ -49,9 +49,10 @@ end semigroup
 
 section
   parameters {A : Type} {s : semigroup A}
-  definition semigroup_has_mul [instance] : including A s, has_mul A := has_mul.mk (semigroup.mul)
+  include s
+  definition semigroup_has_mul [instance] : has_mul A := has_mul.mk (semigroup.mul)
 
-  theorem mul_assoc [instance] {a b c : A} : including A s, a * b * c = a * (b * c) :=
+  theorem mul_assoc [instance] (a b c : A) : a * b * c = a * (b * c) :=
     semigroup.assoc
 end
 
@@ -68,26 +69,28 @@ mk : Π mul: A → A → A,
 namespace comm_semigroup
   section
   parameters {A : Type} {s : comm_semigroup A}
+  variables a b c : A
   definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b
-  definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) :=
+  definition assoc : mul (mul a b) c = mul a (mul b c) :=
     comm_semigroup.rec (λmul assoc comm, assoc) s a b c
-  definition comm {a b : A} : mul a b = mul b a :=
+  definition comm : mul a b = mul b a :=
     comm_semigroup.rec (λmul assoc comm, comm) s a b
   end
 end comm_semigroup
 
 section
   parameters {A : Type} {s : comm_semigroup A}
-  definition comm_semigroup_semigroup [instance] : including A s, semigroup A :=
+  variables a b c : A
-    semigroup.mk (comm_semigroup.mul) (@comm_semigroup.assoc _ _)
+  include s
+  definition comm_semigroup_semigroup [instance] : semigroup A :=
+    semigroup.mk comm_semigroup.mul comm_semigroup.assoc
 
-  theorem mul_comm {a b : A} : including A s, a * b = b * a := comm_semigroup.comm
+  theorem mul_comm : a * b = b * a := !comm_semigroup.comm
 
-  theorem mul_left_comm {a b c : A} : including A s, a * (b * c) = b * (a * c) :=
+  theorem mul_left_comm : a * (b * c) = b * (a * c) :=
-    binary.left_comm (@mul_comm) (@mul_assoc _ _) a b c
+    binary.left_comm mul_comm mul_assoc a b c
 end
 
-
 -- monoid
 -- ------
 
@@ -102,25 +105,28 @@ mk : Π mul: A → A → A,
 namespace monoid
   section
   parameters {A : Type} {s : monoid A}
-  definition mul (a b : A) : A := monoid.rec (λmul one assoc right_id left_id, mul) s a b
+  variables a b c : A
-  definition one : A := monoid.rec (λmul one assoc right_id left_id, one) s
+  definition mul := monoid.rec (λmul one assoc right_id left_id, mul) s a b
-  definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) :=
+  definition one := monoid.rec (λmul one assoc right_id left_id, one) s
+  definition assoc : mul (mul a b) c = mul a (mul b c) :=
     monoid.rec (λmul one assoc right_id left_id, assoc) s a b c
-  definition right_id {a : A} : mul a one = a :=
+  definition right_id : mul a one = a :=
     monoid.rec (λmul one assoc right_id left_id, right_id) s a
-  definition left_id {a : A} : mul one a = a :=
+  definition left_id : mul one a = a :=
     monoid.rec (λmul one assoc right_id left_id, left_id) s a
   end
 end monoid
 
 section
   parameters {A : Type} {s : monoid A}
-  definition monoid_has_one [instance] : including A s, has_one A := has_one.mk (monoid.one)
+  variable a : A
-  definition monoid_semigroup [instance] : including A s, semigroup A :=
+  include s
-    semigroup.mk (monoid.mul) (@monoid.assoc _ _)
+  definition monoid_has_one [instance] : has_one A := has_one.mk (monoid.one)
+  definition monoid_semigroup [instance] : semigroup A :=
+    semigroup.mk monoid.mul monoid.assoc
 
-  theorem mul_right_id {a : A} : including s, a * one = a := monoid.right_id
+  theorem mul_right_id : a * one = a := !monoid.right_id
-  theorem mul_left_id {a : A} : including s, one * a = a := monoid.left_id
+  theorem mul_left_id  : one * a = a := !monoid.left_id
 end
 
 
@@ -139,95 +145,79 @@ mk : Π mul: A → A → A,
 namespace comm_monoid
   section
   parameters {A : Type} {s : comm_monoid A}
-  definition mul (a b : A) : A := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b
+  include s
-  definition one : A := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s
+  variables a b c : A
-  definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) :=
+  definition mul := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b
+  definition one := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s
+  definition assoc : mul (mul a b) c = mul a (mul b c) :=
     comm_monoid.rec (λmul one assoc right_id left_id comm, assoc) s a b c
-  definition right_id {a : A} : mul a one = a :=
+  definition right_id : mul a one = a :=
     comm_monoid.rec (λmul one assoc right_id left_id comm, right_id) s a
-  definition left_id {a : A} : mul one a = a :=
+  definition left_id : mul one a = a :=
     comm_monoid.rec (λmul one assoc right_id left_id comm, left_id) s a
-  definition comm {a b : A} : mul a b = mul b a :=
+  definition comm : mul a b = mul b a :=
     comm_monoid.rec (λmul one assoc right_id left_id comm, comm) s a b
   end
 end comm_monoid
 
 section
   parameters {A : Type} {s : comm_monoid A}
-  definition comm_monoid_monoid [instance] : including A s, monoid A :=
+  include s
-    monoid.mk (comm_monoid.mul) (comm_monoid.one) (@comm_monoid.assoc _ _)
+  definition comm_monoid_monoid [instance] : monoid A :=
-        (@comm_monoid.right_id _ _) (@comm_monoid.left_id _ _)
+    monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc
-  definition comm_monoid_comm_semigroup [instance] : including A s, comm_semigroup A :=
+              comm_monoid.right_id comm_monoid.left_id
-    comm_semigroup.mk (comm_monoid.mul) (@comm_monoid.assoc _ _) (@comm_monoid.comm _ _)
+  definition comm_monoid_comm_semigroup [instance] : comm_semigroup A :=
+    comm_semigroup.mk comm_monoid.mul comm_monoid.assoc comm_monoid.comm
 end
 
-
 -- bundled structures
 -- ------------------
 
 inductive Semigroup [class] : Type := mk : Π carrier : Type, semigroup carrier → Semigroup
-namespace Semigroup
 section
-  parameter (S : Semigroup)
+  parameter S : Semigroup
-  definition carrier : Type := Semigroup.rec (λc s, c) S
+  definition Semigroup.carrier [coercion] : Type := Semigroup.rec (λc s, c) S
-  definition struc : semigroup carrier := Semigroup.rec (λc s, s) S
+  definition Semigroup.struc   [instance] : semigroup S := Semigroup.rec (λc s, s) S
 end
-end Semigroup
-coercion Semigroup.carrier
-instance Semigroup.struc
 
 inductive CommSemigroup [class] : Type :=
   mk : Π carrier : Type, comm_semigroup carrier → CommSemigroup
-namespace CommSemigroup
 section
-  parameter (S : CommSemigroup)
+  parameter S : CommSemigroup
-  definition carrier : Type := CommSemigroup.rec (λc s, c) S
+  definition CommSemigroup.carrier [coercion] : Type := CommSemigroup.rec (λc s, c) S
-  definition struc : comm_semigroup carrier := CommSemigroup.rec (λc s, s) S
+  definition CommSemigroup.struc [instance] : comm_semigroup S := CommSemigroup.rec (λc s, s) S
 end
-end CommSemigroup
-coercion CommSemigroup.carrier
-instance CommSemigroup.struc
 
 inductive Monoid [class] : Type := mk : Π carrier : Type, monoid carrier → Monoid
-namespace Monoid
 section
-  parameter (S : Monoid)
+  parameter S : Monoid
-  definition carrier : Type := Monoid.rec (λc s, c) S
+  definition Monoid.carrier [coercion] : Type := Monoid.rec (λc s, c) S
-  definition struc : monoid carrier := Monoid.rec (λc s, s) S
+  definition Monoid.struc [instance] : monoid S := Monoid.rec (λc s, s) S
 end
-end Monoid
-coercion Monoid.carrier
-instance Monoid.struc
 
 inductive CommMonoid : Type := mk : Π carrier : Type, comm_monoid carrier → CommMonoid
-namespace CommMonoid
 section
-  parameter (S : CommMonoid)
+  parameter S : CommMonoid
-  definition carrier : Type := CommMonoid.rec (λc s, c) S
+  definition CommMonoid.carrier [coercion] : Type := CommMonoid.rec (λc s, c) S
-  definition struc : comm_monoid carrier := CommMonoid.rec (λc s, s) S
+  definition CommMonoid.struc [instance] : comm_monoid S := CommMonoid.rec (λc s, s) S
 end
-end CommMonoid
-coercion CommMonoid.carrier
-instance CommMonoid.struc
-
 end algebra
 
-
 open algebra
 
 section examples
 
 theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm mul_assoc}
+  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
-              ... = a * b * (c * d) : mul_assoc
+              ... = a * b * (c * d) : !mul_assoc
 
 theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
 
 theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm mul_assoc}
+  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
-              ... = a * b * (c * d) : mul_assoc
+              ... = a * b * (c * d) : !mul_assoc
 
 -- for test4b to work, we need instances at the level of the bundled structures as well
 definition Monoid_Semigroup [instance] (M : Monoid) : Semigroup :=
@@ -238,21 +228,21 @@ test1 a b c d
 
 theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {mul_right_id}
+  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : mul_assoc
+            ... = a * (b * c) : !mul_assoc
 
 theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {mul_right_id}
+  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : mul_assoc
+            ... = a * (b * c) : !mul_assoc
 
 theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {mul_right_id}
+  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : mul_assoc
+            ... = a * (b * c) : !mul_assoc
 
 theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {mul_right_id}
+  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : mul_assoc
+            ... = a * (b * c) : !mul_assoc
 end examples