Vertex #

Key arguments (see keyArgs), with constants passed through and everything else canonicalized to bvars (though structured arguments keep their structure). For the bvars, the only information that is preserved is which, if any, of the arguments were equal to one another.

Examples

Class application	`pattern`	Notes
`Module R M`	`#[bvar 0, bvar 1]`	fvars become bvars
`SomeClass α β γ β`	`#[bvar 0, bvar 1, bvar 2, bvar 1]`	repeated fvars reuse bvar index
`Pow α ℕ`	`#[bvar 0, ℕ]`	bare constant is preserved
`IsTrans α (·=·)`	`#[bvar 0, bvar 1]`	opaque relation becomes bvar
`OfNat α 1`	`#[bvar 0, 1]`	nat literal is preserved
`Monoid (List α)`	`#[List (bvar 0)]`	structure inside carrier is preserved
`Monoid (List (List (α × β)))`	`#[List (List ((bvar 0) × (bvar 1)))]`	structure inside carrier is preserved
`Module (α × β) M`	`#[(bvar 0) × (bvar 1), bvar 2]`	structure inside carrier is preserved

levels : UniverseLevels
If the typeclass is universe polymorphic, this is indicated through a single value .polymorphic. If the typeclass's universe levels are concrete, they are all specified through .concrete #[u₁ … uₙ], where e.g. u₁ might be 0 (i.e., not a variable). The fact that we treat all universe polymorphism the same can lead to problems.
For example, consider the following instance:
```
instance CategoryTheory.locallySmall_self.{v, u} (C : Type.{u})
  [inst : CategoryTheory.Category.{v, u} C] : CategoryTheory.LocallySmall.{v, v, u} C inst
```
When scanning this instance, extractEdge? will mint the following edge:
```
{
  src := { name := ``CategoryTheory.Category, pattern := #[#0], levels := .polymorphic },
  tgt := { name := ``CategoryTheory.LocallySmall, pattern := #[#0], levels := .polymorphic }
}
```
The fact that the real target was LocallySmall.{v, v, u} and not LocallySmall.{w, v, u} is lost. This could lead to unsound candidates that the verifier must catch. However, most of the time, the target levels are pinned indirectly by Vertex.pattern. For example:
```
instance ContinuousAdd.to_continuousVAdd.{u} {M : Type.{u}}
  [inst₁ : TopologicalSpace.{u} M]
  [inst₂ : Add.{u} M]
  [inst₃ : ContinuousAdd.{u} M inst₁ inst₂] :
  ContinuousVAdd.{u, u} M M (instVAddOfAdd.{u} M inst₂) inst₁ inst₁
```
When scanning this instance, extractEdge? will mint the following edge:
```
{
  src := { name := ``ContinuousAdd, pattern := #[#0], levels := .polymorphic },
  tgt := { name := ``ContinuousVAdd, pattern := #[#0, #0], levels := .polymorphic }
}
```
Here, even though the information about the universe levels appears lost, it is actually pinned by pattern := #[#0, #0], because the two arguments that the pattern refers to are tied to the two universe levels:
```
class ContinuousVAdd.{u, v}
  (M : Type.{u}) (X : Type.{v}) -- Note: M = X ⟹ u = v
  [inst₁ : VAdd.{u, v} M X]
  [inst₂ : TopologicalSpace.{u} M]
  [inst₃ : TopologicalSpace.{v} X] :
  Prop
```
Future work could include making the handling of universe levels more precise, though we hypothesize the gains from this may be modest.

Instances For

source

def GeneralizationLinter.instBEqVertex.beq :

Vertex → Vertex → Bool

Equations

GeneralizationLinter.instBEqVertex.beq { name := a, pattern := a_1, levels := a_2 } { name := b, pattern := b_1, levels := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
GeneralizationLinter.instBEqVertex.beq x✝¹ x✝ = false

Instances For

source

@[implicit_reducible]

instance GeneralizationLinter.instBEqVertex :

BEq Vertex

Equations

GeneralizationLinter.instBEqVertex = { beq := GeneralizationLinter.instBEqVertex.beq }

source

def GeneralizationLinter.instHashableVertex.hash :

Vertex → UInt64

Equations

GeneralizationLinter.instHashableVertex.hash { name := a, pattern := a_1, levels := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

Instances For

source

@[implicit_reducible]

instance GeneralizationLinter.instHashableVertex :

Hashable Vertex

Equations

GeneralizationLinter.instHashableVertex = { hash := GeneralizationLinter.instHashableVertex.hash }

source

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedVertex :

Inhabited Vertex

Equations

GeneralizationLinter.instInhabitedVertex = { default := GeneralizationLinter.instInhabitedVertex.default }

source

structure GeneralizationLinter.Keyextends GeneralizationLinter.Vertex :

Type

A specific class application parsed at runtime into a (canonicalized) vertex together with the original values of the canonicalized arguments.

name : Lean.Name
pattern : Array Lean.Expr
levels : UniverseLevels

subst : Array Lean.Expr

The concrete terms abstracted by pattern's bvars: subst[k] is the term that bvar k stands for.

Examples

Class application	`pattern`	`subst`
`Module R M`	`#[bvar 0, bvar 1]`	`#[R, M]`
`SomeClass α β γ β`	`#[bvar 0, bvar 1, bvar 2, bvar 1]`	`#[α, β, γ]`
`Pow α ℕ`	`#[bvar 0, ℕ]`	`#[α]`
`IsTrans α (·=·)`	`#[bvar 0, bvar 1]`	`#[α, (·=·)]`
`OfNat α 1`	`#[bvar 0, 1]`	`#[α]`
`Monoid (List α)`	`#[List (bvar 0)]`	`#[α]`
`Monoid (List (List (α × β)))`	`#[List (List ((bvar 0) × (bvar 1)))]`	`#[α, β]`
`Module (α × β) M`	`#[(bvar 0) × (bvar 1), bvar 2]`	`#[α, β, M]`

familyArity : Nat
Length of the decomposed Π-prefix of a family application, 0 (default) for an ordinary application. The prefix itself isn't stored, but rederived from the original binder type later on.

Examples
```
[Group G]             -- familyArity := 0
[∀ i, C (f i)]        -- familyArity := 1
[∀ i [D i], C (f i)]  -- familyArity := 2
```

Instances For

source

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedKey :

Inhabited Key

Equations

GeneralizationLinter.instInhabitedKey = { default := GeneralizationLinter.instInhabitedKey.default }

source

def GeneralizationLinter.subsumes (pattern target : Array Lean.Expr) :

Bool

Returns true iff pattern subsumes target.

Examples

subsumes #[.bvar 0] #[4]                -- true
subsumes #[.bvar 0] #[4, 2]             -- false: size mismatch
subsumes #[.bvar 0, .bvar 1] #[4]       -- false: size mismatch
subsumes #[.bvar 0, .bvar 1] #[4, 2]    -- true
subsumes #[.bvar 0, .bvar 1] #[4, 4]    -- true
subsumes #[.bvar 0, .bvar 0] #[4, 2]    -- false: 2nd occurrence of `.bvar 0` doesn't match 1st
subsumes #[.bvar 0, .bvar 0] #[4, 4]    -- true
subsumes #[.bvar 0] #[List Nat]         -- true
subsumes #[List (.bvar 0)] #[List Nat]  -- true

Equations

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

Instances For

source

def GeneralizationLinter.Vertex.properSubsumers (v : Vertex) (maxCombined : Nat := 2048) :

Array Vertex

If the number of subsumers of v.pattern isn't estimated to exceed maxCombined (default 2048), then all proper subsumers of v.pattern (i.e., subsumers of v.pattern that are not equal to v.pattern) are returned as an array of vertices, where each output vertex w inherits all fields from v except for v.pattern, which instead is set to the subsumer.

Equations

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

Instances For

source

def GeneralizationLinter.Vertex.matchingVertices (query : Vertex) (includeSubsumers : Bool := false) :

Array Vertex

Given a vertex query, returns the array of vertices that match query. This is used to match non-universe-polymorphic vertices with both the corresponding non-universe-polymorphic vertex and the corresponding universe-polymorphic vertex.

If includeSubsumers is true (default false), then the query is extended to any subsuming vertices.

Examples

Small.{0} α will match Small.{0} α and Small α (the latter we understand to be universe-polymorphic).
Small.{123} α will only match Small α, as there is no specific Small.{123} α vertex in the class graph.

Equations

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

Instances For

Documentation

GeneralizationLinter.Helpers.Vertex

Vertex #