package smtml

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Smtml.SymbolSource

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

Name Types

Sourcetype 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

Sourcetype 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

Sourcetype 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

Sourceval attr : namespace

attr represents the attribute namespace.

Sourceval sort : namespace

sort represents the sort (type) namespace.

Sourceval term : namespace

term represents the term (function, constant) namespace.

Sourceval var : namespace

var represents the variable namespace.

Symbol Creation

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

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

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

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

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

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

Sourceval mk : namespace -> string -> t

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

Sourceval 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

Sourceval name : t -> name

name sym returns the name of the symbol sym.

Sourceval namespace : t -> namespace

namespace sym returns the namespace of the symbol sym.

Sourceval type_of : t -> Ty.t

type_of sym returns the type of the symbol sym.

Comparison

Sourceval compare : t -> t -> int

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

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

equal sym1 sym2 checks if sym1 and sym2 are equal.

Pretty Printing

Sourceval pp_namespace : namespace Fmt.t

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

Sourceval pp : t Fmt.t

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

Serialization

Sourceval to_string : t -> string

to_string sym converts the symbol sym to a string representation.

Sourceval to_json : t -> Yojson.Basic.t

to_json sym converts the symbol sym to a JSON representation.

module Map : Smtml_prelude.Map.S with type key = t
OCaml

Innovation. Community. Security.