This file contains well-typedness definitions of TypedExpr
- not {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : UnaryResidualWellTyped UnaryOp.not x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
- neg {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) : UnaryResidualWellTyped UnaryOp.neg x₁ Validation.CedarType.int
- isEmpty {x₁ : Residual} {eltTy : Validation.CedarType} (h₁ : x₁.typeOf = eltTy.set) : UnaryResidualWellTyped UnaryOp.isEmpty x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
- like {x₁ : Residual} {p : Pattern} (h₁ : x₁.typeOf = Validation.CedarType.string) : UnaryResidualWellTyped (UnaryOp.like p) x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
- is {x₁ : Residual} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₂) : UnaryResidualWellTyped (UnaryOp.is ety₁) x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
Instances For
inductive
Cedar.Spec.BinaryResidualWellTyped
(env : Validation.TypeEnv)
:
BinaryOp → Residual → Residual → Validation.CedarType → Prop
- eq_val {env : Validation.TypeEnv} {p₁ p₂ : Value} {ty₁ ty₂ : Validation.CedarType} : BinaryResidualWellTyped env BinaryOp.eq (Residual.val p₁ ty₁) (Residual.val p₂ ty₂) (Validation.CedarType.bool Validation.BoolType.anyBool)
- eq_entity {env : Validation.TypeEnv} {ety₁ ety₂ : EntityType} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = Validation.CedarType.entity ety₂) : BinaryResidualWellTyped env BinaryOp.eq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- eq {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = x₂.typeOf) : BinaryResidualWellTyped env BinaryOp.eq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- memₑ {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = Validation.CedarType.entity ety₂) : BinaryResidualWellTyped env BinaryOp.mem x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- memₛ {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = (Validation.CedarType.entity ety₂).set) : BinaryResidualWellTyped env BinaryOp.mem x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- less_int {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- less_datetime {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : BinaryResidualWellTyped env BinaryOp.less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- less_duration {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : BinaryResidualWellTyped env BinaryOp.less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- lessEq_int {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- lessEq_datetime {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : BinaryResidualWellTyped env BinaryOp.lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- lessEq_duration {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : BinaryResidualWellTyped env BinaryOp.lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- add {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.add x₁ x₂ Validation.CedarType.int
- sub {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.sub x₁ x₂ Validation.CedarType.int
- mul {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : BinaryResidualWellTyped env BinaryOp.mul x₁ x₂ Validation.CedarType.int
- contains {env : Validation.TypeEnv} {x₁ x₂ : Residual} (h₁ : x₁.typeOf = x₂.typeOf.set) : BinaryResidualWellTyped env BinaryOp.contains x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- containsAll {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ty : Validation.CedarType} (h₁ : x₁.typeOf = ty.set) (h₂ : x₂.typeOf = ty.set) : BinaryResidualWellTyped env BinaryOp.containsAll x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- containsAny {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ty : Validation.CedarType} (h₁ : x₁.typeOf = ty.set) (h₂ : x₂.typeOf = ty.set) : BinaryResidualWellTyped env BinaryOp.containsAny x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- hasTag {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety) (h₂ : x₂.typeOf = Validation.CedarType.string) : BinaryResidualWellTyped env BinaryOp.hasTag x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
- getTag {env : Validation.TypeEnv} {x₁ x₂ : Residual} {ety : EntityType} {ty : Validation.CedarType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety) (h₂ : x₂.typeOf = Validation.CedarType.string) (h₃ : env.ets.tags? ety = some (some ty)) : BinaryResidualWellTyped env BinaryOp.getTag x₁ x₂ ty.liftBoolTypes
Instances For
- decimal {s₁ : String} {d₁ : Ext.Decimal} (h₁ : some d₁ = Ext.Decimal.decimal s₁) : ExtResidualWellTyped ExtFun.decimal [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.decimal)
- lessThan {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.lessThan [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
- lessThanOrEqual {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.lessThanOrEqual [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
- greaterThan {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.greaterThan [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
- greaterThanOrEqual {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtResidualWellTyped ExtFun.greaterThanOrEqual [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
- ip {s₁ : String} {ip₁ : IPAddr} (h₁ : some ip₁ = Ext.IPAddr.ip s₁) : ExtResidualWellTyped ExtFun.ip [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.ipAddr)
- isIpv4 {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isIpv4 [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
- isIpv6 {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isIpv6 [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
- isLoopback {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isLoopback [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
- isMulticast {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isMulticast [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
- isInRange {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtResidualWellTyped ExtFun.isInRange [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
- datetime {s₁ : String} {d₁ : Ext.Datetime} (h₁ : some d₁ = Ext.Datetime.parse s₁) : ExtResidualWellTyped ExtFun.datetime [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.datetime)
- duration {s₁ : String} {d₁ : Duration} (h₁ : some d₁ = Ext.Datetime.Duration.parse s₁) : ExtResidualWellTyped ExtFun.duration [Residual.val (Value.prim (Prim.string s₁)) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.duration)
- offset {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.offset [x₁, x₂] (Validation.CedarType.ext Validation.ExtType.datetime)
- durationSince {x₁ x₂ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtResidualWellTyped ExtFun.durationSince [x₁, x₂] (Validation.CedarType.ext Validation.ExtType.duration)
- toDate {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtResidualWellTyped ExtFun.toDate [x₁] (Validation.CedarType.ext Validation.ExtType.datetime)
- toTime {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtResidualWellTyped ExtFun.toTime [x₁] (Validation.CedarType.ext Validation.ExtType.duration)
- toMilliseconds {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toMilliseconds [x₁] Validation.CedarType.int
- toSeconds {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toSeconds [x₁] Validation.CedarType.int
- toMinutes {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toMinutes [x₁] Validation.CedarType.int
- toHours {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toHours [x₁] Validation.CedarType.int
- toDays {x₁ : Residual} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtResidualWellTyped ExtFun.toDays [x₁] Validation.CedarType.int
Instances For
Well-typedness definition for Residual expressions
- val {env : Validation.TypeEnv} {v : Spec.Value} {ty : Validation.CedarType} (h₁ : InstanceOfType env v ty) : WellTyped env (Spec.Residual.val v ty)
- var {env : Validation.TypeEnv} {v : Spec.Var} {ty : Validation.CedarType} (h₁ : Spec.Var.WellTyped env v ty) : WellTyped env (Spec.Residual.var v ty)
- ite {env : Validation.TypeEnv} {x₁ x₂ x₃ : Spec.Residual} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : WellTyped env x₃) (h₄ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₅ : x₂.typeOf = x₃.typeOf) : WellTyped env (x₁.ite x₂ x₃ x₂.typeOf)
- and {env : Validation.TypeEnv} {x₁ x₂ : Spec.Residual} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₄ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : WellTyped env (x₁.and x₂ (Validation.CedarType.bool Validation.BoolType.anyBool))
- or {env : Validation.TypeEnv} {x₁ x₂ : Spec.Residual} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₄ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : WellTyped env (x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool))
- unaryApp {env : Validation.TypeEnv} {op₁ : Spec.UnaryOp} {x₁ : Spec.Residual} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : Spec.UnaryResidualWellTyped op₁ x₁ ty) : WellTyped env (Spec.Residual.unaryApp op₁ x₁ ty)
- binaryApp {env : Validation.TypeEnv} {op₂ : Spec.BinaryOp} {x₁ x₂ : Spec.Residual} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : Spec.BinaryResidualWellTyped env op₂ x₁ x₂ ty) : WellTyped env (Spec.Residual.binaryApp op₂ x₁ x₂ ty)
- hasAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {x₁ : Spec.Residual} {attr : Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) : WellTyped env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool))
- hasAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Spec.Residual} {attr : Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) : WellTyped env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool))
- getAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {rty : Validation.RecordType} {x₁ : Spec.Residual} {attr : Spec.Attr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) (h₃ : Option.map Validation.RecordType.liftBoolTypes (env.ets.attrs? ety) = some rty) (h₄ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty) : WellTyped env (x₁.getAttr attr ty)
- getAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Spec.Residual} {attr : Spec.Attr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) (h₃ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty) : WellTyped env (x₁.getAttr attr ty)
- set {env : Validation.TypeEnv} {ls : List Spec.Residual} {ty : Validation.CedarType} (h₁ : ∀ (x : Spec.Residual), x ∈ ls → WellTyped env x) (h₂ : ∀ (x : Spec.Residual), x ∈ ls → x.typeOf = ty) (h₃ : (ls != []) = true) : WellTyped env (Spec.Residual.set ls ty.set)
- record {env : Validation.TypeEnv} {rty : Validation.RecordType} {m : List (Spec.Attr × Spec.Residual)} (h₁ : ∀ (k : Spec.Attr) (v : Spec.Residual), (k, v) ∈ m → WellTyped env v) (h₂ : rty = Data.Map.make (List.map (fun (x : Spec.Attr × Spec.Residual) => match x with | (a, r) => (a, Validation.Qualified.required r.typeOf)) m)) : WellTyped env (Spec.Residual.record m (Validation.CedarType.record rty))
- call {env : Validation.TypeEnv} {xfn : Spec.ExtFun} {args : List Spec.Residual} {ty : Validation.CedarType} (h₁ : ∀ (x : Spec.Residual), x ∈ args → WellTyped env x) (h₂ : Spec.ExtResidualWellTyped xfn args ty) : WellTyped env (Spec.Residual.call xfn args ty)
- error {env : Validation.TypeEnv} {ty : Validation.CedarType} : WellTyped env (Spec.Residual.error ty)
Instances For
theorem
Cedar.Thm.well_typed_entity
{env : Validation.TypeEnv}
{e : Spec.EntityUID}
{ety : Spec.EntityType}
:
InstanceOfEntityType e ety env →
Residual.WellTyped env (Spec.Residual.val (Spec.Value.prim (Spec.Prim.entityUID e)) (Validation.CedarType.entity ety))