feat(library/vm): expose rb_map object

library/meta/default.lean

@@ -3,4 +3,4 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name meta.options meta.format
+import meta.name meta.options meta.format meta.rb_map

library/meta/rb_map.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import meta.cmp_result meta.name
+
+meta_constant rb_map.{l₁ l₂} : Type.{l₁} → Type.{l₂} → Type.{max l₁ l₂ 1}
+
+namespace rb_map
+meta_constant mk {key : Type} (data : Type)             : (key → key → cmp_result) → rb_map key data
+meta_constant size {key : Type} {data : Type}           : rb_map key data → nat
+meta_constant insert {key : Type} {data : Type}         : rb_map key data → key → data → rb_map key data
+meta_constant erase  {key : Type} {data : Type}         : rb_map key data → key → rb_map key data
+meta_constant contains {key : Type} {data : Type}       : rb_map key data → key → bool
+meta_constant find {key : Type} {data : Type}           : rb_map key data → key → option data
+meta_constant min {key : Type} {data : Type}            : rb_map key data → option data
+meta_constant max {key : Type} {data : Type}            : rb_map key data → option data
+meta_constant fold {key : Type} {data : Type} {A :Type} : rb_map key data → A → (key → data → A → A) → A
+
+open list
+meta_definition of_list {key : Type} {data : Type} (cmp : key → key → cmp_result) : list (key × data) → rb_map key data
+| []           := mk data cmp
+| ((k, v)::ls) := insert (of_list cmp ls) k v
+
+end rb_map
+
+meta_definition nat_map (data : Type) := rb_map nat data
+namespace nat_map
+  export rb_map (hiding mk)
+
+  meta_definition mk (data : Type) : nat_map data :=
+  rb_map.mk data nat.cmp
+end nat_map
+
+meta_definition name_map (data : Type) := rb_map name data
+namespace name_map
+  export rb_map (hiding mk)
+
+  meta_definition mk (data : Type) : name_map data :=
+  rb_map.mk data name.cmp
+end name_map

src/library/vm/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(vm OBJECT vm.cpp vm_nat.cpp vm_string.cpp vm_io.cpp vm_name.cpp vm_options.cpp
-  vm_format.cpp vm_aux.cpp optimize.cpp init_module.cpp)
+  vm_format.cpp vm_rb_map.cpp vm_aux.cpp optimize.cpp init_module.cpp)

src/library/vm/init_module.cpp

@@ -10,6 +10,7 @@ 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_rb_map.h"
 #include "library/vm/vm_aux.h"
 
 namespace lean {
@@ -20,10 +21,12 @@ void initialize_vm_core_module() {
     initialize_vm_name();
     initialize_vm_options();
     initialize_vm_format();
+    initialize_vm_rb_map();
     initialize_vm_aux();
 }
 void finalize_vm_core_module() {
     finalize_vm_aux();
+    finalize_vm_rb_map();
     finalize_vm_format();
     finalize_vm_options();
     finalize_vm_name();

src/library/vm/vm_option.h

@@ -0,0 +1,13 @@
+/*
+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 {
+inline vm_obj mk_vm_none() { return mk_vm_simple(0); }
+inline vm_obj mk_vm_some(vm_obj const & a) { return mk_vm_constructor(1, 1, &a); }
+}

src/library/vm/vm_rb_map.cpp

@@ -0,0 +1,100 @@
+/*
+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 <iostream>
+#include "util/rb_map.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_nat.h"
+#include "library/vm/vm_option.h"
+#include "library/vm/cmp_result.h"
+
+namespace lean {
+struct vm_obj_cmp {
+    vm_obj m_cmp;
+    int operator()(vm_obj const & o1, vm_obj const & o2) const {
+        return cmp_result_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() {}
+};
+
+vm_obj_map const & to_map(vm_obj const & o) {
+    lean_assert(is_external(o));
+    lean_assert(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 vm_rb_map(n));
+}
+
+vm_obj rb_map_mk(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_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());
+}
+
+/*
+meta_constant fold {key : Type} {data : Type} {A :Type} : rb_map key data → A → (key → data → A → A) → A
+*/
+
+void initialize_vm_rb_map() {
+    DECLARE_VM_BUILTIN(name({"rb_map", "mk"}),             rb_map_mk);
+    DECLARE_VM_BUILTIN(name({"rb_map", "size"}),           rb_map_size);
+    DECLARE_VM_BUILTIN(name({"rb_map", "insert"}),         rb_map_insert);
+    DECLARE_VM_BUILTIN(name({"rb_map", "erase"}),          rb_map_erase);
+    DECLARE_VM_BUILTIN(name({"rb_map", "contains"}),       rb_map_contains);
+    DECLARE_VM_BUILTIN(name({"rb_map", "find"}),           rb_map_find);
+    DECLARE_VM_BUILTIN(name({"rb_map", "min"}),            rb_map_min);
+    DECLARE_VM_BUILTIN(name({"rb_map", "max"}),            rb_map_max);
+}
+
+void finalize_vm_rb_map() {
+}
+}

src/library/vm/vm_rb_map.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_rb_map();
+void finalize_vm_rb_map();
+}

tests/lean/run/rb_map1.lean

@@ -0,0 +1,22 @@
+import meta
+
+open nat_map
+
+vm_eval size (insert (insert (mk nat) 10 20) 10 21)
+
+meta_definition m := (insert (insert (insert (mk nat) 10 20) 5 50) 10 21)
+
+vm_eval find m 10
+vm_eval find m 5
+vm_eval find m 8
+vm_eval contains m 5
+vm_eval contains m 8
+
+open list
+
+meta_definition m2 := (of_list nat.cmp [(1, "one"), (2, "two"), (3, "three")])
+
+vm_eval size m2
+vm_eval find m2 1
+vm_eval find m2 4
+vm_eval find m2 3