The Bindlib Library

Version 3.2

bindlib is a library and a camlp4 extension for the Objective-Caml language providing reasonable tools to write programs manipulating data structures with bound variables (like lambda-calculus or quantified formulae). It is quite efficient and easy to use (thanks to the camlp4 extension).

Example

The library comes with some examples, here is one of them: the normalisation of lambda-terms: 
(* lets open the library ! *)
open Bindlib

(* type of pure lambda-terms *)

type term =
  App of term * term
| Abs of (term,term) binder
| FVar of term variable

(* weak head normal form *)

let rec whnf = function
  App(t1,t2) as t0 -> (
    match (whnf t1) with
      Abs f -> whnf (subst f t2)
    | t1' -> if t1' != t1 then App(t1', t2) else t0)
| t -> t

(* call by name normalisation *)
let norm t = let rec fn t =
  match whnf t with
    Abs f ->
      (match f with bind fVar x in u ->
      Abs(^ bindvar x in fn u ^) )
  | t ->
      let rec unwind = function
          FVar(x) -> bindbox_of x
        | App(t1,t2) -> App(^unwind t1,fn t2^)
        | t -> assert false
      in unwind t
in unbox (fn t)
Christophe Raffalli /LAMA, Savoie University / raffalli@univ-savoie.fr