Scope Theory

Abstract interface for theories that determine available scope readings.

structure ScopeTheory.ScopeReading : Type

A scope reading: an ordering of scope-taking elements.

• ordering : List String

  Identifiers for scope-taking elements, in scope order (widest first)

def ScopeTheory.instDecidableEqScopeReading.decEq (x✝ x✝¹ : ScopeReading) : Decidable (x✝ = x✝¹)

Equations

• ScopeTheory.instDecidableEqScopeReading.decEq { ordering := a } { ordering := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance ScopeTheory.instDecidableEqScopeReading : DecidableEq ScopeReading

Equations

• ScopeTheory.instDecidableEqScopeReading = ScopeTheory.instDecidableEqScopeReading.decEq

def ScopeTheory.instBEqScopeReading.beq : ScopeReading → ScopeReading → Bool

Equations

• ScopeTheory.instBEqScopeReading.beq { ordering := a } { ordering := b } = (a == b)
• ScopeTheory.instBEqScopeReading.beq x✝¹ x✝ = false

instance ScopeTheory.instBEqScopeReading : BEq ScopeReading

Equations

• ScopeTheory.instBEqScopeReading = { beq := ScopeTheory.instBEqScopeReading.beq }

instance ScopeTheory.instReprScopeReading : Repr ScopeReading

Equations

• ScopeTheory.instReprScopeReading = { reprPrec := ScopeTheory.instReprScopeReading.repr }

def ScopeTheory.instReprScopeReading.repr : ScopeReading → Nat → Std.Format

Equations

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

def ScopeTheory.instInhabitedScopeReading.default : ScopeReading

Equations

• ScopeTheory.instInhabitedScopeReading.default = { ordering := default }

instance ScopeTheory.instInhabitedScopeReading : Inhabited ScopeReading

Equations

• ScopeTheory.instInhabitedScopeReading = { default := ScopeTheory.instInhabitedScopeReading.default }

def ScopeTheory.ScopeReading.surface (elements : List String) : ScopeReading

The surface scope reading (linear order = scope order)

Equations

• ScopeTheory.ScopeReading.surface elements = { ordering := elements }

def ScopeTheory.ScopeReading.inverse (elements : List String) : ScopeReading

Reverse (inverse) scope reading

Equations

• ScopeTheory.ScopeReading.inverse elements = { ordering := elements.reverse }

structure ScopeTheory.AvailableScopes : Type

The set of available scope readings for a form.

• readings : List ScopeReading

  All available scope readings

• nonempty : self.readings ≠ []

  At least one reading must be available

def ScopeTheory.instReprAvailableScopes.repr : AvailableScopes → Nat → Std.Format

Equations

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

instance ScopeTheory.instReprAvailableScopes : Repr AvailableScopes

Equations

• ScopeTheory.instReprAvailableScopes = { reprPrec := ScopeTheory.instReprAvailableScopes.repr }

def ScopeTheory.AvailableScopes.singleton (r : ScopeReading) : AvailableScopes

Singleton: only one reading available

Equations

• ScopeTheory.AvailableScopes.singleton r = { readings := [r], nonempty := ⋯ }

def ScopeTheory.AvailableScopes.binary (surface inverse : ScopeReading) : AvailableScopes

Binary: exactly two readings (surface and inverse)

Equations

• ScopeTheory.AvailableScopes.binary surface inverse = { readings := [surface, inverse], nonempty := ⋯ }

def ScopeTheory.AvailableScopes.hasReading (a : AvailableScopes) (r : ScopeReading) : Bool

Check if a specific reading is available

Equations

• a.hasReading r = a.readings.contains r

def ScopeTheory.AvailableScopes.isAmbiguous (a : AvailableScopes) : Bool

Is the scope ambiguous (more than one reading)?

Equations

• a.isAmbiguous = decide (a.readings.length > 1)

class ScopeTheory.HasAvailableScopes (T Form : Type) : Type

Typeclass for theories that determine available scope readings.

• availableScopes : Form → AvailableScopes

  Determine available scope readings for a form

def ScopeTheory.getAvailableScopes {T Form : Type} [HasAvailableScopes T Form] (form : Form) : AvailableScopes

Convenience function to get available scopes

Equations

• ScopeTheory.getAvailableScopes form = ScopeTheory.HasAvailableScopes.availableScopes T form

structure ScopeTheory.ScopePreference : Type

A ranked preference over scope readings.

• ranking : List ScopeReading

  Readings ranked by preference (most preferred first)

• scores : List Float

  Scores for each reading (higher = more preferred)

• aligned : self.ranking.length = self.scores.length

  Rankings and scores must align

def ScopeTheory.instReprScopePreference.repr : ScopePreference → Nat → Std.Format

Equations

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

instance ScopeTheory.instReprScopePreference : Repr ScopePreference

Equations

• ScopeTheory.instReprScopePreference = { reprPrec := ScopeTheory.instReprScopePreference.repr }

class ScopeTheory.HasScopePreference (T Form Context : Type) : Type

Typeclass for theories that rank scope readings.

• preferScopes : Form → Context → AvailableScopes → ScopePreference

  Rank available scope readings in context

structure ScopeTheory.BinaryScopeForm (α : Type) : Type

Specialized interface for binary scope ambiguity.

• form : α

  The form/derivation

• scopeTaker1 : String

  First scope-taker (surface-wide)

• scopeTaker2 : String

  Second scope-taker (surface-narrow)

def ScopeTheory.instReprBinaryScopeForm.repr {α✝ : Type} [Repr α✝] : BinaryScopeForm α✝ → Nat → Std.Format

Equations

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

instance ScopeTheory.instReprBinaryScopeForm {α✝ : Type} [Repr α✝] : Repr (BinaryScopeForm α✝)

Equations

• ScopeTheory.instReprBinaryScopeForm = { reprPrec := ScopeTheory.instReprBinaryScopeForm.repr }

inductive ScopeTheory.BinaryScopeAvailability : Type

Binary scope availability: surface only, inverse only, or both.

• surfaceOnly : BinaryScopeAvailability
• inverseOnly : BinaryScopeAvailability
• ambiguous : BinaryScopeAvailability

instance ScopeTheory.instDecidableEqBinaryScopeAvailability : DecidableEq BinaryScopeAvailability

Equations

• ScopeTheory.instDecidableEqBinaryScopeAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance ScopeTheory.instBEqBinaryScopeAvailability : BEq BinaryScopeAvailability

Equations

• ScopeTheory.instBEqBinaryScopeAvailability = { beq := ScopeTheory.instBEqBinaryScopeAvailability.beq }

def ScopeTheory.instBEqBinaryScopeAvailability.beq : BinaryScopeAvailability → BinaryScopeAvailability → Bool

Equations

• ScopeTheory.instBEqBinaryScopeAvailability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def ScopeTheory.instReprBinaryScopeAvailability.repr : BinaryScopeAvailability → Nat → Std.Format

Equations

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

instance ScopeTheory.instReprBinaryScopeAvailability : Repr BinaryScopeAvailability

Equations

• ScopeTheory.instReprBinaryScopeAvailability = { reprPrec := ScopeTheory.instReprBinaryScopeAvailability.repr }

instance ScopeTheory.instInhabitedBinaryScopeAvailability : Inhabited BinaryScopeAvailability

Equations

• ScopeTheory.instInhabitedBinaryScopeAvailability = { default := ScopeTheory.instInhabitedBinaryScopeAvailability.default }

def ScopeTheory.instInhabitedBinaryScopeAvailability.default : BinaryScopeAvailability

Equations

• ScopeTheory.instInhabitedBinaryScopeAvailability.default = ScopeTheory.BinaryScopeAvailability.surfaceOnly

def ScopeTheory.BinaryScopeAvailability.toAvailableScopes (b : BinaryScopeAvailability) (s1 s2 : String) : AvailableScopes

Convert to general AvailableScopes

Equations

• One or more equations did not get rendered due to their size.
• ScopeTheory.BinaryScopeAvailability.surfaceOnly.toAvailableScopes s1 s2 = ScopeTheory.AvailableScopes.singleton (ScopeTheory.ScopeReading.surface [s1, s2])
• ScopeTheory.BinaryScopeAvailability.inverseOnly.toAvailableScopes s1 s2 = ScopeTheory.AvailableScopes.singleton (ScopeTheory.ScopeReading.inverse [s1, s2])

class ScopeTheory.HasBinaryScope (T Form : Type) : Type

Typeclass for binary scope theories.

• binaryScope : BinaryScopeForm Form → BinaryScopeAvailability

  Determine binary scope availability