Skip to content

Commit

Permalink
update comments to point to #395
Browse files Browse the repository at this point in the history
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
  • Loading branch information
cdisselkoen committed Jul 16, 2024
1 parent 777c8fe commit ed32208
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions cedar-lean/Cedar/Partial/Evaluator.lean
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ def evaluateHasAttr (pv : Partial.Value) (a : Attr) (es : Partial.Entities) : Re
| .value v₁ => do
let val ← Partial.hasAttr v₁ a es
.ok (.value val)
| .residual r => .ok (.residual (.hasAttr (.residual r) a)) -- TODO more precise: even though pv is a residual we may know concretely whether it contains the particular attr we care about
| .residual r => .ok (.residual (.hasAttr (.residual r) a)) -- could be more precise; see cedar-spec#395

/-- Analogous to Spec.getAttr but for partial entities -/
def getAttr (v : Spec.Value) (a : Attr) (es : Partial.Entities) : Result Partial.Value := do
Expand All @@ -112,7 +112,7 @@ def getAttr (v : Spec.Value) (a : Attr) (es : Partial.Entities) : Result Partial
def evaluateGetAttr (pv : Partial.Value) (a : Attr) (es : Partial.Entities) : Result Partial.Value := do
match pv with
| .value v₁ => Partial.getAttr v₁ a es
| .residual r => .ok (.residual (.getAttr (.residual r) a)) -- TODO more precise: pv will be a .residual if it contains any unknowns, but we might have a concrete value for the particular attr we care about
| .residual r => .ok (.residual (.getAttr (.residual r) a)) -- could be more precise; see cedar-spec#395

/-- Analogous to Spec.bindAttr but for partial values -/
def bindAttr (a : Attr) (res : Result Partial.Value) : Result (Attr × Partial.Value) := do
Expand Down

0 comments on commit ed32208

Please sign in to comment.