feat(init/data/cached): Caching mechanism [WIP]

library/data/hash_map.lean

@@ -480,6 +480,15 @@ theorem contains_iff (m : hash_map α β) (a : α) (b : β a) :
   m.contains a ↔ a ∈ m.keys :=
 m.is_valid.contains_aux_iff _ _
 
+theorem entries_empty (hash_fn : α → nat) {n} : entries (@mk_hash_map α _ β hash_fn n) = [] :=
+mk_as_list hash_fn _
+
+theorem find_empty (hash_fn : α → nat) {n} (x) : find (@mk_hash_map α _ β hash_fn n) x = none :=
+by { ginduction find (@mk_hash_map α _ β hash_fn n) x with h y, refl,
+     note := (find_iff _ _ _).1 h,
+     rw entries_empty at this,
+     contradiction }
+
 lemma insert_lemma (hash_fn : α → nat) {n n'}
   {bkts : bucket_array α β n} {sz} (v : valid hash_fn bkts sz) :
   valid hash_fn (bkts.foldl (mk_array _ [] : bucket_array α β n') (reinsert_aux hash_fn)) sz :=
@@ -555,6 +564,15 @@ let n'        : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
   buckets  := buckets'',
   is_valid := insert_lemma _ valid' }
 
+theorem insert_hash_fn (m : hash_map α β) (a : α) (b : β a) : (m.insert a b).hash_fn = m.hash_fn :=
+begin
+  cases m, unfold hash_map.insert, simp,
+  cases (by apply_instance : decidable
+    (↑(contains_aux a (bucket_array.read hash_fn buckets a)))) with hc hc; dsimp [dite],
+  cases (by apply_instance : decidable (size + 1 ≤ nbuckets.val)) with hsz hsz; dsimp [ite],
+  all_goals {refl}
+end
+
 theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
   sigma.mk a' b' ∈ (m.insert a b).entries ↔
   if a = a' then b == b' else sigma.mk a' b' ∈ m.entries

library/data/hashed_func.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+import data.hash_map
+
+universes u v
+
+namespace hashed_func
+  variables {α : Type u} [decidable_eq α] {β : α → Type v}
+
+  def cache_ty (f : Π a, β a) (hash_fn : α → ℕ) :=
+  {m : hash_map α β // ∀ x y, m.find x = some y → f x = y}
+
+  instance (f : Π a, β a) (hash_fn : α → ℕ) : inhabited (cache_ty f hash_fn) :=
+  ⟨⟨mk_hash_map hash_fn, λx y h, by rw hash_map.find_empty at h; contradiction⟩⟩
+end hashed_func
+
+structure hashed_func (α : Type u) [decidable_eq α] (β : α → Type v) := mk' ::
+(func : Π a, β a)
+(hash_fn : α → ℕ)
+(cache : cached (hashed_func.cache_ty func hash_fn))
+
+namespace hashed_func
+  variables {α : Type u} [decidable_eq α] {β : α → Type v}
+
+  def mk (f : Π a, β a) (hash_fn : α → ℕ) : hashed_func α β := ⟨f, hash_fn, default _⟩
+
+  def eval : hashed_func α β → Π a, β a | ⟨f, hash_fn, c⟩ a :=
+  c.lift_on
+    (λ⟨m, H⟩, (m.find a).get_or_else $
+      let v := f a in c.update ⟨m.insert a v, λ x y h,
+      begin
+        by_cases a = x with ax,
+        { revert y, rw -ax, intros y h,
+          rw hash_map.find_insert_eq at h,
+          injection h },
+        { rw hash_map.find_insert_ne _ _ _ _ ax at h,
+          exact H x y h }
+      end⟩ v)
+    (λ⟨m, H⟩, begin
+      unfold default inhabited.default hashed_func.eval._match_1,
+      rw hash_map.find_empty,
+      ginduction m.find a with h b; dsimp [option.get_or_else, cached.update, hashed_func.eval._match_1],
+      { refl },
+      { exact H a b h },
+    end)
+
+  instance : has_coe_to_fun (hashed_func α β) := ⟨_, hashed_func.eval⟩
+
+  @[simp] theorem eval_val : ∀ hf : hashed_func α β, eval hf = hf.func
+  | ⟨f, hash_fn, c⟩ := funext $ λ a, by rw [c.cache_eq_empty]; refl
+
+end hashed_func

library/init/data/cached.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+prelude
+import init.data.quot init.data.option.basic init.util
+universes u v
+
+structure cached (α : Type u) [inhabited α] :=
+mk' :: (val : quot (λ x y : α, true))
+
+namespace cached
+  variables {α : Type u} [inhabited α] {β : Type v}
+
+  def mk (v : α) : cached α := ⟨quot.mk _ v⟩
+
+  def empty : cached α := mk (default α)
+  instance : inhabited (cached α) := ⟨empty⟩
+
+  def lift_on (c : cached α) (f : α → β) (h : ∀ x, f (default _) = f x) : β :=
+  quot.lift f (λx y _, (h x).symm.trans (h y)) c.val
+
+  -- This function has a VM implementation to change the value of the cache `c` to `v`
+  def update (c : cached α) (v : α) (f : thunk β) : β := f ()
+
+  @[simp] lemma update_def (c : cached α) (v : α) (f : thunk β) :
+    @update _ _ _ c v f = f () := rfl
+
+  def reset (c : cached α) : thunk β → β := update c (default α)
+
+  @[simp] lemma reset_def (c : cached α) (f : thunk β) :
+    @reset _ _ _ c f = f () := rfl
+
+  theorem cache_eq_empty : ∀ (c : cached α), c = empty
+  | ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
+
+  @[simp] lemma lift_mk {f : α → β} {h} (x) : lift_on (mk x) f h = f x := rfl
+
+  meta def inspect (c : cached α) : α := unchecked_cast c.val
+
+  meta instance [has_to_string α] : has_to_string (cached α) := ⟨to_string ∘ inspect⟩
+
+  meta instance [has_repr α] : has_repr (cached α) := ⟨repr ∘ inspect⟩
+
+end cached
+
+structure memoized (α : Type u) := mk' ::
+(func : unit → α)
+(cache : cached (option {a // func () = a}))
+
+namespace memoized
+  variable {α : Type u}
+
+  def mk (f : thunk α) : memoized α := mk' f (default _)
+
+  def eval : memoized α → α | ⟨f, c⟩ :=
+  c.lift_on
+    (λo, match o with
+      | none := let v := f () in c.update (some ⟨v, rfl⟩) v
+      | some ⟨x, h⟩ := x
+      end)
+    (λo, match o with
+      | none        := rfl
+      | some ⟨x, h⟩ := h
+      end)
+
+  @[simp] theorem mk_eval (f : unit → α) : (@mk _ f).eval = f () := rfl
+
+  @[simp] theorem eval_val : ∀ (f : memoized α), eval f = f.func ()
+  | ⟨f, c⟩ := congr_arg (λ c', eval ⟨f, c'⟩) c.cache_eq_empty
+
+  instance : has_coe_to_fun (memoized α) := ⟨λ_, thunk α, λm _, m.eval⟩
+
+  instance : has_coe (memoized α) α := ⟨λm, m.eval⟩
+
+end memoized

library/init/data/default.lean

@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string
 import init.data.list init.data.sum init.data.subtype init.data.int init.data.array
-import init.data.bool init.data.fin init.data.unsigned
+import init.data.bool init.data.fin init.data.unsigned init.data.cached

src/library/vm/CMakeLists.txt

@@ -1,4 +1,4 @@
 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_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
   vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp
-  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp)
+  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_cached.cpp vm_pos_info.cpp)

src/library/vm/init_module.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_task.h"
 #include "library/vm/vm_parser.h"
 #include "library/vm/vm_array.h"
+#include "library/vm/vm_cached.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -47,9 +48,11 @@ void initialize_vm_core_module() {
     initialize_vm_environment();
     initialize_vm_parser();
     initialize_vm_array();
+    initialize_vm_cached();
 }
 
 void finalize_vm_core_module() {
+    finalize_vm_cached();
     finalize_vm_array();
     finalize_vm_parser();
     finalize_vm_environment();

src/library/vm/vm_cached.cpp

@@ -0,0 +1,67 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Mario Carneiro
+*/
+#include <vector>
+#include "library/vm/vm.h"
+#include "library/trace.h"
+
+#define lean_cached_trace(CODE) lean_trace(name({"cached", "update"}), CODE)
+
+namespace lean {
+struct vm_cached : public vm_external {
+    vm_obj m_default;
+    vm_obj m_value;
+    vm_cached(vm_obj const & def, vm_obj const & v):m_default(def), m_value(v) {}
+    virtual ~vm_cached() {}
+    virtual void dealloc() override { this->~vm_cached(); get_vm_allocator().deallocate(sizeof(vm_cached), this); }
+    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_cached(m_default, m_value); }
+    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_cached))) vm_cached(m_default, m_value); }
+};
+
+vm_obj const & get_cached_default(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_cached*>(to_external(o)));
+    return static_cast<vm_cached*>(to_external(o))->m_default;
+}
+
+vm_obj const & get_cached_value(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_cached*>(to_external(o)));
+    return static_cast<vm_cached*>(to_external(o))->m_value;
+}
+
+vm_obj const & set_cached_value(vm_obj const & o, vm_obj const & v) {
+    lean_vm_check(dynamic_cast<vm_cached*>(to_external(o)));
+    return static_cast<vm_cached*>(to_external(o))->m_value = v;
+}
+
+vm_obj cached_mk(vm_obj const &, vm_obj const & def, vm_obj const & v) {
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_cached))) vm_cached(def, v));
+}
+
+vm_obj cached_update(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & c, vm_obj const & v, vm_obj const & fn) {
+    lean_cached_trace(tout() << "cached update\n";);
+    set_cached_value(c, v);
+    return invoke(fn, mk_vm_unit());
+}
+
+vm_obj cached_val(vm_obj const &, vm_obj const &, vm_obj const & c) {
+    return get_cached_value(c);
+}
+
+unsigned cached_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
+    data.push_back(get_cached_value(o));
+    return 0;
+}
+
+void initialize_vm_cached() {
+    DECLARE_VM_BUILTIN(name({"cached", "mk'"}),              cached_mk);
+    DECLARE_VM_BUILTIN(name({"cached", "val"}),              cached_val);
+    DECLARE_VM_BUILTIN(name({"cached", "update"}),           cached_update);
+    DECLARE_VM_CASES_BUILTIN(name({"cached", "cases_on"}),   cached_cases_on);
+}
+
+void finalize_vm_cached() {
+}
+}

src/library/vm/vm_cached.h

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Mario Carneiro
+*/
+#pragma once
+
+#include "library/vm/vm.h"
+
+namespace lean {
+void initialize_vm_cached();
+void finalize_vm_cached();
+}

tests/lean/run/cached.lean

@@ -0,0 +1,2 @@
+#eval let c := cached.mk 2 in c
+#eval let c := cached.mk 2 in c.update 3 c