package um-abt

You can search for identifiers within the package.

in-package search v0.2.0

package um-abt

um-abt
- Abt
  - Make
    
    Op
    
    Unification
    
    Subst
  - Operator
  - Syntax
    
    Op
    
    Unification
    
    Subst
  - Var
    
    Binding
    
    Map
    
    Set

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

| Free of string
| 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