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).
darcs get http://www.lama.univ-savoie.fr/~raffalli/repos/bindlib
- Bindlib also has a wiki
(* 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)