Binding Semantics

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

structure Interfaces.BindingSemantics.Position : Type

A position in a syntactic structure.

• index : Nat

  Linear index (word position)

instance Interfaces.BindingSemantics.instReprPosition : Repr Position

Equations

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

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

Equations

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

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

Equations

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

instance Interfaces.BindingSemantics.instDecidableEqPosition : DecidableEq Position

Equations

• Interfaces.BindingSemantics.instDecidableEqPosition = Interfaces.BindingSemantics.instDecidableEqPosition.decEq

def Interfaces.BindingSemantics.instBEqPosition.beq : Position → Position → Bool

Equations

• Interfaces.BindingSemantics.instBEqPosition.beq { index := a } { index := b } = (a == b)
• Interfaces.BindingSemantics.instBEqPosition.beq x✝¹ x✝ = false

instance Interfaces.BindingSemantics.instBEqPosition : BEq Position

Equations

• Interfaces.BindingSemantics.instBEqPosition = { beq := Interfaces.BindingSemantics.instBEqPosition.beq }

def Interfaces.BindingSemantics.instHashablePosition.hash : Position → UInt64

Equations

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

instance Interfaces.BindingSemantics.instHashablePosition : Hashable Position

Equations

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

structure Interfaces.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

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

Equations

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

instance Interfaces.BindingSemantics.instReprBindingRelation : Repr BindingRelation

Equations

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

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

Equations

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

instance Interfaces.BindingSemantics.instDecidableEqBindingRelation : DecidableEq BindingRelation

Equations

• Interfaces.BindingSemantics.instDecidableEqBindingRelation = Interfaces.BindingSemantics.instDecidableEqBindingRelation.decEq

structure Interfaces.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

instance Interfaces.BindingSemantics.instReprBindingConfig : Repr BindingConfig

Equations

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

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

Equations

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

def Interfaces.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.