formatting

cfamily.Flags

record Flags

The flags of a conversion: - (left), + (sign), space, # (alternative form), 0 (zeros).

cfamily.Flags.cleared

def Flags.cleared : Flags

No flags.

cfamily.Count

data Count

A width or a precision: not given, a number, or * (from an int argument).

cfamily.LengthModifier

data LengthModifier

A length modifier: none, hh, h, l, ll, z (size_t), j (intmax_t), t (ptrdiff_t), L (long double).

cfamily.FloatStyle

data FloatStyle

How %f, %e, %g write a floating value.

cfamily.ConversionKind

data ConversionKind

What a conversion writes: d i, u, o, x X, c, s, f F e E g G.

cfamily.Conversion

record Conversion

A conversion specification.

cfamily.FormatPiece

data FormatPiece

A piece of a format: a character as is, %%, or a conversion.

cfamily.PrintArgument

data PrintArgument

An argument after the default argument promotions: an integer of its type, a string (its bytes up to the null, or up to a precision: none where reading them is undefined), a double, or a long double (of a format other than double’s).

cfamily.Parsed

record Parsed (A : Type)

A value parsed from the front of a format, and the codes after it.

cfamily.Flags.add

def Flags.add (f : Flags) (c : Nat) : Option Flags

The flags with one more, if the code is a flag.

cfamily.Format.flags

def Format.flags (f : Flags) (cs : List Nat) : Parsed Flags

The flags at the front.

cfamily.Format.isDigit

def Format.isDigit (c : Nat) : Bool

Whether a code is a decimal digit.

cfamily.Format.number

def Format.number (acc : Nat) (cs : List Nat) : Parsed Nat

The decimal number at the front (acc so far).

cfamily.Format.givenCount

def Format.givenCount (cs : List Nat) : Parsed Count

A count from a number at the front.

cfamily.Format.width

def Format.width (cs : List Nat) : Parsed Count

The width: *, digits, or none.

cfamily.Format.precision

def Format.precision (cs : List Nat) : Parsed Count

The precision: . then * or digits (none is 0), or no precision.

cfamily.Format.doubled

def Format.doubled (c : Nat) (single : LengthModifier) (double : LengthModifier) (cs : List Nat) : Parsed LengthModifier

The length after one h or l: doubled (hh, ll), or single.

cfamily.Format.lengthModifier

def Format.lengthModifier (cs : List Nat) : Parsed LengthModifier

The length modifier.

cfamily.Format.floatKind

def Format.floatKind (c : Nat) : Option ConversionKind

The floating conversion of a code: f F e E g G.

cfamily.Format.kind

def Format.kind (c : Nat) : Option ConversionKind

The conversion of a code.

cfamily.Conversion.isBare

def Conversion.isBare (c : Conversion) : Bool

Whether a conversion has nothing between % and its character (%% must be exactly that, C11 7.21.6.1p8).

cfamily.Format.parse

def Format.parse (format : String) : Option (List FormatPiece)

The pieces of a format, none if it is not a valid format.

cfamily.LengthModifier.argumentType

def LengthModifier.argumentType (p : Platform) (signed : Bool) (l : LengthModifier) : IntegerType

The type an integer conversion’s argument has after promotion (hh and h arguments were promoted to int).

cfamily.LengthModifier.writtenType

def LengthModifier.writtenType (p : Platform) (signed : Bool) (l : LengthModifier) : IntegerType

The type an integer is converted back to before it is written (hh and h to the narrow type).

cfamily.ConversionKind.isSigned

def ConversionKind.isSigned (k : ConversionKind) : Bool

Whether a conversion is d or i.

cfamily.PrintArgument.integerAs

def PrintArgument.integerAs (t : IntegerType) (a : PrintArgument) : Option Int

The integer of an argument read as a type: the same type, or its signed or unsigned counterpart with the value in both ranges (C11 7.16.1.1p2).

cfamily.Conversion.flagsFit

def Conversion.flagsFit (c : Conversion) : Bool

Whether the flags and precision suit the conversion: # only with o x X and floating, no 0 or precision with c, no 0 with s (C11 7.21.6.1p6).

cfamily.Format.ofCodes

def Format.ofCodes (codes : List Nat) : String

The characters of codes.

cfamily.Format.copies

def Format.copies (c : Nat) (k : Nat) : String

k copies of a character.

cfamily.Format.digit

def Format.digit (upper : Bool) (d : Nat) : Nat

The digit of a value below 16 (letters upper or lower).

cfamily.Format.digitsIn

def Format.digitsIn (base : Nat) (upper : Bool) (fuel : Nat) (n : Nat) (acc : List Nat) : List Nat

The digits of n in a base, most significant first (acc after them), within fuel.

cfamily.Format.inBase

def Format.inBase (base : Nat) (upper : Bool) (n : Nat) : String

n written in a base.

cfamily.Format.pad

def Format.pad (f : Flags) (width : Nat) (zerosAllowed : Bool) (lead : String) (body : String) : String

A field: the prefix and body padded to the width with spaces (left or right), or zeros after the prefix.

cfamily.Format.zeroPadded

def Format.zeroPadded (n : Nat) (s : String) : String

s padded on the left with zeros to n characters.

cfamily.ConversionKind.base

def ConversionKind.base (k : ConversionKind) : Nat

The base of an integer conversion.

cfamily.ConversionKind.upper

def ConversionKind.upper (k : ConversionKind) : Bool

Whether an integer conversion writes upper case.

cfamily.Format.integerDigits

def Format.integerDigits (k : ConversionKind) (alternative : Bool) (precision : Option Nat) (n : Nat) : String

An integer’s digits: the precision is the least count (default 1; precision 0 and value 0 write none); #o makes the first digit 0.

cfamily.Format.integerPrefix

def Format.integerPrefix (f : Flags) (k : ConversionKind) (v : Int) : String

An integer’s prefix: its sign (d, i), or 0x for #x of a nonzero value.

cfamily.Format.integer

def Format.integer (f : Flags) (width : Nat) (precision : Option Nat) (k : ConversionKind) (v : Int) : String

An integer conversion of a value (already converted back to the written type).

cfamily.Format.exponent

def Format.exponent (x : Int) (upper : Bool) : String

“e+05”: the exponent with a sign and at least two digits.

cfamily.Format.fixed

def Format.fixed (p : Nat) (v : Float) : String

%.pf of a finite value’s magnitude: the value rounded to p places, p digits after the point (none for p = 0).

cfamily.Format.scientific

def Format.scientific (p : Nat) (upper : Bool) (v : Float) : String

%.pe of a finite value’s magnitude: p + 1 significant digits, one before the point.

cfamily.Format.trimmed

def Format.trimmed (fraction : String) : String

The digits after the point with trailing zeros removed.

cfamily.Format.withPoint

def Format.withPoint (keep : Bool) (whole : String) (fraction : String) : String

A whole part and a fraction: with the fraction’s trailing zeros removed (and the point if none remain), unless kept (#g).

cfamily.Format.general

def Format.general (count : Nat) (keep : Bool) (upper : Bool) (s : Significant) : String

%.pg of a finite nonzero magnitude with P significant digits (P = p, or 1 for 0): fixed if the exponent X has -4 <= X < P, else scientific; trailing zeros removed unless kept (#).

cfamily.Format.generalOf

def Format.generalOf (p : Nat) (keep : Bool) (upper : Bool) (v : Float) : String

%.pg of a finite value’s magnitude.

cfamily.Format.pointAfterFirst

def Format.pointAfterFirst (s : String) : String

Inserts the point after the first digit (“3e+00” to “3.e+00”).

cfamily.Format.magnitude

def Format.magnitude (style : FloatStyle) (alternative : Bool) (upper : Bool) (p : Nat) (v : Float) : String

A floating conversion of a finite value’s magnitude; # keeps the point at precision 0 (f, e).

cfamily.Format.special

def Format.special (upper : Bool) (v : Float) : String

inf or nan, upper case for F E G.

cfamily.Format.isNegative

def Format.isNegative (v : Float) : Bool

Whether a floating value is negative (NaN has no sign here).

cfamily.Format.isFinite

def Format.isFinite (v : Float) : Bool

Whether a floating value is finite.

cfamily.Format.float

def Format.float (f : Flags) (width : Nat) (p : Nat) (style : FloatStyle) (upper : Bool) (v : Float) : String

A floating conversion: the sign apart (0 pads after it; inf and nan are not zero padded; NaN takes no + or space, as clang’s libc).

cfamily.Fields

record Fields

The width, the precision and the arguments left, after any * took an int argument (a negative width is the - flag, a negative precision is none).

cfamily.Fields.of

def Fields.of (f : Flags) (width : Nat) (rest : List PrintArgument) : Fields

Fields with a width and no precision yet.

cfamily.Fields.withPrecision

def Fields.withPrecision (w : Fields) (precision : Option Nat) (rest : List PrintArgument) : Fields

The fields with a precision and the arguments after it.

cfamily.Fields.width

def Fields.width (p : Platform) (f : Flags) (c : Count) (args : List PrintArgument) : Option Fields

The width of a conversion.

cfamily.Fields.precision

def Fields.precision (p : Platform) (c : Count) (w : Fields) : Option Fields

The precision of a conversion, after its width.

cfamily.Written

record Written

What a conversion writes, and the arguments after it.

cfamily.Format.integerArgument

def Format.integerArgument (p : Platform) (c : Conversion) (w : Fields) (a : PrintArgument) : Option String

An integer or character conversion of an argument.

cfamily.Format.textArgument

def Format.textArgument (c : Conversion) (w : Fields) (a : PrintArgument) : Option String

A string conversion: no length modifier (%ls is not in the subset), bytes read up to the precision.

cfamily.Format.floatArgument

def Format.floatArgument (c : Conversion) (w : Fields) (a : PrintArgument) : Option String

A floating conversion: no length or l (%lf is %f) with a double, L with a long double (C11 7.21.6.1p7); any other pairing is undefined (p9).

cfamily.Format.convert

def Format.convert (p : Platform) (c : Conversion) (args : List PrintArgument) : Option Written

A conversion of the next argument.

cfamily.Format.write

def Format.write (p : Platform) (pieces : List FormatPiece) (args : List PrintArgument) : Option (List String)

The pieces written with the arguments.

cfamily.Format.print

def Format.print (p : Platform) (format : String) (args : List PrintArgument) : Option String

printf’s output for a format and its arguments; none where the behavior is undefined (C11 7.21.6.1p9, and an output longer than INT_MAX, 7.21.6.1p15).