;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;                        Problem 1 Solution                        ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 
;; Prove: 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2
;; _____________________________________________________________________
;; 
;; P(n): 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2
;; Claim: P(n) is true, for all n >= 1
;; 
;; Proof by Induction on n
;; 
;;     BASE CASE: n = 1
;;        1^3 = 1^2        [This is true]
;; 
;;     INDUCTIVE STEP: Let k >= 1
;;        Assume P(k) is true:
;;          1^3 + ... + k^3 = (1 + ... + k)^2   [Induction Hypothesis]
;;        Prove P(k+1) is also true:
;;          1^3 + ... + k^3 + (k+1)^3 = (1 + ... + k + (k+1))^2
;;    
;;        LEMMA:
;;          1 + 2 + ... + k = k*(k+1)/2
;;          {See Induction Examples Web Page for proof of this equality}
;;    
;;        1^3 + ... + k^3 + (k+1)^3
;;            = (1 + ... + k)^2 + (k+1)^3       [by I.H.]
;;            = (k*(k+1)/2)^2 + (k+1)^3         [by Lemma]
;;            = ((k^2)/4 + (k+1))*(k+1)^2       [by Distribution]
;;            = ((k^2+4k+4)/4)*(k+1)^2          [by Fraction Addition]
;;            = ((k+1)*(k+2)/2)^2               [by Algebra]
;;            = (1 + ... + k + (k+1))^2         [by Lemma]
;;      
;;     Thus we have proven our claim is true by Induction on n
;;                                                                  QED
;; 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;                        Problem 2 Solution                        ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (parse-operands op args ident)
  (cond ((null? (tail args))
          (list ident (parse (first args))))
        ((null? (tail (tail args)))
          (list (parse (first args)) (parse (second args))))
        (else
          (list (parse (first args))
                (parse-list op (tail args))))))

;;;;;; OUTPUT SAMPLE
;; 
;; ==> (unparse (parse '(+ 2 3 (* 4 5 6) 7)))
;; (+ 2 (+ 3 (+ (* 5 6)) 7)))
;;
;; ==> (unparse (parse '(- 1)))
;; (- 0 1)
;;
;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;                        Problem 3 Solution                        ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (extend-env params args env)
  (cond 
    ((not (= (length params) (length args)))
       (error "Number of arguments do not match number of parameters"))
    ((null? params)
       env)
    (else
      (add-binding (make <binding> :name (head params)
                                   :val  (head args))
                   (extend-env (tail params) (tail args) env)))))  

;;;;;; OUTPUT SAMPLE
;; 
;; ==> (start-evaluator)
;; ExpEv> (define-function square (x) (* x x))
;; square
;; ExpEv> (evaluate (sqaure 3))
;; 9
;;
;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;                        Problem 4 Solution                        ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defgeneric (simplify input environment))

(defmethod (simplify symbol env)
  (letrec ((lookup (lambda (rest)
                     (cond ((null? rest) symbol)
                           ((equal? symbol (name (head rest)))
                              (val (head rest)))
                           (else (lookup (tail rest)))))))
     (lookup env)))

(defmethod (simplify exp env)
  (simplify-exp (operator exp)
                (map (lambda (x) (simplify x env)) 
                     (operands exp))
                env))

;;;;;; OUTPUT SAMPLE
;; 
;; ==> (start-evaluator)
;; ExpEv> (define-constant y 10)
;; y
;; ExpEv> (simplify (square (+ 1 y)))
;; (square (+ 10 3))
;;
;;;;;;