Module Smtml.TySource

Type Module. This module defines types and operations for working with SMT types, including unary, binary, relational, ternary, conversion, and n-ary operations. It also provides utilities for type comparison, pretty-printing, and parsing.

Sourcetype _ cast =
  1. | C8 : int cast
    (*

    Cast to an 8-bit integer.

    *)
  2. | C32 : int32 cast
    (*

    Cast to a 32-bit integer.

    *)
  3. | C64 : int64 cast
    (*

    Cast to a 64-bit integer.

    *)

The type _ cast represents type casts for integers of different bit widths.

Type Definitions

Sourcetype t =
  1. | Ty_app
    (*

    Application type.

    *)
  2. | Ty_bitv of int
    (*

    Bitvector type with a specified bit width.

    *)
  3. | Ty_bool
    (*

    Boolean type.

    *)
  4. | Ty_fp of int
    (*

    Floating-point type with a specified bit width.

    *)
  5. | Ty_int
    (*

    Integer type.

    *)
  6. | Ty_list
    (*

    List type.

    *)
  7. | Ty_none
    (*

    None type.

    *)
  8. | Ty_real
    (*

    Real number type.

    *)
  9. | Ty_str
    (*

    String type.

    *)
  10. | Ty_unit
    (*

    Unit type.

    *)
  11. | Ty_regexp
    (*

    Regular expression type.

    *)
  12. | Ty_roundingMode

The type t represents smtml types.

Type Comparison

Sourceval compare : t -> t -> int

compare t1 t2 performs a total order comparison of types t1 and t2.

Sourceval equal : t -> t -> bool

equal t1 t2 checks if types t1 and t2 are equal.

Pretty Printing

Sourceval pp : t Fmt.t

pp fmt t pretty-prints the type t using the formatter fmt.

String Conversion

Sourceval string_of_type : t -> string

string_of_type t converts the type t to a string representation.

Sourceval of_string : string -> (t, [> `Msg of string ]) Smtml_prelude.Result.t

of_string s attempts to parse the string s into a type. Returns Ok t if successful, or an error message otherwise.

Type Size

Sourceval size : t -> int

size t returns the size (in bits) of the type t, if applicable.

Unary Operations

Sourcemodule Unop : sig ... end

Binary Operations

Sourcemodule Binop : sig ... end

Relational Operations

Sourcemodule Relop : sig ... end

Ternary Operations

Sourcemodule Triop : sig ... end

Conversion Operations

Sourcemodule Cvtop : sig ... end

N-ary Operations

Sourcemodule Naryop : sig ... end