polymorphism

cpp.Polymorphism.named

def Polymorphism.named (known : List ClassMembers) (x : String) : Option ClassMembers

The class with a name, among the known ones.

cpp.Polymorphism.isPolymorphic

def Polymorphism.isPolymorphic (known : List ClassMembers) (x : String) : Bool

Whether a class is polymorphic.

cpp.Polymorphism.firstBase

def Polymorphism.firstBase (known : List ClassMembers) (x : String) : Option String

A class’s first base, if it has one and it is not virtual (a virtual base is not where the class is, so the class shares no chain with it).

cpp.Polymorphism.isRoot

def Polymorphism.isRoot (known : List ClassMembers) (x : String) : Bool

Whether a class is a chain’s root: polymorphic, its first base (if any) not.

cpp.Polymorphism.ownRootWithin

def Polymorphism.ownRootWithin (fuel : Nat) (known : List ClassMembers) (x : String) : Option (List Nat)

The path (base positions) from a polymorphic class to its own chain’s root; fuel bounds the depth.

cpp.Polymorphism.ownRoot

def Polymorphism.ownRoot (known : List ClassMembers) (x : String) : Option (List Nat)

The path from a polymorphic class to its own chain’s root.

cpp.Polymorphism.samePath

def Polymorphism.samePath (a : List Nat) (b : List Nat) : Bool

Whether two paths are the same.

cpp.Polymorphism.chainsWithin

def Polymorphism.chainsWithin (fuel : Nat) (known : List ClassMembers) (x : String) : List (List Nat)

The paths from a class to each of its chains’ roots: its own first (if it is polymorphic), then each base’s, except the first base’s own chain, which is the class’s own.

cpp.Polymorphism.identity

def Polymorphism.identity (known : List ClassMembers) (x : String) (root : String) (after : List Nat) (path : List Nat) : String * List Nat

Which subobject a path of base positions from a class reaches: the virtual base it last goes through (the class itself when none, root) and the positions after it; two paths reaching one virtual base’s subobject reach the same.

cpp.Polymorphism.sameSubobject

def Polymorphism.sameSubobject (a : String * List Nat) (b : String * List Nat) : Bool

Whether two subobjects (by identity) are the same.

cpp.Polymorphism.depth

def Polymorphism.depth (known : List ClassMembers) (x : String) (path : List Nat) : Nat

How many levels down from a complete object of a class the subobject at a path is: the non-virtual positions after its virtual base, and one more for the virtual base’s storage.

cpp.Polymorphism.distinctPaths

def Polymorphism.distinctPaths (known : List ClassMembers) (x : String) (paths : List (List Nat)) : List (List Nat)

The paths, each once by the subobject it reaches, kept in order (the first path to a subobject).

cpp.Polymorphism.chains

def Polymorphism.chains (known : List ClassMembers) (x : String) : List (List Nat)

The paths from a class to its chains’ roots (a virtual base’s chains once).

cpp.Polymorphism.pathsWithin

def Polymorphism.pathsWithin (fuel : Nat) (known : List ClassMembers) (x : String) (y : String) : List (List Nat)

Every path from a class to a base (of the class y) within a depth: through each base that reaches it.

cpp.Polymorphism.paths

def Polymorphism.paths (known : List ClassMembers) (x : String) (y : String) : List (List Nat)

Every path from a class to a base of the class y.

cpp.Polymorphism.keepsVirtualBases

def Polymorphism.keepsVirtualBases (known : List ClassMembers) (x : String) : Bool

Whether a class keeps virtual bases.

cpp.Polymorphism.virtualChains

def Polymorphism.virtualChains (known : List ClassMembers) (x : String) : List (List Nat)

A class’s chains that are in its virtual bases (a base subobject of it does not have those where it is).

cpp.Polymorphism.block

def Polymorphism.block (known : List ClassMembers) (c : String) (at : List Nat) : List (List Nat * List Nat)

The construction contexts of a base subobject of class c at a path (its block).

cpp.Polymorphism.constructionRoots

def Polymorphism.constructionRoots (known : List ClassMembers) (x : String) : List (List Nat * String)

A complete object’s base subobjects whose constructors set construction contexts, in order: its non-virtual bases that keep virtual bases, then its virtual bases that do; each with the path to it and its class.

cpp.Polymorphism.constructionContextsOf

def Polymorphism.constructionContextsOf (known : List ClassMembers) (x : String) : List (List Nat * List Nat)

A complete object’s construction contexts (during the construction and destruction of its base subobjects with virtual bases, [class.cdtor]p4): each root’s block in order.

cpp.Polymorphism.countOf

def Polymorphism.countOf (known : List ClassMembers) (x : String) : Nat

How many contexts a class has: its chains’, then its construction contexts.

cpp.Polymorphism.contextCount

def Polymorphism.contextCount (known : List ClassMembers) : Nat

How many contexts the classes have (the first number for the class after them).

cpp.Polymorphism.numberedFrom

def Polymorphism.numberedFrom {A : Type} (first : Nat) (xs : List A) : List (Nat * A)

The numbers from a first one, one for each element.

cpp.ChainContext

def ChainContext : Type

A context with its number: (the complete object’s class, the path to a chain’s root).

cpp.ConstructionContext

def ConstructionContext : Type

A construction context with its number: (the complete object’s class, (the path to the base subobject being constructed or destroyed, the path to a chain’s root)).

cpp.Polymorphism.contexts

def Polymorphism.contexts (known : List ClassMembers) : List ChainContext

The contexts of the program’s classes in order, each with its number: (class, path to a chain’s root); a class’s construction contexts are numbered after its own (Polymorphism.constructionContexts).

cpp.Polymorphism.constructionContexts

def Polymorphism.constructionContexts (known : List ClassMembers) : List ConstructionContext

The construction contexts of the program’s classes, each with its number: (the complete object’s class, (the path to the base subobject being constructed, the path to a chain’s root)).

cpp.Contexts

record Contexts

The program’s contexts, computed once: the chains’ and the construction contexts, each with its number.

cpp.Contexts.of

def Contexts.of (known : List ClassMembers) : Contexts

The contexts of the program’s classes.

cpp.Polymorphism.classAt

def Polymorphism.classAt (known : List ClassMembers) (x : String) (path : List Nat) : Option String

The class of the subobject at a path in an object of a class (the class itself for the empty path).