Module AbtSource

Overview

um-abt is a library for constructing and manipulating the abstract syntax of languages that use variables.

um-abt provides unifiable abstract binding trees (UABTs). An abstract binding tree (ABT) is an abstract syntax tree (AST), enriched with constructs to manage variable binding and scope.

um-abt extends ABTs with support for nominal unification (unificaiton modulo ɑ-equivalence).

Example

A succinct example of the typical use of this library can be seen in the following implementation of the untyped λ-calculus.

Define your language's operators:

 (* Define the usual operators, but without the variables, since we get those free *)
  module O = struct
    type 'a t =
      | App of 'a * 'a
      | Lam of 'a
    [@@deriving eq, map, fold]

    let to_string : string t -> string = function
      | App (l, m) -> Printf.sprintf "(%s %s)" l m
      | Lam abs    -> Printf.sprintf "(λ%s)" abs
  end

(Note the use of ppx_deriving to derive most values automatically.)

Generate your the ABT representing your syntax, and define combinators to easily and safely construct terms of your lanugage construct:

  (* Generate the syntax, which will include a type [t] of the ABTs over the operators **)
  open Abt.Make (O)

  (* Define some constructors to ensure correct construction *)

  let app m n : t =
    (* [op] lifts an operator into an ABT *)
    op (App (m, n))

  let lam x m : t =
    (* ["x" #. scope] binds all free variables named "x" in the [scope] *)
    op (Lam (x #. m))

Define the dynamics of your language (here using the variable substitution function subst, provided by the generated syntax):

  let rec eval : t -> t =
    fun t ->
    match t with
    | Opr (App (m, n)) -> apply (eval m) (eval n)
    (* No other terms can be evaluated *)
    | _                -> t

  and apply : t -> t -> t =
    fun m n ->
    match m with
    | Bnd (bnd, t)  -> subst bnd ~value:n t
    | Opr (Lam bnd) -> eval (apply bnd n)
    (* otherwise the application can't be evaluated *)
    | _             -> app m n

Enjoy unification and ɑ-equivalence:

  (* An example term *)
  let k = lam "x" (lam "y" x)

  (* The generated [Syntax] module includes a [Unification] submodule

     - the [=?=] operator checks for unifiability
     - the [=.=] operator gives an [Ok] result with the unified term, if its operands unify,
       or else an [Error] indicating why the unification failed
     - the [unify] function is like [=.=], but it also gives the substitution used to produce
       a unified term *)
  let ((=?=), (=.=), unify) = Unification.((=?=), (=.=), unify) in

  (* A free variable will unify with anything *)
  assert (v "X" =?= s);

  (* Unification is modulo ɑ-equivalence *)
  assert (lam "y" (lam "x" y) =?= lam "x" (lam "y" x));

  (* Here we unify the free variable "M" with the body of the [k] combinator,
     note that the nominal unification is modulo bound variables: *)
  let unified_term = (lam "z" (v "M") =.= k) |> Result.get_ok in
  assert (to_string unified_term = "(λz.(λy.z))");

Modules and interfaces