From d9a22d43b2eac3af782199ce7aeedd1bf1292069 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 14 Dec 2018 13:54:43 +0100 Subject: [PATCH] feat(library/vm/vm_aux): add primitive for calling old elaborator --- library/init/lean/elaborator.lean | 6 + src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 4 + src/frontends/lean/elaborator.h | 3 + src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/vm_elaborator.cpp | 176 +++++++++++++++++++++++++++ src/frontends/lean/vm_elaborator.h | 14 +++ src/library/compiler/builtin.cpp | 4 + 8 files changed, 211 insertions(+), 1 deletion(-) create mode 100644 src/frontends/lean/vm_elaborator.cpp create mode 100644 src/frontends/lean/vm_elaborator.h diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index bc246cd8f1..eba8a18706 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -11,7 +11,13 @@ import init.lean.expander import init.lean.expr namespace lean +-- TODO(Sebastian): should probably be meta together with the whole elaborator +constant environment : Type +constant environment.empty : environment + namespace elaborator +constant elaborate_command : expr → environment → except string environment + open parser open parser.combinators open parser.term diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 7c640ab768..3d28e4b261 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -6,4 +6,4 @@ inductive_cmds.cpp pp.cpp structure_cmd.cpp structure_instance.cpp init_module.cpp type_util.cpp decl_attributes.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp -brackets.cpp json.cpp typed_expr.cpp choice.cpp) +brackets.cpp json.cpp typed_expr.cpp choice.cpp vm_elaborator.cpp) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 921c4941dc..6ced4d4510 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -4233,6 +4233,10 @@ expr resolve_names(environment const & env, local_context const & lctx, expr con return resolve_names_fn(env, lctx)(e); } +environment elaborate_command(environment const & env, expr const & cmd) { + throw elaborator_exception(cmd, "unexpected input to 'elaborate_command'"); +} + void initialize_elaborator() { g_elab_strategy = new name("elab_strategy"); register_trace_class("elaborator"); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 7cf18b00d4..fad30d621e 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -365,6 +365,9 @@ pair elaborate(environment & env, options const & opts, name const Throw exception is \c ctx does not contain the local constant. */ expr resolve_names(environment const & env, local_context const & lctx, expr const & e); +/** \brief Fall-back interface for the new elaborator */ +environment elaborate_command(environment const & env, expr const & cmd); + void initialize_elaborator(); void finalize_elaborator(); } diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 09b7813aaa..b2815226c1 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "frontends/lean/util.h" #include "frontends/lean/brackets.h" #include "frontends/lean/choice.h" +#include "frontends/lean/vm_elaborator.h" namespace lean { void initialize_frontend_lean_module() { @@ -47,8 +48,10 @@ void initialize_frontend_lean_module() { initialize_notation_cmd(); initialize_frontend_lean_util(); initialize_brackets(); + initialize_vm_elaborator(); } void finalize_frontend_lean_module() { + finalize_vm_elaborator(); finalize_brackets(); finalize_frontend_lean_util(); finalize_notation_cmd(); diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp new file mode 100644 index 0000000000..39bcaba405 --- /dev/null +++ b/src/frontends/lean/vm_elaborator.cpp @@ -0,0 +1,176 @@ +/* +Copyright (c) 2018 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Sebastian Ullrich + +TEMPORARY code for the old runtime +*/ + +#include +#include +#include "util/timeit.h" +#include "library/trace.h" +#include "library/vm/vm.h" +#include "library/vm/vm_string.h" +#include "library/vm/vm_option.h" +#include "library/vm/vm_nat.h" +#include "frontends/lean/elaborator.h" + +namespace lean { +struct vm_env : public vm_external { + environment m_env; + + explicit vm_env(environment const & env) : m_env(env) {} + + virtual ~vm_env() {} + + virtual void dealloc() override { delete this; } + + virtual vm_external *ts_clone(vm_clone_fn const &) {lean_unreachable()} + + virtual vm_external *clone(vm_clone_fn const &) {lean_unreachable()} +}; + +vm_obj vm_environment_empty() { + return mk_vm_external(new vm_env(environment())); +} + +name to_name(vm_obj const & o) { + switch (cidx(o)) { + case 0: return name(); + case 1: { + std::string str = to_string(cfield(o, 1)); + return name(to_name(cfield(o, 0)), str.c_str()); + } + case 2: + return name(to_name(cfield(o, 0)), to_unsigned(cfield(o, 1))); + default: lean_unreachable(); + } +} + +level to_level(vm_obj const & o) { + switch (cidx(o)) { + case 0: + return mk_level_zero(); + case 1: + return mk_succ(to_level(cfield(o, 0))); + case 2: + return mk_max(to_level(cfield(o, 0)), to_level(cfield(o, 1))); + case 3: + return mk_imax(to_level(cfield(o, 0)), to_level(cfield(o, 1))); + case 4: + return mk_univ_param(to_name(cfield(o, 0))); + case 5: + return mk_univ_mvar(to_name(cfield(o, 0))); + default: lean_unreachable(); + } +} + +levels to_levels(vm_obj const & o) { + switch (cidx(o)) { + case 0: + return levels(); + case 1: + return levels(to_level(cfield(o, 0)), to_levels(cfield(o, 1))); + default: lean_unreachable(); + } +} + +binder_info to_binder_info(vm_obj const & o) { + lean_assert(is_simple(o)); + return static_cast(cidx(o)); +} + +kvmap to_kvmap(vm_obj const & o) { + switch (cidx(o)) { + case 0: + return kvmap(); + case 1: { + auto vm_k = cfield(cfield(o, 0), 0); + auto vm_v = cfield(cfield(o, 0), 1); + auto vm_d = cfield(vm_v, 0); + data_value v; + switch (cidx(vm_v)) { + case 0: + v = data_value(to_string(vm_d)); + break; + case 1: + v = data_value(nat(vm_nat_to_mpz1(vm_d))); + break; + case 2: + v = data_value(to_bool(vm_d)); + break; + case 3: + v = data_value(to_name(vm_d)); + break; + default: lean_unreachable(); + } + return kvmap({to_name(vm_k), v}, to_kvmap(cfield(o, 1))); + } + default: lean_unreachable(); + } +} + +expr to_expr(vm_obj const & o) { + switch (cidx(o)) { + case 0: + return mk_bvar(nat(vm_nat_to_mpz1(cfield(o, 0)))); + case 1: + return mk_local(to_name(cfield(o, 0)), to_name(cfield(o, 0)), expr(), mk_binder_info()); + case 2: + return mk_metavar(to_name(cfield(o, 0)), to_expr(cfield(o, 1))); + case 3: + return mk_sort(to_level(cfield(o, 0))); + case 4: + return mk_constant(to_name(cfield(o, 0)), to_levels(cfield(o, 1))); + case 5: + return mk_app(to_expr(cfield(o, 0)), to_expr(cfield(o, 1))); + case 6: + return mk_lambda(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), + to_binder_info(cfield(o, 3))); + case 7: + return mk_pi(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), + to_binder_info(cfield(o, 3))); + case 8: + return mk_let(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3))); + case 9: { + auto l = cfield(o, 0); + switch (cidx(l)) { + case 0: + return mk_lit(literal(to_string(cfield(l, 0)).c_str())); + case 1: + return mk_lit(literal(vm_nat_to_mpz1(cfield(l, 0)))); + default: lean_unreachable(); + } + } + case 10: + return mk_mdata(to_kvmap(cfield(o, 0)), to_expr(cfield(o, 1))); + case 11: + return mk_proj(to_name(cfield(o, 0)), nat(vm_nat_to_mpz1(cfield(o, 1))), to_expr(cfield(o, 2))); + default: lean_unreachable(); + } +} + +/* elaborate_command : expr -> environment -> except string environment */ +// TODO(Sebastian): replace `string` with `message` in the new runtime +vm_obj vm_elaborate_command(vm_obj const & vm_cmd, vm_obj const & vm_e) { + lean_vm_check(dynamic_cast(to_external(vm_e))); + auto env = static_cast(to_external(vm_e))->m_env; + + try { + env = elaborate_command(env, to_expr(vm_cmd)); + return mk_vm_constructor(1, mk_vm_external(new vm_env(env))); + } catch (exception & e) { + return mk_vm_constructor(0, to_obj(e.what())); + } +} + +void initialize_vm_elaborator() { + DECLARE_VM_BUILTIN(name({"lean", "environment", "empty"}), vm_environment_empty); + DECLARE_VM_BUILTIN(name({"lean", "elaborator", "elaborate_command"}), vm_elaborate_command); +} + +void finalize_vm_elaborator() { +} +} diff --git a/src/frontends/lean/vm_elaborator.h b/src/frontends/lean/vm_elaborator.h new file mode 100644 index 0000000000..2cccd77db6 --- /dev/null +++ b/src/frontends/lean/vm_elaborator.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2018 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Sebastian Ullrich + +TEMPORARY code for the old runtime +*/ +#pragma once + +namespace lean { +void initialize_vm_elaborator(); +void finalize_vm_elaborator(); +} diff --git a/src/library/compiler/builtin.cpp b/src/library/compiler/builtin.cpp index b00e003a26..92a4a3b0c1 100644 --- a/src/library/compiler/builtin.cpp +++ b/src/library/compiler/builtin.cpp @@ -148,6 +148,10 @@ void initialize_builtin() { register_builtin(name({"io", "prim", "handle", "flush"}), o_o_o, "io_prim_handle_flush", bc); register_builtin(name({"io", "prim", "handle", "close"}), o_o_o, "io_prim_handle_close", bc); register_builtin(name({"io", "prim", "handle", "get_line"}), o_o_o, "io_prim_handle_get_line", bc); + + // interface to old elaborator + register_builtin(name({"lean", "environment", "empty"}), o, "lean_environment_empty", {}); + register_builtin(name({"lean", "elaborator", "elaborate_command"}), o_o_o, "lean_elaborator_elaborate_command", bb); } void finalize_builtin() {