This file defines the Cedar Term language, a strongly and simply typed IR to which we compile Cedar expressions. The Term language has a straightforward translation to SMTLib. It is designed to reduce the semantic gap between Cedar and SMTLib, and to faciliate proofs of soundness and completeness of the Cedar symbolic compiler.

Terms should not be created directly using Term constructors. Instead, they should be created using the factory functions defined in Factory.lean. The factory functions check the types of their arguments, perform optimizations, and ensure that applying them to well-formed terms results in well-formed terms.

See TermType.lean and Op.lean for definition of Term types and operators.

structure Cedar.SymCC.TermVar : Type

• id : String
• ty : TermType

inductive Cedar.SymCC.TermPrim : Type

• bool : Bool → TermPrim
• bitvec {n : Nat} : BitVec n → TermPrim
• string : String → TermPrim
• entity : Spec.EntityUID → TermPrim
• ext : Spec.Ext → TermPrim

inductive Cedar.SymCC.Term : Type

• prim : TermPrim → Term
• var : TermVar → Term
• none : TermType → Term
• some : Term → Term
• set (elts : Data.Set Term) (eltsTy : TermType) : Term
• record : Data.Map Spec.Attr Term → Term
• app : Op → (args : List Term) → (retTy : TermType) → Term

@[reducible, inline]

abbrev Cedar.SymCC.Term.bool (b : Bool) : Term

Equations

• Cedar.SymCC.Term.bool b = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool b)

@[reducible, inline]

abbrev Cedar.SymCC.Term.bitvec {n : Nat} (bv : BitVec n) : Term

Equations

• Cedar.SymCC.Term.bitvec bv = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec bv)

@[reducible, inline]

abbrev Cedar.SymCC.Term.string (s : String) : Term

Equations

• Cedar.SymCC.Term.string s = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.string s)

@[reducible, inline]

abbrev Cedar.SymCC.Term.entity (uid : Spec.EntityUID) : Term

Equations

• Cedar.SymCC.Term.entity uid = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.entity uid)

@[reducible, inline]

abbrev Cedar.SymCC.Term.ext (xv : Spec.Ext) : Term

Equations

• Cedar.SymCC.Term.ext xv = Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.ext xv)

@[irreducible]

def Cedar.SymCC.Term.typeOf : Term → TermType

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.SymCC.Term.prim l).typeOf = Cedar.SymCC.TermPrim.typeOf✝ l
• (Cedar.SymCC.Term.var v).typeOf = v.ty
• (Cedar.SymCC.Term.none ty).typeOf = ty.option
• t.some.typeOf = t.typeOf.option
• (Cedar.SymCC.Term.app a args ty).typeOf = ty
• (Cedar.SymCC.Term.set elts ty).typeOf = ty.set

@[irreducible]

def Cedar.SymCC.Term.isLiteral : Term → Bool

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.SymCC.Term.prim a).isLiteral = true
• (Cedar.SymCC.Term.none a).isLiteral = true
• t.some.isLiteral = t.isLiteral
• (Cedar.SymCC.Term.set ts eltsTy).isLiteral = ts.all₁ fun (x : { a : Cedar.SymCC.Term // a ∈ ts }) => match x with | ⟨t, property⟩ => t.isLiteral
• x✝.isLiteral = false

instance Cedar.SymCC.instCoeBoolTerm : Coe Bool Term

Equations

• Cedar.SymCC.instCoeBoolTerm = { coe := fun (b : Bool) => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool b) }

instance Cedar.SymCC.instCoeInt64Term : Coe Int64 Term

Equations

• Cedar.SymCC.instCoeInt64Term = { coe := fun (i : Int64) => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec i.toBitVec) }

instance Cedar.SymCC.instCoeOutBitVecTerm {n : Nat} : CoeOut (BitVec n) Term

Equations

• Cedar.SymCC.instCoeOutBitVecTerm = { coe := fun (b : BitVec n) => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec b) }

instance Cedar.SymCC.instCoeStringTerm : Coe String Term

Equations

• Cedar.SymCC.instCoeStringTerm = { coe := fun (s : String) => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.string s) }

instance Cedar.SymCC.instCoeEntityUIDTerm : Coe Spec.EntityUID Term

Equations

• Cedar.SymCC.instCoeEntityUIDTerm = { coe := fun (e : Cedar.Spec.EntityUID) => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.entity e) }

instance Cedar.SymCC.instCoeExtTerm : Coe Spec.Ext Term

Equations

• Cedar.SymCC.instCoeExtTerm = { coe := fun (x : Cedar.Spec.Ext) => Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.ext x) }

instance Cedar.SymCC.instCoeTermVarTerm : Coe TermVar Term

Equations

• Cedar.SymCC.instCoeTermVarTerm = { coe := fun (v : Cedar.SymCC.TermVar) => Cedar.SymCC.Term.var v }

def Cedar.SymCC.instReprTermVar.repr : TermVar → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprTermVar : Repr TermVar

Equations

• Cedar.SymCC.instReprTermVar = { reprPrec := Cedar.SymCC.instReprTermVar.repr }

instance Cedar.SymCC.instDecidableEqTermVar : DecidableEq TermVar

Equations

• Cedar.SymCC.instDecidableEqTermVar = Cedar.SymCC.instDecidableEqTermVar.decEq

def Cedar.SymCC.instDecidableEqTermVar.decEq (x✝ x✝¹ : TermVar) : Decidable (x✝ = x✝¹)

Equations

• Cedar.SymCC.instDecidableEqTermVar.decEq { id := a, ty := a_1 } { id := b, ty := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Cedar.SymCC.instInhabitedTermVar : Inhabited TermVar

Equations

• Cedar.SymCC.instInhabitedTermVar = { default := Cedar.SymCC.instInhabitedTermVar.default }

def Cedar.SymCC.instInhabitedTermVar.default : TermVar

Equations

• Cedar.SymCC.instInhabitedTermVar.default = { id := default, ty := default }

def Cedar.SymCC.instReprTermPrim.repr : TermPrim → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprTermPrim : Repr TermPrim

Equations

• Cedar.SymCC.instReprTermPrim = { reprPrec := Cedar.SymCC.instReprTermPrim.repr }

instance Cedar.SymCC.instDecidableEqTermPrim : DecidableEq TermPrim

Equations

• Cedar.SymCC.instDecidableEqTermPrim = Cedar.SymCC.instDecidableEqTermPrim.decEq

def Cedar.SymCC.instDecidableEqTermPrim.decEq (x✝ x✝¹ : TermPrim) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bool a) (Cedar.SymCC.TermPrim.bool b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bool a) (Cedar.SymCC.TermPrim.bitvec a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bool a) (Cedar.SymCC.TermPrim.string a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bool a) (Cedar.SymCC.TermPrim.entity a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bool a) (Cedar.SymCC.TermPrim.ext a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bitvec a) (Cedar.SymCC.TermPrim.bool a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bitvec a) (Cedar.SymCC.TermPrim.string a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bitvec a) (Cedar.SymCC.TermPrim.entity a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.bitvec a) (Cedar.SymCC.TermPrim.ext a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.string a) (Cedar.SymCC.TermPrim.bool a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.string a) (Cedar.SymCC.TermPrim.bitvec a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.string a) (Cedar.SymCC.TermPrim.string b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.string a) (Cedar.SymCC.TermPrim.entity a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.string a) (Cedar.SymCC.TermPrim.ext a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.entity a) (Cedar.SymCC.TermPrim.bool a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.entity a) (Cedar.SymCC.TermPrim.bitvec a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.entity a) (Cedar.SymCC.TermPrim.string a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.entity a) (Cedar.SymCC.TermPrim.entity b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.entity a) (Cedar.SymCC.TermPrim.ext a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.ext a) (Cedar.SymCC.TermPrim.bool a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.ext a) (Cedar.SymCC.TermPrim.bitvec a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.ext a) (Cedar.SymCC.TermPrim.string a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.ext a) (Cedar.SymCC.TermPrim.entity a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqTermPrim.decEq (Cedar.SymCC.TermPrim.ext a) (Cedar.SymCC.TermPrim.ext b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Cedar.SymCC.instInhabitedTermPrim.default : TermPrim

Equations

• Cedar.SymCC.instInhabitedTermPrim.default = Cedar.SymCC.TermPrim.bool default

instance Cedar.SymCC.instInhabitedTermPrim : Inhabited TermPrim

Equations

• Cedar.SymCC.instInhabitedTermPrim = { default := Cedar.SymCC.instInhabitedTermPrim.default }

instance Cedar.SymCC.instReprTerm : Repr Term

Equations

• Cedar.SymCC.instReprTerm = { reprPrec := Cedar.SymCC.instReprTerm.repr }

partial def Cedar.SymCC.instReprTerm.repr : Term → Nat → Std.Format

def Cedar.SymCC.instInhabitedTerm.default : Term

Equations

• Cedar.SymCC.instInhabitedTerm.default = Cedar.SymCC.Term.prim default

instance Cedar.SymCC.instInhabitedTerm : Inhabited Term

Equations

• Cedar.SymCC.instInhabitedTerm = { default := Cedar.SymCC.instInhabitedTerm.default }

def Cedar.SymCC.Term.hasDecEq (t t' : Term) : Decidable (t = t')

Equations

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

instance Cedar.SymCC.instDecidableEqTerm : DecidableEq Term

Equations

• Cedar.SymCC.instDecidableEqTerm = Cedar.SymCC.Term.hasDecEq

def Cedar.SymCC.TermVar.lt (v v' : TermVar) : Bool

Equations

• v.lt v' = (decide (v.id < v'.id) || decide (v.id = v'.id) && decide (v.ty < v'.ty))

instance Cedar.SymCC.instLTTermVar : LT TermVar

Equations

• Cedar.SymCC.instLTTermVar = { lt := fun (x y : Cedar.SymCC.TermVar) => x.lt y = true }

instance Cedar.SymCC.TermVar.decLt (x y : TermVar) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

def Cedar.SymCC.TermPrim.lt : TermPrim → TermPrim → Bool

Equations

• (Cedar.SymCC.TermPrim.bool b₁).lt (Cedar.SymCC.TermPrim.bool b₂) = decide (b₁ < b₂)
• (Cedar.SymCC.TermPrim.bitvec bv₁).lt (Cedar.SymCC.TermPrim.bitvec bv₂) = (decide (n₁ < n₂) || decide (n₁ = n₂) && decide (bv₁.toNat < bv₂.toNat))
• (Cedar.SymCC.TermPrim.string s₁).lt (Cedar.SymCC.TermPrim.string s₂) = decide (s₁ < s₂)
• (Cedar.SymCC.TermPrim.entity uid₁).lt (Cedar.SymCC.TermPrim.entity uid₂) = decide (uid₁ < uid₂)
• (Cedar.SymCC.TermPrim.ext x₁).lt (Cedar.SymCC.TermPrim.ext x₂) = decide (x₁ < x₂)
• x✝¹.lt x✝ = decide (Cedar.SymCC.TermPrim.mkName✝ x✝¹ < Cedar.SymCC.TermPrim.mkName✝¹ x✝)

instance Cedar.SymCC.instLTTermPrim : LT TermPrim

Equations

• Cedar.SymCC.instLTTermPrim = { lt := fun (x y : Cedar.SymCC.TermPrim) => x.lt y = true }

instance Cedar.SymCC.TermPrim.decLt (x y : TermPrim) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

@[irreducible]

def Cedar.SymCC.Term.lt : Term → Term → Bool

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.SymCC.Term.prim p₁).lt (Cedar.SymCC.Term.prim p₂) = decide (p₁ < p₂)
• (Cedar.SymCC.Term.var v₁).lt (Cedar.SymCC.Term.var v₂) = decide (v₁ < v₂)
• (Cedar.SymCC.Term.none ty₁).lt (Cedar.SymCC.Term.none ty₂) = decide (ty₁ < ty₂)
• t₁.some.lt t₂.some = t₁.lt t₂
• (Cedar.SymCC.Term.set (Cedar.Data.Set.mk ts₁) ty₁).lt (Cedar.SymCC.Term.set (Cedar.Data.Set.mk ts₂) ty₂) = (decide (ty₁ < ty₂) || decide (ty₁ = ty₂) && Cedar.SymCC.Term.ltList✝ ts₁ ts₂)
• (Cedar.SymCC.Term.record (Cedar.Data.Map.mk ats₁)).lt (Cedar.SymCC.Term.record (Cedar.Data.Map.mk ats₂)) = Cedar.SymCC.Term.ltListProd✝ ats₁ ats₂
• x✝¹.lt x✝ = decide (Cedar.SymCC.Term.mkName✝ x✝¹ < Cedar.SymCC.Term.mkName✝¹ x✝)

instance Cedar.SymCC.instLTTerm : LT Term

Equations

• Cedar.SymCC.instLTTerm = { lt := fun (x y : Cedar.SymCC.Term) => x.lt y = true }

instance Cedar.SymCC.Term.decLt (x y : Term) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h