package um-abt

  1. Overview
  2. Docs

Variables, named by strings, which can be bound to a Var.Binding or left free.

module Binding : sig ... end

A binding is an immutable reference, to which a bound can refer.

type t = private
  1. | Free of string
  2. | Bound of Binding.t
    (*

    A varibale of type t is either free or bound.

    *)
val compare : t -> t -> int

Bound variables are equal if they are have the same binding, free variables are greater than bound variables, and variables are otherwise compared lexigraphically by name.

Specifically,

compare a b is 0 iff

  • is_free a && is_free b and name a = name b
  • is_bound a && is_bound b and both a and b are bound to the same binding by way of bind.

compare a b is String.compare (name a) (name b) if is_free a && is_free b or is_bound a && is_bound b.

compare a b is -1 if is_bound a and is_free b or 1 if is_free a and is_bound b

val equal : t -> t -> bool

equal a b is true iff

  • is_free a && is_free b and name a = name b
  • is_bound a && is_bound b and both a and b are bound to the same binding by way of bind.
val is_free : t -> bool
val is_bound : t -> bool
val v : string -> t
val to_string : t -> string
val to_string_debug : t -> string

Includes the unique ID of any bound variables

val name : t -> string

name v is to_string v

val bind : t -> Binding.t -> t option

bind v bnd is Some var when is_free v and name v = Binding.name bnd, where var is a new variable with the same name but bound to bnd. Otherwise, it is None.

See equal.

val is_bound_to : t -> Binding.t -> bool

is_bound_to v bnd is true if v is bound to bnd, via bind

val of_binding : Binding.t -> t

of_binding bnd is a variable bound to bnd

val to_binding : t -> Binding.t option

to_binding v is Some bnd iff v is bound to bnd via bind. Otherwise it is None.

module Set : Set.S with type elt = t
module Map : Map.S with type key = t
OCaml

Innovation. Community. Security.