Binding Semantics

Data types for H&K-style assignment-based binding semantics.

structure BindingSemantics.Position : Type

A position in a syntactic structure.

• index : Nat

  Linear index (word position)

@[implicit_reducible]

instance BindingSemantics.instReprPosition : Repr Position

Equations

• BindingSemantics.instReprPosition = { reprPrec := BindingSemantics.instReprPosition.repr }

def BindingSemantics.instReprPosition.repr : Position → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance BindingSemantics.instDecidableEqPosition : DecidableEq Position

Equations

• BindingSemantics.instDecidableEqPosition = BindingSemantics.instDecidableEqPosition.decEq

def BindingSemantics.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• BindingSemantics.instDecidableEqPosition.decEq { index := a } { index := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def BindingSemantics.instHashablePosition.hash : Position → UInt64

Equations

• BindingSemantics.instHashablePosition.hash { index := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance BindingSemantics.instHashablePosition : Hashable Position

Equations

• BindingSemantics.instHashablePosition = { hash := BindingSemantics.instHashablePosition.hash }

structure BindingSemantics.BindingRelation : Type

A binding relation: which binder binds which bindee.

• binder : Position

  Position of the binder (quantifier, lambda-operator, etc.)

• bindee : Position

  Position of the bindee (pronoun, trace, etc.)

• varIndex : Nat

  The variable index used in the assignment function

@[implicit_reducible]

instance BindingSemantics.instReprBindingRelation : Repr BindingRelation

Equations

• BindingSemantics.instReprBindingRelation = { reprPrec := BindingSemantics.instReprBindingRelation.repr }

def BindingSemantics.instReprBindingRelation.repr : BindingRelation → Nat → Std.Format

Equations

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

def BindingSemantics.instDecidableEqBindingRelation.decEq (x✝ x✝¹ : BindingRelation) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance BindingSemantics.instDecidableEqBindingRelation : DecidableEq BindingRelation

Equations

• BindingSemantics.instDecidableEqBindingRelation = BindingSemantics.instDecidableEqBindingRelation.decEq

structure BindingSemantics.BindingConfig : Type

A complete binding configuration for a structure.

• bindings : List BindingRelation

  All binding relations in the structure

• freeVariables : List (Position × Nat)

  Positions that are free (unbound) variables

def BindingSemantics.instReprBindingConfig.repr : BindingConfig → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance BindingSemantics.instReprBindingConfig : Repr BindingConfig

Equations

• BindingSemantics.instReprBindingConfig = { reprPrec := BindingSemantics.instReprBindingConfig.repr }

def BindingSemantics.BindingConfig.wellFormed (bc : BindingConfig) : Bool

A binding configuration is well-formed.

Equations

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