From 86e231e6c964dc483b747bb9775a6dfd74a6930d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 2 Feb 2018 16:07:29 +0100 Subject: [PATCH] feat(frontends/lean/structure_cmd): make superclass fields inst implicit --- doc/changes.md | 3 +++ src/frontends/lean/structure_cmd.cpp | 10 ++++++++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index 6d3d09e3a7..edd905548f 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -215,6 +215,9 @@ master branch (aka work in progress branch) * leanpkg now always stores .lean package files in a separate `src` directory. +* Structure constructor parameters representing superclasses are now marked as instance implicit. + Note: Instances using the {...} structure notation should not be affected by this change. + *API name changes* v3.3.0 (14 September 2017) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 0889f8caa4..db83990e27 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -498,7 +498,11 @@ struct structure_cmd_fn { fname = *ref; else fname = name(parent_name.get_string()).append_before("to_"); - expr field = mk_local(fname, mk_as_is(parent)); + binder_info bi; + if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) + // make superclass fields inst implicit + bi = mk_inst_implicit_binder_info(); + expr field = mk_local(fname, mk_as_is(parent), bi); m_fields.emplace_back(field, none_expr(), field_kind::subobject); } @@ -1081,6 +1085,8 @@ struct structure_cmd_fn { collect_locals(type, used_locals); collect_locals(val, used_locals); buffer args; + // note: `mk_field_default_value` expects params to be implicit + // and fields to be explicit /* Copy params first */ for (expr const & local : used_locals.get_collected()) { if (is_param(local)) { @@ -1093,7 +1099,7 @@ struct structure_cmd_fn { /* Copy fields it depends on */ for (expr const & local : used_locals.get_collected()) { if (!is_param(local)) - args.push_back(local); + args.push_back(update_local(local, binder_info())); } name decl_name = name(m_name + field.get_name(), "_default"); name decl_prv_name;