conversion

cfamily.CheckResult

data CheckResult (L : Constructs) (A : Type)

The result of checking: a value, a refusal at a node, a construct at a node the model does not provide (named: the program may well be valid, so its verdict is unknown, not reject), or a request of the dialect’s (with the types and written types it carries); checking starts again once the dialect has answered it.

cfamily.rejected

def rejected {L : Constructs} {A : Type} (n : NodeId) (reason : String) : CheckResult L A

A rejection at the node n with the reason in words (not structured yet).

cfamily.undeclaredName

def undeclaredName {L : Constructs} {A : Type} (n : NodeId) (name : String) (what : String) (header : Option String) : CheckResult L A

The name nothing declares, used at the node n as what (variable, function, or name), with the header that declares it when a standard one does (Refusal.undeclared).

cfamily.CheckResult.bind

def CheckResult.bind {L : Constructs} {A : Type} {B : Type} (x : CheckResult L A) (f : A -> CheckResult L B) : CheckResult L B

Checking f on the value, if there is one.

cfamily.CheckResult.within

def CheckResult.within {L : Constructs} {A : Type} (context : String) (r : CheckResult L A) : CheckResult L A

A conversion’s refusal from r as made for the context it is in (initialization, return; without one an assignment’s), which its words depend on (Refusal.withContext).

cfamily.checkMonad

instance checkMonad (L : Constructs) : Monad (CheckResult L)

Checking is a monad: x <- e in do is CheckResult.bind.

cfamily.Ty.integer

def Ty.integer {L : Constructs} (t : Ty L) : Option IntegerType

The integer type of a type, if it is one (const aside).

cfamily.Ty.isScoped

def Ty.isScoped {L : Constructs} (t : Ty L) : Bool

Whether the type t is a scoped enumeration (C++’s enum class): it takes part in arithmetic and conversions only as itself ([conv.prom]p4, [conv.integral]p1), converting to an integer by a cast ([expr.static.cast]p9).

cfamily.Ty.integral

def Ty.integral {L : Constructs} (t : Ty L) : Option IntegerType

The integer type a value of the type t is as a switch’s condition or a cast’s operand: an integer’s, or an enumeration’s (a scoped one’s underlying type, [stmt.switch]p2, [expr.static.cast]p9).

cfamily.Ty.float

def Ty.float {L : Constructs} (t : Ty L) : Option FloatFormat

The floating format of a type, if it is one.

cfamily.Ty.isArithmetic

def Ty.isArithmetic {L : Constructs} (t : Ty L) : Bool

Whether the type is an arithmetic type (integer or floating).

cfamily.Ty.isPointer

def Ty.isPointer {L : Constructs} (t : Ty L) : Bool

Whether the type is a pointer type.

cfamily.Ty.pointee

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

The pointed-to type of a pointer type, else the type itself.

cfamily.Ty.voidPointer

def Ty.voidPointer {L : Constructs} : Ty L

The type void *.

cfamily.Ty.isVoidPointer

def Ty.isVoidPointer {L : Constructs} (t : Ty L) : Bool

Whether the type is void * (with any qualifiers on the void).

cfamily.Ty.isScalar

def Ty.isScalar {L : Constructs} (t : Ty L) : Bool

Whether the type is a scalar type: arithmetic or pointer (C11 6.2.5p21).

cfamily.TypedExpr.isNullConstant

def TypedExpr.isNullConstant {L : Constructs} (e : TypedExpr L) : Bool

Whether an expression is a null pointer constant: the integer 0 or a null pointer (C11 6.3.2.3p3).

cfamily.TypedExpr.nullAs

def TypedExpr.nullAs {L : Constructs} (e : TypedExpr L) (t : Ty L) : TypedExpr L

A null pointer constant as the null pointer of a pointer type, at its node.

cfamily.TypedExpr.rvalue

def TypedExpr.rvalue {L : Constructs} (p : Platform) (e : TypedExpr L) : TypedExpr L

The value of an lvalue: an array decays to a pointer to its first element (C11 6.3.2.1p3).

cfamily.TypedExpr.toIntegerType

def TypedExpr.toIntegerType {L : Constructs} (p : Platform) (t : IntegerType) (e : TypedExpr L) : TypedExpr L

An integer value converted to an integer type (unchanged if it has the type).

cfamily.TypedExpr.toFloatFormat

def TypedExpr.toFloatFormat {L : Constructs} (p : Platform) (f : FloatFormat) (e : TypedExpr L) : TypedExpr L

An arithmetic value converted to a floating format (unchanged if it has the format).

cfamily.Ty.widerFloat

def Ty.widerFloat {L : Constructs} (tgt : Target) (a : Ty L) (b : Ty L) : FloatFormat

The floating format of the usual arithmetic conversions: the wider of the floating operands (C11 6.3.1.8).

cfamily.IntegerType.ofDecimal

def IntegerType.ofDecimal (p : Platform) (v : Int) : Option IntegerType

The type of a decimal integer constant: the first of int, long, long long that holds it (C11 6.4.4.1p5).

cfamily.IntegerSuffix.of

def IntegerSuffix.of (written : String) : Option (Bool * Nat)

The suffixes an integer constant may have (C11 6.4.4.1p1: u, l or ll in either case, in either order; not lL), as whether unsigned and how many l.

cfamily.IntegerType.candidates

def IntegerType.candidates (p : Platform) (unsigned : Bool) (longs : Nat) (decimal : Bool) : List IntegerType

The types an integer constant may have, in order (C11 6.4.4.1p5): from int, long or long long by its l’s; only the unsigned ones with u; a constant not in decimal may also be the unsigned type of each rank.

cfamily.IntegerType.ofWritten

def IntegerType.ofWritten (p : Platform) (v : Int) (suffix : String) (decimal : Bool) : Option IntegerType

The type of an integer constant as written: the first candidate that holds its value; none when the suffix is not one or no candidate holds it.

cfamily.BinaryOp.isShift

def BinaryOp.isShift (op : BinaryOp) : Bool

Whether a binary operator is a shift.

cfamily.Rules.truthType

def Rules.truthType (rules : Rules) (p : Platform) : IntegerType

The type of a truth value under the rules on platform p: bool in C++, int in C (Rules.truthIsBool).

cfamily.BinaryOp.isLogical

def BinaryOp.isLogical (op : BinaryOp) : Bool

Whether a binary operator is && or ||.

cfamily.BinaryOp.isEquality

def BinaryOp.isEquality (op : BinaryOp) : Bool

Whether a binary operator is == or !=.

cfamily.BinaryOp.isRelational

def BinaryOp.isRelational (op : BinaryOp) : Bool

Whether a binary operator is <, <=, > or >=.

cfamily.BinaryOp.takesFloat

def BinaryOp.takesFloat (op : BinaryOp) : Bool

Whether a binary operator applies to floating operands: + - * / and the comparisons (C11 6.5.5p2, 6.5.7p2).

cfamily.TypedExpr.integerBinaryOf

def TypedExpr.integerBinaryOf {L : Constructs} (p : Platform) (truth : IntegerType) (n : NodeId) (op : BinaryOp) (s : IntegerType) (t : IntegerType) (a : TypedExpr L) (b : TypedExpr L) : TypedExpr L

Two integer operands: arithmetic in the common type, a shift in the promoted left type, a comparison of the operands in the common type giving the truth type.

cfamily.TypedExpr.pointerBinaryOf

def TypedExpr.pointerBinaryOf {L : Constructs} (ext : TypeExtension L) (p : Platform) (truth : IntegerType) (n : NodeId) (wrong : String -> Refusal) (op : BinaryOp) (a : TypedExpr L) (b : TypedExpr L) : CheckResult L (TypedExpr L)

Operands with a pointer (C11 6.5.6, 6.5.8, 6.5.9): pointer plus or minus an integer, the difference of two pointers of one type, comparisons of pointers of one type or with a null pointer constant (of the truth type). op is the operator at node n with operands a and b; ext writes the dialect’s types, p is the platform’s sizes, and wrong makes the refusal from the operands’ types written out.

cfamily.TypedExpr.floatBinaryOf

def TypedExpr.floatBinaryOf {L : Constructs} (tgt : Target) (truth : IntegerType) (n : NodeId) (wrong : String -> Refusal) (op : BinaryOp) (a : TypedExpr L) (b : TypedExpr L) : CheckResult L (TypedExpr L)

Floating operands (one at least): converted to the wider format, arithmetic giving it and a comparison the truth type; % shifts and bitwise operators are rejected. op is the operator at node n with operands a and b, tgt the target’s floating formats, and wrong makes the refusal from the operands’ types written out.

cfamily.TypedExpr.scopedBinaryOf

def TypedExpr.scopedBinaryOf {L : Constructs} (ext : TypeExtension L) (p : Platform) (truth : IntegerType) (n : NodeId) (wrong : String -> Refusal) (op : BinaryOp) (a : TypedExpr L) (b : TypedExpr L) : CheckResult L (TypedExpr L)

A binary operator with an operand of a scoped enumeration (C++‘s enum class): only a comparison of two values of the same one, compared as their underlying type ([expr.rel]p6, [expr.eq]p6: the built-in candidates are for the enumeration itself, [over.built]p15); anything else has no operator (clang: invalid operands to binary expression). op is the operator at node n with operands a and b; ext writes the dialect’s types, p is the platform, truth the comparison’s type, and wrong makes the refusal from the operands’ types written out.

cfamily.TypedExpr.binaryOf

def TypedExpr.binaryOf {L : Constructs} (ext : TypeExtension L) (g : Globals L) (tgt : Target) (truth : IntegerType) (n : NodeId) (op : BinaryOp) (a0 : TypedExpr L) (b0 : TypedExpr L) : CheckResult L (TypedExpr L)

A binary operator on two scalar values (struct operands and the dialect’s types are rejected): && and || take any scalars; with a floating operand, floating arithmetic; two integers; else pointers. The comparisons, && and || give the truth type (int in C, bool in C++). op is the operator at node n with operands a0 and b0; ext writes the dialect’s types for the program’s tables g, and tgt is the target.

cfamily.TypedExpr.unaryOf

def TypedExpr.unaryOf {L : Constructs} (rules : Rules) (p : Platform) (n : NodeId) (op : UnaryOp) (a0 : TypedExpr L) : CheckResult L (TypedExpr L)

A unary operator: ! on a scalar gives the truth type (int in C, bool in C++); - on a floating value stays floating;

• is the value itself (C11 6.5.3.3p2), of a pointer too where the dialect allows it; else the promoted integer.

cfamily.ConversionExtension

record ConversionExtension (L : Constructs)

How a dialect converts to and from its own types as if by assignment, or none for the core’s rules (C++: a C string to std::string, an object of a derived class to its base, a value bound to a reference): the converted expression with the statements it needs first (a temporary a const reference binds to).

cfamily.ConversionExtension.empty

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

The conversion extension of a dialect without types of its own.

cfamily.TypedExpr.conditionalType

def TypedExpr.conditionalType {L : Constructs} (ext : TypeExtension L) (tgt : Target) (keepsSame : Bool) (n : NodeId) (a : TypedExpr L) (b : TypedExpr L) : CheckResult L (Ty L)

The type of c ? a : b from the operands’ values (C11 6.5.15p3-6): arithmetic operands give their common type, or their own type when they have the same one and keepsSame (the dialect’s rule, C++ [expr.cond]p7); pointers of one type, a pointer and a null pointer constant, void * and an object pointer; one struct type.

cfamily.TypedExpr.conditionalOther

def TypedExpr.conditionalOther {L : Constructs} (ext : TypeExtension L) (n : NodeId) (a : TypedExpr L) (b : TypedExpr L) (aType : Ty L) (bType : Ty L) : CheckResult L (Ty L)

The type of c ? a : b when a is not an integer.

cfamily.TypedExpr.castTo

def TypedExpr.castTo {L : Constructs} (p : Platform) (ext : TypeExtension L) (n : NodeId) (t : Ty L) (a0 : TypedExpr L) : CheckResult L (TypedExpr L)

A cast (C11 6.5.4): to an arithmetic type from an arithmetic value (or a pointer to _Bool); to a pointer from a null pointer constant, a pointer of that type, or a pointer to a character type when it is to one too (the same object’s bytes, C11 6.3.2.3p7); casts to arrays and structs are not allowed.

cfamily.Ty.noArithmeticConversion

def Ty.noArithmeticConversion {L : Constructs} (source : Ty L) (target : String) : String * Option String

Why a value of the non-arithmetic type source does not convert to an arithmetic one (target is “Integer” or “Floating”), as Refusal.noConversion’s what and name: from a pointer, from a class or other named type (by its name), or from another type.

cfamily.TypedExpr.assignArithmetic

def TypedExpr.assignArithmetic {L : Constructs} (p : Platform) (n : NodeId) (wrong : String -> Option String -> Refusal) (t : Ty L) (a : TypedExpr L) : CheckResult L (TypedExpr L)

The conversion as if by assignment to an arithmetic type (C11 6.5.16.1): from an arithmetic value, or a pointer to _Bool (6.3.1.2); a value that does not convert is refused as wrong makes it from its what and name. a is the value at node n converted to t, with the platform p’s sizes.

cfamily.TypedExpr.assignPointer

def TypedExpr.assignPointer {L : Constructs} (rules : Rules) (ext : TypeExtension L) (p : Platform) (n : NodeId) (wrong : String -> Option String -> Refusal) (t : Ty L) (a0 : TypedExpr L) : CheckResult L (TypedExpr L)

The conversion as if by assignment to a pointer type: a null pointer constant, a pointer of the same type, or between void * and object pointers where the rules allow it; the const of the pointed-to type is kept. a0 is the value at node n converted to t; ext writes the dialect’s types, p is the platform, and wrong makes the refusal from its what and name.

cfamily.TypedExpr.assignTo

def TypedExpr.assignTo {L : Constructs} (rules : Rules) (types : TypeExtension L) (g : Globals L) (p : Platform) (n : NodeId) (t : Ty L) (a : TypedExpr L) : CheckResult L (TypedExpr L)

The core’s conversion as if by assignment (C11 6.5.16.1): arithmetic, pointers, and structs and unions of the same type copied whole; arrays and functions cannot be assigned (a dialect’s own conversions come first, CheckDialect.assignLifted). A value that does not convert is refused with its type and the target’s, written as the dialect’s types write them for the program’s tables g. a is the value at node n converted to t, under the dialect’s rules and the platform p.