From e384b5c5f98d4eeacfe26f69094f2df97e43c133 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Aug 2016 14:56:09 -0700 Subject: [PATCH] refactor(frontends/lean): move structure_instance to separate module --- src/frontends/lean/CMakeLists.txt | 11 +- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/init_module.cpp | 6 +- src/frontends/lean/old_elaborator.cpp | 2 +- src/frontends/lean/structure_cmd.cpp | 119 +------------------- src/frontends/lean/structure_cmd.h | 7 -- src/frontends/lean/structure_instance.cpp | 126 ++++++++++++++++++++++ src/frontends/lean/structure_instance.h | 16 +++ 8 files changed, 152 insertions(+), 137 deletions(-) create mode 100644 src/frontends/lean/structure_instance.cpp create mode 100644 src/frontends/lean/structure_instance.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 61233aef12..ad6875131b 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -3,13 +3,10 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp dependencies.cpp -pp.cpp theorem_queue.cpp -structure_cmd.cpp info_manager.cpp info_annotation.cpp -init_module.cpp -type_util.cpp local_ref_info.cpp -decl_attributes.cpp nested_declaration.cpp -opt_cmd.cpp prenum.cpp -print_cmd.cpp elaborator.cpp pattern_attribute.cpp +pp.cpp theorem_queue.cpp structure_cmd.cpp structure_instance.cpp +info_manager.cpp info_annotation.cpp init_module.cpp +type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp +opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp pattern_attribute.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp inductive_cmds.cpp # LEGACY diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 9ff3c2312a..cea49509ed 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -29,7 +29,7 @@ Author: Leonardo de Moura #include "frontends/lean/util.h" #include "frontends/lean/tokens.h" #include "frontends/lean/info_annotation.h" -#include "frontends/lean/structure_cmd.h" +#include "frontends/lean/structure_instance.h" #include "frontends/lean/nested_declaration.h" #include "frontends/lean/match_expr.h" diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index bec9223d5d..1c5ef01db2 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -16,7 +16,7 @@ Author: Leonardo de Moura #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/inductive_cmd.h" #include "frontends/lean/inductive_cmds.h" -#include "frontends/lean/structure_cmd.h" +#include "frontends/lean/structure_instance.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/parse_table.h" #include "frontends/lean/token_table.h" @@ -50,7 +50,7 @@ void initialize_frontend_lean_module() { initialize_calc(); initialize_inductive_cmd(); initialize_inductive_cmds(); - initialize_structure_cmd(); + initialize_structure_instance(); initialize_info_manager(); initialize_pp(); initialize_server(); @@ -70,7 +70,7 @@ void finalize_frontend_lean_module() { finalize_server(); finalize_pp(); finalize_info_manager(); - finalize_structure_cmd(); + finalize_structure_instance(); finalize_inductive_cmds(); finalize_inductive_cmd(); finalize_calc(); diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index 2258c13d7a..b887edcadb 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -52,7 +52,7 @@ Author: Leonardo de Moura #include "library/tactic/tactic_state.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/local_decls.h" -#include "frontends/lean/structure_cmd.h" +#include "frontends/lean/structure_instance.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/old_elaborator.h" diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index fd0b0aa609..83e8363040 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -57,12 +57,9 @@ Author: Leonardo de Moura #endif namespace lean { -static name * g_tmp_prefix = nullptr; - /** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure - \pre is_structure_like(env, S) -*/ + \pre is_structure_like(env, S) */ static auto get_structure_info(environment const & env, name const & S) -> std::tuple { lean_assert(is_structure_like(env, S)); @@ -918,7 +915,6 @@ environment private_structure_cmd(parser & p) { return structure_cmd_fn(p, true)(); } - void get_structure_fields(environment const & env, name const & S, buffer & fields) { lean_assert(is_structure_like(env, S)); level_param_names ls; unsigned nparams; inductive::intro_rule intro; @@ -950,120 +946,7 @@ bool is_structure(environment const & env, name const & S) { return get_projection_info(env, field_name) != nullptr; } -static name * g_structure_instance_name = nullptr; -static std::string * g_structure_instance_opcode = nullptr; - void register_structure_cmd(cmd_table & r) { add_cmd(r, cmd_info("structure", "declare a new structure/record type", structure_cmd)); } - -[[ noreturn ]] static void throw_se_ex() { throw exception("unexpected occurrence of 'structure instance' expression"); } - -// We encode a 'structure instance' expression using a macro. -// This is a trick to avoid creating a new kind of expression. -// 'Structure instance' expressions are temporary objects used by the elaborator. -// Example: Given -// structure point (A B : Type) := (x : A) (y : B) -// the structure instance -// {| point, x := 10, y := 20 |} -// is compiled into -// point.mk 10 20 -class structure_instance_macro_cell : public macro_definition_cell { - list m_fields; -public: - structure_instance_macro_cell(list const & fs):m_fields(fs) {} - virtual name get_name() const { return *g_structure_instance_name; } - virtual expr check_type(expr const &, abstract_type_context &, bool) const { throw_se_ex(); } - virtual optional expand(expr const &, abstract_type_context &) const { throw_se_ex(); } - virtual void write(serializer & s) const { - s << *g_structure_instance_opcode; - write_list(s, m_fields); - } - list const & get_field_names() const { return m_fields; } -}; - -static expr mk_structure_instance(list const & fs, unsigned num, expr const * args) { - lean_assert(num >= length(fs) + 1); - macro_definition def(new structure_instance_macro_cell(fs)); - return mk_macro(def, num, args); -} - -bool is_structure_instance(expr const & e) { - return is_macro(e) && macro_def(e).get_name() == *g_structure_instance_name; -} - -void destruct_structure_instance(expr const & e, expr & t, buffer & field_names, - buffer & field_values, buffer & using_exprs) { - lean_assert(is_structure_instance(e)); - t = macro_arg(e, 0); - list const & fns = static_cast(macro_def(e).raw())->get_field_names(); - unsigned num_fileds = length(fns); - to_buffer(fns, field_names); - for (unsigned i = 1; i < num_fileds+1; i++) - field_values.push_back(macro_arg(e, i)); - for (unsigned i = num_fileds+1; i < macro_num_args(e); i++) - using_exprs.push_back(macro_arg(e, i)); -} - -static expr parse_struct_expr_core(parser & p, pos_info const & pos, bool curly_bar) { - expr t = p.parse_expr(); - buffer field_names; - buffer field_values; - buffer using_exprs; - while (p.curr_is_token(get_comma_tk())) { - p.next(); - pair, expr> id_e = p.parse_optional_assignment(); - if (id_e.first) { - field_names.push_back(*id_e.first); - field_values.push_back(id_e.second); - } else { - using_exprs.push_back(id_e.second); - } - } - if (curly_bar) - p.check_token_next(get_rcurlybar_tk(), "invalid structure expression, '|}' expected"); - else - p.check_token_next(get_rdcurly_tk(), "invalid structure expression, '⦄' expected"); - buffer args; - args.push_back(t); - args.append(field_values); - args.append(using_exprs); - return p.save_pos(mk_structure_instance(to_list(field_names), args.size(), args.data()), pos); -} - -static expr parse_struct_curly_bar(parser & p, unsigned, expr const *, pos_info const & pos) { - bool curly_bar = true; - return parse_struct_expr_core(p, pos, curly_bar); -} - -static expr parse_struct_dcurly(parser & p, unsigned, expr const *, pos_info const & pos) { - bool curly_bar = false; - return parse_struct_expr_core(p, pos, curly_bar); -} - -void init_structure_instance_parsing_rules(parse_table & r) { - expr x0 = mk_var(0); - r = r.add({notation::transition("{|", notation::mk_ext_action(parse_struct_curly_bar))}, x0); - r = r.add({notation::transition("⦃", notation::mk_ext_action(parse_struct_dcurly))}, x0); -} - -void initialize_structure_cmd() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_structure_instance_name = new name("structure instance"); - g_structure_instance_opcode = new std::string("STI"); - register_macro_deserializer(*g_structure_instance_opcode, - [](deserializer & d, unsigned num, expr const * args) { - list fs; - fs = read_list(d); - if (num < length(fs) + 1) - throw corrupted_stream_exception(); - return mk_structure_instance(fs, num, args); - }); -} - -void finalize_structure_cmd() { - delete g_tmp_prefix; - delete g_structure_instance_opcode; - delete g_structure_instance_name; -} } diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h index bbd01028b8..f54dcff1c7 100644 --- a/src/frontends/lean/structure_cmd.h +++ b/src/frontends/lean/structure_cmd.h @@ -6,17 +6,10 @@ Author: Leonardo de Moura */ #pragma once #include "frontends/lean/cmd_table.h" -#include "frontends/lean/parse_table.h" namespace lean { -void init_structure_instance_parsing_rules(parse_table & r); -bool is_structure_instance(expr const & e); -void destruct_structure_instance(expr const & e, expr & t, buffer & field_names, - buffer & field_values, buffer & using_exprs); void get_structure_fields(environment const & env, name const & S, buffer & fields); void register_structure_cmd(cmd_table & r); environment private_structure_cmd(parser & p); /** \brief Return true iff \c S is a structure created with the structure command */ bool is_structure(environment const & env, name const & S); -void initialize_structure_cmd(); -void finalize_structure_cmd(); } diff --git a/src/frontends/lean/structure_instance.cpp b/src/frontends/lean/structure_instance.cpp new file mode 100644 index 0000000000..c3dd16e7bc --- /dev/null +++ b/src/frontends/lean/structure_instance.cpp @@ -0,0 +1,126 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/sstream.h" +#include "library/kernel_serializer.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/tokens.h" + +namespace lean { +static name * g_structure_instance_name = nullptr; +static std::string * g_structure_instance_opcode = nullptr; + +[[ noreturn ]] static void throw_se_ex() { throw exception("unexpected occurrence of 'structure instance' expression"); } + +/* + We encode a 'structure instance' expression using a macro. + This is a trick to avoid creating a new kind of expression. + 'Structure instance' expressions are temporary objects used by the elaborator. + Example: Given + structure point (A B : Type) := (x : A) (y : B) + the structure instance + {| point, x := 10, y := 20 |} + is compiled into + point.mk 10 20 +*/ +class structure_instance_macro_cell : public macro_definition_cell { + list m_fields; +public: + structure_instance_macro_cell(list const & fs):m_fields(fs) {} + virtual name get_name() const { return *g_structure_instance_name; } + virtual expr check_type(expr const &, abstract_type_context &, bool) const { throw_se_ex(); } + virtual optional expand(expr const &, abstract_type_context &) const { throw_se_ex(); } + virtual void write(serializer & s) const { + s << *g_structure_instance_opcode; + write_list(s, m_fields); + } + list const & get_field_names() const { return m_fields; } +}; + +static expr mk_structure_instance(list const & fs, unsigned num, expr const * args) { + lean_assert(num >= length(fs) + 1); + macro_definition def(new structure_instance_macro_cell(fs)); + return mk_macro(def, num, args); +} + +bool is_structure_instance(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == *g_structure_instance_name; +} + +void destruct_structure_instance(expr const & e, expr & t, buffer & field_names, + buffer & field_values, buffer & using_exprs) { + lean_assert(is_structure_instance(e)); + t = macro_arg(e, 0); + list const & fns = static_cast(macro_def(e).raw())->get_field_names(); + unsigned num_fileds = length(fns); + to_buffer(fns, field_names); + for (unsigned i = 1; i < num_fileds+1; i++) + field_values.push_back(macro_arg(e, i)); + for (unsigned i = num_fileds+1; i < macro_num_args(e); i++) + using_exprs.push_back(macro_arg(e, i)); +} + +static expr parse_struct_expr_core(parser & p, pos_info const & pos, bool curly_bar) { + expr t = p.parse_expr(); + buffer field_names; + buffer field_values; + buffer using_exprs; + while (p.curr_is_token(get_comma_tk())) { + p.next(); + pair, expr> id_e = p.parse_optional_assignment(); + if (id_e.first) { + field_names.push_back(*id_e.first); + field_values.push_back(id_e.second); + } else { + using_exprs.push_back(id_e.second); + } + } + if (curly_bar) + p.check_token_next(get_rcurlybar_tk(), "invalid structure expression, '|}' expected"); + else + p.check_token_next(get_rdcurly_tk(), "invalid structure expression, '⦄' expected"); + buffer args; + args.push_back(t); + args.append(field_values); + args.append(using_exprs); + return p.save_pos(mk_structure_instance(to_list(field_names), args.size(), args.data()), pos); +} + +static expr parse_struct_curly_bar(parser & p, unsigned, expr const *, pos_info const & pos) { + bool curly_bar = true; + return parse_struct_expr_core(p, pos, curly_bar); +} + +static expr parse_struct_dcurly(parser & p, unsigned, expr const *, pos_info const & pos) { + bool curly_bar = false; + return parse_struct_expr_core(p, pos, curly_bar); +} + +void init_structure_instance_parsing_rules(parse_table & r) { + expr x0 = mk_var(0); + r = r.add({notation::transition("{|", notation::mk_ext_action(parse_struct_curly_bar))}, x0); + r = r.add({notation::transition("⦃", notation::mk_ext_action(parse_struct_dcurly))}, x0); +} + +void initialize_structure_instance() { + g_structure_instance_name = new name("structure instance"); + g_structure_instance_opcode = new std::string("STI"); + register_macro_deserializer(*g_structure_instance_opcode, + [](deserializer & d, unsigned num, expr const * args) { + list fs; + fs = read_list(d); + if (num < length(fs) + 1) + throw corrupted_stream_exception(); + return mk_structure_instance(fs, num, args); + }); +} + +void finalize_structure_instance() { + delete g_structure_instance_opcode; + delete g_structure_instance_name; +} +} diff --git a/src/frontends/lean/structure_instance.h b/src/frontends/lean/structure_instance.h new file mode 100644 index 0000000000..e1b0b9b187 --- /dev/null +++ b/src/frontends/lean/structure_instance.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "frontends/lean/parse_table.h" +namespace lean { +void init_structure_instance_parsing_rules(parse_table & r); +bool is_structure_instance(expr const & e); +void destruct_structure_instance(expr const & e, expr & t, buffer & field_names, + buffer & field_values, buffer & using_exprs); +void initialize_structure_instance(); +void finalize_structure_instance(); +}