structure CCG.Scope.ScopeTaker : Type

A scope-taking element in a CCG derivation.

• id : String
• surfacePosition : Nat
• cat : Cat

instance CCG.Scope.instReprScopeTaker : Repr ScopeTaker

Equations

• CCG.Scope.instReprScopeTaker = { reprPrec := CCG.Scope.instReprScopeTaker.repr }

def CCG.Scope.instReprScopeTaker.repr : ScopeTaker → Nat → Std.Format

Equations

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

inductive CCG.Scope.DerivationType : Type

Derivation type for scope analysis.

• directApp : DerivationType
• typeRaised : DerivationType
• composed : DerivationType

instance CCG.Scope.instDecidableEqDerivationType : DecidableEq DerivationType

Equations

• CCG.Scope.instDecidableEqDerivationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance CCG.Scope.instBEqDerivationType : BEq DerivationType

Equations

• CCG.Scope.instBEqDerivationType = { beq := CCG.Scope.instBEqDerivationType.beq }

def CCG.Scope.instBEqDerivationType.beq : DerivationType → DerivationType → Bool

Equations

• CCG.Scope.instBEqDerivationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def CCG.Scope.instReprDerivationType.repr : DerivationType → Nat → Std.Format

Equations

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

instance CCG.Scope.instReprDerivationType : Repr DerivationType

Equations

• CCG.Scope.instReprDerivationType = { reprPrec := CCG.Scope.instReprDerivationType.repr }

def CCG.Scope.analyzeDerivation : DerivStep → DerivationType

Analyze derivation to determine its type.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Scope.analyzeDerivation (CCG.DerivStep.lex a) = CCG.Scope.DerivationType.directApp
• CCG.Scope.analyzeDerivation (a.fcomp a_1) = CCG.Scope.DerivationType.composed
• CCG.Scope.analyzeDerivation (a.bcomp a_1) = CCG.Scope.DerivationType.composed
• CCG.Scope.analyzeDerivation (a.ftr a_1) = CCG.Scope.DerivationType.typeRaised
• CCG.Scope.analyzeDerivation (a.btr a_1) = CCG.Scope.DerivationType.typeRaised

def CCG.Scope.derivationTypeToAvailability : DerivationType → ScopeTheory.BinaryScopeAvailability

Determine scope availability from derivation type.

Equations

• CCG.Scope.derivationTypeToAvailability CCG.Scope.DerivationType.directApp = ScopeTheory.BinaryScopeAvailability.surfaceOnly
• CCG.Scope.derivationTypeToAvailability CCG.Scope.DerivationType.typeRaised = ScopeTheory.BinaryScopeAvailability.ambiguous
• CCG.Scope.derivationTypeToAvailability CCG.Scope.DerivationType.composed = ScopeTheory.BinaryScopeAvailability.ambiguous

structure CCG.Scope.ScopedDerivation : Type

A CCG derivation annotated with scope-taker information.

• deriv : DerivStep
• scopeTakers : List ScopeTaker
• hasTwoOrMore : self.scopeTakers.length ≥ 2

instance CCG.Scope.instReprScopedDerivation : Repr ScopedDerivation

Equations

• CCG.Scope.instReprScopedDerivation = { reprPrec := CCG.Scope.instReprScopedDerivation.repr }

def CCG.Scope.instReprScopedDerivation.repr : ScopedDerivation → Nat → Std.Format

Equations

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

def CCG.Scope.ScopedDerivation.availability (sd : ScopedDerivation) : ScopeTheory.BinaryScopeAvailability

Equations

• sd.availability = CCG.Scope.derivationTypeToAvailability (CCG.Scope.analyzeDerivation sd.deriv)

def CCG.Scope.ScopedDerivation.toAvailableScopes (sd : ScopedDerivation) : ScopeTheory.AvailableScopes

Equations

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

def CCG.Scope.everyHorse_surface : DerivStep

Equations

• CCG.Scope.everyHorse_surface = (CCG.DerivStep.lex { form := "every horse", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "didn't jump", cat := CCG.IV })

def CCG.Scope.everyHorse_inverse : DerivStep

Equations

• CCG.Scope.everyHorse_inverse = ((CCG.DerivStep.lex { form := "every horse", cat := CCG.NP }).ftr CCG.S).fcomp (CCG.DerivStep.lex { form := "didn't jump", cat := CCG.IV })