(* Exercise 1 *)
(* Look at the following type definition. *)
type color = Red | Yellow | Blue | Green | Orange | Other of string
type favorite = Color of color | Movie of string | Tvshow of string |
    Number of float | Letter of char

(* We've defined some sample lists of favorite movies/colors/etc.
 * You can think of each of these lists as representing someone's
 * input describing their favorite things. 
 * You may want to use these for testing your functions later.*)

let a : favorite list = [Movie "Love Story"; Color Blue;
                         Tvshow "The Simpsons"; Color Orange];;

let b : favorite list = [Number 1.0; Number 2.0; Number 5.0;
                         Number 14.0; Number 42.0];;

let c : favorite list = [Movie "A Beautiful Mind"; Tvshow "House";
                         Letter 'P'; Color Orange];;

let d : favorite list = [Tvshow "Lost"; Number 3.14];;

let students = [a; b; c; d];;
							 
(* 1a. Define a value of type favorite list for someone whose
 * favorite color is Crimson and whose favorite number is 5. *)

let prob1a : favorite list = failwith "unimplemented";;

(* 1b. Write a function that takes a value of type favorite list (like the
 * ones above) and returns the title of this person's favorite movie, or 
 * None if a favorite movie isn't given. If multiple movies are listed, 
 * return the first. What return type does this function have? *)


(*
let rec favmovie (lst: favorite list) : ???  =
*)


(* 1c. Write a function that takes a value of type favorite list and returns 
 * true if and only if this person has listed Orange as a favorite color. *)

(*
let rec princetonpride (lst: favorite list) : ??? =
*)


(* Exercise 2 *)
(* 2a. Define an algebraic data type representing either ints or floats *)

(*
type realnum = 
*)

(* 2b. Define a function testing whether two realnums are equal. It shouldn't
 * matter whether they are ints or floats, e.g (realequal 4 4.0) => True. *)

(*
let realequal (a: realnum) (b: realnum) : bool = failwith "unimplemented";;
*)

(* Exercise 3: an expansion of last week's "form", as seen in precept *)
type var = string
type form =   
    Var of var 
  | And of forms
  | Or of forms
and type forms = form list;;

type env = (var * bool) list;;

(* We have defined a variable type 'var' and a boolean formula that is 
 * made up of 'And's and 'Or's of variables. An environment is a mapping 
 * from variables to boolean values. 
 *)

(* 3a. Write a function that given a boolean formula returns the list of all
 * unique variables that may be found in the bolean formula 
 *)

   
let fVars (f:form) : var list  = failwith "unimplemented";;


(* 3b. Write a function that takes a boolean formula and returns 
 * Some e -- if there exists a satisfying environment for the formula
 *             (and e is one such satisfying assignment)
 * None   -- if there does not exist a satisfying assignment
 *)

let is_Sat (f: form) : env option = failwith "unimplemented";;

(* 3c.  Add a negation formula (Not of form) to the formula representation
 * above and update your functions for finding the free variables, 
 * satisfying assignments, etc. 
 *) 


(* Exercise 4 *)

(* 4a. Given the function below, give a short proof that
 * double N = 2*N
*)
let double (n: int) : int =
  n + n
;;


(*
  4b. Given the function below, prove that for any natural number N:
  sum_sqrs N = (N * (N+1) * (2*N + 1))/6
  
  You may assume that we have already proved this lemma:
   If N=k+1 and N is a natural number > 0, 
   then k must also be a natural number
*)

let rec sum_sqrs (n: int) : int =
  if n <= 0 then 0
  else (n*n) + sum_sqrs(n-1)
;;

(*
  4c. Given the functions below, prove that for any list:
  behead ( prepend xs x) = xs
*)

let prepend (xs: 'a list) (x: 'a) : 'a list =
  x::xs
;;

let behead (xs: 'a list) =
  match xs with
  | [] -> []
  | hd::tl -> tl
;;


(* 
   4d. Given the function below, prove that for any list:
   noop xs = xs
*)

let rec noop (xs: 'a list) : 'a list =
  match xs with
  | [] -> []
  | hd::tl -> hd :: noop tl
;;