Source

ocaml-lib / lambda.ml

Sébastien Ferré fb3942c 






Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 

Sébastien Ferré fb3942c 

Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 



Sébastien Ferré 6f6bd36 

Sébastien Ferré fb3942c 


Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 


Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 

Sébastien Ferré 6f6bd36 

Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 


Sébastien Ferré fb3942c 

Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 




Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 


Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 

Sébastien Ferré fb3942c 

Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 


Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 






Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 

Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 








Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 



Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 








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