Library Memo

Require Import Vbase MyInt31.
Require Parray.
Require Import Aref.
Require Import Program.

Section Memo.

We assume a suitable argument type A with a decidable equality and a hash function mapping to 31-bit integers.

Variable A : Type.
Variable eqA : forall x y : A, { x = y } + { x <> y }.
Variable hash : A -> int31.

We also assume the result type is B and the function we are memorising is f.

Variable B : Type.
Variable f : A -> B.

The internal data structure used by the memorisation optimisation is an array of pair options, such that the presence of a (a,b) pair in the array ensures that b = f a.

Definition cache :=
  { c : Parray.t (option (A * B)) |
      forall a b, Parray.get c (hash a) = Some (a, b) -> b = f a }.

A few helper lemmas

Lemma gsD T (a: Parray.t T) x y z w:
  Parray.get (Parray.set a x y) z = w ->
  Parray.get a z = w \/ y = w.
  rewrite !( _ z), Parray.length_set,; desf; vauto.
  auto using Parray.length_pos.

Lemma memorize_helper :
  forall (x : A) (c : cache) (x0 : A) (v : B)
    (H : Parray.get (Parray.set (`c) (hash x) (Some (x, f x))) (hash x0) = Some (x0, v)),
    v = f x0.
Proof. destruct c; ins; apply gsD in H; desf; eauto. Qed.

The computation performed by memo: search the array; if there is a corresponding entry in the cache, return it; otherwise call f and add the result to the cache.

Program Definition memo_upd (c : cache) a : (cache * B) :=
  let h := hash a in
  match Parray.get c (hash a) with
    | None =>
      let b := f a in
      (Parray.set c h (Some (a, b)), b)
    | Some (a', b) =>
      if eqA a a' then
        (c, b)
          let b := f a in
          (Parray.set c h (Some (a, b)), b)
Solve Obligations using eauto using memorize_helper.

The main entry point (memo) creates an adjustable reference containing an initially empty cache and returns an adjusting read performing the previous memo_upd function.

Program Definition memo :=
  let r := aref_val (fun _ : cache => f) (Parray.create 100 None) in
  aref_getu memo_upd _ _ r.
Next Obligation. by rewrite Parray.gcreate in *. Qed.
Next Obligation. unfold memo_upd; des_eqrefl; desf; auto using (proj2_sig x). Qed.

Finally, we prove correctness of the memoisation operation.

Lemma memo_eq : memo = f.
Proof. by unfold memo; rewrite aref_getuE, aref_get_val. Qed.

End Memo.