217 lines
7.7 KiB
C++
217 lines
7.7 KiB
C++
/*
|
|
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 <vector>
|
|
#include <iostream>
|
|
#include "util/rb_map.h"
|
|
#include "library/vm/vm.h"
|
|
#include "library/vm/vm_nat.h"
|
|
#include "library/vm/vm_name.h"
|
|
#include "library/vm/vm_option.h"
|
|
#include "library/vm/vm_ordering.h"
|
|
|
|
namespace lean {
|
|
struct vm_obj_cmp {
|
|
vm_obj m_cmp;
|
|
int operator()(vm_obj const & o1, vm_obj const & o2) const {
|
|
return ordering_to_int(invoke(m_cmp, o1, o2));
|
|
}
|
|
vm_obj_cmp() {}
|
|
explicit vm_obj_cmp(vm_obj const & cmp):m_cmp(cmp) {}
|
|
};
|
|
|
|
typedef rb_map<vm_obj, vm_obj, vm_obj_cmp> vm_obj_map;
|
|
|
|
struct vm_rb_map : public vm_external {
|
|
vm_obj_map m_map;
|
|
vm_rb_map(vm_obj_map const & m):m_map(m) {}
|
|
virtual ~vm_rb_map() {}
|
|
virtual void dealloc() override { this->~vm_rb_map(); get_vm_allocator().deallocate(sizeof(vm_rb_map), this); }
|
|
virtual vm_external * ts_clone(vm_clone_fn const &) override;
|
|
virtual vm_external * clone(vm_clone_fn const &) override { lean_unreachable(); }
|
|
};
|
|
|
|
/* Auxiliary object used by vm_rb_map::ts_clone.
|
|
This is the "thread safe" version used when creating a ts_vm_obj that contains
|
|
a nested vm_rb_map. */
|
|
struct vm_rb_map_ts_copy : public vm_external {
|
|
vm_obj m_cmp;
|
|
std::vector<pair<vm_obj, vm_obj>> m_entries;
|
|
virtual ~vm_rb_map_ts_copy() {
|
|
/* The object ts_vm_obj manages the life cycle of all vm_obj's.
|
|
We should prevent this destructor from invoking the destructor of m_cmp and the
|
|
vm_obj's nested in m_entries. */
|
|
m_cmp.steal_ptr();
|
|
for (auto & p : m_entries) {
|
|
if (p.first.is_ptr())
|
|
p.first.steal_ptr();
|
|
if (p.second.is_ptr())
|
|
p.second.steal_ptr();
|
|
}
|
|
}
|
|
virtual void dealloc() override { lean_unreachable(); }
|
|
virtual vm_external * ts_clone(vm_clone_fn const &) override { lean_unreachable(); }
|
|
virtual vm_external * clone(vm_clone_fn const &) override;
|
|
};
|
|
|
|
vm_external * vm_rb_map::ts_clone(vm_clone_fn const & fn) {
|
|
vm_rb_map_ts_copy * r = new vm_rb_map_ts_copy();
|
|
r->m_cmp = fn(m_map.get_cmp().m_cmp);
|
|
m_map.for_each([&](vm_obj const & k, vm_obj const & v) {
|
|
r->m_entries.emplace_back(fn(k), fn(v));
|
|
});
|
|
return r;
|
|
}
|
|
|
|
vm_external * vm_rb_map_ts_copy::clone(vm_clone_fn const & fn) {
|
|
vm_obj new_cmp = fn(m_cmp);
|
|
vm_obj_map new_map = vm_obj_map(vm_obj_cmp(new_cmp));
|
|
for (auto const & p : m_entries) {
|
|
new_map.insert(fn(p.first), fn(p.second));
|
|
}
|
|
return new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(new_map);
|
|
}
|
|
|
|
vm_obj_map const & to_map(vm_obj const & o) {
|
|
lean_vm_check(dynamic_cast<vm_rb_map*>(to_external(o)));
|
|
return static_cast<vm_rb_map*>(to_external(o))->m_map;
|
|
}
|
|
|
|
vm_obj to_obj(vm_rb_map const & n) {
|
|
return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(n));
|
|
}
|
|
|
|
vm_obj rb_map_mk_core(vm_obj const &, vm_obj const &, vm_obj const & cmp) {
|
|
return to_obj(vm_obj_map(vm_obj_cmp(cmp)));
|
|
}
|
|
|
|
vm_obj rb_map_size(vm_obj const &, vm_obj const &, vm_obj const & m) {
|
|
return mk_vm_nat(to_map(m).size());
|
|
}
|
|
|
|
vm_obj rb_map_empty(vm_obj const &, vm_obj const &, vm_obj const & m) {
|
|
return mk_vm_bool(to_map(m).empty());
|
|
}
|
|
|
|
vm_obj rb_map_insert(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k, vm_obj const & d) {
|
|
return to_obj(insert(to_map(m), k, d));
|
|
}
|
|
|
|
vm_obj rb_map_erase(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k) {
|
|
return to_obj(erase(to_map(m), k));
|
|
}
|
|
|
|
vm_obj rb_map_contains(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k) {
|
|
return mk_vm_bool(to_map(m).contains(k));
|
|
}
|
|
|
|
vm_obj rb_map_find(vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & k) {
|
|
if (auto d = to_map(m).find(k))
|
|
return mk_vm_some(*d);
|
|
else
|
|
return mk_vm_none();
|
|
}
|
|
|
|
vm_obj rb_map_min(vm_obj const &, vm_obj const &, vm_obj const & m) {
|
|
if (to_map(m).empty())
|
|
return mk_vm_none();
|
|
else
|
|
return mk_vm_some(to_map(m).min());
|
|
}
|
|
|
|
vm_obj rb_map_max(vm_obj const &, vm_obj const &, vm_obj const & m) {
|
|
if (to_map(m).empty())
|
|
return mk_vm_none();
|
|
else
|
|
return mk_vm_some(to_map(m).max());
|
|
}
|
|
|
|
vm_obj rb_map_fold(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & m, vm_obj const & a, vm_obj const & fn) {
|
|
vm_obj r = a;
|
|
to_map(m).for_each([&](vm_obj const & k, vm_obj const & d) {
|
|
r = invoke(fn, k, d, r);
|
|
});
|
|
return r;
|
|
}
|
|
|
|
struct vm_name_set : public vm_external {
|
|
name_set m_val;
|
|
vm_name_set(name_set const & v):m_val(v) {}
|
|
virtual ~vm_name_set() {}
|
|
virtual void dealloc() override { this->~vm_name_set(); get_vm_allocator().deallocate(sizeof(vm_name_set), this); }
|
|
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_name_set(m_val); }
|
|
virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_name_set))) vm_name_set(m_val); }
|
|
};
|
|
|
|
bool is_name_set(vm_obj const & o) {
|
|
return is_external(o) && dynamic_cast<vm_name_set*>(to_external(o));
|
|
}
|
|
|
|
name_set const & to_name_set(vm_obj const & o) {
|
|
lean_vm_check(dynamic_cast<vm_name_set*>(to_external(o)));
|
|
return static_cast<vm_name_set*>(to_external(o))->m_val;
|
|
}
|
|
|
|
vm_obj to_obj(name_set const & n) {
|
|
return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_name_set))) vm_name_set(n));
|
|
}
|
|
|
|
vm_obj mk_name_set() {
|
|
return to_obj(name_set());
|
|
}
|
|
|
|
vm_obj name_set_size(vm_obj const & m) {
|
|
return mk_vm_nat(to_name_set(m).size());
|
|
}
|
|
|
|
vm_obj name_set_empty(vm_obj const & m) {
|
|
return mk_vm_bool(to_name_set(m).empty());
|
|
}
|
|
|
|
vm_obj name_set_insert(vm_obj const & m, vm_obj const & k) {
|
|
return to_obj(insert(to_name_set(m), to_name(k)));
|
|
}
|
|
|
|
vm_obj name_set_erase(vm_obj const & m, vm_obj const & k) {
|
|
return to_obj(erase(to_name_set(m), to_name(k)));
|
|
}
|
|
|
|
vm_obj name_set_contains(vm_obj const & m, vm_obj const & k) {
|
|
return mk_vm_bool(to_name_set(m).contains(to_name(k)));
|
|
}
|
|
|
|
vm_obj name_set_fold(vm_obj const &, vm_obj const & m, vm_obj const & a, vm_obj const & fn) {
|
|
vm_obj r = a;
|
|
to_name_set(m).for_each([&](name const & k) {
|
|
r = invoke(fn, to_obj(k), r);
|
|
});
|
|
return r;
|
|
}
|
|
|
|
void initialize_vm_rb_map() {
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "mk_core"}), rb_map_mk_core);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "size"}), rb_map_size);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "empty"}), rb_map_empty);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "insert"}), rb_map_insert);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "erase"}), rb_map_erase);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "contains"}), rb_map_contains);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "find"}), rb_map_find);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "min"}), rb_map_min);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "max"}), rb_map_max);
|
|
DECLARE_VM_BUILTIN(name({"native", "rb_map", "fold"}), rb_map_fold);
|
|
|
|
DECLARE_VM_BUILTIN(name({"mk_name_set"}), mk_name_set);
|
|
DECLARE_VM_BUILTIN(name({"name_set", "size"}), name_set_size);
|
|
DECLARE_VM_BUILTIN(name({"name_set", "empty"}), name_set_empty);
|
|
DECLARE_VM_BUILTIN(name({"name_set", "insert"}), name_set_insert);
|
|
DECLARE_VM_BUILTIN(name({"name_set", "erase"}), name_set_erase);
|
|
DECLARE_VM_BUILTIN(name({"name_set", "contains"}), name_set_contains);
|
|
DECLARE_VM_BUILTIN(name({"name_set", "fold"}), name_set_fold);
|
|
}
|
|
|
|
void finalize_vm_rb_map() {
|
|
}
|
|
}
|