Source

ocaml-lib / lambda.ml

(* objectives:
   - lambda terms as data structures, rather than code
   - introspection of abstractions
   - safety w.r.t. variable names (avoiding variable renaming)
   - internal beta-reduction + customization
   - typed lambda-terms, verified by Caml
*)

class virtual ['a] term =
  object (self)
    method virtual case : 'a
    method subst : (int * 'a term) list -> 'a term = fun env -> (self :> 'a term)
    method reduce : 'a term = (self :> 'a term)
    method virtual to_string : string
    method map : ('a -> 'a term) -> 'a term = fun f -> (self :> 'a term)
  end

type ('a, 'b) expr = Expr of 'a term

class ['a] var (id : int) =
  object (self)
    inherit ['a] term
    val id = id
    method case = `Var id
    method subst env =
      try List.assoc id env
      with Not_found -> (self :> 'a term)
    method to_string = "x" ^ string_of_int id
    method map f = (f (`Var id) :> 'a term)
(*    method fold_left f init = f init self#case *)
  end

class ['a] abs (x : int) (t : 'a term) =
  object (self)
    inherit ['a] term
    val x = x
    val t = t
    method case = `Abs (x,t)
    method subst env = ({<x = x; t = t#subst env>} :> 'a term)
    method reduce = ({<x = x; t = t#reduce>} :> 'a term)
    method to_string = "x" ^ string_of_int x ^ "\\" ^ t#to_string
    method map f = f (`Abs (x, t#map f))
  end
let cpt = ref 0
let abs =
  fun (f : 'a term -> 'a term) ->
    let x = incr cpt; !cpt in
    (new abs x (f (new var x :> 'a term)) :> 'a term)
let eabs (f : ('a,'b) expr -> ('a,'c) expr) : ('a,'b -> 'c) expr =
  Expr (abs (fun x -> let Expr y = f (Expr x) in y))

class ['a] app (t : 'a term) (u : 'a term) =
  object (self)
    inherit ['a] term
    val t = t
    val u = u
    method case = `App (t,u)
    method subst env = ({<t = t#subst env; u = u#subst env>} :> 'a term)
    method reduce =
      let t' = t#reduce in
      match t'#case with
      | `Abs (x,v) -> (v#subst [(x, u)])#reduce
      | _ -> ({<t = t'; u = u#reduce>} :> 'a term)
    method to_string = "(" ^ t#to_string ^ " " ^ u#to_string ^ ")"
    method map f = f (`App (t#map f, u#map f))
  end
let app t u = (new app t u :> 'a term)
let eapp (Expr t : ('a,'b -> 'c) expr) (Expr u : ('a,'b) expr) : ('a,'c) expr =
  Expr (app t u)

(* Optional *)
type 'a case =
    [ `Var of int
    | `Abs of int * 'a
    | `App of 'a * 'a ]
type closed_term = 'a case term as 'a
type 'b closed_expr = (closed_term case,'b) expr

let t0 () : closed_term = abs (fun x -> app x x)
(* let et0 = eabs (fun x -> eapp x x) *) (* should not typecheck *)

(* another (orthogonal) implementation of reduce *)
let reduce_case reduce_rec =
  function
    | `Var x -> new var x
    | `Abs (x,v') -> new abs x v'
    | `App (u',v') ->
	match u'#case with
	| `Abs (x,w) -> reduce_rec (w#subst [(x, v')])
	| _ -> new app u' v'
let rec reduce t = t#map (reduce_case reduce)

let rec reduce t =
  match t#case with
  | `Var x -> new var x
  | `Abs (x,v) -> new abs x (reduce v)
  | `App (u,v) ->
      let u' = reduce u in
      let v' = reduce v in
      match u'#case with
      | `Abs (x,w) -> reduce (w#subst [(x,v')])
      | _ -> new app u' v'

let rec to_string t =
  match t#case with
  | `Var x -> "x" ^ string_of_int x
  | `Abs (x,v) -> "x" ^ string_of_int x ^ "\\" ^ to_string v
  | `App (u,v) -> "(" ^ to_string u ^ ", " ^ to_string v ^ ")"

class ['a] to_string = (* allows extendable recursion without need for additional names *)
  object (self)
    method apply (t : 'a term case) : string =
      match t with
      | `Var x -> "x" ^ string_of_int x
      | `Abs (x,v) -> "x" ^ string_of_int x ^ "\\" ^ self#apply v#case
      | `App (u,v) -> "(" ^ self#apply u#case ^ ", " ^ self#apply v#case ^ ")"
  end

(* Tests *)

let test () =
  let t = abs (fun p2 -> abs (fun np -> abs (fun x -> app np (abs (fun y -> app (app p2 x) y))))) in
  let t1 = t#reduce in
  print_endline t1#to_string

let etest () =
  let Expr t =
    eabs (fun (p2 : ('a,'e -> 'e -> 's) expr) ->
      eabs (fun (np : ('a,('e -> 's) -> 's) expr) ->
	eabs (fun x ->
	  eapp np 
	    (eabs (fun y ->
	      eapp (eapp p2 x) y))))) in
  let t1 = t#reduce in
  print_endline t1#to_string

(* Extension with constants *)

class ['a,'c] const (c : 'c) =
  object
    inherit ['a] term
    val c = c
    method case = `Const c
    method to_string = "const"
  end
let const c = new const c
let econst c : ('a,'b) expr = Expr (const c)

type ('a,'c) case2 = [ 'a case | `Const of 'c]

class ['a,'c] to_string2 =
  object
    inherit ['a] to_string as to_string
    method apply t =
      match t with
      | #case as t1 -> to_string#apply t1
      | `Const (c : 'c) -> "const"
  end

let etest2 () =
  let Expr t = eapp (eabs (fun (x : ('a,'b) expr) -> x)) (econst 1 : ('a,'b) expr) in
  print_endline (to_string2#apply t#case);
  let t1 = t#reduce in
  print_endline t1#to_string