refactor(library): move vm to a separate directory

src/CMakeLists.txt

@@ -350,6 +350,8 @@ set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
 # set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
 # add_subdirectory(library/blast/forward)
 # set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:forward>)
+add_subdirectory(library/vm)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:vm>)
 add_subdirectory(library/compiler)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
 add_subdirectory(frontends/lean)

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();

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

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"

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 {

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"

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();

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();
 }

src/library/vm/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(vm OBJECT vm.cpp vm_nat.cpp init_module.cpp)

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();
+}
+}

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();
+}

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<vm_obj_cell*> & 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<pair<unsigned, vm_function>>();
 }
 
-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<unsigned long long>(cidx(a1)) + static_cast<unsigned long long>(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<pair<unsigned, vm_function>>();
-    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;
 }
 }

src/library/vm/vm.h

@@ -430,6 +430,9 @@ optional<vm_decl> 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();
 }

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<unsigned long long>(cidx(a1)) + static_cast<unsigned long long>(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() {
+}
+}

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();
+}