Convert a list of characters to Text.
$$\text{pack}([c_1, \ldots, c_n]) = \text{"c_1 \ldots c_n"}$$
Equations
- Data.Text.pack cs = String.ofList cs
Instances For
Convert Text to a list of characters.
$$\text{unpack}(t) = [t_0, t_1, \ldots, t_{n-1}]$$
Equations
- t.unpack = String.toList t
Instances For
A Text containing a single character.
$$\text{singleton}(c) = \text{"c"}$$
Equations
Instances For
Is the Text empty?
$$\text{null}(t) \iff |t| = 0$$
Equations
- t.null = String.isEmpty t
Instances For
The number of characters (code points) in the Text.
$$\text{length}(t) = |t|$$
Equations
- t.length = (String.toList t).length
Instances For
Compare the length of a Text against a Nat.
Returns Ordering.lt, Ordering.eq, or Ordering.gt.
$$\text{compareLength}(t, n) = \text{compare}(|t|, n)$$
Equations
- t.compareLength n = compare t.length n
Instances For
Apply a function to every character. $$\text{map}(f, t) = \text{pack}(\text{List.map}\ f\ (\text{unpack}\ t))$$
Equations
- Data.Text.map f t = Data.Text.pack (List.map f (String.toList t))
Instances For
Insert a separator Text between elements and concatenate.
$$\text{intercalate}(sep, [t_1, \ldots, t_k]) = t_1 \mathbin{+\!\!+} sep \mathbin{+\!\!+} \cdots \mathbin{+\!\!+} t_k$$
Equations
- sep.intercalate ts = String.intercalate sep ts
Instances For
Insert a character between each character of the Text.
$$\text{intersperse}(c, \text{"abc"}) = \text{"acbcc"}$$
Equations
- Data.Text.intersperse c t = match String.toList t with | [] => Data.Text.empty | [x] => Data.Text.singleton x | x :: xs => Data.Text.pack (x :: List.flatMap (fun (ch : Char) => [c, ch]) xs)
Instances For
Reverse the characters. $$\text{reverse}(\text{"abc"}) = \text{"cba"}$$
Equations
Instances For
Replace all non-overlapping occurrences of needle with replacement.
$$\text{replace}(\text{needle}, \text{replacement}, t)$$
Equations
- needle.replace replacement t = if String.isEmpty needle = true then t else have parts := String.splitOn t needle; String.intercalate replacement parts
Instances For
Case-fold: convert to lower case for case-insensitive comparisons.
$$\text{toCaseFold}(t) \approx \text{toLower}(t)$$
Note: Full Unicode case folding is approximated by toLower.
Equations
Instances For
Convert all characters to lower case. $$\text{toLower}(\text{"ABC"}) = \text{"abc"}$$
Equations
Instances For
Convert all characters to upper case. $$\text{toUpper}(\text{"abc"}) = \text{"ABC"}$$
Equations
Instances For
Title case: capitalize the first character, lowercase the rest. $$\text{toTitle}(\text{"hello world"}) = \text{"Hello world"}$$
Equations
- t.toTitle = match String.toList t with | [] => Data.Text.empty | c :: cs => Data.Text.pack (c.toUpper :: List.map Data.Text.charToLower✝ cs)
Instances For
Left-justify to width n with fill character c.
$$\text{justifyLeft}(n, c, t) = t \mathbin{+\!\!+} \text{replicate}(n - |t|, c)$$
Equations
- Data.Text.justifyLeft n c t = if t.length ≥ n then t else t ++ Data.Text.pack (List.replicate (n - t.length) c)
Instances For
Right-justify to width n with fill character c.
$$\text{justifyRight}(n, c, t) = \text{replicate}(n - |t|, c) \mathbin{+\!\!+} t$$
Equations
- Data.Text.justifyRight n c t = if t.length ≥ n then t else Data.Text.pack (List.replicate (n - t.length) c) ++ t
Instances For
Left fold over characters. $$\text{foldl}(f, z, t) = f(\ldots f(f(z, t_0), t_1) \ldots, t_{n-1})$$
Equations
- Data.Text.foldl f z t = List.foldl f z (String.toList t)
Instances For
Strict left fold (same as foldl in Lean since evaluation is strict).
$$\text{foldl'}(f, z, t) = \text{foldl}(f, z, t)$$
Equations
- Data.Text.foldl' f z t = Data.Text.foldl f z t
Instances For
Right fold over characters. $$\text{foldr}(f, z, t) = f(t_0, f(t_1, \ldots f(t_{n-1}, z)))$$
Equations
- Data.Text.foldr f z t = List.foldr f z (String.toList t)
Instances For
Concatenate a list of Texts.
$$\text{concat}([t_1, \ldots, t_k]) = t_1 \mathbin{+\!\!+} \cdots \mathbin{+\!\!+} t_k$$
Equations
- Data.Text.concat ts = String.join ts
Instances For
Map a function over characters and concatenate the results. $$\text{concatMap}(f, t) = \text{concat}(\text{map}(f, \text{unpack}(t)))$$
Equations
- Data.Text.concatMap f t = String.join (List.map f (String.toList t))
Instances For
Does any character satisfy the predicate? $$\text{any}(p, t) = \exists c \in t.\; p(c)$$
Equations
- Data.Text.any p t = (String.toList t).any p
Instances For
Do all characters satisfy the predicate? $$\text{all}(p, t) = \forall c \in t.\; p(c)$$
Equations
- Data.Text.all p t = (String.toList t).all p
Instances For
Maximum character in a non-empty Text.
$$\text{maximum}(t) = \max(t),\quad \text{requires } |t| > 0$$
Instances For
Minimum character in a non-empty Text.
$$\text{minimum}(t) = \min(t),\quad \text{requires } |t| > 0$$
Instances For
The first character of a non-empty Text.
$$\text{head}(t) = t_0,\quad \text{requires } |t| > 0$$
Instances For
The last character of a non-empty Text.
$$\text{last}(t) = t_{|t|-1},\quad \text{requires } |t| > 0$$
Instances For
All characters except the first. $$\text{tail}(t) = t[1..],\quad \text{requires } |t| > 0$$
Instances For
All characters except the last. $$\text{init}(t) = t[..|t|-1],\quad \text{requires } |t| > 0$$
Equations
- t.init h✝ = Data.Text.pack (String.toList t).dropLast
Instances For
Prepend a character. $$\text{cons}(c, t) = c : t$$
Equations
- Data.Text.cons c t = Data.Text.pack (c :: String.toList t)
Instances For
Append a character. $$\text{snoc}(t, c) = t \mathbin{+\!\!+} [c]$$
Equations
- t.snoc c = Data.Text.pack (String.toList t ++ [c])
Instances For
Decompose into head and tail, or none if empty.
$$\text{uncons}(t) = \begin{cases} \text{some}(t_0, t[1..]) & |t| > 0 \\ \text{none} & |t| = 0 \end{cases}$$
Equations
Instances For
Decompose into init and last, or none if empty.
$$\text{unsnoc}(t) = \begin{cases} \text{some}(t[..|t|-1], t_{|t|-1}) & |t| > 0 \\ \text{none} & |t| = 0 \end{cases}$$
Equations
Instances For
Take the first n characters.
$$\text{take}(n, t) = t[0..n]$$
Equations
- Data.Text.take n t = Data.Text.pack (List.take n (String.toList t))
Instances For
Drop the first n characters.
$$\text{drop}(n, t) = t[n..]$$
Equations
- Data.Text.drop n t = Data.Text.pack (List.drop n (String.toList t))
Instances For
Take characters from the front while the predicate holds. $$\text{takeWhile}(p, t) = t[0..k]$$ where $k$ is the first index where $p$ fails.
Equations
- Data.Text.takeWhile p t = Data.Text.pack (List.takeWhile p (String.toList t))
Instances For
Drop characters from the front while the predicate holds. $$\text{dropWhile}(p, t) = t[k..]$$ where $k$ is the first index where $p$ fails.
Equations
- Data.Text.dropWhile p t = Data.Text.pack (List.dropWhile p (String.toList t))
Instances For
Drop characters from the end while the predicate holds. $$\text{dropWhileEnd}(p, t)$$
Equations
Instances For
Drop characters from both ends while the predicate holds. $$\text{dropAround}(p, t) = \text{dropWhile}(p, \text{dropWhileEnd}(p, t))$$
Equations
Instances For
Strip leading and trailing whitespace. $$\text{strip}(t)$$
Equations
Instances For
Strip leading whitespace. $$\text{stripStart}(t)$$
Equations
Instances For
Strip trailing whitespace. $$\text{stripEnd}(t)$$
Equations
Instances For
Split at position n.
$$\text{splitAt}(n, t) = (\text{take}(n, t), \text{drop}(n, t))$$
Equations
- Data.Text.splitAt n t = (Data.Text.pack (List.take n (String.toList t)), Data.Text.pack (List.drop n (String.toList t)))
Instances For
Break a Text at the first occurrence of needle.
Returns (before, matchAndAfter). If not found, returns (t, "").
$$\text{breakOn}(\text{needle}, t) = (t[..i], t[i..])$$
Equations
- One or more equations did not get rendered due to their size.
Instances For
Span: take while predicate holds, then return both parts. $$\text{span}(p, t) = (\text{takeWhile}(p, t), \text{dropWhile}(p, t))$$
Equations
- Data.Text.span p t = (Data.Text.pack (List.takeWhile p (String.toList t)), Data.Text.pack (List.drop (List.takeWhile p (String.toList t)).length (String.toList t)))
Instances For
Group consecutive characters by a custom equality. $$\text{groupBy}(eq, t)$$
Equations
- Data.Text.groupBy eq t = Data.Text.groupByAux✝ eq (String.toList t) []
Instances For
Group consecutive equal characters. $$\text{group}(\text{"aabbbca"}) = [\text{"aa"}, \text{"bbb"}, \text{"c"}, \text{"a"}]$$
Equations
- t.group = Data.Text.groupBy (fun (x1 x2 : Char) => x1 == x2) t
Instances For
All initial segments. $$\text{inits}(\text{"abc"}) = [\text{""}, \text{"a"}, \text{"ab"}, \text{"abc"}]$$
Equations
- t.inits = List.map (fun (n : Nat) => Data.Text.pack (List.take n (String.toList t))) (List.range ((String.toList t).length + 1))
Instances For
All final segments. $$\text{tails}(\text{"abc"}) = [\text{"abc"}, \text{"bc"}, \text{"c"}, \text{""}]$$
Equations
- t.tails = List.map (fun (n : Nat) => Data.Text.pack (List.drop n (String.toList t))) (List.range ((String.toList t).length + 1))
Instances For
Split on a separator string. $$\text{splitOn}(\text{","}, \text{"a,b,c"}) = [\text{"a"}, \text{"b"}, \text{"c"}]$$
Equations
- sep.splitOn t = if String.isEmpty sep = true then List.map Data.Text.singleton (String.toList t) else String.splitOn t sep
Instances For
Split on characters satisfying a predicate. $$\text{split}(p, t)$$ splits at every character where $p$ holds.
Equations
- Data.Text.split p t = Data.Text.split.go p (String.toList t) [] []
Instances For
Equations
- Data.Text.split.go p [] a✝¹ a✝ = (Data.Text.pack a✝¹.reverse :: a✝).reverse
- Data.Text.split.go p (c :: cs) a✝¹ a✝ = if p c = true then Data.Text.split.go p cs [] (Data.Text.pack a✝¹.reverse :: a✝) else Data.Text.split.go p cs (c :: a✝¹) a✝
Instances For
Split into chunks of at most n characters. Fuel-limited to ensure termination.
$$\text{chunksOf}(n, t)$$
Equations
- Data.Text.chunksOf n t = if (n == 0) = true then [t] else have cs := String.toList t; Data.Text.chunksOf.go n cs cs.length []
Instances For
Equations
- Data.Text.chunksOf.go n [] a✝¹ a✝ = a✝.reverse
- Data.Text.chunksOf.go n a✝¹ 0 a✝ = a✝.reverse
- Data.Text.chunksOf.go n a✝¹ fuel.succ a✝ = Data.Text.chunksOf.go n (List.drop n a✝¹) fuel (Data.Text.pack (List.take n a✝¹) :: a✝)
Instances For
Split into lines. $$\text{lines}(\text{"a\\nb\\nc"}) = [\text{"a"}, \text{"b"}, \text{"c"}]$$
Equations
- t.lines = String.splitOn t "\n"
Instances For
Split into words (on whitespace). $$\text{words}(\text{"hello world"}) = [\text{"hello"}, \text{"world"}]$$
Equations
- t.words = List.filter (fun (w : Data.Text) => !String.isEmpty w) (Data.Text.split Char.isWhitespace t)
Instances For
Join lines with newlines. $$\text{unlines}([\text{"a"}, \text{"b"}]) = \text{"a\\nb\\n"}$$
Equations
- Data.Text.unlines ts = "\n".intercalate ts ++ if ts.isEmpty = true then "" else "\n"
Instances For
Join words with spaces. $$\text{unwords}([\text{"hello"}, \text{"world"}]) = \text{"hello world"}$$
Equations
- Data.Text.unwords ts = " ".intercalate ts
Instances For
Is pfx a prefix of t?
$$\text{isPrefixOf}(\text{pfx}, t) \iff t \text{ starts with } \text{pfx}$$
Equations
- pfx.isPrefixOf t = String.startsWith t pfx
Instances For
Is sfx a suffix of t?
$$\text{isSuffixOf}(\text{sfx}, t) \iff t \text{ ends with } \text{sfx}$$
Equations
- sfx.isSuffixOf t = String.endsWith t sfx
Instances For
Is needle contained in t?
$$\text{isInfixOf}(\text{needle}, t) \iff \text{needle} \subseteq t$$
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Strip a prefix, returning none if not a prefix.
$$\text{stripPrefix}(\text{pfx}, t)$$
Equations
- pfx.stripPrefix t = if String.startsWith t pfx = true then some (Data.Text.pack (List.drop (String.toList pfx).length (String.toList t))) else none
Instances For
Strip a suffix, returning none if not a suffix.
$$\text{stripSuffix}(\text{sfx}, t)$$
Equations
- sfx.stripSuffix t = if String.endsWith t sfx = true then some (Data.Text.pack (List.take ((String.toList t).length - (String.toList sfx).length) (String.toList t))) else none
Instances For
Does the character occur in the Text?
$$\text{elem}(c, t) = \exists i.\; t_i = c$$
Equations
- Data.Text.elem c t = List.elem c (String.toList t)
Instances For
Find the first character satisfying a predicate. $$\text{find}(p, t)$$
Equations
- Data.Text.find p t = List.find? p (String.toList t)
Instances For
Keep only characters satisfying a predicate. $$\text{filter}(p, t) = [c \in t \mid p(c)]$$
Equations
- Data.Text.filter p t = Data.Text.pack (List.filter p (String.toList t))
Instances For
Partition into (satisfying, not-satisfying). $$\text{partition}(p, t) = (\text{filter}(p, t), \text{filter}(\neg p, t))$$
Equations
- Data.Text.partition p t = match List.partition p (String.toList t) with | (yes, no) => (Data.Text.pack yes, Data.Text.pack no)
Instances For
Count non-overlapping occurrences of a substring. $$\text{count}(\text{needle}, t)$$
Equations
- needle.count t = if String.isEmpty needle = true then (String.toList t).length + 1 else have parts := String.splitOn t needle; parts.length - 1
Instances For
Zip two Texts into a list of character pairs.
$$\text{zip}(s, t) = [(s_0, t_0), (s_1, t_1), \ldots]$$
Equations
- s.zip t = (String.toList s).zip (String.toList t)
Instances For
Zip two Texts with a combining function.
$$\text{zipWith}(f, s, t) = [f(s_0, t_0), f(s_1, t_1), \ldots]$$
Equations
- Data.Text.zipWith f s t = Data.Text.pack (List.zipWith f (String.toList s) (String.toList t))