package um-abt

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Overview
Example
Interfaces
Top-level modules

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

Overview

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

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

um-abt also supports unification over ABTs.

Example

A typical example of a module satisfying this interface, used to represent the syntax of the untyped lambda calculus:

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

include Abt.Make (O)

Note the use of ppx_deriving to derive most values automatically.

Interfaces

module type Operator = sig ... end

The interface for a module that defines the operators of a language

Top-level modules

module Var : sig ... end

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

module type Syntax = sig ... end

module Make (Op : Operator) : Syntax with module Op = Op

Make (Op) is a module for constructing and manipulating the Syntax of a language with Operators defined by Op.