This file defines the ADT for representing symbolic tags.

We currently represent with two total unary functions:

• keys : E -> Set String maps each instance of the entity type E to a set of strings. This set represents all tags that are attached to the given instance of E.
• vals : {"entity" : E, "tag" : String} -> T maps pairs of E and String to a tag value of type T. This is equivalent to using a binary function of type E -> String -> T to represent tag values, but we don't need to introduce binary functions into the Term language. It may be necessary to do so in the future if it turns out that wrapping the entity and string arguments into a value doesn't perform well enough.

With this representation, testing if an entity e has the tag s amounts to checking if s is a member of keys e. Safely getting the value of the tag s for the entity e amounts to returning none if s is not a member of es keys set, and otherwise returnng vals e s.

structure Cedar.SymCC.SymTags : Type

• keys : UnaryFunction
• vals : UnaryFunction

def Cedar.SymCC.SymTags.hasTag (τs : SymTags) (entity tag : Term) : Term

Equations

• τs.hasTag entity tag = Cedar.SymCC.Factory.set.member tag (Cedar.SymCC.Factory.app τs.keys entity)

def Cedar.SymCC.SymTags.getTag! (τs : SymTags) (entity tag : Term) : Term

Equations

• τs.getTag! entity tag = Cedar.SymCC.Factory.app τs.vals (Cedar.SymCC.Factory.tagOf entity tag)

def Cedar.SymCC.SymTags.getTag (τs : SymTags) (entity tag : Term) : Term

Equations

• τs.getTag entity tag = Cedar.SymCC.Factory.ifTrue (τs.hasTag entity tag) (τs.getTag! entity tag)

def Cedar.SymCC.instReprSymTags.repr : SymTags → Nat → Std.Format

Equations

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

instance Cedar.SymCC.instReprSymTags : Repr SymTags

Equations

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

def Cedar.SymCC.instInhabitedSymTags.default : SymTags

Equations

• Cedar.SymCC.instInhabitedSymTags.default = { keys := default, vals := default }

instance Cedar.SymCC.instInhabitedSymTags : Inhabited SymTags

Equations

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

instance Cedar.SymCC.instDecidableEqSymTags : DecidableEq SymTags

Equations

• Cedar.SymCC.instDecidableEqSymTags = Cedar.SymCC.instDecidableEqSymTags.decEq

def Cedar.SymCC.instDecidableEqSymTags.decEq (x✝ x✝¹ : SymTags) : Decidable (x✝ = x✝¹)

Equations

• Cedar.SymCC.instDecidableEqSymTags.decEq { keys := a, vals := a_1 } { keys := b, vals := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯