Caching Queries Made by a Computation #
This file defines a modifier QueryImpl.withCaching that modifies a query implementation to
cache results to return to the same query in the future.
We also define a plain caching oracle and random oracles as special cases of this.
def
QueryImpl.withCaching
{ι : Type u}
[DecidableEq ι]
{spec : OracleSpec ι}
{m : Type u → Type v}
[Monad m]
(so : QueryImpl spec m)
:
QueryImpl spec (StateT spec.QueryCache m)
Modify a query implementation to cache previous call and return that output in the future.
Equations
Instances For
@[simp]
theorem
QueryImpl.withCaching_apply
{ι : Type u}
[DecidableEq ι]
{spec : OracleSpec ι}
{m : Type u → Type v}
[Monad m]
(so : QueryImpl spec m)
(t : spec.Domain)
:
so.withCaching t = do
let __do_lift ← get
match __do_lift t with
| some u => pure u
| none => do
let u ← liftM (so t)
modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery t u)
@[reducible, inline]
def
randomOracle
{ι : Type}
[DecidableEq ι]
{spec : OracleSpec ι}
[(t : spec.Domain) → SampleableType (spec.Range t)]
:
QueryImpl spec (StateT spec.QueryCache ProbComp)
Equations
Instances For
@[reducible, inline]
def
cachingOracle
{ι : Type u}
[DecidableEq ι]
{spec : OracleSpec ι}
:
QueryImpl spec (StateT spec.QueryCache (OracleComp spec))
Oracle for caching queries to the oracles in spec, querying fresh values if needed.
Equations
Instances For
theorem
cachingOracle.apply_eq
{ι : Type u}
[DecidableEq ι]
{spec : OracleSpec ι}
(t : spec.Domain)
:
cachingOracle t = do
let __do_lift ← get
match __do_lift t with
| some u => pure u
| none => do
let u ← liftM (OracleQuery.query t)
modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery t u)