arrays

cpp.Ty.dimensions

def Ty.dimensions {L : Constructs} (t : Ty L) : List Nat * Ty L

The lengths of an array type’s dimensions, outermost first, and its element type.

cpp.Ty.withoutConstElements

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

An array type with its elements’ const taken away (as an object under construction is, [class.ctor]p5).

cpp.TypeSyntax.withoutConstElements

def TypeSyntax.withoutConstElements (t : TypeSyntax) : Option TypeSyntax

A written array type with its elements’ const taken away, if they are const.

cpp.Arrays.ofClass

def Arrays.ofClass (g : Globals Cpp.constructs) (t : TypeSyntax) : Option ClassMembers

The class of an array’s elements, when the written type is an array of a class with constructors or a destructor.

cpp.Arrays.constructedClass

def Arrays.constructedClass (g : Globals Cpp.constructs) (t : TypeSyntax) : Option ClassMembers

The class of an element type (after its dimensions) when its objects are constructed or destroyed.

cpp.Arrays.elementOf

def Arrays.elementOf (p : Platform) (n : NodeId) (element : Ty Cpp.constructs) (array : TypedExpr Cpp.constructs) (k : Nat) : TypedExpr Cpp.constructs

The k-th element of an array (an lvalue): *(a + k) with the array decayed.

cpp.Arrays.leafLvalue

def Arrays.leafLvalue (p : Platform) (n : NodeId) (t : Ty Cpp.constructs) (array : TypedExpr Cpp.constructs) (j : Nat) : TypedExpr Cpp.constructs

The j-th element (row by row) of an array (an lvalue) of a type.

cpp.Arrays.lastFirst

def Arrays.lastFirst (make : Nat -> List TypedCpp) (j : Nat) (left : Nat) (acc : List TypedCpp) : List TypedCpp

The statements for the elements j, j + 1, … (left of them) put before acc, each in front of the earlier ones: the last element’s first. A loop (the call is the last thing done): an array of ten thousand elements made the list functions’ recursion overflow the browser’s stack.

cpp.Arrays.destroyingLeaves

def Arrays.destroyingLeaves (p : Platform) (functions : List (CheckedFunction Cpp.constructs)) (t : Ty Cpp.constructs) (array : TypedExpr Cpp.constructs) (count : Nat) : List TypedCpp

The destruction of an array’s first count elements (row by row), the last first.

cpp.Arrays.destroyingThrough

def Arrays.destroyingThrough (p : Platform) (functions : List (CheckedFunction Cpp.constructs)) (element : Ty Cpp.constructs) (pointer : TypedExpr Cpp.constructs) (count : Nat) : List TypedCpp

The destruction of the first count elements a pointer points to (new[]’s), the last first.

cpp.Arrays.givenWithin

def Arrays.givenWithin (fuel : Nat) (listing : Bool) (lengths : List Nat) (start : Nat) (xs : List Init) : List (Nat * Init)

The elements an initializer list gives, by their index (row by row) and their initializers: a nested list gives a row, an expression the next element (a list in a list is the next row’s). In the last dimension a nested list is the next element’s own ([dcl.init.list]p3.6, Q qs[2] = {{1, 2}, {3, 4}}, the backing array of vector<pair<int, int>> v = {{1, 2}}): always when the element’s class has an initializer-list constructor (listing: the list is that constructor’s, vector<vector<int>> d = {{4, 1}}), else when its items are expressions (the constructor’s arguments). The array has the given lengths; xs are the items, the first at index start; fuel bounds the nesting.

cpp.Arrays.given

def Arrays.given (listing : Bool) (lengths : List Nat) (i : Option Init) : List (Nat * Init)

The elements the initializer i gives an array of the given lengths (none for no initializer); listing as for Arrays.givenWithin.

cpp.Arrays.guardName

def Arrays.guardName (key : String) : String

The guard of an array’s construction, by a key the scope has once (the declaration’s or the member’s name).

cpp.Arrays.countName

def Arrays.countName (guardName : String) : String

The count of the elements a guard’s array has constructed (a variable beside the guard).

cpp.Arrays.sourceElement

def Arrays.sourceElement (n : NodeId) (lengths : List Nat) (j : Expr) (from : Expr) : Expr

The element of a source array (of the given lengths) an element is constructed from: an xvalue array’s elements are xvalues ([expr.sub]p2), each moved from.

cpp.Arrays.elided

def Arrays.elided (cls : ClassMembers) (args : List Expr) : List Expr

An element’s arguments, a prvalue of its class (C(args)) given alone being that object, constructed in place from args (C++17’s guaranteed elision, [dcl.init]p17.6.1). Not provided: a call’s result likewise.

cpp.Arrays.element

def Arrays.element (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (place : Expr) (cls : ClassMembers) (construct : List Expr -> CheckResult Cpp.constructs TypedCpp) (x : Init) : CheckResult Cpp.constructs TypedCpp

An element (at place) of an array of the class cls from its initializer x: a list is the initializer-list constructor’s when the class has one (Construction.fromList, with k, c and env), else, as an expression, the arguments construct takes.

cpp.Arrays.building

def Arrays.building (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (key : String) (target : Expr) (t : Ty Cpp.constructs) (cls : ClassMembers) (given : List (Nat * Init)) (source : Option Expr) : CheckResult Cpp.constructs (List TypedCpp)

The construction of an array (the target, of type t) of a class, element by element: a guard with the count beside it, the elements given (an expression, or a list: the initializer-list constructor’s when the class has one, else the constructor’s arguments), then a loop over the rest, each by the default constructor or from the source array’s element of the same index; the count follows each element.

cpp.Arrays.declaration

def Arrays.declaration (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (x : DeclId) (name : String) (t : TypeSyntax) (cls : ClassMembers) (i : Option Init) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

A declaration of an array of a class: reserved, its elements constructed in a block (whose guard ends with it), then an object. Designators are not done (an array’s are clang’s extension in C++, and each element is constructed).

cpp.Arrays.member

def Arrays.member (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (y : String) (args : List Expr) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

A member that is an array, initialized in a constructor: an array of a class element by element (its guard in the constructor’s scope, destroying the constructed elements when an exception leaves the constructor), from the source array’s elements for a copy; any other copied from the source as a whole. None for a member that is no array.

cpp.Arrays.variableLength

def Arrays.variableLength (dialect : Target -> CheckDialect Cpp.constructs) (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (s : Stmt) (cls : ClassMembers) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

The statement s, a variable length array of objects of the class cls (GNU’s extension, which clang and g++ accept in C++), checked in the context c and the scope env with what constructing uses (k): declared as the dialect for the program’s target (dialect) declares one (the length checked and evaluated once, the assumption noted; a length not positive stops), reserved while its elements are default-initialized one by one in order of their index ([dcl.init]p7.2, [class.init]p1), the loop’s bound the length the array has at run time; a guard (a pointer to the first element, with the count constructed beside it) destroys the constructed ones, the last first, when a constructor throws (as for new T[n], [except.ctor]p3). The array’s end destroys its elements in reverse order from the length its block has ([class.dtor]p13). An array of arrays of the class is not done (the guard counts elements of one dimension).

cpp.Arrays.statement

def Arrays.statement (dialect : Target -> CheckDialect Cpp.constructs) (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (s : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

C++’s statement s of arrays of objects, in the context c and the scope env with what constructing uses (k): a declaration of one, a member that is an array initialized in a constructor, a variable length array of them (declared by the dialect for the target, dialect).

cpp.Arrays.constructedCount

def Arrays.constructedCount (s : State Cpp.constructs) (guardName : String) : Nat

The count a guard’s array has constructed (the variable beside the guard; none counted is 0).

cpp.Arrays.destroys

def Arrays.destroys (functions : List (CheckedFunction Cpp.constructs)) (t : Ty Cpp.constructs) : Bool

Whether an array’s elements are of a class with a destructor the program has.

cpp.Arrays.ending

def Arrays.ending (target : Target) (functions : List (CheckedFunction Cpp.constructs)) (s : State Cpp.constructs) (x : DeclId) (c : Block Cpp.constructs) (unwinding : Bool) : List TypedCpp

What runs before an object ends, with arrays of a class: an array’s elements destroyed, the last first; an array’s guard (or new[]’s, with a count beside it), when an exception leaves the scope, the elements constructed so far; anything else as Construction.ending says.