variables

cfamily.Param.declarationName

def Param.declarationName (p : Param) : DeclId * String

A parameter’s declaration and name.

cfamily.Item.declarationNames

def Item.declarationNames (it : Item) : List (DeclId * String)

The declarations of an item: a global, or a function’s parameters and body.

cfamily.Dialect.names

def Dialect.names {L : Constructs} (d : Dialect L) (p : Program) : List (DeclId * String)

The names of a program’s declarations (declaration node to source name), after the dialect’s passes; not those of the library’s C functions it uses (the host shows their calls without variables).

cfamily.View

record View (L : Constructs)

What writing values needs: the names, the declarations of the blocks, the memory, how types are written, and the platform.

cfamily.View.nameOf

def View.nameOf {L : Constructs} (v : View L) (x : DeclId) : String

The source name of a declaration (its node when it has none).

cfamily.View.hasName

def View.hasName {L : Constructs} (v : View L) (x : DeclId) : Bool

Whether a declaration has a source name (temporaries the checker made have none and are not shown).

cfamily.View.declarationOf

def View.declarationOf {L : Constructs} (v : View L) (b : Nat) : Option DeclId

The declaration a block belongs to, if any.

cfamily.View.blockType

def View.blockType {L : Constructs} (v : View L) (b : Nat) : Ty L

The type of a block’s object (int when the block is gone).

cfamily.View.path

def View.path {L : Constructs} (t : Ty L) (path : List Nat) : String

A path written by the types along it: [k] in arrays, .f in structs and unions.

cfamily.View.fieldPath

def View.fieldPath {L : Constructs} (fs : List (FieldTy L)) (k : Nat) (rest : List Nat) : String

The k-th member’s part of a path, then the rest.

cfamily.View.escape

def View.escape (s : String) : String

A string written as a C string literal’s contents (newline, double quote and backslash escaped).

cfamily.View.pointer

def View.pointer {L : Constructs} (v : View L) (p : Pointer) : String

A pointer written as C: NULL, the stream, a literal, &x, &a[2], &s.f, &x + 1, (heap b)…, (dangling).

cfamily.View.value

def View.value {L : Constructs} (v : View L) (x : Value) : String

A scalar value written as C.

cfamily.View.activeBits

def View.activeBits {L : Constructs} (v : View L) (fs : List (FieldTy L)) (places : List Placed) (k : Nat) (bits : List ObjectBit) : String

A union kept as bits: its k-th member as .name = value.

cfamily.View.designated

def View.designated {L : Constructs} (v : View L) (t : Ty L) (o : Object) : Option String

What a variable of a type that designates an object (a reference) shows: the object its address points to, of the type’s child; none when the address is not an object’s.

cfamily.View.memberNamed

def View.memberNamed {L : Constructs} (name : String) (fs : List (FieldTy L)) (xs : List Object) : Option (Ty L * Object)

A member’s object of an aggregate by its name, with its type.

cfamily.View.elementsAt

def View.elementsAt {L : Constructs} (v : View L) (u : Ty L) (count : Nat) (p : Value) : Option (Ty L * List Object)

The elements of type u from where a pointer value points in an array block: count of them (none for any other value).

cfamily.View.countOf

def View.countOf (o : Object) : Nat

The count an integer member holds (0 when it holds none).

cfamily.View.pointedElements

def View.pointedElements {L : Constructs} (v : View L) (stored : Ty L * Object) (count : Nat) : Option (Ty L * List Object)

The elements a pointer member points to, count of them.

cfamily.View.sequenceElements

def View.sequenceElements {L : Constructs} (v : View L) (fs : List (FieldTy L)) (xs : List Object) : Option (Ty L * List Object)

The elements a sequence’s members say it has: size_ of them from where data_ points (none when they cannot be read), with their type.

cfamily.View.shallow

def View.shallow {L : Constructs} (v : View L) (o : Object) : String

An element of a sequence as a debugger shows it: a scalar’s value (? if indeterminate), an aggregate as {...} (the elements come from the memory, not from inside the object: they are not shown deeper).

cfamily.View.sequence

def View.sequence {L : Constructs} (v : View L) (characters : Bool) (fs : List (FieldTy L)) (xs : List Object) : String

A sequence as a debugger’s pretty printer shows it: characters as a string literal, elements as {a, b}; {...} when its elements cannot be read.

cfamily.View.variable

def View.variable {L : Constructs} (v : View L) (x : DeclId) (c : Block L) : Json

A variable as JSON: {id, name, type, value, declNode}; the value is null for an uninitialized scalar, and a reference’s is what it refers to.

cfamily.View.variables

def View.variables {L : Constructs} (v : View L) (scopes : List Scope) : List Json

The named variables of scopes, innermost first.

cfamily.Activation

record Activation

A level of the call stack: its function, the node it is at, its scopes.

cfamily.Frame.activations

def Frame.activations {L : Constructs} (entry : String) (node : NodeId) (scopes : List Scope) (k : List (Frame L)) : List Activation

The levels of the call stack from the frames out, innermost first: each call frame ends a level (the callee) and the next one is at the call’s node with the saved scopes; the last is the run’s entry (of the name given).

cfamily.Configuration.activations

def Configuration.activations {L : Constructs} (entry : String) (node : NodeId) (x : Configuration L) : List Activation

The levels of a configuration stopped at a node (the outermost is the run’s entry, of the name given).

cfamily.Dialect.platform

def Dialect.platform {L : Constructs} (d : Dialect L) : Platform

The dialect’s platform.

cfamily.Dialect.view

def Dialect.view {L : Constructs} (d : Dialect L) (tt : TypeText L) (names : List (DeclId * String)) (levels : List Activation) (s : State L) : View L

The view of a stopped configuration’s state.

cfamily.Activation.frame

def Activation.frame {L : Constructs} (v : View L) (a : Activation) : DapFrame

A level as the host shows it, its variables without the global scope.

cfamily.Dialect.frames

def Dialect.frames {L : Constructs} (d : Dialect L) (tt : TypeText L) (names : List (DeclId * String)) (node : NodeId) (x : Configuration L) : String

The call stack as JSON, innermost first; each level’s variables without the global scope.

cfamily.Dialect.globals

def Dialect.globals {L : Constructs} (d : Dialect L) (tt : TypeText L) (names : List (DeclId * String)) (x : Configuration L) : String

The global variables as JSON.

cfamily.State.feed

def State.feed {L : Constructs} (s : State L) (text : String) : State L

The state with more standard input (the host’s text, as the bytes the program reads).

cfamily.Configuration.feed

def Configuration.feed {L : Constructs} (text : String) (x : Configuration L) : Configuration L

More standard input for a paused run.

cfamily.View.decimal

def View.decimal (cs : List Nat) : Option Int

An integer written in decimal with an optional sign, if the text is one.

cfamily.View.character

def View.character (t : IntegerType) (cs : List Nat) : Option Int

A character constant ‘c’ as a character type’s value (a signed char’s above 127 is negative).

cfamily.View.integerOf

def View.integerOf (t : IntegerType) (text : String) : Option Int

An integer of the type from the text a user writes: decimal with an optional sign; true or false for bool; ‘c’ for a character type.

cfamily.Activation.scopesAt

def Activation.scopesAt (levels : List Activation) (n : Nat) : Option (List Scope)

The scopes of the n-th level (0 is the innermost).

cfamily.Configuration.setVariable

def Configuration.setVariable {L : Constructs} (n : Nat) (x : DeclId) (text : String) (c : Configuration L) : Either String (Configuration L)

Sets an integer variable of the n-th level from its source text: the error says why when it cannot.