(* Mini-project/Homework on the Lambda-calculus *)

(* This file contains an OCaml implementation of the lambda-calculus,
   extended to include integers and strings as primitive data types.
   You can use the functions in this file to play around with
   lambda terms in formulating the solutions to the exercises at
   the bottom.

   Note that the answers to all of these problems are in
   Pierce.  Don't look at the answers until you've played around
   with it all yourself! *)

(* lambda calculus extended with integers *)

(* The encoding of lambda terms uses a trick called "higher-order
   abstract syntax".  Whenever you want to write the term
   \x.\y. (x y), you write instead
   Lambda (fun x -> Lambda (fun y -> App (x,y)))
   In essence, variables come from OCaml, rather than as part
   of term type definition.
*)

type term =
  Lambda of (term -> term)
| App of term * term
| Int of int

(* beta reduction: reduces the innermost, leftmost application.
   Notice that it doesn't reduce the argument before applying
   the function. *)
let rec beta t =
  match t with
    (Lambda _ | Int _) -> t
  | App ((Int _),_) -> raise (Invalid_argument "application of Int")
  | App ((Lambda f),t2) -> f t2
  | App (t1,t2) -> App ((beta t1),t2)

(* transitive closure of beta *)
let rec eval t =
  match t with
    (Lambda _ | Int _) -> t
  | _ -> let res = beta t in eval res

(* Church numerals; some constants *)
let zero = Lambda (fun f -> Lambda (fun x -> x))
let one = Lambda (fun f -> Lambda (fun x -> App (f, x)))
let two = Lambda (fun f -> Lambda (fun x -> App (f,App (f, x))))

(* Church numerals; some functions *)

(* returns 0 if the given church numeral is not zero,
   returns 1 if the given church numeral is zero *)
let iszero = Lambda (fun n -> 
  App (App (n,(Lambda (fun f -> (Int 0)))),Int 1))

(* the successor function; adds one to the given Church numeral *)
let succ =
  Lambda (fun n ->
    Lambda (fun f ->
      Lambda (fun x -> App (f, (App (App (n,f), x))))))

(* converts a Church numeral to an integer *)
let ctoi t =
  let inc = Lambda (fun t -> 
    (* calling eval is cheating a bit ... *)
    match (eval t) with
      Int i -> Int (i+1)
    | _ -> raise (Invalid_argument "not an int!")) in
  eval (App (App (t,inc), (Int 0)))

(* Here are some warm-ups, so you understand how these functions work. *)

let x = ctoi zero;;  (* evaluates to Int 0 *)
let y = ctoi (App (succ,one));;  (* evaluates to Int 2 *)
let z = eval (App (iszero,zero));;  (* evaluates to Int 1 *)
let nz = eval (App (iszero, App (succ,one)));;  (* evaluates to Int 0 *)

(************************************************************************)

(* Here are the exercises *)

(* 1. write an Ocaml function itoc that turns a non-negative integer
   into a Church numeral.  Extra credit: do it tail-recursively. *)

let itoc i = zero (* XXX fill in your code here *)

(* Test for part 1. *)
let ten = ctoi (itoc 10);; (* should be Int 10 *)
let w = ctoi (itoc 0);; (* should be Int 0 *)

(************************************************************************)

(* 2. Consider the following OCaml function cwhat.  What well-known
   arithmetic function does this compute?  Justify your answer 
   by including some experiments. *)

let cwhat m n = 
  Lambda (fun f -> 
    Lambda (fun x ->
      App (App (m,f), (App (App (n,f),x)))))


(************************************************************************)

(* 3. Implement a two-argument function cmul that multiples Church
   numerals.  This is considerably simpler than the definition of
   cwhat, above. *)

let mul m n = zero  (* XXX fill in your code here *)

(* Some tests *)
let f = ctoi (mul two two);;   (* Should be Int 4 *)
let twenty = ctoi (mul two (itoc 10));;  (* Should be Int 20 *)
let z2 = ctoi (mul two zero);;  (* Should be Int 0 *)


(************************************************************************)

(* 4. Implement exponentiation m to the n power.  This is even simpler
   than multiplication! *)

let exp m n = zero  (* XXX fill in your code here *)

(* Some tests *)
let eight = ctoi (exp two (App (succ,two)));;
let unit = ctoi (exp two one);;
let off = ctoi (exp two zero);;

(************************************************************************)

(* 5. Write an encoding of lists.  You should write the following
   definitions as values of type term: nil, head, cons, tail, and isnil.
   These should obey the following laws (according to beta reduction)

      head (cons e1 e2) = e1
      tail (cons e1 e2) = e2
      isnil nil e1 e2 = e1
      isnil (cons e1 e2) e3 e4 = e4

   This is exercise 5.2.8 of Pierce (Chap 5).  Feel free to write
   in paper rather than type it all in, if that turns out to be
   too difficult.

   For extra credit, write a routine that sums a list of integers!
*)