Library Memo
Require Import Vbase MyInt31.
Require Parray.
Require Import Aref.
Require Import Program.
Section Memo.
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.
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.
Proof.
rewrite !(Parray.gu _ z), Parray.length_set, Parray.gs; desf; vauto.
auto using Parray.length_pos.
Qed.
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)
else
let b := f a in
(Parray.set c h (Some (a, b)), b)
end.
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.