dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Module Dolmen_type . Strings . Smtlib2 . Tff . T . String
val of_ustring : string -> Type.T.t

Create a string from a unicode UTF-8 encoded string (with escape sequences already interpreted as unicode characters).

val length : Type.T.t -> Type.T.t

Length of a string expression.

val at : Type.T.t -> Type.T.t -> Type.T.t

Get the char at the given position.

val is_digit : Type.T.t -> Type.T.t

Is the string a singleton string with a single digit character ?

val to_code : Type.T.t -> Type.T.t

Returns the code point of the single character of the string, or (-1) is the string is not a singleton.

val of_code : Type.T.t -> Type.T.t

Returns the singleton string whose only character is the given code point.

val to_int : Type.T.t -> Type.T.t

Evaluates the string as a decimal natural number, or (-1) if it's not possible.

val of_int : Type.T.t -> Type.T.t

Convert an int expression to a string in decimal representation.

val concat : Type.T.t -> Type.T.t -> Type.T.t

String concatenation.

val sub : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Substring extraction.

val index_of : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Index of the first occurrence of the second string in first one, starting at the position of the third argument.

val replace : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Replace the first occurrence.

val replace_all : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Replace all occurrences.

val replace_re : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Replace the leftmost, shortest re ocurrence.

val replace_re_all : Type.T.t -> Type.T.t -> Type.T.t -> Type.T.t

Replace left-to-right, each shortest non empty re occurrence.

val is_prefix : Type.T.t -> Type.T.t -> Type.T.t

First string is a prefix of the second one.

val is_suffix : Type.T.t -> Type.T.t -> Type.T.t

First string is a suffix of the second one.

val contains : Type.T.t -> Type.T.t -> Type.T.t

First string contains the second one.

val lt : Type.T.t -> Type.T.t -> Type.T.t

Lexicographic strict ordering.

val leq : Type.T.t -> Type.T.t -> Type.T.t

Lexicographic large ordering.

val in_re : Type.T.t -> Type.T.t -> Type.T.t

String Regular languager membership

Sub-module used for namespacing for the regular language part of the theory requirements.