max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-18 07:18:17 -08:00
parent 3bc61e7ee9
commit fbf4fd27cb
10 changed files with 56 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
stage0/library/Init/Lean/Name.c generated
View file

@ -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:
{

2
stage0/src/frontends/lean/elaborator.cpp generated
View file

@ -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);

21
stage0/src/frontends/lean/parser.cpp generated
View file

@ -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<expr> 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;

4
stage0/src/frontends/lean/util.cpp generated
View file

@ -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();
}

16
stage0/src/library/constants.cpp generated
View file

@ -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; }

4
stage0/src/library/constants.h generated
View file

@ -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();

4
stage0/src/library/constants.txt generated
View file

@ -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

2
stage0/src/library/equations_compiler/elim_match.cpp generated
View file

@ -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<name> I_name = is_constructor(e)) return is_nontrivial_enum(*I_name);
return false;

16
stage0/src/library/equations_compiler/util.cpp generated
View file

@ -302,20 +302,8 @@ pair<environment, expr> 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<expr> 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()))

2
stage0/src/library/equations_compiler/util.h generated
View file

@ -96,7 +96,7 @@ pair<environment, expr> 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 ...),