Source

ocaml-lib / lambda.ml

Full commit
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é 06460f4 
Sébastien Ferré 6f6bd36 

Sébastien Ferré fb3942c 

Sébastien Ferré 06460f4 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 06460f4 

Sébastien Ferré 6f6bd36 
Sébastien Ferré 06460f4 
Sébastien Ferré fb3942c 
Sébastien Ferré 06460f4 

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

Sébastien Ferré 06460f4 
Sébastien Ferré 6f6bd36 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 


Sébastien Ferré fb3942c 

Sébastien Ferré 06460f4 
Sébastien Ferré fb3942c 
Sébastien Ferré 6f6bd36 
Sébastien Ferré 06460f4 




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é 06460f4 



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é 06460f4 
Sébastien Ferré fb3942c 


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

Sébastien Ferré 6f6bd36 
Sébastien Ferré 06460f4 










Sébastien Ferré fb3942c 
Sébastien Ferré 06460f4 























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é 06460f4 




























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