From fbf4fd27cb32d261a85314c29a375adae55fc839 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2019 07:18:17 -0800 Subject: [PATCH] chore: update stage0 --- stage0/library/Init/Lean/Name.c | 18 ++++++++++++++++ stage0/src/frontends/lean/elaborator.cpp | 2 +- stage0/src/frontends/lean/parser.cpp | 21 +++++++++++++++++-- stage0/src/frontends/lean/util.cpp | 4 ++-- stage0/src/library/constants.cpp | 16 +++++++------- stage0/src/library/constants.h | 4 ++-- stage0/src/library/constants.txt | 4 ++-- .../library/equations_compiler/elim_match.cpp | 2 +- .../src/library/equations_compiler/util.cpp | 16 ++------------ stage0/src/library/equations_compiler/util.h | 2 +- 10 files changed, 56 insertions(+), 33 deletions(-) diff --git a/stage0/library/Init/Lean/Name.c b/stage0/library/Init/Lean/Name.c index 39b573c0a9..9c28d924ea 100644 --- a/stage0/library/Init/Lean/Name.c +++ b/stage0/library/Init/Lean/Name.c @@ -49,8 +49,10 @@ lean_object* l_Lean_mkStrName(lean_object*, lean_object*); lean_object* l_Lean_Name_DecidableEq; uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*); lean_object* l_Nat_repr(lean_object*); +lean_object* l_Lean_mkNameStr(lean_object*, lean_object*); lean_object* l_Lean_Name_append(lean_object*, lean_object*); lean_object* l_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_mkNameNum(lean_object*, lean_object*); size_t lean_name_hash_usize(lean_object*); lean_object* l_Lean_Name_HasAppend___closed__1; lean_object* l_Lean_Name_DecidableRel___boxed(lean_object*, lean_object*); @@ -8934,6 +8936,22 @@ x_4 = lean_box(x_3); return x_4; } } +lean_object* l_Lean_mkNameStr(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_mkNameNum(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_name_mk_numeral(x_1, x_2); +return x_3; +} +} lean_object* l_List_foldl___main___at_String_toName___spec__1(lean_object* x_1, lean_object* x_2) { _start: { diff --git a/stage0/src/frontends/lean/elaborator.cpp b/stage0/src/frontends/lean/elaborator.cpp index 8403d57bd3..f7c3c89c74 100644 --- a/stage0/src/frontends/lean/elaborator.cpp +++ b/stage0/src/frontends/lean/elaborator.cpp @@ -2496,7 +2496,7 @@ class validate_and_collect_lhs_mvars : public replace_visitor { virtual expr visit_app(expr const & e) override { expr it = e; while (true) { - if (is_nat_int_char_string_name_value(ctx(), it)) + if (is_nat_int_char_string_value(ctx(), it)) return e; if (!is_app(it) && !is_constant(it)) return visit(it); diff --git a/stage0/src/frontends/lean/parser.cpp b/stage0/src/frontends/lean/parser.cpp index 5dd8eac7e5..33b5d97ae9 100644 --- a/stage0/src/frontends/lean/parser.cpp +++ b/stage0/src/frontends/lean/parser.cpp @@ -391,7 +391,7 @@ void parser::add_local_expr(name const & n, expr const & p, bool is_variable) { static void check_no_metavars(name const & n, expr const & e) { lean_assert(is_local_p(e)); if (has_metavar(e)) { - throw generic_exception(none_expr(), [=](formatter const & fmt) { + throw generic_exception(none_expr(), [=](formatter const & /* fmt */) { format r("failed to add declaration '"); r += format(n); r += format("' to local context, type has metavariables"); @@ -1522,7 +1522,24 @@ struct to_pattern_fn { } } - expr operator()(expr const & e, bool skip_main_fn) { + expr fix_quoted_name(expr const & e) { + if (!is_app_of(e, get_lean_mk_name_str_name())) return e; + buffer args; + get_app_args(e, args); + args[0] = fix_quoted_name(args[0]); + return mk_app(mk_constant(get_lean_name_mk_string_name()), args); + } + + expr fix_quoted_names(expr const & e) { + return replace(e, [&](expr const & e) { + if (is_app_of(e, get_lean_mk_name_str_name())) + return some_expr(fix_quoted_name(e)); + return none_expr(); + }); + } + + expr operator()(expr const & e0, bool skip_main_fn) { + expr e = fix_quoted_names(e0); collect_new_locals(e, skip_main_fn); expr r = visit(e); return r; diff --git a/stage0/src/frontends/lean/util.cpp b/stage0/src/frontends/lean/util.cpp index 2ba8cf5a6f..4a700a136b 100644 --- a/stage0/src/frontends/lean/util.cpp +++ b/stage0/src/frontends/lean/util.cpp @@ -351,9 +351,9 @@ expr quote(name const & n) { case name_kind::ANONYMOUS: return mk_constant(get_lean_name_anonymous_name()); case name_kind::NUMERAL: - return mk_app(mk_constant(get_lean_name_mk_numeral_name()), quote(n.get_prefix()), quote(n.get_numeral().get_small_value())); // HACK: it may crash if numeral is not small + return mk_app(mk_constant(get_lean_mk_name_num_name()), quote(n.get_prefix()), quote(n.get_numeral().get_small_value())); // HACK: it may crash if numeral is not small case name_kind::STRING: - return mk_app(mk_constant(get_lean_name_mk_string_name()), quote(n.get_prefix()), quote(n.get_string().data())); // HACK: accessing Lean string as C String + return mk_app(mk_constant(get_lean_mk_name_str_name()), quote(n.get_prefix()), quote(n.get_string().data())); // HACK: accessing Lean string as C String } lean_unreachable(); } diff --git a/stage0/src/library/constants.cpp b/stage0/src/library/constants.cpp index 3eb799e985..a526c40d2c 100644 --- a/stage0/src/library/constants.cpp +++ b/stage0/src/library/constants.cpp @@ -54,8 +54,6 @@ name const * g_eq_of_heq = nullptr; name const * g_eq_true_intro = nullptr; name const * g_eq_false_intro = nullptr; name const * g_eq_self_iff_true = nullptr; -name const * g_lean_level = nullptr; -name const * g_lean_expr = nullptr; name const * g_lean_message_data = nullptr; name const * g_lean_monad_tracer_trace = nullptr; name const * g_false = nullptr; @@ -120,6 +118,8 @@ name const * g_lean_name = nullptr; name const * g_lean_name_anonymous = nullptr; name const * g_lean_name_mk_numeral = nullptr; name const * g_lean_name_mk_string = nullptr; +name const * g_lean_mk_name_num = nullptr; +name const * g_lean_mk_name_str = nullptr; name const * g_lean_parser_leading_node = nullptr; name const * g_lean_parser_trailing_node = nullptr; name const * g_nat = nullptr; @@ -243,8 +243,6 @@ void initialize_constants() { g_eq_true_intro = new name{"eqTrueIntro"}; g_eq_false_intro = new name{"eqFalseIntro"}; g_eq_self_iff_true = new name{"eqSelfIffTrue"}; - g_lean_level = new name{"Lean", "Level"}; - g_lean_expr = new name{"Lean", "Expr"}; g_lean_message_data = new name{"Lean", "MessageData"}; g_lean_monad_tracer_trace = new name{"Lean", "MonadTracer", "trace"}; g_false = new name{"False"}; @@ -309,6 +307,8 @@ void initialize_constants() { g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"}; g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"}; g_lean_name_mk_string = new name{"Lean", "Name", "mkString"}; + g_lean_mk_name_num = new name{"Lean", "mkNameNum"}; + g_lean_mk_name_str = new name{"Lean", "mkNameStr"}; g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"}; g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"}; g_nat = new name{"Nat"}; @@ -433,8 +433,6 @@ void finalize_constants() { delete g_eq_true_intro; delete g_eq_false_intro; delete g_eq_self_iff_true; - delete g_lean_level; - delete g_lean_expr; delete g_lean_message_data; delete g_lean_monad_tracer_trace; delete g_false; @@ -499,6 +497,8 @@ void finalize_constants() { delete g_lean_name_anonymous; delete g_lean_name_mk_numeral; delete g_lean_name_mk_string; + delete g_lean_mk_name_num; + delete g_lean_mk_name_str; delete g_lean_parser_leading_node; delete g_lean_parser_trailing_node; delete g_nat; @@ -622,8 +622,6 @@ name const & get_eq_of_heq_name() { return *g_eq_of_heq; } name const & get_eq_true_intro_name() { return *g_eq_true_intro; } name const & get_eq_false_intro_name() { return *g_eq_false_intro; } name const & get_eq_self_iff_true_name() { return *g_eq_self_iff_true; } -name const & get_lean_level_name() { return *g_lean_level; } -name const & get_lean_expr_name() { return *g_lean_expr; } name const & get_lean_message_data_name() { return *g_lean_message_data; } name const & get_lean_monad_tracer_trace_name() { return *g_lean_monad_tracer_trace; } name const & get_false_name() { return *g_false; } @@ -688,6 +686,8 @@ name const & get_lean_name_name() { return *g_lean_name; } name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; } name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; } name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; } +name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; } +name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; } name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; } name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; } name const & get_nat_name() { return *g_nat; } diff --git a/stage0/src/library/constants.h b/stage0/src/library/constants.h index 62d0bfaa7f..73d5934b65 100644 --- a/stage0/src/library/constants.h +++ b/stage0/src/library/constants.h @@ -56,8 +56,6 @@ name const & get_eq_of_heq_name(); name const & get_eq_true_intro_name(); name const & get_eq_false_intro_name(); name const & get_eq_self_iff_true_name(); -name const & get_lean_level_name(); -name const & get_lean_expr_name(); name const & get_lean_message_data_name(); name const & get_lean_monad_tracer_trace_name(); name const & get_false_name(); @@ -122,6 +120,8 @@ name const & get_lean_name_name(); name const & get_lean_name_anonymous_name(); name const & get_lean_name_mk_numeral_name(); name const & get_lean_name_mk_string_name(); +name const & get_lean_mk_name_num_name(); +name const & get_lean_mk_name_str_name(); name const & get_lean_parser_leading_node_name(); name const & get_lean_parser_trailing_node_name(); name const & get_nat_name(); diff --git a/stage0/src/library/constants.txt b/stage0/src/library/constants.txt index a13cf44922..66f7a6e47f 100644 --- a/stage0/src/library/constants.txt +++ b/stage0/src/library/constants.txt @@ -49,8 +49,6 @@ eqOfHeq eqTrueIntro eqFalseIntro eqSelfIffTrue -Lean.Level -Lean.Expr Lean.MessageData Lean.MonadTracer.trace False @@ -115,6 +113,8 @@ Lean.Name Lean.Name.anonymous Lean.Name.mkNumeral Lean.Name.mkString +Lean.mkNameNum +Lean.mkNameStr Lean.Parser.leadingNode Lean.Parser.trailingNode Nat diff --git a/stage0/src/library/equations_compiler/elim_match.cpp b/stage0/src/library/equations_compiler/elim_match.cpp index 6d4ce52249..e466a1f6c2 100644 --- a/stage0/src/library/equations_compiler/elim_match.cpp +++ b/stage0/src/library/equations_compiler/elim_match.cpp @@ -324,7 +324,7 @@ struct elim_match_fn { bool is_value(type_context_old & ctx, expr const & e) { try { if (!m_use_ite) return false; - if (is_nat_int_char_string_name_value(ctx, e)) return true; + if (is_nat_int_char_string_value(ctx, e)) return true; // TODO(Leo, Sebastian): decide whether we ever want to have this behavior back // if (optional I_name = is_constructor(e)) return is_nontrivial_enum(*I_name); return false; diff --git a/stage0/src/library/equations_compiler/util.cpp b/stage0/src/library/equations_compiler/util.cpp index 049edc20fa..687fe5fb5c 100644 --- a/stage0/src/library/equations_compiler/util.cpp +++ b/stage0/src/library/equations_compiler/util.cpp @@ -302,20 +302,8 @@ pair mk_aux_definition(environment const & env, options const return mk_pair(new_env, r); } -bool is_name_value(expr const & e) { - if (is_constant(e, get_lean_name_anonymous_name())) - return true; - buffer args; - expr const & fn = get_app_args(e, args); - if (is_constant(fn, get_lean_name_mk_string_name()) && args.size() == 2) - return is_name_value(args[0]) && is_string_value(args[1]); - if (is_constant(fn, get_lean_name_mk_numeral_name()) && args.size() == 2) - return is_name_value(args[0]) && is_num(args[1]); - return false; -} - -bool is_nat_int_char_string_name_value(type_context_old & ctx, expr const & e) { - if (is_char_value(ctx, e) || is_string_value(e) || is_name_value(e)) return true; +bool is_nat_int_char_string_value(type_context_old & ctx, expr const & e) { + if (is_char_value(ctx, e) || is_string_value(e)) return true; if (is_signed_num(e)) { expr type = ctx.infer(e); if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type())) diff --git a/stage0/src/library/equations_compiler/util.h b/stage0/src/library/equations_compiler/util.h index aa8b617001..48dd1b45e9 100644 --- a/stage0/src/library/equations_compiler/util.h +++ b/stage0/src/library/equations_compiler/util.h @@ -96,7 +96,7 @@ pair mk_aux_definition(environment const & env, options const equations_header const & header, name const & n, name const & actual_n, expr const & type, expr const & value); /* Return true iff e is a nat, int, char or string value. */ -bool is_nat_int_char_string_name_value(type_context_old & ctx, expr const & e); +bool is_nat_int_char_string_value(type_context_old & ctx, expr const & e); /* Given a variable (x : I A idx), where (I A idx) is an inductive datatype, for each constructor c of (I A idx), this function invokes fn(t, new_vars) where t is of the form (c A ...),