arithmetic

cfamily.Evaluated

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

A value with the notes made on the way, a stop, or out of fuel.

cfamily.Evaluated.bind

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

The notes of the first, then the second’s (a stop drops them: the stop is what is reported).

cfamily.Evaluated.of

def Evaluated.of {L : Constructs} {A : Type} (a : A) : Evaluated L A

A value with no notes.

cfamily.Evaluated.stop

def Evaluated.stop {L : Constructs} {A : Type} (n : NodeId) (b : Behavior) : Evaluated L A

A stop at a node for a behavior the standard leaves open.

cfamily.Evaluated.noting

def Evaluated.noting {L : Constructs} {A : Type} (n : NodeId) (b : Behavior) (x : Evaluated L A) : Evaluated L A

A result with a behavior the standard leaves open noted at a node (the verdict is unknown unless a later stop decides it).

cfamily.Evaluated.noted

def Evaluated.noted {L : Constructs} {A : Type} (n : NodeId) (b : Behavior) (a : A) : Evaluated L A

A value, with a note at a node.

cfamily.Evaluated.integer

def Evaluated.integer {L : Constructs} (v : Int) : Evaluated L Value

An integer value.

cfamily.Value.ofTruth

def Value.ofTruth (b : Bool) : Int

1 for true, 0 for false (the value of a comparison, C11 6.5.8p6).

cfamily.Value.integer

def Value.integer (v : Value) : Int

The integer of a value (the checker guarantees it is one).

cfamily.Value.pointer

def Value.pointer (v : Value) : Pointer

The pointer of a value.

cfamily.Value.floating

def Value.floating (v : Value) : Float

The floating value of a value.

cfamily.Value.truth

def Value.truth (v : Value) : Bool

Whether a scalar is true: not zero, not null (C11 6.8.4.1p2); NaN is true.

cfamily.IntegerType.result

def IntegerType.result {L : Constructs} (n : NodeId) (t : IntegerType) (operator : String) (operands : List Int) (v : Int) : Evaluated L Value

The result v at the node n of an operation in the type t, by operator on operands: a signed one in range, else overflow (with the operation, as the problem’s details); an unsigned one wrapped.

cfamily.IntegerType.divide

def IntegerType.divide {L : Constructs} (n : NodeId) (t : IntegerType) (remainder : Bool) (a : Int) (b : Int) : Evaluated L Value

a / b or a % b: b is not zero, and a signed quotient is in range.

cfamily.IntegerType.shift

def IntegerType.shift {L : Constructs} (intoUnsigned : Bool) (n : NodeId) (t : IntegerType) (left : Bool) (a : Int) (b : Int) : Evaluated L Value

a << b or a >> b: 0 <= b < width; a signed left shift needs a >= 0 and an in-range result.

cfamily.IntegerType.bitwise

def IntegerType.bitwise (t : IntegerType) (op : BinaryOp) (a : Int) (b : Int) : Int

A bitwise operation on the values’ representations in the type’s width.

cfamily.BinaryOp.compareIntegers

def BinaryOp.compareIntegers (op : BinaryOp) (a : Int) (b : Int) : Bool

A comparison of integers.

cfamily.IntegerType.binary

def IntegerType.binary {L : Constructs} (rules : Rules) (n : NodeId) (t : IntegerType) (op : BinaryOp) (a : Int) (b : Int) : Evaluated L Value

A binary operation on integers of a type (the operands already converted to it).

cfamily.IntegerType.unary

def IntegerType.unary {L : Constructs} (n : NodeId) (t : IntegerType) (op : UnaryOp) (v : Value) : Evaluated L Value

A unary operation: -a (overflow for the least signed value), !a, ~a, +a (the promoted value itself).

cfamily.Value.toInteger

def Value.toInteger (t : IntegerType) (v : Value) : Int

A value converted to an integer type: to _Bool its truth (C11 6.3.1.2p1), else wrapped (6.3.1.3; a signed result out of range is implementation-defined, and every implementation wraps).

cfamily.Float.toInteger

def Float.toInteger {L : Constructs} (n : NodeId) (t : IntegerType) (x : Float) : Evaluated L Value

A floating value converted to an integer type: to _Bool its truth, else truncated, which must be in range (C11 6.3.1.4p1; what out of range means is the dialect’s rule, read when the run is judged).

cfamily.BinaryOp.compareFloats

def BinaryOp.compareFloats (op : BinaryOp) (x : Float) (y : Float) : Bool

A comparison of floating values (IEEE: NaN is unordered, so only != holds).

cfamily.Float.divideBy

def Float.divideBy {L : Constructs} (rules : Rules) (n : NodeId) (f : FloatFormat) (x : Float) (y : Float) : Evaluated L Value

x / y: the IEEE result; dividing by zero is noted where the dialect’s standard leaves it undefined.

cfamily.Float.binary

def Float.binary {L : Constructs} (rules : Rules) (n : NodeId) (f : FloatFormat) (op : BinaryOp) (x : Float) (y : Float) : Evaluated L Value

A binary operation on floating values of a format.