Skip to main content

Text

Reference for mo:core/Text in the core library.

Text wraps Unicode text construction, search, tokenization, and casing helpers. Many operations are trusted primitive wrappers, so precise proofs should rely on documented contracts and Text.Spec.size, not on implicit Unicode internals.

Import​

mo:core/Text

Status​

  • Runtime module

Public API​

Types​

  • Text, Pattern

Modules​

  • Spec

Functions​

fromChar(c : Char) : Text​

Converts between the module type and the target representation.

Contract

ensures size(result) == 1;

Use when: crossing between this module's value and another representation.

fromArray(a : [Char]) : Text​

Converts between the module type and the target representation.

Contract

ensures size(result) == a.size();

Use when: crossing between this module's value and another representation.

fromVarArray(a : [var Char]) : Text​

Converts between the module type and the target representation.

Contract

ensures size(result) == a.size();

Use when: crossing between this module's value and another representation.

toIter(t : Text) : Iter.Iter<Char>​

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

foldLeft<A>(text : Text, base : A, combine : (A, Char) -> A) : A​

Folds the structure by applying the supplied accumulator function.

Use when: code or specifications need this operation with the documented contract.

toArray(t : Text) : [Char]​

Converts between the module type and the target representation.

Contract

ensures result.size() == size(t);

Use when: crossing between this module's value and another representation.

toVarArray(t : Text) : [var Char]​

Converts between the module type and the target representation.

Contract

ensures result.size() == size(t);

Use when: crossing between this module's value and another representation.

fromIter(cs : Iter.Iter<Char>) : Text​

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

isEmpty(t : Text) : Bool​

Checks the predicate described by the return contract.

Contract

ensures result == (t == "");
ensures result == (size(t) == 0);

Use when: a branch condition or contract needs this predicate as a named fact.

size(t : Text) : Nat​

Returns the length or cardinality represented by the value.

Contract

ensures result == Spec.size(t);
ensures result >= 0;
ensures t == "" ==> result == 0;

Use when: code or specifications need this operation with the documented contract.

concat(t1 : Text, t2 : Text) : Text​

Performs the corresponding text transformation.

Contract

ensures result == (t1 # t2);
ensures size(result) == size(t1) + size(t2);

Use when: code or specifications need this operation with the documented contract.

reverse(t : Text) : Text​

Performs the corresponding text transformation.

Contract

ensures size(result) == size(t);

Use when: code or specifications need this operation with the documented contract.

equal(t1 : Text, t2 : Text) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (t1 == t2);

Use when: code or contracts need an explicit comparison helper instead of an operator.

notEqual(t1 : Text, t2 : Text) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (t1 != t2);

Use when: code or contracts need an explicit comparison helper instead of an operator.

less(t1 : Text, t2 : Text) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (t1 < t2);

Use when: code or contracts need an explicit comparison helper instead of an operator.

lessOrEqual(t1 : Text, t2 : Text) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (t1 <= t2);

Use when: code or contracts need an explicit comparison helper instead of an operator.

greater(t1 : Text, t2 : Text) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (t1 > t2);

Use when: code or contracts need an explicit comparison helper instead of an operator.

greaterOrEqual(t1 : Text, t2 : Text) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (t1 >= t2);

Use when: code or contracts need an explicit comparison helper instead of an operator.

compare(t1 : Text, t2 : Text) : Types.Order​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == #less ==> t1 < t2;
ensures result == #equal ==> t1 == t2;
ensures result == #greater ==> t1 > t2;
ensures t1 < t2 ==> result == #less;
ensures t1 == t2 ==> result == #equal;
ensures t1 > t2 ==> result == #greater;

Use when: code or contracts need an explicit comparison helper instead of an operator.

join(sep : Text, ts : Iter.Iter<Text>) : Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

map(t : Text, f : Char -> Char) : Text​

Transforms the contained values with the supplied function while preserving the documented shape.

Contract

ensures size(result) == size(t);

Use when: code or specifications need this operation with the documented contract.

flatMap(t : Text, f : (c : Char) -> Text) : Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

split(t : Text, p : Pattern) : Iter.Iter<Text>​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

tokens(t : Text, p : Pattern) : Iter.Iter<Text>​

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

contains(t : Text, p : Pattern) : Bool​

Checks the predicate described by the return contract.

Use when: a branch condition or contract needs this predicate as a named fact.

startsWith(t : Text, p : Pattern) : Bool​

Checks whether the text has the requested prefix or suffix pattern.

Use when: code or specifications need this operation with the documented contract.

endsWith(t : Text, p : Pattern) : Bool​

Checks whether the text has the requested prefix or suffix pattern.

Use when: code or specifications need this operation with the documented contract.

replace(t : Text, p : Pattern, r : Text) : Text​

Returns or applies the corresponding update to the structure.

Use when: the postcondition must relate the updated value to the previous one.

stripStart(t : Text, p : Pattern) : ?Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

stripEnd(t : Text, p : Pattern) : ?Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

trimStart(t : Text, p : Pattern) : Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

trimEnd(t : Text, p : Pattern) : Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

trim(t : Text, p : Pattern) : Text​

Performs the corresponding text transformation.

Use when: code or specifications need this operation with the documented contract.

compareWith(t1 : Text, t2 : Text, cmp : (Char, Char) -> Types.Order) : Types.Order​

Compares two texts using the supplied character comparator.

Use when: code or specifications need this operation with the documented contract.

encodeUtf8(t : Text) : Blob​

Converts between Text and its UTF-8 Blob representation.

Use when: code or specifications need this operation with the documented contract.

decodeUtf8(b : Blob) : ?Text​

Converts between Text and its UTF-8 Blob representation.

Use when: code or specifications need this operation with the documented contract.

toLower(t : Text) : Text​

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

toUpper(t : Text) : Text​

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

toText(t : Text) : Text​

Converts between the module type and the target representation.

Contract

ensures result == t;

Use when: crossing between this module's value and another representation.

Spec Module​

Spec Functions​

size(t : Text) : Nat​

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

Summary​

  • Runtime module under mo:core/Text.
  • Exposes 39 public functions.
  • Includes 1 spec helpers in Spec.