Module Smtml.Value

Concrete Values Module. This module defines types and utilities for working with concrete values, including integers, floats, strings, lists, and applications. It provides functions for type checking, comparison, mapping, and conversion to/from strings and JSON.

Value Types

type t =
  1. | True
    (*

    Boolean true.

    *)
  2. | False
    (*

    Boolean false.

    *)
  3. | Unit
    (*

    Unit value.

    *)
  4. | Int of int
    (*

    Integer value.

    *)
  5. | Real of float
    (*

    Real number value.

    *)
  6. | Str of string
    (*

    String value.

    *)
  7. | Num of Num.t
    (*

    Numeric value.

    *)
  8. | Bitv of Bitvector.t
    (*

    Bitvector value.

    *)
  9. | List of t list
    (*

    List of values.

    *)
  10. | App : [> `Op of string ] * t list -> t
    (*

    Application of an operator to a list of values.

    *)
  11. | Re_none
  12. | Re_all
  13. | Re_allchar
  14. | Nothing
    (*

    Represents an undefined or missing value.

    *)

The type t represents concrete values.

val type_of : t -> Ty.t

type_of v returns the type of the value v.

Comparison

val hash : t -> int
val compare : t -> t -> int

compare v1 v2 provides a total ordering over values of type t. It returns a negative integer if v1 is less than v2, zero if they are equal, and a positive integer if v1 is greater than v2.

val equal : t -> t -> bool

equal v1 v2 returns true if v1 and v2 are equal, otherwise false.

Mapping

val map : t -> (t -> t) -> t

map v f applies the function f to the value v. If v is a list, f is applied to each element.

val (let+) : t -> (t -> t) -> t

let+ v f is a convenience operator for applying f to v.

val default_of_type : Ty.t -> t

default_of_type ty returns the default value for type ty.

Pretty Printing

val pp : t Fmt.t

pp fmt v pretty-prints the value v using the formatter fmt.

val pp_safe : t Fmt.t

pp_safe is a round-trip safe formatter for values of type t.

val pp_with : printer:Ty.printer -> t Fmt.t

pp_with ~printer allows explicit selection of the printing format.

Serialization

val to_string : t -> string

to_string v converts the value v to a string representation.

val of_string : Ty.t -> string -> (t, [> `Msg of string ]) Smtml_prelude.result

of_string ty s attempts to parse the string s as a value of type ty. Returns Ok v on success, or an error message if parsing fails.

val to_json : t -> Yojson.Safe.t

to_json v converts the value v into a JSON representation.

module Smtlib : sig ... end