text

python.Text.within

def Text.within (c : Nat) (ranges : List (Nat * Nat)) : Bool

Whether the code point c is in one of the ranges (both ends included).

python.Text.isSpace

def Text.isSpace (c : Nat) : Bool

Whether the code point c is whitespace (CPython’s str.isspace: every code point that is).

python.Text.isDigit

def Text.isDigit (c : Nat) : Bool

Whether the code point c is a decimal digit 0-9.

python.Text.isUpper

def Text.isUpper (c : Nat) : Bool

Whether the code point c is an ASCII capital letter.

python.Text.isLower

def Text.isLower (c : Nat) : Bool

Whether the code point c is an ASCII small letter.

python.Text.isCased

def Text.isCased (c : Nat) : Bool

Whether the code point c is an ASCII letter (a letter with case).

python.Character

data Character

What the model knows of a code point: a letter with case (an ASCII letter), a code point without case (whether it is a letter, a decimal digit, whitespace), or one past what the model classifies.

python.Text.caselessLetters

def Text.caselessLetters : List (Nat * Nat)

The letters without case the model knows (CPython’s str.isalpha): iteration marks, kana, bopomofo, CJK ideographs, Hangul syllables, halfwidth kana and Hangul.

python.Text.caselessBlocks

def Text.caselessBlocks : List (Nat * Nat)

The blocks whose other code points are known to be without case and neither letters, digits nor whitespace: general punctuation, CJK symbols, kana, bopomofo, halfwidth and fullwidth forms (but the fullwidth Latin letters, which have case).

python.Text.character

def Text.character (c : Nat) : Character

What the model knows of the code point c.

python.Text.classified

def Text.classified (cs : Codes) : Bool

Whether the model knows the class of every code point of the text cs.

python.Text.asciiDigit

def Text.asciiDigit (c : Nat) : Nat

The code point c as CPython reads numbers: a fullwidth digit as its ASCII digit, whitespace as a space.

python.Text.upper

def Text.upper (c : Nat) : Nat

The code point c in capitals (ASCII only).

python.Text.lower

def Text.lower (c : Nat) : Nat

The code point c in small letters (ASCII only).

python.Text.dropWhile

def Text.dropWhile (p : Nat -> Bool) (cs : Codes) : Codes

The code points of cs after the leading ones that p holds for.

python.Text.takeWhile

def Text.takeWhile (p : Nat -> Bool) (cs : Codes) : Codes

The leading code points of cs that p holds for.

python.Text.dropEnd

def Text.dropEnd (p : Nat -> Bool) (cs : Codes) : Codes

The code points of cs without the trailing ones that p holds for.

python.Text.strip

def Text.strip (cs : Codes) : Codes

The code points of cs without whitespace at either end (s.strip()).

python.Text.same

def Text.same (a : Codes) (b : Codes) : Bool

Whether the texts a and b are the same.

python.Text.wordsWithin

def Text.wordsWithin (fuel : Nat) (cs : Codes) : List Codes

The words of cs between whitespace (s.split(): runs of whitespace are one separator, none at either end), within fuel words.

python.Text.words

def Text.words (cs : Codes) : List Codes

The words of cs between whitespace (s.split()).

python.Text.splitWithin

def Text.splitWithin (fuel : Nat) (separator : Codes) (piece : Codes) (cs : Codes) : List Codes

The pieces of cs between occurrences of separator (not empty), after piece, the current piece so far, within fuel steps.

python.Text.split

def Text.split (separator : Codes) (cs : Codes) : List Codes

The pieces of cs between occurrences of separator (s.split(sep), separator not empty).

python.Text.usedUp

def Text.usedUp (k : Option Nat) : Bool

Whether k, the count of replacements left, is used up (none: no limit).

python.Text.oneLess

def Text.oneLess (k : Option Nat) : Option Nat

One replacement fewer left than k (none stays none).

python.Text.replaceWithin

def Text.replaceWithin (fuel : Nat) (old : Codes) (new : Codes) (k : Option Nat) (cs : Codes) : Codes

s.replace(old, new, k) on cs: old (not empty) replaced by new at most k times, within fuel steps.

python.Text.replaceEmpty

def Text.replaceEmpty (new : Codes) (k : Option Nat) (cs : Codes) : Codes

s.replace("", new, k) on cs: new before each code point and at the end, at most k times.

python.Text.replace

def Text.replace (old : Codes) (new : Codes) (k : Option Nat) (cs : Codes) : Codes

s.replace(old, new, k) on cs: old replaced by new at most k times (k none: every occurrence).

python.Text.countWithin

def Text.countWithin (fuel : Nat) (part : Codes) (cs : Codes) : Nat

How many times part (not empty) occurs in cs without overlapping, within fuel steps.

python.Text.count

def Text.count (part : Codes) (cs : Codes) : Nat

s.count(part) on cs for a part that is not empty.

python.Text.title

def Text.title (afterCased : Bool) (cs : Codes) : Codes

s.title() on cs: a letter with case in capitals after a code point without case, in small letters after one with case (afterCased: whether the code point before had case).

python.Text.digits

def Text.digits (value : Nat) (afterDigit : Bool) (cs : Codes) : Option Nat

The decimal digits cs with single underscores between digits as a natural (value is the value so far, afterDigit whether the code point before was a digit); none for anything else, or nothing.

python.Text.digitsAfterUnderscore

def Text.digitsAfterUnderscore (value : Nat) (cs : Codes) : Option Nat

The digits cs after an underscore, with value the value so far: a digit must come next.

python.Text.sign

def Text.sign (cs : Codes) : Bool * Codes

A leading sign taken off cs: whether it was a minus, and the rest.

python.Text.signedInt

def Text.signedInt (negative : Bool) (n : Nat) : Int

The natural n as an int, negated when negative.

python.Text.toInt

def Text.toInt (cs : Codes) : Option Int

int(s) of the decimal text cs: none when it is not one.

python.Text.exponent

def Text.exponent (cs : Codes) : Option Int

A decimal exponent’s text cs after e: a sign and digits.

python.Text.optionalDigits

def Text.optionalDigits (cs : Codes) : Option Nat

The digits cs that may be absent: zero when there are none.

python.Text.decimal

def Text.decimal (negative : Bool) (cs : Codes) : Option Float

A decimal float’s text cs without its sign (negative when it was a minus): digits, a fraction, an exponent (e or E), correctly rounded.

python.Text.toFloat

def Text.toFloat (cs : Codes) : Option Float

float(s) of the text cs: a decimal, or inf, infinity, nan in any case, with a sign; none when it is none of these.