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 ι}
[spec.DecidableEq]
{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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
QueryImpl.withCaching_apply
{ι : Type u}
[DecidableEq ι]
{spec : OracleSpec ι}
[spec.DecidableEq]
{m : Type u → Type v}
[Monad m]
{α : Type u}
(so : QueryImpl spec m)
(q : spec.OracleQuery α)
:
so.withCaching.impl q = match α, q with
| .(spec.range i), OracleSpec.query i t => do
let __do_lift ← get
match __do_lift i t with
| some u => pure u
| none => do
let u ← liftM (so.impl (OracleSpec.query i t))
modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery i t u)
@[reducible, inline]
def
cachingOracle
{ι : Type u}
[DecidableEq ι]
{spec : OracleSpec ι}
[spec.DecidableEq]
:
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 ι}
[spec.DecidableEq]
{α : Type u}
(q : spec.OracleQuery α)
:
cachingOracle.impl q = match α, q with
| .(spec.range i), OracleSpec.query i t => do
let __do_lift ← get
match __do_lift i t with
| some u => pure u
| none => do
let u ← liftM (OracleSpec.query i t)
modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery i t u)
@[reducible, inline]
def
randomOracle
{ι : Type}
[DecidableEq ι]
{spec : OracleSpec ι}
[spec.DecidableEq]
[(i : ι) → OracleComp.SelectableType (spec.range i)]
:
QueryImpl spec (StateT spec.QueryCache (OracleComp unifSpec))
Random Oracle implemented as a uniform selection oracle with caching
Equations
Instances For
theorem
randOracle.apply_eq
{ι : Type}
[DecidableEq ι]
{spec : OracleSpec ι}
[spec.DecidableEq]
[(i : ι) → OracleComp.SelectableType (spec.range i)]
{α : Type}
(q : spec.OracleQuery α)
:
randomOracle.impl q = match α, q with
| .(spec.range i), OracleSpec.query i t => do
let __do_lift ← get
match __do_lift i t with
| some u => pure u
| none => do
let u ← liftM ($ᵗspec.range i)
modifyGet fun (cache : spec.QueryCache) => (u, cache.cacheQuery i t u)