From bbff564a1ce5a58f3226f044c8efc7855fbb7ebe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 6 Sep 2014 11:05:07 -0700 Subject: [PATCH] feat(frontends/lean): persistent notation in sections Signed-off-by: Leonardo de Moura --- library/data/list/basic.lean | 5 --- library/struc/binary.lean | 50 ++++++++++++------------- src/frontends/lean/notation_cmd.cpp | 56 +++++++++++++++++++++++++++- src/frontends/lean/parser_config.cpp | 8 ++-- src/library/scoped_ext.h | 1 + tests/lean/run/algebra1.lean | 2 +- tests/lean/run/cody1.lean | 2 +- tests/lean/run/cody2.lean | 2 +- tests/lean/run/group.lean | 2 +- tests/lean/run/group2.lean | 2 +- tests/lean/run/n4.lean | 4 +- tests/lean/run/secnot.lean | 25 +++++++++++++ 12 files changed, 115 insertions(+), 44 deletions(-) create mode 100644 tests/lean/run/secnot.lean diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 98daa1e25..b797b1b6d 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -276,10 +276,5 @@ nat.rec (λl, head x l) (λm f l, f (tail l)) n l theorem nth_zero {x : T} {l : list T} : nth x l 0 = head x l theorem nth_succ {x : T} {l : list T} {n : ℕ} : nth x l (succ n) = nth x (tail l) n - end - --- declare global notation outside the section -infixl `++` := concat - end list diff --git a/library/struc/binary.lean b/library/struc/binary.lean index cb60d8d12..2803ad305 100644 --- a/library/struc/binary.lean +++ b/library/struc/binary.lean @@ -5,32 +5,30 @@ import logic.core.eq open eq_ops namespace binary -section - parameter {A : Type} - parameter f : A → A → A - infixl `*`:75 := f + context + parameter {A : Type} + parameter f : A → A → A + infixl `*`:75 := f + abbreviation commutative := ∀{a b}, a*b = b*a + abbreviation associative := ∀{a b c}, (a*b)*c = a*(b*c) + end - abbreviation commutative := ∀a b, a*b = b*a - abbreviation associative := ∀a b c, (a*b)*c = a*(b*c) -end + context + parameter {A : Type} + parameter {f : A → A → A} + hypothesis H_comm : commutative f + hypothesis H_assoc : associative f + infixl `*`:75 := f + theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) := + take a b c, calc + a*(b*c) = (a*b)*c : H_assoc⁻¹ + ... = (b*a)*c : {H_comm} + ... = b*(a*c) : H_assoc -section - parameter {A : Type} - parameter {f : A → A → A} - infixl `*`:75 := f - hypothesis H_comm : commutative f - hypothesis H_assoc : associative f - - theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) := - take a b c, calc - a*(b*c) = (a*b)*c : (H_assoc _ _ _)⁻¹ - ... = (b*a)*c : {H_comm _ _} - ... = b*(a*c) : H_assoc _ _ _ - - theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b := - take a b c, calc - (a*b)*c = a*(b*c) : H_assoc _ _ _ - ... = a*(c*b) : {H_comm _ _} - ... = (a*c)*b : (H_assoc _ _ _)⁻¹ -end + theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b := + take a b c, calc + (a*b)*c = a*(b*c) : H_assoc + ... = a*(c*b) : {H_comm} + ... = (a*c)*b : H_assoc⁻¹ + end end binary diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index f5d9fdff9..f0a0b3fc0 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -7,7 +7,11 @@ Author: Leonardo de Moura #include #include #include +#include "util/sstream.h" #include "kernel/abstract.h" +#include "kernel/replace_fn.h" +#include "library/scoped_ext.h" +#include "library/explicit.h" #include "frontends/lean/parser.h" namespace lean { @@ -69,6 +73,54 @@ environment precedence_cmd(parser & p) { return add_token(p.env(), tk.c_str(), prec); } +/** \brief Auxiliary function for #cleanup_section_notation. */ +expr cleanup_section_notation_core(parser & p, expr const & e) { + if (is_implicit(e)) { + return cleanup_section_notation_core(p, get_implicit_arg(e)); + } else if (is_explicit(e)) { + return cleanup_section_notation_core(p, get_explicit_arg(e)); + } else if (is_app(e)) { + buffer args; + expr const & f = get_app_args(e, args); + for (expr arg : args) { + if (!is_explicit(arg)) + throw parser_error("unexpected expression in (section) notation", p.pos_of(arg)); + arg = get_explicit_arg(arg); + if (!is_local(arg)) + throw parser_error("unexpected expression in (section) notation", p.pos_of(arg)); + binder_info bi = local_info(arg); + if (!bi.is_strict_implicit() && !bi.is_implicit()) + throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(arg) + << "' in (section) notation that is not implicit", p.pos_of(e)); + } + return cleanup_section_notation_core(p, f); + } else if (is_constant(e)) { + return p.save_pos(mk_constant(const_name(e)), p.pos_of(e)); + } else if (is_local(e)) { + throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(e) + << "' in (section) notation", p.pos_of(e)); + } else { + throw parser_error("unexpected expression in (section) notation", p.pos_of(e)); + } +} + +/** \brief Replace reference to implicit section local constants and universes with placeholders. + + \remark Throws an exception if \c e contains a local constant that is not implicit. +*/ +expr cleanup_section_notation(parser & p, expr const & e) { + if (!in_section(p.env())) + return e; + return replace(e, [&](expr const & e) { + if (is_local(e)) + throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(e) + << "' in (section) notation", p.pos_of(e)); + if (is_implicit(e)) + return some_expr(cleanup_section_notation_core(p, e)); + return none_expr(); + }); +} + enum class mixfix_kind { infixl, infixr, postfix, prefix }; using notation::mk_expr_action; @@ -102,7 +154,7 @@ static pair> parse_mixfix_notation(parser if (k == mixfix_kind::infixr && *prec == 0) throw parser_error("invalid infixr declaration, precedence must be greater than zero", p.pos()); p.check_token_next(g_assign, "invalid notation declaration, ':=' expected"); - expr f = p.parse_expr(); + expr f = cleanup_section_notation(p, p.parse_expr()); char const * tks = tk.c_str(); switch (k) { case mixfix_kind::infixl: @@ -166,7 +218,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer & new_t static expr parse_notation_expr(parser & p, buffer const & locals) { expr r = p.parse_expr(); - return abstract(r, locals.size(), locals.data()); + return cleanup_section_notation(p, abstract(r, locals.size(), locals.data())); } static expr g_local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 195b12318..1676faee9 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -54,8 +54,8 @@ struct token_config { } }; -template class scoped_ext; -typedef scoped_ext token_ext; +template class scoped_ext; +typedef scoped_ext token_ext; environment add_token(environment const & env, token_entry const & e) { return token_ext::add_entry(env, get_dummy_ios(), e); @@ -188,8 +188,8 @@ struct notation_config { } }; -template class scoped_ext; -typedef scoped_ext notation_ext; +template class scoped_ext; +typedef scoped_ext notation_ext; environment add_notation(environment const & env, notation_entry const & e) { return notation_ext::add_entry(env, get_dummy_ios(), e); diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 265500572..bc6022758 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -38,6 +38,7 @@ name const & get_namespace(environment const & env); list const & get_namespaces(environment const & env); bool in_section_or_context(environment const & env); bool in_context(environment const & env); +inline bool in_section(environment const & env) { return in_section_or_context(env) && !in_context(env); } /** \brief Check if \c n may be a reference to a namespace, if it is return it. The procedure checks if \c n is a registered namespace, if it is not, it tries diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean index 6ce0a6d73..0bfeb9ecd 100644 --- a/tests/lean/run/algebra1.lean +++ b/tests/lean/run/algebra1.lean @@ -2,7 +2,7 @@ import logic abbreviation Type1 := Type.{1} -section +context parameter {A : Type} parameter f : A → A → A parameter one : A diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean index e4a7484a1..c58e1ffa7 100644 --- a/tests/lean/run/cody1.lean +++ b/tests/lean/run/cody1.lean @@ -2,7 +2,7 @@ import logic abbreviation subsets (P : Type) := P → Prop. -section +context hypothesis A : Type. diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean index 557290cfe..4aa70076e 100644 --- a/tests/lean/run/cody2.lean +++ b/tests/lean/run/cody2.lean @@ -2,7 +2,7 @@ import logic open eq abbreviation subsets (P : Type) := P → Prop. -section +context hypothesis A : Type. diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index b74370e51..477b95cc0 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -1,6 +1,6 @@ import logic -section +context parameter {A : Type} parameter f : A → A → A parameter one : A diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index c432a20ba..f2627850f 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -1,6 +1,6 @@ import logic -section +context parameter {A : Type} parameter f : A → A → A parameter one : A diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean index 50093aae5..fc9b6afb3 100644 --- a/tests/lean/run/n4.lean +++ b/tests/lean/run/n4.lean @@ -1,5 +1,5 @@ definition Prop [inline] : Type.{1} := Type.{0} -section +context variable N : Type.{1} variables a b c : N variable and : Prop → Prop → Prop @@ -17,4 +17,4 @@ end check T (* print(get_env():find("T"):value()) -*) \ No newline at end of file +*) diff --git a/tests/lean/run/secnot.lean b/tests/lean/run/secnot.lean new file mode 100644 index 000000000..e5ee67637 --- /dev/null +++ b/tests/lean/run/secnot.lean @@ -0,0 +1,25 @@ +import data.num + +section +parameter {A : Type} +definition f (a b : A) := a +infixl `◀`:65 := f +parameters a b : A +check a ◀ b +end + +inductive list (T : Type) : Type := +nil {} : list T, +cons : T → list T → list T + +namespace list +section +variable {T : Type} +notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l +check [10, 20, 30] +end +end list + +open list +check [10, 20, 40] +check 10 ◀ 20