From 9256618d67dbe9e39c22cbd6932166fe5d7dc48c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Oct 2018 11:31:09 -0700 Subject: [PATCH] chore(library/vm): remove `vm_name` --- src/frontends/lean/elaborator.cpp | 1 - src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 3 - src/library/vm/vm.cpp | 1 - src/library/vm/vm_name.cpp | 105 ------------------------------ src/library/vm/vm_name.h | 16 ----- 6 files changed, 1 insertion(+), 127 deletions(-) delete mode 100644 src/library/vm/vm_name.cpp delete mode 100644 src/library/vm/vm_name.h diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a2cc98f4ba..90cd7326ea 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -38,7 +38,6 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/aux_definition.h" #include "library/check.h" -#include "library/vm/vm_name.h" #include "library/compiler/compiler.h" #include "library/tactic/kabstract.h" #include "library/tactic/tactic_state.h" diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index fda219152e..9a35329b40 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp +add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 1190d2e09c..8e607968d7 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "library/vm/vm_int.h" #include "library/vm/vm_aux.h" #include "library/vm/vm_io.h" -#include "library/vm/vm_name.h" #include "library/vm/vm_array.h" #include "library/vm/vm_string.h" #include "library/vm/vm_platform.h" @@ -21,7 +20,6 @@ void initialize_vm_core_module() { initialize_vm_int(); initialize_vm_aux(); initialize_vm_io(); - initialize_vm_name(); initialize_vm_array(); initialize_vm_string(); initialize_vm_platform(); @@ -31,7 +29,6 @@ void finalize_vm_core_module() { finalize_vm_platform(); finalize_vm_string(); finalize_vm_array(); - finalize_vm_name(); finalize_vm_io(); finalize_vm_aux(); finalize_vm_int(); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 97027f18dc..dc2c5aeaf7 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -27,7 +27,6 @@ Author: Leonardo de Moura #include "library/time_task.h" #include "library/vm/vm.h" #include "library/vm/vm_string.h" -#include "library/vm/vm_name.h" #include "library/vm/vm_option.h" #ifndef LEAN_DEFAULT_PROFILER_FREQ diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp deleted file mode 100644 index 690f063b77..0000000000 --- a/src/library/vm/vm_name.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/* -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 -#include "library/util.h" -#include "library/vm/vm.h" -#include "library/vm/vm_nat.h" -#include "library/vm/vm_string.h" -#include "library/vm/vm_ordering.h" - -namespace lean { -struct vm_name : public vm_external { - name m_val; - vm_name(name const & v):m_val(v) {} - virtual ~vm_name() {} - virtual void dealloc() override { delete this; } - virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_name(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new vm_name(m_val); } -}; - -bool is_name(vm_obj const & o) { - return is_external(o) && dynamic_cast(to_external(o)); -} - -name const & to_name(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_val; -} - -vm_obj to_obj(name const & n) { - return mk_vm_external(new vm_name(n)); -} - -vm_obj name_anonymous() { - return to_obj(name()); -} - -vm_obj name_mk_string(vm_obj const & n, vm_obj const & s) { - std::string str = to_string(s); - return to_obj(name(to_name(n), str.c_str())); -} - -vm_obj name_mk_numeral(vm_obj const & n, vm_obj const & num) { - return to_obj(name(to_name(n), to_unsigned(num))); -} - -unsigned name_cases_on(vm_obj const & o, buffer & data) { - name const & n = to_name(o); - if (n.is_anonymous()) { - return 0; - } else if (n.is_string()) { - data.push_back(to_obj(n.get_prefix())); - data.push_back(to_obj(n.get_string().to_std_string())); - return 1; - } else { - data.push_back(to_obj(n.get_prefix())); - data.push_back(mk_vm_nat(n.get_numeral().to_mpz())); - return 2; - } -} - -vm_obj name_has_decidable_eq(vm_obj const & o1, vm_obj const & o2) { - return mk_vm_bool(to_name(o1) == to_name(o2)); -} - -vm_obj name_cmp(vm_obj const & o1, vm_obj const & o2) { - return int_to_ordering(quick_cmp(to_name(o1), to_name(o2))); -} - -vm_obj name_lex_cmp(vm_obj const & o1, vm_obj const & o2) { - return int_to_ordering(cmp(to_name(o1), to_name(o2))); -} - -vm_obj name_append_after(vm_obj const & n, vm_obj const & i) { - return to_obj(to_name(n).append_after(force_to_unsigned(i, 0))); -} - -vm_obj name_append(vm_obj const & n1, vm_obj const & n2) { - return to_obj(to_name(n1) + to_name(n2)); -} - -vm_obj name_is_internal(vm_obj const & n) { - return mk_vm_bool(is_internal_name(to_name(n))); -} - -void initialize_vm_name() { - DECLARE_VM_BUILTIN(name({"lean", "name", "anonymous"}), name_anonymous); - DECLARE_VM_BUILTIN(name({"lean", "name", "mk_string"}), name_mk_string); - DECLARE_VM_BUILTIN(name({"lean", "name", "mk_numeral"}), name_mk_numeral); - DECLARE_VM_BUILTIN(name({"lean", "name", "has_decidable_eq"}), name_has_decidable_eq); - DECLARE_VM_BUILTIN(name({"name", "cmp"}), name_cmp); - DECLARE_VM_BUILTIN(name({"name", "lex_cmp"}), name_lex_cmp); - DECLARE_VM_BUILTIN(name({"name", "append"}), name_append); - DECLARE_VM_BUILTIN(name({"lean", "name", "is_internal"}), name_is_internal); - DECLARE_VM_BUILTIN(name({"lean", "name", "append_after"}), name_append_after); - DECLARE_VM_CASES_BUILTIN(name({"lean", "name", "cases_on"}), name_cases_on); -} - -void finalize_vm_name() { -} -} diff --git a/src/library/vm/vm_name.h b/src/library/vm/vm_name.h deleted file mode 100644 index 71babdf961..0000000000 --- a/src/library/vm/vm_name.h +++ /dev/null @@ -1,16 +0,0 @@ -/* -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 "library/vm/vm.h" - -namespace lean { -bool is_name(vm_obj const & o); -name const & to_name(vm_obj const & o); -vm_obj to_obj(name const & n); -void initialize_vm_name(); -void finalize_vm_name(); -}