From 8e6de933948748b26ff685bedb76f3e691df9e36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 26 Oct 2014 09:47:11 -0700 Subject: [PATCH] fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant --- src/frontends/lean/builtin_exprs.cpp | 4 +- src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/parser.cpp | 20 ++++--- src/frontends/lean/parser.h | 15 +++-- tests/lean/run/tree2.lean | 84 ++++++++++++++++++++++++++++ 5 files changed, 108 insertions(+), 17 deletions(-) create mode 100644 tests/lean/run/tree2.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 69343f0cc..2b6a8b968 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -128,7 +128,7 @@ static environment open_tactic_namespace(parser & p) { } static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { - parser::no_undef_id_error_scope scope(p); + parser::undef_id_to_local_scope scope(p); environment env = open_tactic_namespace(p); expr t = p.parse_scoped_expr(0, nullptr, env); return p.mk_by(t, pos); @@ -140,7 +140,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) { optional pre_tac = get_begin_end_pre_tactic(p.env()); buffer tacs; bool first = true; - parser::no_undef_id_error_scope scope(p); + parser::undef_id_to_local_scope scope(p); environment env = open_tactic_namespace(p); while (!p.curr_is_token(get_end_tk())) { if (first) { diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 3b4bd83dd..18bcf9013 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -698,7 +698,7 @@ struct inductive_cmd_fn { } environment operator()() { - parser::no_undef_id_error_scope err_scope(m_p); + parser::undef_id_to_const_scope err_scope(m_p); buffer decls; { parser::local_scope scope(m_p); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 6b2caa2c8..f3e527285 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -75,12 +75,10 @@ parser::local_scope::~local_scope() { m_p.m_env = m_env; } -parser::no_undef_id_error_scope::no_undef_id_error_scope(parser & p):m_p(p), m_old(m_p.m_no_undef_id_error) { - m_p.m_no_undef_id_error = true; -} -parser::no_undef_id_error_scope::~no_undef_id_error_scope() { - m_p.m_no_undef_id_error = m_old; -} +parser::undef_id_to_const_scope::undef_id_to_const_scope(parser & p): + flet(p.m_undef_id_behavior, undef_id_behavior::AssumeConstant) {} +parser::undef_id_to_local_scope::undef_id_to_local_scope(parser & p): + flet(p.m_undef_id_behavior, undef_id_behavior::AssumeLocal) {} static name * g_tmp_prefix = nullptr; @@ -104,7 +102,7 @@ parser::parser(environment const & env, io_state const & ios, m_parser_scope_stack = s->m_parser_scope_stack; } m_num_threads = num_threads; - m_no_undef_id_error = false; + m_undef_id_behavior = undef_id_behavior::Error; m_found_errors = false; m_used_sorry = false; updt_options(); @@ -1067,8 +1065,12 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { r = save_pos(mk_choice(new_as.size(), new_as.data()), p); save_overload(*r); } - if (!r && m_no_undef_id_error) - r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p); + if (!r) { + if (m_undef_id_behavior == undef_id_behavior::AssumeConstant) + r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p); + else if (m_undef_id_behavior == undef_id_behavior::AssumeLocal) + r = save_pos(mk_local(id, mk_expr_placeholder()), p); + } if (!r) throw parser_error(sstream() << "unknown identifier '" << id << "'", p); save_type_info(*r); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index cefd3e653..c3e369f81 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/flet.h" #include "util/script_state.h" #include "util/name_map.h" #include "util/exception.h" @@ -80,6 +81,8 @@ typedef std::vector snapshot_vector; enum class keep_theorem_mode { All, DiscardImported, DiscardAll }; +enum class undef_id_behavior { Error, AssumeConstant, AssumeLocal }; + class parser { environment m_env; io_state m_ios; @@ -105,7 +108,7 @@ class parser { // By default, when the parser finds a unknown identifier, it signs an error. // When the following flag is true, it creates a constant. // This flag is when we are trying to parse mutually recursive declarations. - bool m_no_undef_id_error; + undef_id_behavior m_undef_id_behavior; optional m_has_num; optional m_has_string; optional m_has_tactic_decls; @@ -371,11 +374,13 @@ public: /** \brief Return all local level declarations */ list> const & get_local_level_entries() const { return m_local_level_decls.get_entries(); } /** \brief By default, when the parser finds a unknown identifier, it signs an error. - This scope object temporarily changes this behavior. In any scope where this object - is declared, the parse creates a constant even when the identifier is unknown. - This behavior is useful when we are trying to parse mutually recursive declarations. + These scope objects temporarily change this behavior. In any scope where this object + is declared, the parse creates a constant/local even when the identifier is unknown. + This behavior is useful when we are trying to parse mutually recursive declarations and + tactics. */ - struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); }; + struct undef_id_to_const_scope : public flet { undef_id_to_const_scope(parser & p); }; + struct undef_id_to_local_scope : public flet { undef_id_to_local_scope(parser &); }; /** \brief Elaborate \c e, and tolerate metavariables in the result. */ std::tuple elaborate_relaxed(expr const & e, list const & ctx = list()); diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean new file mode 100644 index 000000000..38083fa90 --- /dev/null +++ b/tests/lean/run/tree2.lean @@ -0,0 +1,84 @@ +import logic data.prod +open eq.ops prod tactic + +inductive tree (A : Type) := +leaf : A → tree A, +node : tree A → tree A → tree A + +inductive one.{l} : Type.{max 1 l} := +star : one + +set_option pp.universes true + +namespace tree + section + universe variables l₁ l₂ + variable {A : Type.{l₁}} + variable (C : tree A → Type.{l₂}) + definition below (t : tree A) : Type := + rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + end + + section + universe variables l₁ l₂ + variable {A : Type.{l₁}} + variable {C : tree A → Type.{l₂}} + definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t + := have general : C t × below C t, from + rec_on t + (λa, (H (leaf a) one.star, one.star)) + (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), + have b : below C (node l r), from + (pr₁ Hl, pr₁ Hr, pr₂ Hl, pr₂ Hr), + have c : C (node l r), from + H (node l r) b, + (c, b)), + pr₁ general + end + + definition no_confusion_type {A : Type} (P : Type) (t₁ t₂ : tree A) : Type := + cases_on t₁ + (λ a₁, cases_on t₂ + (λ a₂, (a₁ = a₂ → P) → P) + (λ l₂ r₂, P)) + (λ l₁ r₁, cases_on t₂ + (λ a₂, P) + (λ l₂ r₂, (l₁ = l₂ → r₁ = r₂ → P) → P)) + + set_option pp.universes true + check no_confusion_type + + definition no_confusion {A : Type} {P : Type} {t₁ t₂ : tree A} : t₁ = t₂ → no_confusion_type P t₁ t₂ := + assume e₁ : t₁ = t₂, + have aux₁ : t₁ = t₁ → no_confusion_type P t₁ t₁, from + take h, cases_on t₁ + (λ a, assume h : a = a → P, h (eq.refl a)) + (λ l r, assume h : l = l → r = r → P, h (eq.refl l) (eq.refl r)), + eq.rec aux₁ e₁ e₁ + + check no_confusion + + theorem leaf_ne_tree {A : Type} (a : A) (l r : tree A) : leaf a ≠ node l r := + assume h : leaf a = node l r, + no_confusion h + + constant A : Type₁ + constants l₁ l₂ r₁ r₂ : tree A + axiom node_eq : node l₁ r₁ = node l₂ r₂ + check no_confusion node_eq + + definition tst : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂ := no_confusion node_eq + check tst (λ e₁ e₂, e₁) + + theorem node.inj1 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ := + assume h, + have trivial : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂, from no_confusion h, + trivial (λ e₁ e₂, e₁) + + theorem node.inj2 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ := + begin + intro h, + apply (no_confusion h), + intros, assumption + end +end tree