literals

cfamily.Text.digitValue

def Text.digitValue (c : Nat) : Nat

The value of a digit (letters for 10 to 15), 99 if it is none.

cfamily.FloatToken

record FloatToken

A floating value read from text: the value, how many codes it used, and whether it is out of range.

cfamily.FloatToken.after

def FloatToken.after (k : Nat) (t : FloatToken) : FloatToken

The token having used k more codes (a sign, a prefix).

cfamily.Text.lower

def Text.lower (c : Nat) : Nat

A code in lower case.

cfamily.Text.digitIn

def Text.digitIn (base : Nat) (c : Nat) : Option Nat

The value of a digit in base 10 or 16, if it is one.

cfamily.Digits

record Digits

Digits of a base: the value, how many, and the codes after them.

cfamily.Text.digits

def Text.digits (base : Nat) (acc : Nat) (count : Nat) (cs : List Nat) : Digits

The digits at the front in a base (acc and count so far).

cfamily.Text.startsWith

def Text.startsWith (c : Nat) (cs : List Nat) : Bool

Whether the codes start with c.

cfamily.Text.exponent

def Text.exponent (cs : List Nat) : Int * Nat

An exponent after e or p: an optional sign and at least one digit; with no digit, none of it counts (1e reads only 1). The count includes the e or p.

cfamily.Text.outOfRange

def Text.outOfRange (f : FloatFormat) (v : Float) : Bool

Whether a rounded value is out of range: infinite, or zero or subnormal (below 2^(precision - 1) in mantissa).

cfamily.Text.value

def Text.value (f : FloatFormat) (binary : Bool) (negative : Bool) (m : Nat) (e : Int) : FloatToken

m * 10^e rounded to the format f (m * 2^e when binary), negated when negative; beyond any range of the format it overflows or underflows without computing the power (the bound grows with the format’s exponent range: a long double reaches 1e4932).

cfamily.Text.number

def Text.number (f : FloatFormat) (base : Nat) (negative : Bool) (cs : List Nat) : Option FloatToken

A number in a base (10, or 16 after 0x): digits [. digits] [e or p exponent], at least one digit.

cfamily.Text.hexadecimal

def Text.hexadecimal (f : FloatFormat) (negative : Bool) (cs : List Nat) : Option FloatToken

A hexadecimal number after 0x (with no hexadecimal digit after it, it is not one: only the 0 is read).

cfamily.Text.startsWithWord

def Text.startsWithWord (word : List Nat) (cs : List Nat) : Bool

Whether the codes start with the word (in any case).

cfamily.Text.special

def Text.special (negative : Bool) (cs : List Nat) : Option FloatToken

inf, infinity or nan, in any case.

cfamily.Text.toFloat

def Text.toFloat (f : FloatFormat) (cs : List Nat) : Option FloatToken

strtod without skipping white space: after an optional sign, the longest valid prefix (hexadecimal, inf or nan, decimal), none if there is none.

cfamily.Literal.float

def Literal.float (format : FloatFormat) (text : String) : Option Float

The value of a floating constant as written: the whole text read as strtod reads it (decimal or hexadecimal, an optional sign as the syntax may send for a negated constant); none if the text is not one.