Source

ocaml-lib / lambda.ml

Full commit
(* 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 virtual map : ('a -> 'a term) -> 'a term
(*
    method virtual fold_left : 'b. ('b -> 'a -> 'b) -> 'b -> 'b
*)
  end

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

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

class ['a] abs (x : 'a var) (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#to_string ^ "\\" ^ t#to_string
    method map f = f (`Abs (x, t#map f))
  end
let abs (f : 'a term -> 'a term) =
  let x = new var in
  (new abs x (f (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 =
      match t#case with
      | `Abs (x,v) -> (v#subst [(Oo.id x, u)])#reduce
      | _ -> ({<t = t#reduce; 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 'a * '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 *)

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

(* 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