(* COMP 302 Winter 2013 HOMEWORK 2
   Instructors: Francisco Ferreira, Andrew Cave
   Due 1st February 2013, at the BEGINNING OF CLASS (2:35pm)
 *)

(* Question 1 code for reference *)
infix 3 \/

fun m \/ n = Int.max (m,n)

datatype mobile = Object of int | Wire of mobile * mobile

fun mobile_max (Object n) = n
  | mobile_max (Wire (l,r)) = (mobile_max l) \/ (mobile_max r)

fun mobile_max_acc (Object n) m = n \/ m
  | mobile_max_acc (Wire (l,r)) m = mobile_max_acc l (mobile_max_acc r m)

exception NotImplemented

(* Question 1.1:

Theorem: for any M : mobile, reflect (reflect M) => M
Proof: By structural induction on M.

Case: M = Object n
   reflect (reflect (Object n))
=> reflect (Object n)             (by program reflect)
=> Object n                       (by program reflect)

Case: M = Wire (l,r)
We are granted the I.H: reflect (reflect l) => l and reflect (reflect r) => r

   reflect (reflect (Wire (l,r))
=> reflect (Wire (reflect r, reflect l))                (by program reflect)
=> Wire (reflect (reflect l), reflect (reflect r))      (by program reflect)
=> Wire (l,r)                                           (by I.H.)

*)

(* Question 1.2
We must generalize the statement to:

Lemma: for any M:mobile and x:int, mobile_max_acc M x = (mobile_max M) \/ x
Proof: By structural induction on M.

Case: M = Object n
   mobile_max_acc (Object n) x
=> n \/ x                        (by program mobile_max_acc)

On the other side,
   (mobile_max (Object n)) \/ x
=> n \/ x                        (by program mobile_max)

As required.

Case: M = Wire (l, r)
We are granted the I.H: for any y, mobile_max_acc l y = (mobile_max l) \/ y
                    and for any y, mobile_max_acc r y = (mobile_max r) \/ y

   mobile_max_acc (Wire (l,r)) x
=> mobile_max_acc l (mobile_max_acc r x)      (by program mobile_max_acc)
=  mobile_max_acc l ((mobile_max r) \/ x)     (by I.H. 2 with y = x)
=  (mobile_max l) \/ ((mobile_max r) \/ x)    (by I.H. 1 with y = (mobile_max r) \/ x)
=  (mobile_max l \/ mobile_max r) \/ x        (by associativity of \/)
<= (mobile_max (Wire (l,r)) \/ x              (by program mobile_max)

As required.

Theorem: for any M with positive weights, mobile_max_acc M 0 = mobile_max M
Proof:
Using the lemma with x = 0, we obtain:
mobile_max_acc M 0 = (mobile_max M) \/ 0

And (mobile_max M) \/ 0 = mobile_max M        (property of \/, since mobile_max M is positive)
So we are done.
*)


(* Question 2: Associative lists *)

(* Question 2.1 *)
fun zipWith f xs ys = ListPair.foldr (fn (x,y,z) => (f (x,y))::z) [] (xs,ys) 

(* Question 2.2 *)
fun ziprev xs ys = zipWith (fn (x,y) => (x,y)) xs (List.rev ys)

(* Question 2.3 *)
fun lookup k [] = NONE 
  | lookup k ((k',v)::xs) = if k = k' then SOME v else lookup k xs

(* Question 2.4 *)
type dict = string -> int option

val empty : dict = fn key => NONE

fun insert (k,v) d = fn key => if k = key then SOME v else d key

fun lookup2 k d = d k


(* Question 3 preamble *)

(* Suspended computation : we can suspend computation
   by wrapping it in a closure. *)
datatype 'a susp = Susp of (unit -> 'a)

(* delay: *)
fun delay (f ) = Susp(f)

(* force: *)
fun force (Susp(f)) = f ()

(* ---------------------------------------------------- *)
(* Define an infinite stream *)
datatype 'a stream' = Cons of 'a  * 'a stream
withtype 'a stream = ('a stream') susp

(* ---------------------------------------------------- *)
(* Inspect a stream up to n elements 
   take : int -> 'a stream' susp -> 'a list
   take': int -> 'a stream' -> 'a list
*)
fun take 0 s = []
  | take n (s) = take' n (force s)
and take' 0 s = []
  | take' n (Cons(x,xs)) = x::(take (n-1) xs)

(* Question 3.1 *)
fun hailstones n =
 Susp(fn () => Cons(n, hailstones (if n mod 2 = 0 then n div 2 else 3*n + 1)))

(* Examples:

- take 20 (hailstones 13);
val it = [13,40,20,10,5,16,8,4,2,1,4,2,...] : int list

- take 20 (hailstones 8);
val it = [8,4,2,1,4,2,1,4,2,1,4,2,...] : int list

*)

(* Question 3.2 *)

fun unfold f x = Susp(fn () => Cons(x, unfold f (f x)))

fun deriv f x = let val h = 0.0000001 in (f (x + h) - f x) / h end

fun newton f guess = unfold (fn c => c - (f c) / (deriv f c)) guess 

(* Example:

- take 10 (newton (fn x => x*x - 2.0) 7.0)
val it =
  [7.0,3.64285718209,2.09593841013,1.52508247335,1.41824348423,1.41421928801,
   1.41421356238,1.41421356237,1.41421356237,1.41421356237] : real list

*)