This file defines the semantics of Cedar operators and expressions.

def Cedar.Spec.intOrErr : Option Int64 → Result Value

Equations

• Cedar.Spec.intOrErr (some i) = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i))
• Cedar.Spec.intOrErr none = Except.error Cedar.Spec.Error.arithBoundsError

def Cedar.Spec.apply₁ : UnaryOp → Value → Result Value

Equations

• Cedar.Spec.apply₁ Cedar.Spec.UnaryOp.not (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b)) = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool !b))
• Cedar.Spec.apply₁ Cedar.Spec.UnaryOp.neg (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i)) = Cedar.Spec.intOrErr i.neg?
• Cedar.Spec.apply₁ Cedar.Spec.UnaryOp.isEmpty (Cedar.Spec.Value.set s) = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool s.isEmpty))
• Cedar.Spec.apply₁ (Cedar.Spec.UnaryOp.like p) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)) = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (Cedar.Spec.wildcardMatch s p)))
• Cedar.Spec.apply₁ (Cedar.Spec.UnaryOp.is ety) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)) = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (ety == uid.ty)))
• Cedar.Spec.apply₁ x✝¹ x✝ = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.inₑ (uid₁ uid₂ : EntityUID) (es : Entities) : Bool

Equations

• Cedar.Spec.inₑ uid₁ uid₂ es = (uid₁ == uid₂ || (es.ancestorsOrEmpty uid₁).contains uid₂)

def Cedar.Spec.inₛ (uid : EntityUID) (vs : Data.Set Value) (es : Entities) : Result Value

Equations

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

def Cedar.Spec.hasTag (uid : EntityUID) (tag : String) (es : Entities) : Result Value

Equations

• Cedar.Spec.hasTag uid tag es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool ((es.tagsOrEmpty uid).contains tag)))

def Cedar.Spec.getTag (uid : EntityUID) (tag : String) (es : Entities) : Result Value

Equations

• Cedar.Spec.getTag uid tag es = do let __do_lift ← es.tags uid __do_lift.findOrErr tag Cedar.Spec.Error.tagDoesNotExist

def Cedar.Spec.apply₂ (op₂ : BinaryOp) (v₁ v₂ : Value) (es : Entities) : Result Value

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.eq v₁ v₂ es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (v₁ == v₂)))
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.add (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i)) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int j)) es = Cedar.Spec.intOrErr (i.add? j)
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.sub (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i)) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int j)) es = Cedar.Spec.intOrErr (i.sub? j)
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.mul (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i)) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int j)) es = Cedar.Spec.intOrErr (i.mul? j)
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.contains (Cedar.Spec.Value.set vs₁) v₂ es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (vs₁.contains v₂)))
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.containsAll (Cedar.Spec.Value.set vs₁) (Cedar.Spec.Value.set vs₂) es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (vs₂.subset vs₁)))
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.containsAny (Cedar.Spec.Value.set vs₁) (Cedar.Spec.Value.set vs₂) es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (vs₁.intersects vs₂)))
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.mem (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid₁)) (Cedar.Spec.Value.set vs) es = Cedar.Spec.inₛ uid₁ vs es
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.hasTag (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid₁)) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string tag)) es = Cedar.Spec.hasTag uid₁ tag es
• Cedar.Spec.apply₂ Cedar.Spec.BinaryOp.getTag (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid₁)) (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string tag)) es = Cedar.Spec.getTag uid₁ tag es
• Cedar.Spec.apply₂ op₂ v₁ v₂ es = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.attrsOf (v : Value) (lookup : EntityUID → Result (Data.Map Attr Value)) : Result (Data.Map Attr Value)

Equations

• Cedar.Spec.attrsOf (Cedar.Spec.Value.record r) lookup = Except.ok r
• Cedar.Spec.attrsOf (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)) lookup = lookup uid
• Cedar.Spec.attrsOf v lookup = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.hasAttr (v : Value) (a : Attr) (es : Entities) : Result Value

Equations

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

def Cedar.Spec.getAttr (v : Value) (a : Attr) (es : Entities) : Result Value

Equations

• Cedar.Spec.getAttr v a es = do let r ← Cedar.Spec.attrsOf v es.attrs r.findOrErr a Cedar.Spec.Error.attrDoesNotExist

def Cedar.Spec.bindAttr {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (a : Attr) (res : m α) : m (Attr × α)

Equations

• Cedar.Spec.bindAttr a res = do let v ← res pure (a, v)

@[irreducible]

def Cedar.Spec.evaluate (x : Expr) (req : Request) (es : Entities) : Result Value

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.evaluate (Cedar.Spec.Expr.lit l) req es = Except.ok (Cedar.Spec.Value.prim l)
• Cedar.Spec.evaluate (Cedar.Spec.Expr.var Cedar.Spec.Var.principal) req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.principal))
• Cedar.Spec.evaluate (Cedar.Spec.Expr.var Cedar.Spec.Var.action) req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.action))
• Cedar.Spec.evaluate (Cedar.Spec.Expr.var Cedar.Spec.Var.resource) req es = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID req.resource))
• Cedar.Spec.evaluate (Cedar.Spec.Expr.var Cedar.Spec.Var.context) req es = Except.ok (Cedar.Spec.Value.record req.context)
• Cedar.Spec.evaluate (x₁.ite x₂ x₃) req es = do let b ← Cedar.Spec.Result.as Bool (Cedar.Spec.evaluate x₁ req es) if b = true then Cedar.Spec.evaluate x₂ req es else Cedar.Spec.evaluate x₃ req es
• Cedar.Spec.evaluate (Cedar.Spec.Expr.unaryApp op₁ x₁) req es = do let v₁ ← Cedar.Spec.evaluate x₁ req es Cedar.Spec.apply₁ op₁ v₁
• Cedar.Spec.evaluate (Cedar.Spec.Expr.binaryApp op₂ x₁ x₂) req es = do let v₁ ← Cedar.Spec.evaluate x₁ req es let v₂ ← Cedar.Spec.evaluate x₂ req es Cedar.Spec.apply₂ op₂ v₁ v₂ es
• Cedar.Spec.evaluate (x₁.hasAttr a) req es = do let v₁ ← Cedar.Spec.evaluate x₁ req es Cedar.Spec.hasAttr v₁ a es
• Cedar.Spec.evaluate (x₁.getAttr a) req es = do let v₁ ← Cedar.Spec.evaluate x₁ req es Cedar.Spec.getAttr v₁ a es