Documentation

VCVio.OracleComp.OracleContext

Bundled Oracle Specs and Implementations #

This file defines a type OracleContext ι m that provides an ambient set of oracles, along with an implementation of those oracles in the monad m.

source
structure OracleContext (ι : Type u) (m : Type v → Type w) :
Type ((max u v w) + 1)

An OracleContext ι m bundles a specification spec of oracles with input set ι and an implementation of the oracles in terms of the monad m. Structures can extend this to get

Instances For
    source
    @[reducible]
    def OracleSpec.defaultContext {ι : Type u} (spec : OracleSpec ι) :
    OracleContext spec.Domain (OracleComp spec)

    Convert an OracleSpec into an OracleContext with OracleComp as the implementation monad, using the identity implementation for queries.

    Equations
      Instances For
        source
        instance OracleContext.instInhabitedOfPure {ι : Type u_1} {m : Type u → Type v} [Pure m] :
        Inhabited (OracleContext ι m)
        Equations
          source
          @[reducible]
          def OracleContext.ofImpl {ι : Type u_1} {spec : OracleSpec ι} {m : Type u → Type v} (impl : QueryImpl spec m) :
          OracleContext ι m

          Convert a QueryImpl into an OracleContext by bundling the OracleSpec corresponding to the particular implementation.

          Equations
            Instances For
              source
              @[reducible]
              def OracleContext.add {ι : Type u_1} {ι' : Type u_2} {m : Type u → Type v} (O : OracleContext ι m) (O' : OracleContext ι' m) :
              OracleContext (ι ⊕ ι') m

              Combine two oracle contexts with the same target monad, giving access to both ambient oracles and implementing queries to each independently.

              Equations
                Instances For
                  source
                  instance OracleContext.instHAddSum {ι : Type u_1} {ι' : Type u_2} {m : Type u → Type v} :
                  HAdd (OracleContext ι m) (OracleContext ι' m) (OracleContext (ι ⊕ ι') m)
                  Equations
                    source
                    @[simp]
                    theorem OracleContext.add_def {ι : Type u_1} {ι' : Type u_2} {m : Type u → Type v} (O : OracleContext ι m) (O' : OracleContext ι' m) :
                    O + O' = O.add O'
                    source
                    theorem OracleContext.spec_add {ι : Type u_1} {ι' : Type u_2} {m : Type u → Type v} (O : OracleContext ι m) (O' : OracleContext ι' m) :
                    (O + O').spec = O.spec + O'.spec
                    source
                    theorem OracleContext.impl_add {ι : Type u_1} {ι' : Type u_2} {m : Type u → Type v} (O : OracleContext ι m) (O' : OracleContext ι' m) :
                    (O + O').impl = O.impl + O'.impl