diff --git a/library/init/lean/ir/instances.lean b/library/init/lean/ir/instances.lean index 91e5e9096f..54c0e9b0c2 100644 --- a/library/init/lean/ir/instances.lean +++ b/library/init/lean/ir/instances.lean @@ -42,13 +42,7 @@ instance var_has_lt : has_lt var := (name.has_lt_quick : has_lt name) instance blockid_has_lt : has_lt blockid := (name.has_lt_quick : has_lt name) instance fnid_has_lt : has_lt fnid := (name.has_lt_quick : has_lt name) -instance var_has_dec_eq : decidable_eq var := infer_instance_as (decidable_eq name) -instance blockid_has_dec_eq : decidable_eq blockid := infer_instance_as (decidable_eq name) -instance fnid_has_dec_eq : decidable_eq fnid := infer_instance_as (decidable_eq name) - -instance var_hashable : hashable var := infer_instance_as (hashable name) -instance blockid_hashable : hashable blockid := infer_instance_as (hashable name) -instance fnid_hashable : hashable fnid := infer_instance_as (hashable name) +attribute [derive decidable_eq hashable] var blockid fnid def var_set := rbtree var (<) def blockid_set := rbtree blockid (<) diff --git a/library/init/lean/parser/macro.lean b/library/init/lean/parser/macro.lean index 780e5d4a3f..8227a9d151 100644 --- a/library/init/lean/parser/macro.lean +++ b/library/init/lean/parser/macro.lean @@ -11,17 +11,14 @@ namespace parser local attribute [instance] name.has_lt_quick -@[irreducible] def parse_m (r σ) := except_t string $ reader_t r $ state σ +@[irreducible, derive monad monad_except monad_reader monad_state] +def parse_m (r σ) := except_t string $ reader_t r $ state σ namespace parse_m section local attribute [reducible] parse_m -instance (r σ) : monad (parse_m r σ) := infer_instance ---instance (r σ) : monad_run _ (parse_m r σ) := by apply_instance -instance (r σ) : monad_except string (parse_m r σ) := infer_instance -instance (r σ) : monad_reader r (parse_m r σ) := infer_instance -instance (r σ) : monad_state σ (parse_m r σ) := infer_instance +-- not clear how to auto-derive these instance (r σ σ') : monad_state_adapter σ σ' (parse_m r σ) (parse_m r σ') := infer_instance instance (r r' σ) : monad_reader_adapter r r' (parse_m r σ) (parse_m r' σ) := infer_instance diff --git a/library/init/lean/parser/reader/basic.lean b/library/init/lean/parser/reader/basic.lean index 2c65a0a551..7a04f3bbde 100644 --- a/library/init/lean/parser/reader/basic.lean +++ b/library/init/lean/parser/reader/basic.lean @@ -34,6 +34,7 @@ private def with_recurse_aux : nat → m r def with_recurse (max_rec := 1000) : rec_t r m r := ⟨λ _, rec.run (with_recurse_aux base rec max_rec)⟩ +-- not clear how to auto-derive these given the additional constraints instance : monad (rec_t r m) := infer_instance instance [alternative m] : alternative (rec_t r m) := infer_instance instance : has_monad_lift m (rec_t r m) := infer_instance @@ -69,7 +70,8 @@ structure reader_state := structure reader_config := mk -@[irreducible] def read_m := rec_t syntax $ reader_t reader_config $ state_t reader_state $ parsec syntax +@[irreducible, derive monad alternative monad_reader monad_state monad_parsec monad_except] +def read_m := rec_t syntax $ reader_t reader_config $ state_t reader_state $ parsec syntax structure reader := (read : read_m syntax) @@ -77,13 +79,6 @@ structure reader := namespace read_m local attribute [reducible] read_m -instance : monad read_m := infer_instance -instance : alternative read_m := infer_instance -instance : monad_reader reader_config read_m := infer_instance -instance : monad_state reader_state read_m := infer_instance -instance : monad_parsec syntax read_m := infer_instance -instance : monad_except (parsec.message syntax) read_m := infer_instance - protected def run (cfg : reader_config) (st : reader_state) (s : string) (r : read_m syntax) : syntax × list message := match (((r.run (monad_parsec.error "no recursive parser at top level")).run cfg).run st).parse_with_eoi s with diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index cfb209152b..40a6e07cf4 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -403,7 +403,7 @@ public: names const & extra_locals = names()); /** Always parses an expression. Returns a synthetic sorry even if no input is consumed. */ - expr parse_expr(unsigned rbp = 0); + virtual expr parse_expr(unsigned rbp = 0) override final; /** Tries to parse an expression, or else consumes no input. */ optional maybe_parse_expr(unsigned rbp = 0); /** \brief Parse an (optionally) qualified expression. diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index a9f93a777b..9f2e1717ea 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -18,4 +18,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp documentation.cpp check.cpp parray.cpp process.cpp pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp context_cache.cpp unique_id.cpp persistent_context_cache.cpp elab_context.cpp - scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp) + scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp + derive_attribute.cpp) diff --git a/src/library/abstract_parser.h b/src/library/abstract_parser.h index df7981050d..4b6445c621 100644 --- a/src/library/abstract_parser.h +++ b/src/library/abstract_parser.h @@ -35,5 +35,7 @@ public: virtual unsigned parse_small_nat() = 0; virtual std::string parse_string_lit() = 0; + /** Always parses an expression. Returns a synthetic sorry even if no input is consumed. */ + virtual expr parse_expr(unsigned rbp = 0) = 0; }; } diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp new file mode 100644 index 0000000000..3e9fd838b9 --- /dev/null +++ b/src/library/derive_attribute.cpp @@ -0,0 +1,134 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include +#include "runtime/sstream.h" +#include "kernel/find_fn.h" +#include "kernel/old_type_checker.h" +#include "kernel/inductive/inductive.h" +#include "library/util.h" +#include "library/scoped_ext.h" +#include "library/kernel_serializer.h" +#include "library/user_recursors.h" +#include "library/aux_recursors.h" +#include "library/attribute_manager.h" +#include "library/type_context.h" +#include "library/app_builder.h" +#include "library/class.h" +#include "library/protected.h" + +namespace lean { +struct exprs_attribute_data : public attr_data { + exprs m_args; + exprs_attribute_data(list_ref const & args) : m_args(args) {} + exprs_attribute_data() {} + + virtual unsigned hash() const override { + unsigned h = 0; + for (auto const & arg : m_args) { + h = ::lean::hash(h, ::lean::hash(arg)); + } + return h; + } + void write(serializer & s) const { + s << m_args; + } + void read(deserializer & d) { + m_args = read_exprs(d); + } + void parse(abstract_parser & p) override { + while (!p.curr_is_token("]")) { + m_args = cons(p.parse_expr(10000), m_args); + } + } + virtual void print(std::ostream & out) override { + out << "<>"; + } +}; + +typedef typed_attribute exprs_attribute; + +static exprs_attribute const & get_derive_attribute() { + return static_cast(get_system_attribute("derive")); +} + +static environment derive(environment env, name const & n, exprs const & clss) { + for (auto const & cls : clss) { + auto const & d = env.get(n); + if (!is_constant(cls) || !d.is_definition()) + throw exception("don't know how to derive this"); + auto const & cls_d = env.get(const_name(cls)); + type_context_old ctx(env); + auto ls = param_names_to_levels(d.get_univ_params()); + auto tgt = mk_const(n, ls); + auto real_tgt = instantiate_univ_params(d.get_value(), d.get_univ_params(), ls); + auto tgt_ty = instantiate_univ_params(d.get_type(), d.get_univ_params(), ls); + auto cls_ty = env.get(const_name(cls)).get_type(); + levels new_meta_ls; + for (unsigned i = 0; i < length(cls_d.get_univ_params()); i++) + new_meta_ls = cons(ctx.mk_univ_metavar_decl(), new_meta_ls); + cls_ty = instantiate_univ_params(cls_ty, cls_d.get_univ_params(), new_meta_ls); + if (!is_pi(cls_ty)) + throw exception("don't know how to derive this"); + auto expected_tgt_ty = cls_ty; + while (is_pi(expected_tgt_ty) && is_class_out_param(binding_domain(expected_tgt_ty))) { + expected_tgt_ty = binding_body(expected_tgt_ty); + } + expected_tgt_ty = binding_domain(expected_tgt_ty); + auto tgt_num_args = get_expect_num_args(ctx, tgt_ty); + auto expected_tgt_num_args = get_expect_num_args(ctx, expected_tgt_ty); + buffer n_params; + // use lower arity for instance like `monad` where the class expects a partially applied argument + for (unsigned i = 0; i < tgt_num_args - expected_tgt_num_args; i++) { + auto param = ctx.push_local_from_binding(tgt_ty); + tgt = mk_app(tgt, param); + real_tgt = mk_app(real_tgt, param); + n_params.push_back(param); + tgt_ty = instantiate(binding_body(tgt_ty), param); + } + ctx.unify(tgt_ty, expected_tgt_ty); + buffer params; + while (is_pi(cls_ty) && is_class_out_param(binding_domain(cls_ty))) { + params.push_back(ctx.mk_metavar_decl(ctx.lctx(), binding_domain(cls_ty))); + cls_ty = binding_body(cls_ty); + } + params.push_back(tgt); + tgt = mk_app(ctx, const_name(cls), params.size(), ¶ms[0]); + params.pop_back(); + params.push_back(real_tgt); + real_tgt = mk_app(ctx, const_name(cls), params.size(), ¶ms[0]); + auto inst = ctx.mk_class_instance(real_tgt); + if (!inst) + throw exception(sstream() << "failed to derive " << tgt); + tgt = ctx.mk_pi(n_params, tgt); + auto inst2 = ctx.mk_lambda(n_params, inst.value()); + auto new_n = n + const_name(cls); + auto def = mk_definition(env, new_n, d.get_univ_params(), + ctx.instantiate_mvars(tgt), inst2, d.is_meta()); + auto cdef = check(env, def); + env = module::add(env, cdef); + env = add_instance(env, new_n, LEAN_DEFAULT_PRIORITY, true); + env = add_protected(env, new_n); + } + return env; +} + +void initialize_derive_attribute() { + register_system_attribute(exprs_attribute("derive", "auto-derive type classes", + [](environment const & env, io_state const &, name const & n, unsigned, + bool persistent) { + if (!persistent) + throw exception("invalid [derive] attribute, must be persistent"); + auto const & data = *get_derive_attribute().get(env, n); + return derive(env, n, data.m_args); + })); +} + +void finalize_derive_attribute() { +} +} diff --git a/src/library/derive_attribute.h b/src/library/derive_attribute.h new file mode 100644 index 0000000000..47b77d4f38 --- /dev/null +++ b/src/library/derive_attribute.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#pragma once +namespace lean { +void initialize_derive_attribute(); +void finalize_derive_attribute(); +} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 2deecaf044..7ae40bb13d 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -53,6 +53,7 @@ Author: Leonardo de Moura #include "library/error_msgs.h" #include "library/formatter.h" #include "library/pos_info_provider.h" +#include "library/derive_attribute.h" namespace lean { void initialize_library_core_module() { @@ -65,9 +66,11 @@ void initialize_library_core_module() { initialize_module(); initialize_scoped_ext(); initialize_attribute_manager(); + initialize_derive_attribute(); } void finalize_library_core_module() { + finalize_derive_attribute(); finalize_attribute_manager(); finalize_scoped_ext(); finalize_module();