max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/vm): remove vm_list

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-02 08:44:05 -07:00
parent 429f844fbe
commit 3ac6eab393
8 changed files with 9 additions and 227 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/tactic/tactic_state.cpp
View file

@ -22,7 +22,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_options.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_io.h"
#include "library/vm/interaction_state_imp.h"

3
src/library/vm/CMakeLists.txt
View file

@ -1,3 +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
vm_options.cpp vm_format.cpp vm_list.cpp
vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp)
vm_options.cpp vm_format.cpp vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp)

3
src/library/vm/init_module.cpp
View file

@ -12,7 +12,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_name.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_format.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_array.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_platform.h"
@ -27,7 +26,6 @@ void initialize_vm_core_module() {
initialize_vm_name();
initialize_vm_options();
initialize_vm_format();
initialize_vm_list();
initialize_vm_array();
initialize_vm_string();
initialize_vm_platform();
@ -37,7 +35,6 @@ void finalize_vm_core_module() {
finalize_vm_platform();
finalize_vm_string();
finalize_vm_array();
finalize_vm_list();
finalize_vm_format();
finalize_vm_options();
finalize_vm_name();

1
src/library/vm/interaction_state_imp.h
View file

@ -18,7 +18,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
#include "library/vm/vm_options.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_pos_info.h"
#include "library/compiler/vm_compiler.h"

10
src/library/vm/vm_io.cpp
View file

@ -32,7 +32,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_nat.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_io.h"
#include "library/vm/vm_list.h"
namespace lean {
static vm_obj const REAL_WORLD = mk_vm_simple(0);
@ -323,10 +322,17 @@ static vm_obj io_set_cwd(vm_obj const & cwd, vm_obj const &) {
static std::vector<std::string> * g_cmdline_args = nullptr;
static vm_obj to_list(buffer<vm_obj> const & ls) {
vm_obj obj = mk_vm_simple(0);
for (unsigned i = ls.size(); i > 0; i--)
obj = mk_vm_constructor(1, ls[i - 1], obj);
return obj;
}
static vm_obj io_cmdline_args() {
buffer<vm_obj> objs;
for (auto & s : *g_cmdline_args) objs.push_back(to_obj(s));
return to_obj(objs);
return to_list(objs);
}
void set_io_cmdline_args(std::vector<std::string> const & args) {

145
src/library/vm/vm_list.cpp
View file

@ -1,145 +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 "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_list.h"
namespace lean {
template<typename A>
struct vm_list : public vm_external {
list<A> m_val;
vm_list(list<A> const & v):m_val(v) {}
virtual ~vm_list() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_list<A>(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_list<A>(m_val); }
};
template<typename A>
struct vm_list_ref : public vm_external {
list_ref<A> m_val;
vm_list_ref(list_ref<A> const & v):m_val(v) {}
virtual ~vm_list_ref() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_list_ref<A>(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_list_ref<A>(m_val); }
};
template<typename A>
vm_obj list_to_obj(list<A> const & l) {
return mk_vm_external(new vm_list<A>(l));
}
template<typename A>
vm_obj list_ref_to_obj(list_ref<A> const & l) {
return mk_vm_external(new vm_list_ref<A>(l));
}
vm_obj to_obj(names const & ls) { return list_ref_to_obj(ls); }
vm_obj to_obj(list<list<expr>> const & ls) { return list_to_obj(ls); }
vm_obj to_obj(buffer<name> const & ls) { return to_obj(names(ls)); }
#define MK_TO_LIST(A, ToA) \
list<A> to_list_ ## A(vm_obj const & o) { \
if (is_simple(o)) { \
return list<A>(); \
} else if (is_constructor(o)) { \
return list<A>(ToA(cfield(o, 0)), to_list_ ## A(cfield(o, 1))); \
} else { \
lean_vm_check(dynamic_cast<vm_list<A>*>(to_external(o))); \
return static_cast<vm_list<A>*>(to_external(o))->m_val; \
} \
}
#define MK_TO_LIST_REF(A, ToA) \
static list_ref<A> to_list_ref_ ## A(vm_obj const & o) { \
if (is_simple(o)) { \
return list_ref<A>(); \
} else if (is_constructor(o)) { \
return list_ref<A>(ToA(cfield(o, 0)), to_list_ref_ ## A(cfield(o, 1))); \
} else { \
lean_vm_check(dynamic_cast<vm_list_ref<A>*>(to_external(o))); \
return static_cast<vm_list_ref<A>*>(to_external(o))->m_val; \
} \
}
MK_TO_LIST_REF(name, to_name)
names to_names(vm_obj const & o) { return to_list_ref_name(o); }
#define MK_TO_BUFFER(A, ToA) \
void to_buffer_ ## A(vm_obj const & o, buffer<A> & r) { \
if (is_simple(o)) { \
return; \
} else if (is_constructor(o)) { \
r.push_back(ToA(cfield(o, 0))); \
to_buffer_ ## A(cfield(o, 1), r); \
} else { \
lean_vm_check(dynamic_cast<vm_list<A>*>(to_external(o))); \
to_buffer(static_cast<vm_list<A>*>(to_external(o))->m_val, r); \
} \
}
MK_TO_BUFFER(name, to_name)
template<typename A>
unsigned list_cases_on_core(list<A> const & l, buffer<vm_obj> & data) {
if (empty(l)) {
return 0;
} else {
data.push_back(to_obj(head(l)));
data.push_back(list_to_obj(tail(l)));
return 1;
}
}
template<typename A>
unsigned list_ref_cases_on_core(list_ref<A> const & l, buffer<vm_obj> & data) {
if (empty(l)) {
return 0;
} else {
data.push_back(to_obj(head(l)));
data.push_back(list_ref_to_obj(tail(l)));
return 1;
}
}
unsigned list_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
if (is_simple(o)) {
return 0;
} else if (is_constructor(o)) {
data.append(csize(o), cfields(o));
return 1;
} else {
if (auto l = dynamic_cast<vm_list_ref<name>*>(to_external(o))) {
return list_ref_cases_on_core(l->m_val, data);
} else {
lean_unreachable();
}
}
}
vm_obj to_obj(list<unsigned> const & ls) {
return to_vm_list(ls, [&](unsigned n) { return mk_vm_nat(n); });
}
vm_obj to_obj(buffer<vm_obj> const & ls) {
vm_obj obj = mk_vm_nil();
for (unsigned i = ls.size(); i > 0; i--)
obj = mk_vm_cons(ls[i - 1], obj);
return obj;
}
void initialize_vm_list() {
DECLARE_VM_CASES_BUILTIN(name({"list", "cases_on"}), list_cases_on);
}
void finalize_vm_list() {
}
}

72
src/library/vm/vm_list.h
View file

@ -1,72 +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 "kernel/expr.h"
#include "library/vm/vm.h"
namespace lean {
names to_names(vm_obj const & o);
/* Given an object o : list name, store its contents at \c r */
void to_buffer_name(vm_obj const & o, buffer<name> & r);
vm_obj to_obj(buffer<name> const & ls);
vm_obj to_obj(names const & ls);
levels to_levels(vm_obj const & o);
/* Given an object o : list level, store its contents at \c r */
void to_buffer_level(vm_obj const & o, buffer<level> & r);
vm_obj to_obj(buffer<level> const & ls);
vm_obj to_obj(levels const & ls);
list<expr> to_list_expr(vm_obj const & o);
/* Given an object o : list expr, store its contents at \c r */
void to_buffer_expr(vm_obj const & o, buffer<expr> & r);
vm_obj to_obj(buffer<expr> const & ls);
vm_obj to_obj(list<expr> const & ls);
vm_obj to_obj(list<list<expr>> const & ls);
template<typename A, typename F>
vm_obj to_vm_list(list<A> const & ls, F const & fn) {
if (empty(ls)) return mk_vm_simple(0);
else return mk_vm_constructor(1, fn(head(ls)), to_vm_list(tail(ls), fn));
}
vm_obj to_obj(list<unsigned> const & ls);
vm_obj to_obj(buffer<vm_obj> const & ls);
/* Helper functions for accessing (list A) when A is not expr, name nor level */
inline bool is_nil(vm_obj const & o) { return is_simple(o); }
inline vm_obj head(vm_obj const & o) { lean_assert(!is_nil(o)); return cfield(o, 0); }
inline vm_obj tail(vm_obj const & o) { lean_assert(!is_nil(o)); return cfield(o, 1); }
inline vm_obj mk_vm_nil() { return mk_vm_simple(0); }
inline vm_obj mk_vm_cons(vm_obj const & h, vm_obj const & t) { return mk_vm_constructor(1, h, t); }
template<typename A, typename F>
list<A> to_list(vm_obj const & o, F const & fn) {
if (is_simple(o)) {
return list<A>();
} else if (is_constructor(o)) {
return list<A>(fn(cfield(o, 0)), to_list<A>(cfield(o, 1), fn));
} else {
lean_unreachable();
}
}
template<typename A, typename F>
list_ref<A> to_list_ref(vm_obj const & o, F const & fn) {
if (is_simple(o)) {
return list_ref<A>();
} else if (is_constructor(o)) {
return list_ref<A>(fn(cfield(o, 0)), to_list_ref<A>(cfield(o, 1), fn));
} else {
lean_unreachable();
}
}
void initialize_vm_list();
void finalize_vm_list();
}

1
src/library/vm/vm_name.cpp
View file

@ -11,7 +11,6 @@ Author: Leonardo de Moura
#include "library/vm/vm_nat.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_ordering.h"
#include "library/vm/vm_list.h"
namespace lean {
struct vm_name : public vm_external {