@[reducible, inline]

abbrev Cedar.TPE.EntityLoader : Type

Loads everything requested by the set of entity ids, returning Option.none for missing entities. Loading more entities than requested is okay. See EntityLoader.WellBehaved for a formal definition.

Equations

• Cedar.TPE.EntityLoader = (Cedar.Data.Set Cedar.Spec.EntityUID → Cedar.Data.Map Cedar.Spec.EntityUID Cedar.TPE.MaybeEntityData)

def Cedar.TPE.batchedEvalLoop (residual : Spec.Residual) (req : Spec.Request) (loader : EntityLoader) (store : PartialEntities) : Nat → Spec.Residual

The batched evaluation loop

1. Asks for any new entities referenced by the residual
2. Partially evaluates now that new entities are loaded
3. Exits if a value has been found or it hits the maximum iteration limit

Equations

• One or more equations did not get rendered due to their size.
• Cedar.TPE.batchedEvalLoop residual req loader store 0 = residual

def Cedar.TPE.batchedEvaluate (x : Validation.TypedExpr) (req : Spec.Request) (loader : EntityLoader) (iters : Nat) : Spec.Residual

Evaluate a cedar expression using an EntityLoader instead of a full Entities store. Performs a maximum of iter number of calls to loader, but may perform fewer when a value is found.

Equations

• Cedar.TPE.batchedEvaluate x req loader iters = Cedar.TPE.batchedEvalLoop (Cedar.TPE.evaluate x.toResidual req.asPartialRequest Cedar.Data.Map.empty) req loader Cedar.Data.Map.empty iters

def Cedar.TPE.entityLoaderFor (es : Spec.Entities) (uids : Data.Set Spec.EntityUID) : Data.Map Spec.EntityUID (Option Spec.EntityData)

Create an entity loader for a given entity store. This is used for testing.

Equations

• One or more equations did not get rendered due to their size.