From 01d4644026285aeebb35094dc82930dd9cc90f1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Oct 2014 08:52:35 -0700 Subject: [PATCH] fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored --- src/frontends/lean/parser.cpp | 30 ++++--- src/frontends/lean/parser.h | 35 +++++--- tests/lean/run/group3.lean | 154 ++++++++++++++++------------------ 3 files changed, 111 insertions(+), 108 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index aa71c670f..6aaa876c6 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -93,11 +93,11 @@ parser::parser(environment const & env, io_state const & ios, m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) { if (s) { - m_local_level_decls = s->m_lds; - 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_local_level_decls = s->m_lds; + m_local_decls = s->m_eds; + m_variables = s->m_vars; + m_include_vars = s->m_include_vars; + 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 const & args, pos_info const & p void parser::push_local_scope(bool save_options) { m_local_level_decls.push(); m_local_decls.push(); + optional opts; if (save_options) - m_options_stack = cons(optional(m_ios.get_options()), m_options_stack); - else - m_options_stack = cons(optional(), m_options_stack); + opts = m_ios.get_options(); + m_parser_scope_stack = cons(parser_scope_stack_elem(opts, m_variables, m_include_vars), + 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)); - if (auto const & it = head(m_options_stack)) { - m_ios.set_options(*it); + lean_assert(!is_nil(m_parser_scope_stack)); + auto s = head(m_parser_scope_stack); + 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(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() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d2d1307b3..4d038d156 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -43,26 +43,35 @@ struct parser_error : public exception { struct interrupt_parser {}; typedef local_decls local_expr_decls; typedef local_decls local_level_decls; -typedef list> 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 m_options; + name_set m_variables; + name_set m_include_vars; + parser_scope_stack_elem(optional 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; + /** \brief Snapshot of the state of the Lean parser */ struct snapshot { - environment m_env; - local_level_decls m_lds; - 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; - unsigned m_line; + environment m_env; + local_level_decls m_lds; + 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 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, - unsigned line): + name_set const & vars, name_set const & includes, options const & opts, + 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_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; diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean index 04ba739f9..5fcc1ab84 100644 --- a/tests/lean/run/group3.lean +++ b/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 := - semigroup.mk (comm_semigroup.mul) (@comm_semigroup.assoc _ _) + variables a b c : A + 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) := - binary.left_comm (@mul_comm) (@mul_assoc _ _) a b c + theorem mul_left_comm : a * (b * c) = b * (a * 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 - definition one : A := monoid.rec (λmul one assoc right_id left_id, one) s - definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := + variables a b c : A + definition mul := monoid.rec (λmul one assoc right_id left_id, mul) s a b + 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) - definition monoid_semigroup [instance] : including A s, semigroup A := - semigroup.mk (monoid.mul) (@monoid.assoc _ _) + variable a : A + include s + 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_left_id {a : A} : including s, one * a = a := monoid.left_id + theorem mul_right_id : a * one = a := !monoid.right_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 - definition one : A := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s - definition assoc {a b c : A} : mul (mul a b) c = mul a (mul b c) := + include s + variables a b c : A + 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 := - monoid.mk (comm_monoid.mul) (comm_monoid.one) (@comm_monoid.assoc _ _) - (@comm_monoid.right_id _ _) (@comm_monoid.left_id _ _) - definition comm_monoid_comm_semigroup [instance] : including A s, comm_semigroup A := - comm_semigroup.mk (comm_monoid.mul) (@comm_monoid.assoc _ _) (@comm_monoid.comm _ _) + include s + definition comm_monoid_monoid [instance] : monoid A := + monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc + comm_monoid.right_id comm_monoid.left_id + 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) - definition carrier : Type := Semigroup.rec (λc s, c) S - definition struc : semigroup carrier := Semigroup.rec (λc s, s) S - end -end Semigroup -coercion Semigroup.carrier -instance Semigroup.struc +section + parameter S : Semigroup + definition Semigroup.carrier [coercion] : Type := Semigroup.rec (λc s, c) S + definition Semigroup.struc [instance] : semigroup S := Semigroup.rec (λc s, s) S +end inductive CommSemigroup [class] : Type := mk : Π carrier : Type, comm_semigroup carrier → CommSemigroup -namespace CommSemigroup - section - parameter (S : CommSemigroup) - definition carrier : Type := CommSemigroup.rec (λc s, c) S - definition struc : comm_semigroup carrier := CommSemigroup.rec (λc s, s) S - end -end CommSemigroup -coercion CommSemigroup.carrier -instance CommSemigroup.struc +section + parameter S : CommSemigroup + definition CommSemigroup.carrier [coercion] : Type := CommSemigroup.rec (λc s, c) S + definition CommSemigroup.struc [instance] : comm_semigroup S := CommSemigroup.rec (λc s, s) S +end inductive Monoid [class] : Type := mk : Π carrier : Type, monoid carrier → Monoid -namespace Monoid - section - parameter (S : Monoid) - definition carrier : Type := Monoid.rec (λc s, c) S - definition struc : monoid carrier := Monoid.rec (λc s, s) S - end -end Monoid -coercion Monoid.carrier -instance Monoid.struc +section + parameter S : Monoid + definition Monoid.carrier [coercion] : Type := Monoid.rec (λc s, c) S + definition Monoid.struc [instance] : monoid S := Monoid.rec (λc s, s) S +end inductive CommMonoid : Type := mk : Π carrier : Type, comm_monoid carrier → CommMonoid -namespace CommMonoid - section - parameter (S : CommMonoid) - definition carrier : Type := CommMonoid.rec (λc s, c) S - definition struc : comm_monoid carrier := CommMonoid.rec (λc s, s) S - end -end CommMonoid -coercion CommMonoid.carrier -instance CommMonoid.struc - +section + parameter S : CommMonoid + definition CommMonoid.carrier [coercion] : Type := CommMonoid.rec (λc s, c) S + definition CommMonoid.struc [instance] : comm_monoid S := CommMonoid.rec (λc s, s) S +end 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) : mul_assoc + a * (b * c) * d = a * b * c * d : {symm !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) : mul_assoc + a * (b * c) * d = a * b * c * d : {symm !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 * (b * c) : mul_assoc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = 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 * (b * c) : mul_assoc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = 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 * (b * c) : mul_assoc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = 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 * (b * c) : mul_assoc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = a * (b * c) : !mul_assoc end examples