feat: maxSharing primitives

src/Init/Default.lean

@@ -13,3 +13,4 @@ import Init.System
 import Init.Util
 import Init.Fix
 import Init.LeanInit
+import Init.MaxSharing

src/Init/MaxSharing.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Util
+import Init.Data.HashMap
+import Init.Data.HashSet
+import Init.Data.PersistentHashSet
+import Init.Data.PersistentHashMap
+
+namespace MaxSharing
+/-
+  The max sharing primitives are implemented internally.
+  They use maps and sets of Lean objects. We have two versions:
+  one using `HashMap` and `HashSet`, and another using
+  `PersistentHashMap` and `PersistentHashSet`.
+  These maps and sets are "instantiated here using the "unsafe"
+  primitives `Object.eq`, `Object.hash`, and `ptrAddrUnsafe`. -/
+
+constant ObjectPointed : PointedType := arbitrary _
+def Object : Type := ObjectPointed.type
+instance Object.inhabited : Inhabited Object := ⟨ObjectPointed.val⟩
+
+unsafe def Object.ptrEq (a b : Object) : Bool :=
+ptrAddrUnsafe a == ptrAddrUnsafe b
+
+unsafe def Object.ptrHash (a : Object) : USize :=
+ptrAddrUnsafe a
+
+@[extern "lean_maxsharing_eq"]
+unsafe constant Object.eq (a b : @& Object) : Bool := arbitrary _
+
+@[extern "lean_maxsharing_hash"]
+unsafe constant Object.hash (a : @& Object) : USize := arbitrary _
+
+unsafe def ObjectMap : Type := @HashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩
+unsafe def ObjectSet : Type := @HashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩
+unsafe def ObjectPersistentMap : Type := @PersistentHashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩
+unsafe def ObjectPersistentSet : Type := @PersistentHashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩
+
+@[export lean_mk_object_map]
+unsafe def mkObjectMap : Unit → ObjectMap :=
+fun _ => @mkHashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩ 1024
+
+@[export lean_object_map_find]
+unsafe def ObjectMap.find? (m : ObjectMap) (k : Object) : Option Object :=
+@HashMap.find? Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩ m k
+
+@[export lean_object_map_insert]
+unsafe def ObjectMap.insert (m : ObjectMap) (k v : Object) : ObjectMap :=
+@HashMap.insert Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩ m k v
+
+@[export lean_mk_object_set]
+unsafe def mkObjectSet : Unit → ObjectSet :=
+fun _ => @mkHashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩ 1024
+
+@[export lean_object_set_find]
+unsafe def ObjectSet.find? (s : ObjectSet) (o : Object) : Option Object :=
+@HashSet.find? Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
+
+@[export lean_object_set_insert]
+unsafe def ObjectSet.insert (s : ObjectSet) (o : Object) : ObjectSet :=
+@HashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
+
+@[export lean_mk_object_pmap]
+unsafe def mkObjectPersistentMap : Unit → ObjectPersistentMap :=
+fun _ => @PersistentHashMap.empty Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩
+
+@[export lean_object_pmap_find]
+unsafe def ObjectPersistentMap.find? (m : ObjectPersistentMap) (k : Object) : Option Object :=
+@PersistentHashMap.find? Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩ m k
+
+@[export lean_object_pmap_insert]
+unsafe def ObjectPersistentMap.insert (m : ObjectPersistentMap) (k v : Object) : ObjectPersistentMap :=
+@PersistentHashMap.insert Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩ m k v
+
+@[export lean_mk_object_pset]
+unsafe def mkObjectPersistentSet : Unit → ObjectPersistentSet :=
+fun _ => @PersistentHashSet.empty Object ⟨Object.eq⟩ ⟨Object.hash⟩
+
+@[export lean_object_pset_find]
+unsafe def ObjectPersistentSet.find? (s : ObjectPersistentSet) (o : Object) : Option Object :=
+@PersistentHashSet.find? Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
+
+@[export lean_object_pset_insert]
+unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : ObjectPersistentSet :=
+@PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
+
+#exit -- REMOVE after update stage0
+
+/- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/
+constant StatePointed : PointedType := arbitrary _
+abbrev State : Type := StatePointed.type
+@[extern "lean_maxsharing_mk_state"]
+constant mkState : Unit → State := fun _ => StatePointed.val
+def State.empty : State := mkState ()
+instance State.inhabited : Inhabited State := ⟨State.empty⟩
+
+/- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/
+constant PersistentStatePointed : PointedType := arbitrary _
+abbrev PersistentState : Type := PersistentStatePointed.type
+@[extern "lean_maxsharing_mk_pstate"]
+constant mkPersistentState : Unit → PersistentState := fun _ => PersistentStatePointed.val
+def PersistentState.empty : PersistentState := mkPersistentState ()
+instance PersistentState.inhabited : Inhabited PersistentState := ⟨PersistentState.empty⟩
+abbrev PState : Type := PersistentState
+
+@[extern "lean_state_maxsharing"]
+def State.maxSharing {α} (s : State) (a : α) : α × State :=
+(a, s)
+
+@[extern "lean_persistent_state_maxsharing"]
+def PersistentState.maxSharing {α} (s : PersistentState) (a : α) : α × PersistentState :=
+(a, s)
+
+end MaxSharing
+
+def maxSharing {α} (a : α) : α :=
+(MaxSharing.State.empty.maxSharing a).1

src/runtime/CMakeLists.txt

@@ -1,7 +1,7 @@
 set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp mpq.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
-platform.cpp alloc.cpp allocprof.cpp)
+platform.cpp alloc.cpp allocprof.cpp maxsharing.cpp)
 add_library(runtime OBJECT ${RUNTIME_OBJS})
 add_library(leanruntime ${RUNTIME_OBJS})
 

src/runtime/maxsharing.cpp

@@ -0,0 +1,72 @@
+/*
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "runtime/object.h"
+#include "runtime/hash.h"
+
+namespace lean {
+
+extern "C" uint8 lean_maxsharing_eq(b_obj_arg o1, b_obj_arg o2) {
+    lean_assert(!lean_is_scalar(o1));
+    lean_assert(!lean_is_scalar(o2));
+    size_t sz1 = lean_object_byte_size(o1);
+    size_t sz2 = lean_object_byte_size(o2);
+    if (sz1 != sz2) return false;
+    return memcmp(o1, o2, sz1) == 0;
+}
+
+extern "C" usize lean_maxsharing_hash(b_obj_arg o) {
+    lean_assert(!lean_is_scalar(o));
+    size_t sz = lean_object_byte_size(o);
+    return hash_str(sz, reinterpret_cast<char const *>(o), 17);
+}
+
+// unsafe def mkObjectMap : Unit → ObjectMap
+extern "C" obj_res lean_mk_object_map(obj_arg);
+// unsafe def ObjectMap.find? (m : ObjectMap) (k : Object) : Option Object
+extern "C" obj_res lean_object_map_find(obj_arg m, obj_arg k);
+// unsafe def ObjectMap.insert (m : ObjectMap) (k v : Object) : ObjectMap
+extern "C" obj_res lean_object_map_insert(obj_arg m, obj_arg k, obj_arg v);
+
+// unsafe def mkObjectSet : Unit → ObjectSet
+extern "C" obj_res lean_mk_object_set(obj_arg);
+// unsafe def ObjectSet.find? (s : ObjectSet) (o : Object) : Option Object
+extern "C" obj_res lean_object_set_find(obj_arg s, obj_arg o);
+// unsafe def ObjectSet.insert (s : ObjectSet) (o : Object) : ObjectSet
+extern "C" obj_res lean_object_set_insert(obj_arg s, obj_arg o);
+
+// unsafe def mkObjectPersistentMap : Unit → ObjectPersistentMap
+extern "C" obj_res lean_mk_object_pmap(obj_arg);
+// unsafe def ObjectPersistentMap.find? (m : ObjectPersistentMap) (k : Object) : Option Object
+extern "C" obj_res lean_object_pmap_find(obj_arg m, obj_arg k);
+// unsafe def ObjectPersistentMap.insert (m : ObjectPersistentMap) (k v : Object) : ObjectPersistentMap
+extern "C" obj_res lean_object_pmap_insert(obj_arg m, obj_arg k, obj_arg v);
+
+// unsafe def mkObjectPersistentSet : Unit → ObjectPersistentSet
+extern "C" obj_res lean_mk_object_pset(obj_arg);
+// unsafe def ObjectPersistentSet.find? (s : ObjectPersistentSet) (o : Object) : Option Object
+extern "C" obj_res lean_object_pset_find(obj_arg s, obj_arg o);
+// unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : ObjectPersistentSet
+extern "C" obj_res lean_object_pset_insert(obj_arg s, obj_arg o);
+
+static obj_res pack_state(obj_arg m, obj_arg s) {
+    object * r = alloc_cnstr(0, 2, 0);
+    cnstr_set(r, 0, m);
+    cnstr_set(r, 1, s);
+    return r;
+}
+
+/*
+extern "C" obj_res lean_maxsharing_mk_state(obj_arg) {
+    return pack_state(lean_mk_object_map(box(0)), lean_mk_object_set(box(0)));
+}
+
+extern "C" obj_res lean_maxsharing_mk_pstate(obj_arg) {
+    return pack_state(lean_mk_object_pmap(box(0)), lean_mk_object_pset(box(0)));
+}
+*/
+
+};