Documentation

Cedar.Validation.TypedExpr

This file defines a type annotated version of the Cedar AST

inductive Cedar.Validation.TypedExpr :

A type annotated Cedar AST. This should have exactly the same variants as the unannotated Expr data type, but each variant carries an additional ty that stores the type of the expression.

lit (p : Spec.Prim) (ty : CedarType) : TypedExpr
var (v : Spec.Var) (ty : CedarType) : TypedExpr
ite (cond thenExpr elseExpr : TypedExpr) (ty : CedarType) : TypedExpr
and (a b : TypedExpr) (ty : CedarType) : TypedExpr
or (a b : TypedExpr) (ty : CedarType) : TypedExpr
unaryApp (op : Spec.UnaryOp) (expr : TypedExpr) (ty : CedarType) : TypedExpr
binaryApp (op : Spec.BinaryOp) (a b : TypedExpr) (ty : CedarType) : TypedExpr
getAttr (expr : TypedExpr) (attr : Spec.Attr) (ty : CedarType) : TypedExpr
hasAttr (expr : TypedExpr) (attr : Spec.Attr) (ty : CedarType) : TypedExpr
extHasAttr (expr : TypedExpr) (attr : Spec.Attr) (attrs : List Spec.Attr) (ty : CedarType) : TypedExpr
set (ls : List TypedExpr) (ty : CedarType) : TypedExpr
record (map : List (Spec.Attr × TypedExpr)) (ty : CedarType) : TypedExpr
call (xfn : Spec.ExtFun) (args : List TypedExpr) (ty : CedarType) : TypedExpr

Instances For

@[instance_reducible]

instance Cedar.Validation.instReprTypedExpr :

Equations

Cedar.Validation.instReprTypedExpr = { reprPrec := Cedar.Validation.instReprTypedExpr.repr }

partial def Cedar.Validation.instReprTypedExpr.repr :

TypedExpr → Nat → Std.Format

@[instance_reducible]

instance Cedar.Validation.instInhabitedTypedExpr :

Inhabited TypedExpr

Equations

Cedar.Validation.instInhabitedTypedExpr = { default := Cedar.Validation.instInhabitedTypedExpr.default }

def Cedar.Validation.decTypedExpr (x y : TypedExpr) :

Decidable (x = y)

Equations

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

Instances For

@[instance_reducible]

instance Cedar.Validation.instDecidableEqTypedExpr :

DecidableEq TypedExpr

Equations

Cedar.Validation.instDecidableEqTypedExpr = Cedar.Validation.decTypedExpr

def Cedar.Validation.TypedExpr.typeOf :

TypedExpr → CedarType

Equations

(Cedar.Validation.TypedExpr.lit a a_1).typeOf = a_1
(Cedar.Validation.TypedExpr.var a a_1).typeOf = a_1
(a.ite a_1 a_2 a_3).typeOf = a_3
(a.and a_1 a_2).typeOf = a_2
(a.or a_1 a_2).typeOf = a_2
(Cedar.Validation.TypedExpr.unaryApp a a_1 a_2).typeOf = a_2
(Cedar.Validation.TypedExpr.binaryApp a a_1 a_2 a_3).typeOf = a_3
(a.getAttr a_1 a_2).typeOf = a_2
(a.hasAttr a_1 a_2).typeOf = a_2
(a.extHasAttr a_1 a_2 a_3).typeOf = a_3
(Cedar.Validation.TypedExpr.set a a_1).typeOf = a_1
(Cedar.Validation.TypedExpr.record a a_1).typeOf = a_1
(Cedar.Validation.TypedExpr.call a a_1 a_2).typeOf = a_2

Instances For

@[irreducible]

def Cedar.Validation.TypedExpr.toExpr :

TypedExpr → Spec.Expr

Equations

One or more equations did not get rendered due to their size.
(Cedar.Validation.TypedExpr.lit a a_1).toExpr = Cedar.Spec.Expr.lit a
(Cedar.Validation.TypedExpr.var a a_1).toExpr = Cedar.Spec.Expr.var a
(a.ite a_1 a_2 a_3).toExpr = a.toExpr.ite a_1.toExpr a_2.toExpr
(a.and a_1 a_2).toExpr = a.toExpr.and a_1.toExpr
(a.or a_1 a_2).toExpr = a.toExpr.or a_1.toExpr
(Cedar.Validation.TypedExpr.unaryApp a a_1 a_2).toExpr = Cedar.Spec.Expr.unaryApp a a_1.toExpr
(Cedar.Validation.TypedExpr.binaryApp a a_1 a_2 a_3).toExpr = Cedar.Spec.Expr.binaryApp a a_1.toExpr a_2.toExpr
(a.getAttr a_1 a_2).toExpr = a.toExpr.getAttr a_1
(a.hasAttr a_1 a_2).toExpr = a.toExpr.hasAttr a_1
(a.extHasAttr a_1 a_2 a_3).toExpr = a.toExpr.extHasAttr a_1 a_2
(Cedar.Validation.TypedExpr.set a a_1).toExpr = Cedar.Spec.Expr.set (a.map₁ fun (x : { x : Cedar.Validation.TypedExpr // x ∈ a }) => match x with | ⟨e, property⟩ => e.toExpr)

Instances For

@[irreducible]

def Cedar.Validation.TypedExpr.liftBoolTypes :

TypedExpr → TypedExpr

Equations

One or more equations did not get rendered due to their size.
(Cedar.Validation.TypedExpr.lit a a_1).liftBoolTypes = Cedar.Validation.TypedExpr.lit a a_1.liftBoolTypes
(Cedar.Validation.TypedExpr.var a a_1).liftBoolTypes = Cedar.Validation.TypedExpr.var a a_1.liftBoolTypes
(a.ite a_1 a_2 a_3).liftBoolTypes = a.liftBoolTypes.ite a_1.liftBoolTypes a_2.liftBoolTypes a_3.liftBoolTypes
(a.and a_1 a_2).liftBoolTypes = a.liftBoolTypes.and a_1.liftBoolTypes a_2.liftBoolTypes
(a.or a_1 a_2).liftBoolTypes = a.liftBoolTypes.or a_1.liftBoolTypes a_2.liftBoolTypes
(Cedar.Validation.TypedExpr.unaryApp a a_1 a_2).liftBoolTypes = Cedar.Validation.TypedExpr.unaryApp a a_1.liftBoolTypes a_2.liftBoolTypes
(Cedar.Validation.TypedExpr.binaryApp a a_1 a_2 a_3).liftBoolTypes = Cedar.Validation.TypedExpr.binaryApp a a_1.liftBoolTypes a_2.liftBoolTypes a_3.liftBoolTypes
(a.getAttr a_1 a_2).liftBoolTypes = a.liftBoolTypes.getAttr a_1 a_2.liftBoolTypes
(a.hasAttr a_1 a_2).liftBoolTypes = a.liftBoolTypes.hasAttr a_1 a_2.liftBoolTypes
(a.extHasAttr a_1 a_2 a_3).liftBoolTypes = a.liftBoolTypes.extHasAttr a_1 a_2 a_3.liftBoolTypes

Instances For