(* Search for "FIX" to find all the places where you must make changes
     in this file. *)

  (* Your first task in this problem is to implement a function fv 
     that takes a lambda-calculus term and returns the set of variables
     that appear free in that term.  
     We will represent variables using strings.  
     That means that the function fv must return a set of strings.
     You do not have to implement sets (and operations on sets) yourself.
     Instead we will use the set implementation in the standard library.

     The standard library defines a Set module that we first "specialize"
     to get sets of strings.  That is the first line below.  It's okay if 
     you don't quite undertand what this line is doing yet; see below. *)
  
  module String_set = Set.Make (String)


  (* Now we open the String_set module we've created.  The module provides
     us with a value "empty" that is the empty set of strings.  It also 
     provides us with a number of operations that we can use to manipulate 
     sets of strings, such as adding an element (add), removing an element
     (remove), set union (union), checking if a set is empty (is_empty), 
     checking if a given element is in a set (mem), and many more.  
     To see the full list of operations provided, start the ocaml 
     interactive system and type "#use "lambda.ml";;" and take a look at 
     the signature of our String_set module. 
     Recall that once we have opened a module, we can just say "empty" 
     when we want the empty set of strings, rather than typing out 
     "String_set.empty", and similarly for all the other operations 
     provided by String_set*)

  open String_set

  (* define var to be the string type *)
  type var = string

  (* define a type for "sets of variables" *)
  type var_set = String_set.t

  (* define terms of the lambda-calculus *)
  type term = 
  | Var of var
  | Lam of var * term 
  | App of term * term


(****************************************************************)
 
  let id : term = Lam ("x",Var "x")
  let selfapp : term = Lam ("x",App (Var "x",Var "x"))
  let loop : term = App (selfapp,selfapp)
  let eg1 : term = Lam ("x", Lam ("x", App (Var "x",Var "x")))
  let eg2 : term = Lam ("x", Lam ("y", App (Var "x",Var "y")))
  
(****************************************************************)

  (* Your first task is to define the function that computes the set of 
     free variables of a term.  The function takes a term and returns 
     a set of variables.  
     Currently, the function is pretty useless; it always returns an 
     empty set of variables, no matter what the term.  But notice that
     this was sufficient to get the function fv to typecheck. *)

  let fv (e:term) : var_set = empty  (* FIX *)


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

  (* Next, define a function that prints a set of variables 
    (i.e., a set of strings) 
    You must change this function to properly print members of 
    the set s.  The desired format is: {x, y, z}. *)

  let print_varset (s:var_set) : unit =    (* FIX *)
    print_string "FOO\n"

  (* make sure you test your implementation of fv; here is one simple
     test case to start, though it won't work right until you get 
     print_varset working as it should *)

  let _ = print_varset (fv (Lam ("x", App (Var "y", Var "z")))) 


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

  (* a function for printing lambda-calculus terms *)
  let print_term e =
    let rec aux e =
        match e with
          Lam (x,e) -> "lam " ^ x ^ "." ^ (aux e)
        | App (e1, e2) -> "(" ^ (aux e1) ^ ") (" ^ (aux e2) ^ ")"
        | Var v -> v
    in
      print_string (aux e); print_string "\n"

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

  (* a useful function for creating fresh variable names x1, x2, ... *)
  let count : int ref = ref 0
  let freshvar () = 
    let c = !count in
      (count := c + 1; "z"^(string_of_int c))

(****************************************************************)
  
  (* Your next task is to implement capture-avoiding substitution. 
     In class, we wrote "e{e1/x}" for "subst e e1 x" 
     You will probably want to use the function freshvar (defined above)
     to generate fresh variables names *)

  let subst (e:term) (e1:term) (x:var) : term = id  (* FIX *)

  (* Write a function that determines whether a term e is a value. 
     "isval e" returns true if e is a value (i.e., a lambda-term \x.e) 
     and returns false otherwise *)

  let isval (e:term) : bool = true  (* FIX *)

  (* Finally, implement the CBV big-step operational semantics for 
     lambda calculus.  Note that "eval" stands for big-step.  
     Here "eval e" takes a closed term e (i.e., a term with no free 
     variables).  If e is not closed, the function should raise the 
     exception TermNotClosed.  Given a closed term e, "eval e" should 
     return a value (i.e., a lambda-term \x.e' ) if e terminates; 
     otherwise it should diverge.  (Note that if it diverges, you 
     will have to enter Control C to interrupt the execution.) *)

  (* Before you implement eval, make sure you write down the big-step
     CBV operational semantics for the lambda calculus on paper. *)

  (* Raise exception Term NotClosed if the argument is not a 
     closed expression *)

  exception TermNotClosed
  
  let eval (e:term) : term = id  (* FIX *)

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

  (* if e evaluates to e' then "evalsto e" returns e'' where e'' 
     is alpha-equivalent to e' *)

  let evalsto (e:term) : unit =
    (print_string "The term:\n\t\t";
     print_term e;
     print_string "Evaluates to:\n\t\t";
     print_term (eval e))