[lambda.git] / code / lambda.ml

(* *)

module Private =  struct
    type var_t = int*string
    let var v = (0,v)
    let string_of_var (i,v) = v ^ String.make i '\''
    let equal_var (i1,v1) (i2,v2) = i1 == i2 && (String.compare v1 v2 == 0)

    type lambda_t = [ `Var of var_t | `Lam of var_t * lambda_t | `App of lambda_t * lambda_t ]

    type debruijn_t = [ `Var of var_t | `DVar of int | `DLam of debruijn_t | `DApp of debruijn_t*debruijn_t ]

    let db_subst (expr : debruijn_t) (m : int) (repl : debruijn_t) =
        let rec rename m i = function
        | `Var _ as term -> term
        | `DVar j as term when j < i -> term
        | `DVar j -> `DVar (j + m - 1)
        | `DApp(n1,n2) -> `DApp(rename m i n1, rename m i n2)
        | `DLam n -> `DLam(rename m (i+1) n)
        in let rec loop m = function
        | `Var _ as term -> term
        | `DVar n as term when n < m -> term
        | `DVar n when n > m -> `DVar (n-1)
        | `DVar n -> rename n 1 repl
        | `DApp(m1,m2) -> `DApp(loop m m1, loop m m2)
        | `DLam mterm -> `DLam(loop (m+1) mterm)
        in loop m expr

    let db (expr : lambda_t) : debruijn_t =
        let pos seq (target : var_t) handler default =
            let rec loop (i : int) = function
            | [] -> default
            | x::xs when equal_var x target -> handler i
            | _::xs -> loop (i+1) xs
            in loop 1 seq
        in let rec loop seq = function
        | `Var v as term -> pos seq v (fun i -> `DVar i) term
        | `Lam (v,t) -> `DLam(loop (v::seq) t)
        | `App (t1,t2) -> `DApp(loop seq t1, loop seq t2)
        in loop [] expr

    let rec db_equal (t1 : debruijn_t) (t2 : debruijn_t) = match (t1,t2) with
    | (`Var v1,`Var v2) -> equal_var v1 v2
    | (`DVar i1, `DVar i2) -> i1 == i2
    | (`DApp(m1,m2),`DApp(n1,n2)) -> db_equal m1 n1 && db_equal m2 n2
    | (`DLam(t1),`DLam(t2)) -> db_equal t1 t2
    | _ -> false

    let rec db_contains (t1 : debruijn_t) (t2 : debruijn_t) = match (t1,t2) with
    | (`Var v1,`Var v2) -> equal_var v1 v2
    | (`DVar i1, `DVar i2) -> i1 == i2
    | (`DApp(m1,m2),`DApp(n1,n2)) when db_equal m1 n1 && db_equal m2 n2 -> true
    | (`DApp(m1,m2), term) -> db_contains m1 term || db_contains m2 term
    | (`DLam(t1),`DLam(t2)) when db_equal t1 t2 -> true
    | (`DLam(t1), term) -> db_contains t1 term
    | _ -> false

    (* non-normalizing string_of_lambda *)
    let string_of_lambda (expr : lambda_t) =
        let rec top = function
            | `Var v -> string_of_var v
            | `Lam _ as t -> "fun " ^ funct t
            | `App ((`App _ as t1),t2) -> top t1 ^ " " ^ atom t2
            | `App (t1,t2) -> atom t1 ^ " " ^ atom t2
        and atom = function
            | `Var v -> string_of_var v
            | `Lam _ as t -> "(fun " ^ funct t ^ ")"
            | `App _ as t -> "(" ^ top t ^ ")"
        and funct = function
            | `Lam (v,(`Lam _ as t)) -> (string_of_var v) ^ " " ^ funct t
            | `Lam (v,t) -> (string_of_var v) ^ " -> " ^ top t
        in top expr


    (* evaluator based on http://okmij.org/ftp/Haskell/Lambda_calc.lhs *)

    (* if v occurs free_in term, returns Some v' where v' is the highest-tagged
     * variable with the same name as v occurring (free or bound) in term *)

    let free_in ((tag, name) as v) term =
        let rec loop = function
        | `Var((tag', name') as v') ->
                if name <> name' then false, v
                else if tag = tag' then true, v
                else false, v'
        | `App(t1, t2) ->
                let b1, ((tag1, _) as v1) = loop t1 in
                let b2, ((tag2, _) as v2) = loop t2 in
                b1 || b2, if tag1 > tag2 then v1 else v2
        | `Lam(x, _) when x = v -> (false, v)
        | `Lam(_, body) -> loop body
        in match loop term with
        | false, _ -> None
        | true, v -> Some v

    let rec subst v st = function
        | term when st = `Var v -> term
        | `Var x when x = v -> st
        | `Var _ as term -> term
        | `App(t1,t2) -> `App(subst v st t1, subst v st t2)
        | `Lam(x, _) as term when x = v -> term
        (* if x is free in the inserted term st, a capture is possible
         * we handle by ...
         *)
        | `Lam(x, body) ->
                (match free_in x st with
                (* x not free in st, can substitute st for v without any captures *)
                | None -> `Lam(x, subst v st body)
                (* x free in st, need to alpha-convert `Lam(x, body) *)
                | Some max_x ->  
                    let bump_tag (tag, name) (tag', _) =
                        (max tag tag') + 1, name in
                    let bump_tag' ((_, name) as v1) ((_, name') as v2) =
                        if name = name' then bump_tag v1 v2 else v1 in
                    (* bump x > max_x from st, then check whether
                     * it also needs to be bumped > v
                     *)
                    let uniq_x = bump_tag' (bump_tag x max_x) v in
                    let uniq_x' = (match free_in uniq_x body with
                        | None -> uniq_x
                        (* bump uniq_x > max_x' from body *)
                        | Some max_x' -> bump_tag uniq_x max_x'
                    ) in
                    (* alpha-convert body *)
                    let body' = subst x (`Var uniq_x') body in
                    (* now substitute st for v *)
                    `Lam(uniq_x', subst v st body')
                )

    let check_eta = function
        | `Lam(v, `App(t, `Var u)) when v = u && free_in v t = None -> t
        | (_ : lambda_t) as term -> term

    exception Lambda_looping;;

    let eval ?(eta=false) (expr : lambda_t) : lambda_t =
        let rec looping (body : debruijn_t) = function
        | [] -> false
        | x::xs when db_equal body x -> true
        | _::xs -> looping body xs
        in let rec loop (stack : lambda_t list) (body : lambda_t) = 
            match body with
            | `Var v as term -> unwind term stack
            | `App(t1, t2) as term -> loop (t2::stack) t1
            | `Lam(v, body) -> (match stack with
                | [] ->
                    let term = (`Lam(v, loop [] body)) in
                        if eta then check_eta term else term
                | t::rest -> loop rest (subst v t body)
            )
        and unwind t1 = function
        | [] -> t1
        | t2::ts -> unwind (`App(t1, loop [] t2)) ts
        in loop [] expr


    (* (Oleg's version of) Ken's evaluator; doesn't seem to work -- requires laziness? *)

    let eval' ?(eta=false) (expr : lambda_t) : lambda_t =
        let rec loop = function
        | `Var v as term -> term
        | `Lam(v, body) ->
                let term = (`Lam(v, loop body)) in
                    if eta then check_eta term else term
        | `App(`App _ as t1, t2) ->
            (match loop t1 with
                | `Lam _ as redux -> loop (`App(redux, t2))
                | nonred_head -> `App(nonred_head, loop t2)
            )
        | `App(t1, t2) -> `App(t1, loop t2)
        in loop expr

    let cbv ?(aggressive=true) (expr : lambda_t) : lambda_t =
        let rec loop = function
        | `Var x as term -> term
        | `App(t1,t2) ->
                let t2' = loop t2 in
                (match loop t1 with
                | `Lam(x, t) -> loop (subst x t2' t)
                | _ as term -> `App(term, t2')
                )
        | `Lam(x, t) as term ->
                if aggressive then `Lam(x, loop t)
                else term
        in loop expr



    (*
        module Sorted = struct
            let rec cons y = function
                | x :: _ as xs when x = y -> xs
                | x :: xs when x < y -> x :: cons y xs
                | xs [* [] or x > y *] -> y :: xs

            let rec mem y = function
                | x :: _ when x = y -> true
                | x :: xs when x < y -> mem y xs
                | _ [* [] or x > y *] -> false

            let rec remove y = function
                | x :: xs when x = y -> xs
                | x :: xs when x < y -> x :: remove y xs
                | xs [* [] or x > y *] -> xs

            let rec merge x' y' = match x', y' with
                | [], ys -> ys
                | xs, [] -> xs
                | x::xs, y::ys ->
                    if x < y then x :: merge xs y'
                    else if x = y then x :: merge xs ys
                    else [* x > y *] y :: merge x' ys
        end

        let free_vars (expr : lambda_t) : string list =
            let rec loop = function
                | `Var x -> [x]
                | `Lam(x,t) -> Sorted.remove x (loop t)
                | `App(t1,t2) -> Sorted.merge (loop t1) (loop t2)
            in loop expr

        let free_in v (expr : lambda_t) =
            Sorted.mem v (free_vars t)

        let new_var =
            let counter = ref 0 in
            fun () -> (let z = !counter in incr counter; "_v"^(string_of_int z))

        ...
        | `Lam(x, body) as term when not (free_in v body) -> term
        | `Lam(y, body) when not (free_in y st) -> `Lam(y, subst v st body)
        | `Lam(y, body) ->
            let z = new_var () in
            subst v st (`Lam(z, subst y (`Var z) body))
    *)



    (*

    let bound_vars (expr : lambda_t) : string list =
        let rec loop = function
            | `Var x -> []
            | `Lam(x,t) -> Sorted.cons x (loop t)
            | `App(t1,t2) -> Sorted.merge (loop t1) (loop t2)
        in loop expr

    let reduce_cbv ?(aggressive=true) (expr : lambda_t) : lambda_t =
        let rec loop = function
        | `Var x as term -> term
        | `App(t1,t2) ->
                let t2' = loop t2 in
                (match loop t1 with
                | `Lam(x, t) -> loop (subst x t2' t)
                | _ as term -> `App(term, t2')
                )
        | `Lam(x, t) as term ->
                if aggressive then `Lam(x, loop t)
                else term
        in loop expr

    let reduce_cbn (expr : lambda_t) : lambda_t =
        let rec loop = function
        | `Var x as term -> term
        | `Lam(v, body) ->
                check_eta (`Lam(v, loop body))
        | `App(t1,t2) ->
                (match loop t1 with
                | `Lam(x, t) -> loop (subst x t2 t)
                | _ as term -> `App(term, loop t2)
                )
        in loop expr

    *)


    (*

    type env_t = (string * lambda_t) list

    let subst body x value =
        ((fun env ->
            let new_env = (x, value) :: env in
            body new_env) : env_t -> lambda_t)

    type strategy_t = By_value | By_name

    let eval (strategy : strategy_t) (expr : lambda_t) : lambda_t =
        in let rec inner = function
            | `Var x as t ->
                (fun env ->
                    try List.assoc x env with
                    | Not_found -> t)
            | `App(t1, value) -> 
                (fun env ->
                    let value' =
                        if strategy = By_value then inner value env else value in
                    (match inner t1 env with
                    | `Lam(x, body) ->
                        let body' = (subst (inner body) x value' env) in
                        if strategy = By_value then body' else inner body' env
                    | (t1' : lambda_t) -> `App(t1', inner value env)
                    )
                )
            | `Lam(x, body) ->
                (fun env ->
                    let v = new_var () in
                    `Lam(v, inner body ((x,`Var v) :: env)))
        in inner expr ([] : env_t)

    let pp_env env =
        let rec loop acc = function
            | [] -> acc
            | (x,term)::es -> loop ((x ^ "=" ^ string_of_lambda term) :: acc) es
        in "[" ^ (String.concat ", " (loop [] (List.rev env))) ^ "]"

    let eval (strategy : strategy_t) (expr : lambda_t) : lambda_t =
        let new_var =
            let counter = ref 0 in
            fun () -> (let z = !counter in incr counter; "_v"^(string_of_int z))
        in let rec inner term =
            begin
            Printf.printf "starting [ %s ]\n" (string_of_lambda term);
            let res = match term with
            | `Var x as t ->
                (fun env ->
                    try List.assoc x env with
                    | Not_found -> t)
            | `App(t1, value) -> 
                (fun env ->
                    let value' =
                        if strategy = By_value then inner value env else value in
                    (match inner t1 env with
                    | `Lam(x, body) ->
                        let body' = (subst (inner body) x value' env) in
                        if strategy = By_value then body' else inner body' env
                    | (t1' : lambda_t) -> `App(t1', inner value env)
                    )
                )
            | `Lam(x, body) ->
                (fun env ->
                    let v = new_var () in
                    `Lam(v, inner body ((x,`Var v) :: env)))
            in
            (fun env -> 
                (Printf.printf "%s with %s => %s\n" (string_of_lambda term) (pp_env env) (string_of_lambda (res env)); res env))
            end
        in inner expr ([] : env_t)

    *)

    let normal ?(eta=false) expr = eval ~eta expr

    let normal_string_of_lambda ?(eta=false) (expr : lambda_t) =
        string_of_lambda (normal ~eta expr)

    let rec to_int expr = match expr with
        | `Lam(s, `Lam(z, `Var z')) when z' = z -> 0
        | `Lam(s, `Var s') when s = s' -> 1
        | `Lam(s, `Lam(z, `App (`Var s', t))) when s' = s -> 1 + to_int (`Lam(s, `Lam(z, t)))
        | _ -> failwith (normal_string_of_lambda expr ^ " is not a church numeral")

    let int_of_lambda ?(eta=false) (expr : lambda_t) =
        to_int (normal ~eta expr)

end

type lambda_t = Private.lambda_t
open Private
let var = var
let pp, pn, pi = string_of_lambda, normal_string_of_lambda, int_of_lambda
let pnv,piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr))
let db, db_equal, db_contains = db, db_equal, db_contains