Legend:
Library
Module
Module type
Parameter
Class
Class type
This module defines the builtins that are defined by Dolmen.
Builtins are particularly used in typed expressions see Dolmen.Std.Expr, in order to give more information about constants which have builtin semantics.
Users are encouraged to match builtins rather than specific symbols when inspecting typed expressions, as this basically allows to match on the semantics of an identifier rather than matching on the syntaxic value of an identifier. For instance, equality can take an arbitrary number of arguments, and thus in order to have well-typed terms, each arity of equality gives rise to a different symbol (because the symbol's type depends on the arity desired), but all these symbols have the Equal builtin.
In the following we will use pseudo-code to describe the arity and actual type associated to builtins. These will follow ocaml's notation for types with an additional syntax using dots for arbitrary arity. Some examples:
ttype is a type constant
ttype -> ttype is a type constructor (e.g. list)
int is a constant of type int
float -> int is a unary function
'a. 'a -> 'a is a polymorphic unary function
'a. 'a -> ... -> Prop describes a family of functions that take a type and then an arbitrary number of arguments of that type, and return a proposition (this is for instance the type of equality).
Additionally, due to some languages having overloaded operators, and in order to not have too verbose names, some of these builtins may have overloaded signtures, such as comparisons on numbers which can operate on integers, rationals, or reals. Note that arbitrary arity operators (well family of operators) can be also be seen as overloaded operators. Overloaded types (particularly for numbers) are written:
{a=(Int|Rational|Real)} a -> a -> Prop, where the notable difference with polymorphic functions is that functions of this type does not take a type argument.
Coercion: 'a 'b. 'a -> 'b: Coercion/cast operator, i.e. allows to cast values of some type to another type. This is a polymorphic operator that takes two type arguments a and b, a value of type a, and returns a value of type b. The interpretation/semantics of this cast can remain up to the user. This operator is currently mainly used to cast numeric types when this transormation is exact (i.e. an integer casted into a rational, which is always possible and exact, or the cast of a rational into an integer, as long as the cast is guarded by a clause verifying the rational is an integer).
Int: ttype the type for signed integers of arbitrary precision.
*)
| Integerof string
(*
Integer s: Int: integer litteral. The string s should be the decimal representation of an integer with arbitrary precision (hence the use of strings rather than the limited precision int).
*)
| Rat
(*
Rat: ttype the type for signed rationals.
*)
| Rationalof string
(*
Rational s: Rational: rational litteral. The string s should be the decimal representation of a rational (see the various languages spec for more information).
*)
| Real
(*
Real: ttype the type for signed reals.
*)
| Decimalof string
(*
Decimal s: Real: real litterals. The string s should be a floating point representatoin of a real. Not however that reals here means the mathematical abstract notion of real numbers, including irrational, non-algebric numbers, and is thus not restricted to floating point numbers, although these are the only litterals supported.
*)
| Lt
(*
Lt: {a=(Int|Rational|Real)} a -> a -> Prop: strict comparison (less than) on numbers (whether integers, rationals, or reals).
*)
| Leq
(*
Leq:{a=(Int|Rational|Real)} a -> a -> Prop: large comparison (less or equal than) on numbers (whether integers, rationals, or reals).
*)
| Gt
(*
Gt:{a=(Int|Rational|Real)} a -> a -> Prop: strict comparison (greater than) on numbers (whether integers, rationals, or reals).
*)
| Geq
(*
Geq:{a=(Int|Rational|Real)} a -> a -> Prop: large comparison (greater or equal than) on numbers (whether integers, rationals, or reals).
*)
| Minus
(*
Minus:{a=(Int|Rational|Real)} a -> a: arithmetic unary negation/minus on numbers (whether integers, rationals, or reals).
*)
| Add
(*
Add:{a=(Int|Rational|Real)} a -> a -> a: arithmetic addition on numbers (whether integers, rationals, or reals).
*)
| Sub
(*
Sub:{a=(Int|Rational|Real)} a -> a -> a: arithmetic substraction on numbers (whether integers, rationals, or reals).
*)
| Mul
(*
Mul:{a=(Int|Rational|Real)} a -> a -> a: arithmetic multiplication on numbers (whether integers, rationals, or reals).
*)
| Div
(*
Div:{a=(Rational|Real)} a -> a -> a: arithmetic exact division on numbers (rationals, or reals, but **not** integers).
*)
| Div_e
(*
Div_e:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer euclidian quotient (whether integers, rationals, or reals). If D is positive then Div_e (N,D) is the floor (in the type of N and D) of the real division N/D, and if D is negative then Div_e (N,D) is the ceiling of N/D.
*)
| Div_t
(*
Div_t:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer truncated quotient (whether integers, rationals, or reals). Div_t (N,D) is the truncation of the real division N/D.
*)
| Div_f
(*
Div_f:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer floor quotient (whether integers, rationals, or reals). Div_t (N,D) is the floor of the real division N/D.
*)
| Modulo_e
(*
Modulo_e:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer euclidian remainder (whether integers, rationals, or reals). It is defined by the following equation: Div_e (N, D) * D + Modulo(N, D) = N.
*)
| Modulo_t
(*
Modulo_t:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer truncated remainder (whether integers, rationals, or reals). It is defined by the following equation: Div_t (N, D) * D + Modulo_t(N, D) = N.
*)
| Modulo_f
(*
Modulo_f:{a=(Int|Rational|Real)} a -> a -> a: arithmetic integer floor remainder (whether integers, rationals, or reals). It is defined by the following equation: Div_f (N, D) * D + Modulo_f(N, D) = N.
*)
| Abs
(*
Abs: Int -> Int: absolute value on integers.
*)
| Divisible
(*
Divisible: Int -> Int -> Prop: divisibility predicate on integers. Smtlib restricts applications of this predicate to have a litteral integer for the divisor/second argument.
*)
| Is_int
(*
Is_int:{a=(Int|Rational|Real)} a -> Prop: integer predicate for numbers: is the given number an integer.
*)
| Is_rat
(*
Is_rat:{a=(Int|Rational|Real)} a -> Prop: rational predicate for numbers: is the given number an rational.
*)
| Floor
(*
Floor:{a=(Int|Rational|Real)} a -> a: floor function on numbers, defined in tptp as the largest intger not greater than the argument.
*)
| Ceiling
(*
Ceiling:{a=(Int|Rational|Real)} a -> a: ceiling function on numbers, defined in tptp as the smallest intger not less than the argument.
*)
| Truncate
(*
Truncate:{a=(Int|Rational|Real)} a -> a: ceiling function on numbers, defined in tptp as the nearest integer value with magnitude not greater than the absolute value of the argument.
*)
| Round
(*
Round:{a=(Int|Rational|Real)} a -> a: rounding function on numbers, defined in tptp as the nearest intger to the argument; when the argument is halfway between two integers, the nearest even integer to the argument.
Array: ttype -> ttype -> ttype: the type constructor for polymorphic functional arrays. An (src, dst) Array is an array from expressions of type src to expressions of type dst. Typically, such arrays are immutables.
*)
| Store
(*
Store: 'a 'b. ('a, 'b) Array -> 'a -> 'b -> ('a, 'b) Array: store operation on arrays. Returns a new array with the key bound to the given value (shadowing the previous value associated to the key).
*)
| Select
(*
Select: 'a 'b. ('a, 'b) Array -> 'a -> 'b: select operation on arrays. Returns the value associated to the given key. Typically, functional arrays are complete, i.e. all keys are mapped to a value.
Bitv_shl: Bitv(n) -> Bitv(n) -> Bitv(n): shift left (equivalent to multiplication by 2^x where x is the value of the second argument).
*)
| Bitv_lshr
(*
Bitv_lshr: Bitv(n) -> Bitv(n) -> Bitv(n): logical shift right (equivalent to unsigned division by 2^x, where x is the value of the second argument).
*)
| Bitv_ashr
(*
Bitv_ashr: Bitv(n) -> Bitv(n) -> Bitv(n): Arithmetic shift right, like logical shift right except that the most significant bits of the result always copy the most significant bit of the first argument.
RoundingMode: ttype: type for enumerated type of rounding modes.
*)
| RoundNearestTiesToEven
(*
RoundNearestTiesToEven : RoundingMode:
*)
| RoundNearestTiesToAway
(*
RoundNearestTiesToAway : RoundingMode:
*)
| RoundTowardPositive
(*
RoundTowardPositive : RoundingMode
*)
| RoundTowardNegative
(*
RoundTowardNegative : RoundingMode
*)
| RoundTowardZero
(*
RoundTowardZero : RoundingMode
*)
| Floatof int * int
(*
Float(e,s): ttype: type constructor for floating point of exponent of size e and significand of size s (hidden bit included). Those size are greater than 1
*)
| Fpof int * int
(*
Fp(e, s): Bitv(1) -> Bitv(e) -> Bitv(s-1) -> Fp(e,s): bitvector literal. The IEEE-format is used for the conversion sb^se^ss. All the NaN are converted to the same value.
Str_at: String -> Int -> String: Singleton string containing a character at given position or empty string when position is out of range. The leftmost position is 0.
*)
| Str_to_code
(*
Str_to_code: String -> Int: Str_to_code s is the code point of the only character of s, if s is a singleton string; otherwise, it is -1.
*)
| Str_of_code
(*
Str_of_code: Int -> String: Str_of_code n is the singleton string whose only character is code point n if n is in the range 0, 196607; otherwise, it is the empty string.
*)
| Str_is_digit
(*
Str_is_digit: String -> Prop: Digit check Str.is_digit s is true iff s consists of a single character which is a decimal digit, that is, a code point in the range 0x0030 ... 0x0039.
*)
| Str_to_int
(*
Str_to_int: String -> Int: Conversion to integers Str.to_int s with s consisting of digits (in the sense of str.is_digit) evaluates to the positive integer denoted by s when seen as a number in base 10 (possibly with leading zeros). It evaluates to -1 if s is empty or contains non-digits.
*)
| Str_of_int
(*
Str_of_int : Int -> String: Conversion from integers. Str.from_int n with n non-negative is the corresponding string in decimal notation, with no leading zeros. If n < 0, it is the empty string.
Str_sub: String -> Int -> Int -> String: Str_sub s i n evaluates to the longest (unscattered) substring of s of length at most n starting at position i. It evaluates to the empty string if n is negative or i is not in the interval 0,l-1 where l is the length of s.
*)
| Str_index_of
(*
Str_index_of: String -> String -> Int -> Int: Index of first occurrence of second string in first one starting at the position specified by the third argument. Str_index_of s t i, with 0 <= i <= |s| is the position of the first occurrence of t in s at or after position i, if any. Otherwise, it is -1. Note that the result is i whenever i is within the range 0, |s| and t is empty.
*)
| Str_replace
(*
Str_replace: String -> String -> String -> String: Replace Str_replace s t t' is the string obtained by replacing the first occurrence of t in s, if any, by t'. Note that if t is empty, the result is to prepend t' to s; also, if t does not occur in s then the result is s.
*)
| Str_replace_all
(*
Str_replace_all: String -> String -> String -> String: Str_replace_all s t t’ is s if t is the empty string. Otherwise, it is the string obtained from s by replacing all occurrences of t in s by t’, starting with the first occurrence and proceeding in left-to-right order.
*)
| Str_replace_re
(*
Str_replace_re: String -> String_RegLan -> String -> String: Str_replace_re s r t is the string obtained by replacing the shortest leftmost non-empty match of r in s, if any, by t. Note that if t is empty, the result is to prepend t to s.
*)
| Str_replace_re_all
(*
Str_replace_re_all: String -> String_RegLan -> String -> String: Str_replace_re_all s r t is the string obtained by replacing, left-to right, each shortest *non-empty* match of r in s by t.
*)
| Str_is_prefix
(*
Str_is_prefix: String -> String -> Prop: Prefix check Str_is_prefix s t is true iff s is a prefix of t.
*)
| Str_is_suffix
(*
Str_is_suffix: String -> String -> Prop: Suffix check Str_is_suffix s t is true iff s is a suffix of t.
*)
| Str_contains
(*
Str_contains: String -> String -> Prop: Inclusion check Str_contains s t is true iff s contains t.
String_RegLan: ttype: type constructor for Regular languages over strings.
*)
| Re_empty
(*
Re_empty: String_RegLan: the empty language.
*)
| Re_all
(*
Re_all: String_RegLan: the language of all strings.
*)
| Re_allchar
(*
Re_allchar: String_RegLan: the language of all singleton strings.
*)
| Re_of_string
(*
Re_of_string: String -> String_RegLan: the singleton language with a single string.
*)
| Re_range
(*
Re_range: String -> String -> String_RegLan: Language range Re_range s1 s2 is the set of all *singleton* strings s such that Str_lexicographic_large s1 s s2 provided s1 and s1 are singleton. Otherwise, it is the empty language.
*)
| Re_concat
(*
Re_concat: String_RegLan -> String_RegLan -> String_RegLan: language concatenation.
*)
| Re_union
(*
Re_union: String_RegLan -> String_RegLan -> String_RegLan: language union.
*)
| Re_inter
(*
Re_inter: String_RegLan -> String_RegLan -> String_RegLan: language intersection.