From 399b83122c35d4c1fa269d7bc84851b4fa0daa7f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 May 2016 14:40:15 -0700 Subject: [PATCH] refactor(library): move vm to a separate directory --- src/CMakeLists.txt | 2 + src/init/init.cpp | 11 +- src/library/CMakeLists.txt | 2 +- src/library/compiler/lambda_lifting.cpp | 2 +- src/library/compiler/util.cpp | 2 +- src/library/compiler/vm_compiler.cpp | 2 +- src/library/init_module.cpp | 14 +- src/library/init_module.h | 2 + src/library/vm/CMakeLists.txt | 1 + src/library/vm/init_module.cpp | 26 ++++ src/library/vm/init_module.h | 15 ++ src/library/{ => vm}/vm.cpp | 174 +--------------------- src/library/{ => vm}/vm.h | 3 + src/library/vm/vm_nat.cpp | 186 ++++++++++++++++++++++++ src/library/vm/vm_nat.h | 12 ++ 15 files changed, 273 insertions(+), 181 deletions(-) create mode 100644 src/library/vm/CMakeLists.txt create mode 100644 src/library/vm/init_module.cpp create mode 100644 src/library/vm/init_module.h rename src/library/{ => vm}/vm.cpp (77%) rename src/library/{ => vm}/vm.h (99%) create mode 100644 src/library/vm/vm_nat.cpp create mode 100644 src/library/vm/vm_nat.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4d729d9496..b246f43a0f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -350,6 +350,8 @@ set(LEAN_OBJS ${LEAN_OBJS} $) # set(LEAN_OBJS ${LEAN_OBJS} $) # add_subdirectory(library/blast/forward) # set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/vm) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/compiler) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lean) diff --git a/src/init/init.cpp b/src/init/init.cpp index cc04de5b20..f2aa1b17e9 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura // #include "library/tactic/init_module.h" #include "library/definitional/init_module.h" #include "library/print.h" +#include "library/vm/init_module.h" #include "library/compiler/init_module.h" #include "frontends/lean/init_module.h" #include "init/init.h" @@ -33,21 +34,27 @@ void initialize() { initialize_quotient_module(); initialize_hits_module(); init_default_print_fn(); + initialize_library_core_module(); + initialize_vm_core_module(); initialize_library_module(); + initialize_compiler_module(); // initialize_tactic_module(); // initialize_blast_module(); initialize_definitional_module(); - initialize_compiler_module(); initialize_frontend_lean_module(); + initialize_vm_module(); } void finalize() { run_thread_finalizers(); + finalize_vm_module(); finalize_frontend_lean_module(); - finalize_compiler_module(); finalize_definitional_module(); // finalize_blast_module(); // finalize_tactic_module(); + finalize_compiler_module(); finalize_library_module(); + finalize_vm_core_module(); + finalize_library_core_module(); finalize_hits_module(); finalize_quotient_module(); finalize_inductive_module(); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index a8945c49ee..8bf6359cf0 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp defeq_simplifier.cpp proof_irrel_expr_manager.cpp - local_context.cpp metavar_context.cpp type_context.cpp vm.cpp + local_context.cpp metavar_context.cpp type_context.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 67b1f00852..b3a7a0969c 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/normalize.h" #include "library/util.h" -#include "library/vm.h" +#include "library/vm/vm.h" #include "library/compiler/util.h" #include "library/compiler/erase_irrelevant.h" #include "library/compiler/compiler_step_visitor.h" diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index 38d7a1e426..1c45a2c5f9 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/aux_recursors.h" #include "library/util.h" -#include "library/vm.h" +#include "library/vm/vm.h" #include "library/type_context.h" namespace lean { diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 419d73200a..6f3bc797de 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "library/constants.h" #include "library/trace.h" -#include "library/vm.h" +#include "library/vm/vm.h" #include "library/util.h" #include "library/compiler/simp_inductive.h" #include "library/compiler/erase_irrelevant.h" diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index d257da9f29..7899eca090 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "library/trace.h" #include "library/constants.h" -#include "library/vm.h" #include "library/unifier.h" #include "library/kernel_serializer.h" #include "library/let.h" @@ -60,11 +59,17 @@ Author: Leonardo de Moura namespace lean { -void initialize_library_module() { +void initialize_library_core_module() { initialize_constants(); initialize_trace(); - initialize_vm(); +} +void finalize_library_core_module() { + finalize_trace(); + finalize_constants(); +} + +void initialize_library_module() { // TODO(Leo): delete legacy.... initialize_old_converter(); initialize_old_default_converter(); @@ -166,9 +171,6 @@ void finalize_library_module() { finalize_attribute_manager(); finalize_metavar_context(); finalize_local_context(); - finalize_vm(); - finalize_constants(); - finalize_trace(); // TODO(Leo): delete legacy.... finalize_old_converter(); diff --git a/src/library/init_module.h b/src/library/init_module.h index 78e228b702..31e56a5bc2 100644 --- a/src/library/init_module.h +++ b/src/library/init_module.h @@ -7,6 +7,8 @@ Author: Leonardo de Moura #pragma once namespace lean { +void initialize_library_core_module(); +void finalize_library_core_module(); void initialize_library_module(); void finalize_library_module(); } diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt new file mode 100644 index 0000000000..c6ef65688a --- /dev/null +++ b/src/library/vm/CMakeLists.txt @@ -0,0 +1 @@ +add_library(vm OBJECT vm.cpp vm_nat.cpp init_module.cpp) \ No newline at end of file diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp new file mode 100644 index 0000000000..65360bc7b3 --- /dev/null +++ b/src/library/vm/init_module.cpp @@ -0,0 +1,26 @@ +/* +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 "library/vm/vm.h" +#include "library/vm/vm_nat.h" + +namespace lean { +void initialize_vm_core_module() { + initialize_vm_core(); + initialize_vm_nat(); +} +void finalize_vm_core_module() { + finalize_vm_nat(); + finalize_vm_core(); +} + +void initialize_vm_module() { + initialize_vm(); +} +void finalize_vm_module() { + finalize_vm(); +} +} diff --git a/src/library/vm/init_module.h b/src/library/vm/init_module.h new file mode 100644 index 0000000000..ab61f82a3b --- /dev/null +++ b/src/library/vm/init_module.h @@ -0,0 +1,15 @@ +/* +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 + +namespace lean { +void initialize_vm_core_module(); +void finalize_vm_core_module(); + +void initialize_vm_module(); +void finalize_vm_module(); +} diff --git a/src/library/vm.cpp b/src/library/vm/vm.cpp similarity index 77% rename from src/library/vm.cpp rename to src/library/vm/vm.cpp index 177be7378e..99904d9e01 100644 --- a/src/library/vm.cpp +++ b/src/library/vm/vm.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "util/parray.h" #include "library/constants.h" -#include "library/vm.h" +#include "library/vm/vm.h" namespace lean { void vm_obj_cell::dec_ref(vm_obj & o, buffer & todelete) { @@ -532,183 +532,19 @@ void display_vm_code(std::ostream & out, environment const & env, unsigned code_ } } -// ======================================= -// Builtin nat operations -#define MAX_SMALL_NAT 1u<<31 - -vm_obj mk_vm_nat(unsigned n) { - if (n < MAX_SMALL_NAT) - return mk_vm_simple(n); - else - return mk_vm_mpz(mpz(n)); +void initialize_vm_core() { + g_vm_builtins = new name_map>(); } -vm_obj mk_vm_nat(mpz const & n) { - if (n < MAX_SMALL_NAT) - return mk_vm_simple(n.get_unsigned_int()); - else - return mk_vm_mpz(n); -} - -MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz1); -MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz2); - -static mpz const & to_mpz1(vm_obj const & o) { - if (is_simple(o)) { - mpz & r = get_mpz1(); - r = cidx(o); - return r; - } else { - return to_mpz(o); - } -} - -static mpz const & to_mpz2(vm_obj const & o) { - if (is_simple(o)) { - mpz & r = get_mpz2(); - r = cidx(o); - return r; - } else { - return to_mpz(o); - } -} - -static void nat_succ(vm_state & s) { - vm_obj const & a = s.get(0); - if (is_simple(a)) { - s.push(mk_vm_nat(cidx(a) + 1)); - } else { - s.push(mk_vm_mpz(to_mpz1(a) + 1)); - } -} - -static void nat_add(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - s.push(mk_vm_nat(cidx(a1) + cidx(a2))); - } else { - s.push(mk_vm_mpz(to_mpz1(a1) + to_mpz2(a2))); - } -} - -static void nat_mul(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - unsigned long long r = static_cast(cidx(a1)) + static_cast(cidx(a2)); - if (r < MAX_SMALL_NAT) { - s.push(mk_vm_simple(r)); - return; - } - } - s.push(mk_vm_mpz(to_mpz1(a1) * to_mpz2(a2))); -} - -static void nat_sub(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - unsigned v1 = cidx(a1); - unsigned v2 = cidx(a2); - if (v2 > v1) - s.push(mk_vm_simple(0)); - else - s.push(mk_vm_nat(v1 - v2)); - } else { - mpz const & v1 = to_mpz1(a1); - mpz const & v2 = to_mpz2(a2); - if (v2 > v1) - s.push(mk_vm_simple(0)); - else - s.push(mk_vm_nat(v1 - v2)); - } -} - -static void nat_div(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - unsigned v1 = cidx(a1); - unsigned v2 = cidx(a2); - if (v2 == 0) - s.push(mk_vm_simple(0)); - else - s.push(mk_vm_nat(v1 / v2)); - } else { - mpz const & v1 = to_mpz1(a1); - mpz const & v2 = to_mpz2(a2); - if (v2 == 0) - s.push(mk_vm_simple(0)); - else - s.push(mk_vm_nat(v1 / v2)); - } -} - -static void nat_mod(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - unsigned v1 = cidx(a1); - unsigned v2 = cidx(a2); - if (v2 == 0) - s.push(a1); - else - s.push(mk_vm_nat(v1 % v2)); - } else { - mpz const & v1 = to_mpz1(a1); - mpz const & v2 = to_mpz2(a2); - if (v2 == 0) - s.push(a1); - else - s.push(mk_vm_nat(v1 % v2)); - } -} - -static void nat_gcd(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - mpz r; - gcd(r, to_mpz1(a1), to_mpz2(a2)); - s.push(mk_vm_nat(r)); -} - -static void nat_has_decidable_eq(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - return s.push(mk_vm_bool(cidx(a1) == cidx(a2))); - } else { - return s.push(mk_vm_bool(to_mpz1(a1) == to_mpz2(a2))); - } -} - -static void nat_has_decidable_le(vm_state & s) { - vm_obj const & a1 = s.get(0); - vm_obj const & a2 = s.get(1); - if (is_simple(a1) && is_simple(a2)) { - return s.push(mk_vm_bool(cidx(a1) <= cidx(a2))); - } else { - return s.push(mk_vm_bool(to_mpz1(a1) <= to_mpz2(a2))); - } +void finalize_vm_core() { + delete g_vm_builtins; } void initialize_vm() { - g_vm_builtins = new name_map>(); - declare_vm_builtin(get_nat_succ_name(), 1, nat_succ); - declare_vm_builtin(get_nat_add_name(), 2, nat_add); - declare_vm_builtin(get_nat_mul_name(), 2, nat_mul); - declare_vm_builtin(get_nat_sub_name(), 2, nat_sub); - declare_vm_builtin(get_nat_div_name(), 2, nat_div); - declare_vm_builtin(get_nat_mod_name(), 2, nat_mod); - declare_vm_builtin(get_nat_gcd_name(), 2, nat_gcd); - declare_vm_builtin(get_nat_has_decidable_eq_name(), 2, nat_has_decidable_eq); - declare_vm_builtin(get_nat_has_decidable_le_name(), 2, nat_has_decidable_le); g_ext = new vm_decls_reg(); } void finalize_vm() { delete g_ext; - delete g_vm_builtins; } } diff --git a/src/library/vm.h b/src/library/vm/vm.h similarity index 99% rename from src/library/vm.h rename to src/library/vm/vm.h index a9491f0047..8d8d7bc726 100644 --- a/src/library/vm.h +++ b/src/library/vm/vm.h @@ -430,6 +430,9 @@ optional get_vm_decl(environment const & env, name const & n); void display_vm_code(std::ostream & out, environment const & env, unsigned code_sz, vm_instr const * code); +void initialize_vm_core(); +void finalize_vm_core(); + void initialize_vm(); void finalize_vm(); } diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp new file mode 100644 index 0000000000..3d39ecfc02 --- /dev/null +++ b/src/library/vm/vm_nat.cpp @@ -0,0 +1,186 @@ +/* +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 "library/constants.h" +#include "library/vm/vm.h" + +namespace lean { +// ======================================= +// Builtin nat operations +#define MAX_SMALL_NAT 1u<<31 + +vm_obj mk_vm_nat(unsigned n) { + if (n < MAX_SMALL_NAT) + return mk_vm_simple(n); + else + return mk_vm_mpz(mpz(n)); +} + +vm_obj mk_vm_nat(mpz const & n) { + if (n < MAX_SMALL_NAT) + return mk_vm_simple(n.get_unsigned_int()); + else + return mk_vm_mpz(n); +} + +MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz1); +MK_THREAD_LOCAL_GET_DEF(mpz, get_mpz2); + +static mpz const & to_mpz1(vm_obj const & o) { + if (is_simple(o)) { + mpz & r = get_mpz1(); + r = cidx(o); + return r; + } else { + return to_mpz(o); + } +} + +static mpz const & to_mpz2(vm_obj const & o) { + if (is_simple(o)) { + mpz & r = get_mpz2(); + r = cidx(o); + return r; + } else { + return to_mpz(o); + } +} + +static void nat_succ(vm_state & s) { + vm_obj const & a = s.get(0); + if (is_simple(a)) { + s.push(mk_vm_nat(cidx(a) + 1)); + } else { + s.push(mk_vm_mpz(to_mpz1(a) + 1)); + } +} + +static void nat_add(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + s.push(mk_vm_nat(cidx(a1) + cidx(a2))); + } else { + s.push(mk_vm_mpz(to_mpz1(a1) + to_mpz2(a2))); + } +} + +static void nat_mul(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + unsigned long long r = static_cast(cidx(a1)) + static_cast(cidx(a2)); + if (r < MAX_SMALL_NAT) { + s.push(mk_vm_simple(r)); + return; + } + } + s.push(mk_vm_mpz(to_mpz1(a1) * to_mpz2(a2))); +} + +static void nat_sub(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + unsigned v1 = cidx(a1); + unsigned v2 = cidx(a2); + if (v2 > v1) + s.push(mk_vm_simple(0)); + else + s.push(mk_vm_nat(v1 - v2)); + } else { + mpz const & v1 = to_mpz1(a1); + mpz const & v2 = to_mpz2(a2); + if (v2 > v1) + s.push(mk_vm_simple(0)); + else + s.push(mk_vm_nat(v1 - v2)); + } +} + +static void nat_div(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + unsigned v1 = cidx(a1); + unsigned v2 = cidx(a2); + if (v2 == 0) + s.push(mk_vm_simple(0)); + else + s.push(mk_vm_nat(v1 / v2)); + } else { + mpz const & v1 = to_mpz1(a1); + mpz const & v2 = to_mpz2(a2); + if (v2 == 0) + s.push(mk_vm_simple(0)); + else + s.push(mk_vm_nat(v1 / v2)); + } +} + +static void nat_mod(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + unsigned v1 = cidx(a1); + unsigned v2 = cidx(a2); + if (v2 == 0) + s.push(a1); + else + s.push(mk_vm_nat(v1 % v2)); + } else { + mpz const & v1 = to_mpz1(a1); + mpz const & v2 = to_mpz2(a2); + if (v2 == 0) + s.push(a1); + else + s.push(mk_vm_nat(v1 % v2)); + } +} + +static void nat_gcd(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + mpz r; + gcd(r, to_mpz1(a1), to_mpz2(a2)); + s.push(mk_vm_nat(r)); +} + +static void nat_has_decidable_eq(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + return s.push(mk_vm_bool(cidx(a1) == cidx(a2))); + } else { + return s.push(mk_vm_bool(to_mpz1(a1) == to_mpz2(a2))); + } +} + +static void nat_has_decidable_le(vm_state & s) { + vm_obj const & a1 = s.get(0); + vm_obj const & a2 = s.get(1); + if (is_simple(a1) && is_simple(a2)) { + return s.push(mk_vm_bool(cidx(a1) <= cidx(a2))); + } else { + return s.push(mk_vm_bool(to_mpz1(a1) <= to_mpz2(a2))); + } +} + +void initialize_vm_nat() { + declare_vm_builtin(get_nat_succ_name(), 1, nat_succ); + declare_vm_builtin(get_nat_add_name(), 2, nat_add); + declare_vm_builtin(get_nat_mul_name(), 2, nat_mul); + declare_vm_builtin(get_nat_sub_name(), 2, nat_sub); + declare_vm_builtin(get_nat_div_name(), 2, nat_div); + declare_vm_builtin(get_nat_mod_name(), 2, nat_mod); + declare_vm_builtin(get_nat_gcd_name(), 2, nat_gcd); + declare_vm_builtin(get_nat_has_decidable_eq_name(), 2, nat_has_decidable_eq); + declare_vm_builtin(get_nat_has_decidable_le_name(), 2, nat_has_decidable_le); +} + +void finalize_vm_nat() { +} +} diff --git a/src/library/vm/vm_nat.h b/src/library/vm/vm_nat.h new file mode 100644 index 0000000000..d48a2859cd --- /dev/null +++ b/src/library/vm/vm_nat.h @@ -0,0 +1,12 @@ +/* +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 + +namespace lean { +void initialize_vm_nat(); +void finalize_vm_nat(); +}