;;; This file contains code from the figures of the draft chapter 13
;;; of "Essentials of Programming Languages".
;;;
;;; Copyright (c) 1994, D. Friedman, M. Wand, and C. Haynes

(load "~max/www-docs/courses/S2000/MCS-287/code/drscheme-eopl.ss")
;; chap13-parser-etc.ss is based on EOPL appendices B-F, with additions 
;;  for chapter 13
(load "~max/www-docs/courses/S2000/MCS-287/labs/lab4/chap13-parser-etc.ss")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; The environment ADT is pretty much the same as in the previous lab,
;; but I've eliminated the-empty-env and replaced it with
;; make-empty-env, a procedure for creating a new empty environment.
;; I did this because in this lab you may wind up with several
;; initially empty environments, some of which might have bindings
;; added, so that they don't stay empty.  Thus it would be bad if they
;; were all the same environment.

;; EOPL page 142 defines environments as finite functions, but this
;; won't work well when definitions are added to the language (p. 159),
;; since a definition should really add a new binding to the existing
;; top-level environment, rather than extending it to create a new environment.
;; (That way, any procedures closed over the top-level environment have
;; access to the new binding.  This permits recursion, including mutual
;; recursion.  Even procedures closed over an extension of the top-level
;; environment, rather than the top-level environment itself, ought to have
;; access to the new binding, provided it isn't shadowed by an inner binding.)
;; The definitions below produce an env ADT that can be used just like the one
;; on EOPL p. 142, but with the extra operation add-binding-to-env!.

(define-record forever-empty-env ())
(define-record extended-env (syms vals base-env))

(define make-empty-env
  (lambda ()
    (make-extended-env '() '() (make-forever-empty-env))))

(define extend-env make-extended-env)

(define apply-env
  (lambda (env sym)
    (variant-case env
      (forever-empty-env () (error "no binding for symbol" sym))
      (extended-env
       (syms vals base-env)
       (letrec ((loop (lambda (syms vals)
                        (cond ((null? syms)
                               (apply-env base-env sym))
                              ((eq? (car syms) sym)
                               (car vals))
                              (else
                               (loop (cdr syms) (cdr vals)))))))
         (loop syms vals)))
      (else (error "illegal environment" env)))))

(define add-binding-to-env!
  (lambda (sym val env)
    (set-extended-env-syms! env (cons sym (extended-env->syms env)))
    (set-extended-env-vals! env (cons val (extended-env->vals env)))))

(define compose
  (lambda (f g)
    (lambda (x)
      (f (g x)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Figure 13.1.4

(define domains (compose cdr tcons->types))
(define range (compose car tcons->types))

(define integer-type (make-tcons 'int '()))
(define boolean-type (make-tcons 'bool '()))

(define type-of-datum
  (lambda (datum)
    (if (integer? datum) integer-type boolean-type)))

(define proc-type?
  (lambda (type)
    (and (tcons? type) (eq? '-> (tcons->name type)))))

(define make-proc-type
  (lambda (domain-types range-type)
    (make-tcons '-> (cons range-type domain-types))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Type environments

(define make-empty-tenv make-empty-env)
(define extend-tenv extend-env)
(define apply-tenv apply-env)
(define add-binding-to-tenv! add-binding-to-env!)

(define init-tenv 
  (extend-env
   '(+ - * add1 sub1 zero eq)
   (list (make-proc-type (list integer-type integer-type) integer-type)
         (make-proc-type (list integer-type integer-type) integer-type)
         (make-proc-type (list integer-type integer-type) integer-type)
         (make-proc-type (list integer-type) integer-type)
         (make-proc-type (list integer-type) integer-type)
         (make-proc-type (list integer-type) boolean-type)
         (make-proc-type (list integer-type integer-type) boolean-type))
    (make-empty-tenv)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Figures 13.1.5-13.1.9

(define match-types
  (letrec
    ((same-type?
       (lambda (type1 type2)
         (let ((types1 (tcons->types type1))
               (types2 (tcons->types type2)))
           (and (eq? (tcons->name type1) (tcons->name type2))
             (= (length types1) (length types2))
             (andmap2 same-type? types1 types2))))))
    (lambda (type1 type2)
      (if (not (same-type? type1 type2))
        (type-error "Incompatible types:" type1 type2)))))

(define match-types-pairwise
  (lambda (types1 types2)
    (for-each match-types types1 types2)))

(define andmap2
  (lambda (predicate list1 list2)
    (or (null? list1)
      (and (predicate (car list1) (car list2))
        (andmap2 predicate (cdr list1) (cdr list2))))))

(define type-error
  (lambda ls
    (display "Type error: ")
    (display (car ls))
    (newline)
    (for-each
      (lambda (type) (displayln (unparse-type type)))
      (cdr ls))
    (error)))

(define type-of-exp
  (lambda (exp tenv)
    (trace-entry exp)
    (let ((answer
            (variant-case exp
              (lit (datum) (type-of-datum datum))
              (varref (var) (apply-tenv tenv var))
              (if (test-exp then-exp else-exp)
                (let ((test-exp-type (type-of-exp test-exp tenv))
                      (then-exp-type (type-of-exp then-exp tenv))
                      (else-exp-type (type-of-exp else-exp tenv)))
                  (match-types test-exp-type boolean-type)
                  (match-types then-exp-type else-exp-type)
                  then-exp-type))
              (app (rator rands)
                (type-of-app
                  (type-of-exp rator tenv)
                  (types-of-rands rands tenv)))
              (let (decls body)
                (type-of-exp body
                  (extend-tenv
                    (map decl->var decls)
                    (types-of-let-rands decls tenv)
                    tenv)))
              (letrec (decls body)
                (for-each (compose check-letrec-decl-exp decl->exp) 
                  decls)
                (type-of-exp body (letrec-tenv decls tenv)))
              (assert (type exp) (type-of-assert type exp tenv))
              (proc (formals body) (type-of-proc formals body tenv))
              (else (error "Invalid abstract syntax:" exp)))))
      (trace-exit answer)
      answer)))

(define types-of-rands
  (lambda (rands tenv)
    (map (lambda (rand) (type-of-exp rand tenv)) 
      rands)))

(define trace-depth-counter 0)

(define trace-type-of-exp #t)

(define trace-entry
  (lambda (exp)
    (if trace-type-of-exp
      (begin
        (set! trace-depth-counter (+ trace-depth-counter 1))
        (displayln trace-depth-counter " Entering with "
          (unparse exp))))))

(define trace-exit
  (lambda (type)
    (if trace-type-of-exp
      (begin
        (displayln trace-depth-counter " Leaving with "
          (unparse-type type))
        (set! trace-depth-counter (- trace-depth-counter 1))))))

(define type-of-app
  (lambda (rator-type rand-types)
    (if (proc-type? rator-type)
      (match-types-pairwise (domains rator-type) rand-types)
      (type-error "Not a procedure type:" rator-type))
    (range rator-type)))

(define types-of-let-rands
  (lambda (decls tenv) (types-of-rands (map decl->exp decls) tenv)))

(define check-letrec-decl-exp
  (lambda (exp)
    (if (not (and (assert? exp) (proc? (assert->exp exp))))
      (error "Invalid declaration expression:" exp))))

(define letrec-tenv
  (lambda (decls tenv)
    (let ((vars (map decl->var decls))
          (assert-exps (map decl->exp decls)))
      (let ((var-types (map assert->type assert-exps)))
        (let ((new-tenv (extend-tenv vars var-types tenv)))
          (for-each
            (lambda (assert-exp) (type-of-exp assert-exp new-tenv))
            assert-exps)
          new-tenv)))))

(define type-of-assert
  (lambda (assert-type exp tenv)
    (variant-case exp
      (proc (formals body)
        (if (proc-type? assert-type)
          (if (= (length formals) (length (domains assert-type)))
            (match-types (range assert-type)
              (type-of-exp body (extend-tenv formals (domains assert-type) tenv)))
            (error "Domain does not match formals" formals assert-type))
          (type-error "Assert type is not a procedure type:" assert-type)))
      (else (match-types (type-of-exp exp tenv) assert-type)))
    assert-type))

(define type-of-proc
  (lambda (formals body tenv) (error "Procedure not inside an assert:" formals body)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The user interface to the type checker is type.
;; This block of code also has a couple needed helper procedures:

(define unparse-type
  (lambda (type)
    (variant-case type
      (tcons
       (name types)
       (case name
         ((int bool) name)
         ((->) (list name (map unparse-type (cdr types))
                     (unparse-type (car types))))
         (else (cons name (map unparse-type types)))))
      (namedtype (name) name)
      (else (error "unknown type in unparse-type" type)))))

(define type
  (lambda (s)
    (unparse-type (type-of-exp (character-string-parser s) init-tenv))))

(define displayln
  (lambda args
    (for-each display args)
    (newline)))

(define unparse
  (lambda (x)
    x))