resolution

cfamily.TypeExtension

record TypeExtension (L : Constructs)

How a dialect resolves, compares and lays out its own types. resolve gets the written type and its children (the written types inside it, in order) resolved; same compares two tags (the core compares children); layout gives the size and alignment of a tag from its children’s; layoutOverride lays out a whole type the dialect lays out its own way (C++’s classes, by the Itanium ABI), or none for the core’s rules. typeText is how the dialect writes a type in a problem’s details, given the program’s tables (as the type query writes it).

cfamily.TypeText.tagOf

def TypeText.tagOf (u : String * List (String * TypeSyntax)) : String

The tag of the struct or union u in a program’s tables.

cfamily.TypeText.ofC

def TypeText.ofC {L : Constructs} (g : Globals L) : TypeText L

How C writes the types of a program whose tables are g: _Bool, a struct or union after its keyword (a union by the program’s union tags).

cfamily.TypeExtension.empty

def TypeExtension.empty {L : Constructs} : TypeExtension L

The extension of a dialect without types of its own (its types written as C writes them).

cfamily.TypeExtension.write

def TypeExtension.write {L : Constructs} (ext : TypeExtension L) (g : Globals L) (t : Ty L) : String

The type t written as the dialect’s extension ext writes it for the program’s tables g, in a problem’s details.

cfamily.IntegerType.ofSyntax

def IntegerType.ofSyntax (p : Platform) (t : TypeSyntax) : Option IntegerType

The integer type a written integer type names on a platform, if it is one.

cfamily.ResolvedTypes

def ResolvedTypes (L : Constructs) : Type

Resolved types, or none if one does not resolve.

cfamily.ResolvedResult

def ResolvedResult (L : Constructs) : Type

A resolved function result (some none is void), or none if it does not resolve.

cfamily.Ty.constOf

def Ty.constOf {L : Constructs} (t : Ty L) : Ty L

A type qualified const: the const of an array is its elements’ (C11 6.7.3p9).

cfamily.Ty.ofSyntaxWithin

def Ty.ofSyntaxWithin {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (fuel : Nat) (t : TypeSyntax) : Option (Ty L)

Resolves a written type; fuel bounds the typedef chains (a typedef naming itself resolves to none).

cfamily.Ty.pointableWithin

def Ty.pointableWithin {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (fuel : Nat) (u : TypeSyntax) : Option (Ty L)

A written type a pointer or an array is formed of, resolved: none when the dialect’s type cannot be (C++’s references, [dcl.ptr]p4, [dcl.array]p1).

cfamily.Ty.bitField

def Ty.bitField {L : Constructs} (w : Nat) (t : Ty L) : Option (Ty L)

An integer type narrowed to a bit-field’s width; none if the type is not an integer type or is narrower (C11 6.7.2.1p4).

cfamily.Ty.childWithin

def Ty.childWithin {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (fuel : Nat) (u : TypeSyntax) : ResolvedTypes L

A written type inside a dialect’s type, resolved as its only child.

cfamily.Ty.ofSyntaxAll

def Ty.ofSyntaxAll {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (fuel : Nat) (ts : List TypeSyntax) : ResolvedTypes L

Resolves written types in order; none if any does not resolve.

cfamily.Ty.resultWithin

def Ty.resultWithin {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (fuel : Nat) (r : Option TypeSyntax) : ResolvedResult L

Resolves a function type’s result.

cfamily.Ty.functionOf

def Ty.functionOf {L : Constructs} (parameters : ResolvedTypes L) (result : ResolvedResult L) : Option (Ty L)

A function type from its resolved parameters and result.

cfamily.Ty.extensionWith

def Ty.extensionWith {L : Constructs} (ext : TypeExtension L) (g : Globals L) (t : TypeSyntax) (children : ResolvedTypes L) : Option (Ty L)

A dialect’s type syntax with its children resolved, or none if a child does not resolve.

cfamily.Ty.ofSyntax

def Ty.ofSyntax {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (t : TypeSyntax) : Option (Ty L)

Resolves a written type; typedef chains are bounded by the number of typedefs.