;;; Sample solutions for MP8

Task 1.
=======

  ;; bound-variables : Program -> Listof[Symbol]
  ;;
  ;; (bound-variables pgm) returns a list of the variables that
  ;; occur bound in pgm or are bound in the standard initial
  ;; environment.

  (define (bound-variables pgm)
    (cases program pgm
     (a-program (defns exp)
      (apply append
             '(true false x)
             (map (lambda (defn)
                    (cases definition defn
                     (proc-definition (id bvars body)
                      (cons id bvars))))
                  defns)))))


Task 2.
=======

  ;; well-typed-expression? : Expression -> Boolean
  ;;
  ;; (well-typed-expression? exp) returns true if and only if
  ;; (a-program '() exp) is well-typed.

  (define (well-typed-expression? exp)
    (well-typed? (a-program '() exp)))


Task 3.
=======

Note: This version fixes a bug for if expressions
that was pointed out to us by Vicky Chan.

  ;; collect-constraints : Program -> Listof[TypeConstraint]
  ;;
  ;; (collect-constraints pgm) returns a list of type constraints
  ;; that are satisfiable if and only pgm is well-typed.
  ;;
  ;; precondition: No variable is bound in more than one place.

  (define (collect-constraints pgm)
    (cases program pgm
     (a-program (defns exp)
      (let* ((bvars (bound-variables pgm))
             (env (bound-variables-env bvars))
             (tvar (fresh-type-variable)))
        (append (list
                 (make-type-constraint (apply-env env 'true) (bool-type))
                 (make-type-constraint (apply-env env 'false) (bool-type))
                 (make-type-constraint (apply-env env 'x) (int-type)))
                (collect-constraints-for-definitions defns env)
                (collect-constraints-for-expression exp tvar env))))))

  ;; collect-constraints-for-definitions : Listof[Definition] * Env
  ;;                                       -> Listof[TypeConstraint]
  ;;
  ;; (collect-constraints-for-definitions defns env)
  ;; returns a list of type constraints that are satisfiable
  ;; if and only the given definitions are well-typed.
  ;;
  ;; precondition: env associates all bound variables with
  ;; distinct type variables.

  (define (collect-constraints-for-definitions defns env)
   (cond ((null? defns) '())
         (else
          (cases definition (car defns)
           (proc-definition (id bvars body)
            (let* ((tvar0 (apply-env env id))
                   (tvars (map (lambda (bvar) (apply-env env bvar))
                               bvars))
                   (tvar (fresh-type-variable))
                   (ty0 (proc-type tvars tvar))
                   (tc0 (make-type-constraint tvar0 ty0))
                   (tcs (collect-constraints-for-expression body tvar env)))
              (append
               (cons tc0 tcs)
               (collect-constraints-for-definitions (cdr defns) env))))))))

  ;; collect-constraints-for-expression : Expression * TypeVariable * Env
  ;;                                      -> Listof[TypeConstraint]
  ;;
  ;; (collect-constraints-for-expression exp tvar env)
  ;; returns a list of type constraints that are satisfiable
  ;; if and only the given expression is well-typed.
  ;;
  ;; precondition: tvar is a fresh type variable that stands
  ;; for the type of exp
  ;;
  ;; precondition: env associates all bound variables with
  ;; distinct type variables.

  (define (collect-constraints-for-expression exp tvar env)
    (cases expression exp

        (lit-exp (num)
          (list (make-type-constraint tvar (int-type))))

        (var-exp (id)
          (let ((tvar1 (apply-env env id)))
            (if tvar1
                (list (make-type-constraint tvar tvar1))
                (list (make-type-constraint tvar (int-type))
                      (make-type-constraint tvar (bool-type))))))

        (binop-exp (op exp1 exp2)
          (let* ((tvar1 (fresh-type-variable))
                 (tcs1 (collect-constraints-for-expression exp1 tvar1 env))
                 (tvar2 (fresh-type-variable))
                 (tcs2 (collect-constraints-for-expression exp2 tvar2 env))
                 (ty (op-type op))
                 (argtypes (proc-type-argument-types ty))
                 (ty1 (car argtypes))
                 (ty2 (cadr argtypes))
                 (ty3 (proc-type-result-type ty)))
            (append (list (make-type-constraint tvar1 ty1)
                          (make-type-constraint tvar2 ty2)
                          (make-type-constraint tvar ty3))
                    tcs1
                    tcs2)))

        (if-exp (exp1 exp2 exp3)
          (let* ((tvar1 (fresh-type-variable))
                 (tcs1 (collect-constraints-for-expression exp1 tvar1 env))
                 (tvar2 (fresh-type-variable))
                 (tcs2 (collect-constraints-for-expression exp2 tvar2 env))
                 (tvar3 (fresh-type-variable))
                 (tcs3 (collect-constraints-for-expression exp3 tvar3 env)))
            (append (list (make-type-constraint tvar1 (bool-type))
                          (make-type-constraint tvar2 tvar3)
                          (make-type-constraint tvar2 tvar))
                    tcs1
                    tcs2
                    tcs3)))

        (call-exp (rator rands)
          (let* ((tvar0 (fresh-type-variable))
                 (tcs0 (collect-constraints-for-expression rator tvar0 env))
                 (tvars (map (lambda (rand) (fresh-type-variable))
                             rands))
                 (tcss (map (lambda (rand tvar)
                              (collect-constraints-for-expression
                               rand tvar env))
                            rands
                            tvars))
                 (ty0 (proc-type tvars tvar)))
            (cons (make-type-constraint tvar0 ty0)
                  (apply append
                         tcs0
                         tcss))))))

  ;; op-type : Binop -> Type
  ;;
  ;; (op-type op) returns the type of op

  (define (op-type op)
    (cases binop op
     (op-plus    () (proc-type (list (int-type) (int-type)) (int-type)))
     (op-minus   () (proc-type (list (int-type) (int-type)) (int-type)))
     (op-times   () (proc-type (list (int-type) (int-type)) (int-type)))
     (op-less    () (proc-type (list (int-type) (int-type)) (bool-type)))
     (op-equal   () (proc-type (list (int-type) (int-type)) (bool-type)))
     (op-greater () (proc-type (list (int-type) (int-type)) (bool-type)))))
  
  ;; bound-variables-env : Listof[Identifier] -> Env
  ;;
  ;; (bound-variables-env bvars) returns an environment
  ;; that associates each identifier in bvars with a fresh type variable.

  (define (bound-variables-env bvars)
    (cond ((null? bvars)
           (empty-env))
          (else
           (extend-env (car bvars)
                       (fresh-type-variable)
                       (bound-variables-env (cdr bvars))))))


Task 4.
=======

Yes, the program is type-safe because its execution cannot
result in a type error.

No, the program is not well-typed because the type system for
PROC cannot express a type t such that t = (t -> (int -> int)).
Hence there is no possible type for a procedure that accepts
itself as an argument.