Module Smtml.Symbol

Symbol Module. This module defines names, namespaces, and typed symbols, providing utilities for creating, comparing, and manipulating symbols.

Name Types

type name =
  1. | Simple of string
    (*

    A simple name represented as a string.

    *)
  2. | Indexed of {
    1. basename : string;
      (*

      The base name.

      *)
    2. indices : string list;
      (*

      A list of indices associated with the name.

      *)
    }

The type name represents a symbol name, which can either be a simple string or an indexed name with a base name and a list of indices.

Namespace Types

type namespace =
  1. | Attr
    (*

    Attributes.

    *)
  2. | Sort
    (*

    Sorts (types).

    *)
  3. | Term
    (*

    Terms (functions, constants).

    *)
  4. | Var
    (*

    Variables.

    *)

The type namespace classifies symbols into different kinds of identifiers.

Symbol Types

type t = {
  1. ty : Ty.t;
    (*

    The type of the symbol.

    *)
  2. name : name;
    (*

    The name of the symbol.

    *)
  3. namespace : namespace;
    (*

    The namespace to which the symbol belongs.

    *)
}

The type t represents a symbol, consisting of a type, a name, and a namespace.

Namespace Constants

val attr : namespace

attr represents the attribute namespace.

val sort : namespace

sort represents the sort (type) namespace.

val term : namespace

term represents the term (function, constant) namespace.

val var : namespace

var represents the variable namespace.

Symbol Creation

val (@:) : string -> Ty.t -> t

s @: ty creates a symbol with name s and type ty, belonging to the term (function, constant) namespace.

val make : Ty.t -> string -> t

make ty s creates a symbol with type ty and name s in the term (function, constant) namespace.

val make3 : Ty.t -> name -> namespace -> t

make3 ty name ns creates a symbol with type ty, name name, and namespace ns.

val mk : namespace -> string -> t

mk ns s creates a symbol with name s in the specified namespace ns with a default type.

val indexed : namespace -> string -> string list -> t

indexed ns basename indices creates a symbol with an indexed name, where basename is the base name and indices are the associated indices.

Symbol Accessors

val name : t -> name

name sym returns the name of the symbol sym.

val namespace : t -> namespace

namespace sym returns the namespace of the symbol sym.

val type_of : t -> Ty.t

type_of sym returns the type of the symbol sym.

Comparison

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

compare sym1 sym2 performs a total order comparison of sym1 and sym2.

val equal : t -> t -> Smtml_prelude.Bool.t

equal sym1 sym2 checks if sym1 and sym2 are equal.

Pretty Printing

val pp_namespace : namespace Fmt.t

pp_namespace fmt ns pretty-prints the namespace ns using the formatter fmt.

val pp : t Fmt.t

pp fmt sym pretty-prints the symbol sym using the formatter fmt.

Serialization

val to_string : t -> string

to_string sym converts the symbol sym to a string representation.

val to_json : t -> Yojson.Safe.t

to_json sym converts the symbol sym to a JSON representation.

module Map : Smtml_prelude.Map.S with type key = t
module Smtlib : sig ... end