;;; Polymorphic type checking for Scheme
;;;
;;; SYNOPSIS: the main useful routines are:
;;;           type-check-file, which reads expressions from a file,
;;;                            and checks them.
;;;           type-check-loop, which reads expressions or definitions and type
;;;                            checks them
;;;           type-check, which takes a single (quoted) expression
;;;                       and type checks it
;;;
;;; BUGS: The Scheme primitive load should be handled by type checking the
;;;       given file.
;;;       There is no checking for syntax errors.
;;;       Any error stops type checking in type-check-file and type-check-loop.
;;;       Procedures etc. must be defined before being used.
;;;       There begin special form is not handled, neither are implicit begins
;;;       There is no handling of procedures that can take a variable number
;;;       of arguments.
;;;       The types of the built-in primitives have not been carefully checked.

;;; AUTHOR: Gary T. Leavens



(load-quietly-from-lib "polytype.ss")
(load-quietly-from-lib "deep-recur-abs.ss")

(define type-check-file ; TYPE: (-> (string) void)
  (lambda (fname)
    (if (string? fname)
	(with-input-from-file
	  fname
	  (lambda () (type-check-loop-helper "")))
	(error "type-check-file expects a string argument"))))

(define type-check-loop ; TYPE: (-> () void)
  (lambda ()
    (type-check-loop-helper
      "enter expression (or done to exit): ")))

(define type-check-loop-helper ; TYPE: (-> (string) void)
  (lambda (prompt-str)
    ; EFFECT: prompt with prompt-str, read expressions and type check,
    ;         until done or EOF is entered
    (display prompt-str)
    (let ((expr (read)))
      (cond
	((or (eof-object? expr) (eq? expr 'done))
	 (display "Bye.")
	 (newline))
	(else (type-check expr)
	      (type-check-loop-helper prompt-str))))))


(define type-check  ; TYPE: (-> (expression) void)
  (lambda (expr)
    ; MODIFIES: global-var-types
    ; EFFECT: if expr has a type, print the type,
    ;          otherwise give an error.
    ;         for define expressions, installs the name and its type
    ;         in the global-var-types.
    (cond
      ((procedure? expr)
       (error "you have to quote your expression argument"))
      ((and (pair? expr) (eq? (car expr) 'define))
       (let ((name (cadr expr))
	     (its-type (type (desugar expr))))
	 (set! global-var-types (env-update name its-type global-var-types))
	 (display name)
	 (display " : ")
	 (type-write (type-translate its-type))))
      ((not (pair? expr)) (type-write (type-translate (type expr))))
      (else (type-write (type-translate (type (desugar expr))))))
    (newline)))

(define desugar ; TYPE: (-> (s-expression) s-expression)
  ; ENSURES: result is the same as the argument except that
  ;          define is replaced by letrec, and cond by nested ifs
  ; BUGS: this only handles top-level defines
  (deep-recur-abs
    '()
    (lambda (a d)
      (cond
	((eq? a 'define)
	 (list 'letrec (list (list (car d) (cadr d))) (car d)))
	((eq? a 'cond) (cond->if d))
	(else (cons a d))
	 ))
    cons
    (lambda (x) (not (or (pair? x) (null? x))))
    ))

(define cond->if ; TYPE: (-> (list cond-clause) if-expression)
  (lambda (clauses)
    ; REQUIRES: there are no syntax errors in the clauses
    ; ENSURES: result is an if expression equivalent to the cond
    (cond
      ((null? clauses) (write "undefined"))
      ((eq? (caar clauses) 'else) (cadar clauses))
      (else (list 'if (caar clauses)
		      (cadar clauses)
		      (cond->if (cdr clauses)))))))


;;; translation to a form with nested arguments, and better variable names
;;; for the types.   For example,
;;; (type-translate '(-> number ?3 ?2)) ==> (-> (number S) T)

(define type-translate   ; TYPE: (-> (unnested-type) nested-type)
  (lambda (typ)
    ; ENSURES: result is typ with argument types nested, and with
    ;          type variables translated into letters if possible.
    (cond
     ((pair? typ) (nest-args (better-variables typ (type-vars typ))))
     ((variable? typ) "T")
     (else typ))))

(define type-vars    ; TYPE: (-> ((tree symbol)) (list symbol))
  (lambda (typ)
    ; ENSURES: result is a list of all the type variables in typ,
    ;          and no element of result occurs twice in result
    ((deep-recur-abs
       '()
       (lambda (a d)
	 ; REQUIRES: a is a symbol
	 ; ENSURES: result only contains a if a is a variable not in d
	 (if (and (variable? a) (not (memq a d)))
	     (cons a d)
	     d))
       (letrec
	 ((union ; TYPE: (-> ((list symbol) (list symbol)) (list of symbol))
	    (lambda (s1 s2)
	      ; REQUIRES: s2 has no duplicates
	      ; ENSURES: result has the elements of s1 and s2,
	      ;          but no duplicates
	      (cond
		((null? s1) s2)
		((memq (car s1) s2) (union (cdr s1) s2))
		(else (cons (car s1) (union (cdr s1) s2)))))))
	 union)
       symbol?)
     typ)))

(define better-variables
  ; TYPE: (-> ((tree symbol) (list symbol)) (tree (or symbol string)))
  (lambda (typ vars)
    ; ENSURES: result is typ with some type variables in typ
    ;          replaced by better variable names
    (letrec
      ((helper
	 ; TYPE: (-> ((tree symbol) (list symbol) (list string))
	 ;           (tree (or symbol string)))
	 (lambda (typ vars better-names)
	   ; ENSURES: result is typ with each occurrence of vars replaced
	   ;          with a better-name, until the better names run out...
	   (cond
	    ((or (null? vars) (null? better-names))
	     typ)
	    (else
	     (helper (substq-all (car better-names) (car vars) typ)
		     (cdr vars)
		     (cdr better-names)))))))
      (helper typ
	      vars
	      (if (= 1 (length vars))
		  '("T")
		  '("S" "T" "U" "V" "W" "X" "Y" "Z"
			"A" "B" "C" "D" "E" "F" "G" "H" "I" "J" "K" "L"
			"M" "N" "O" "P" "Q" "R"))))))

(define substq-all
  ; TYPE: (-> (string symbol (tree (or symbol string))
  ;           (tree (or symbol string))))
  (lambda (new old tr)
    ; ENSURES: result is tr with all occurrences of old replaced by new
    ((deep-recur-abs
       '()
       (lambda (a d) (if (eq? a old) (cons new d) (cons a d)))
       cons
       (lambda (x) (or (symbol? x) (string? x))))
     tr)))

(define nest-args
  ; TYPE: (-> (tree (or string symbol)) (tree (or string symbol)))
  (deep-recur-abs
       '()
       (lambda (a d)
	 (if (eq? a '->)
	     (list '-> (rdc d) (last-item d))
	     (cons a d)))
       cons
       (lambda (x) (or (symbol? x) (string? x)))))
    
(define type-write ; TYPE: (-> (nested-type) void)
  display)

(define rdc ; TYPE: (-> ((list T)) (list T))
  (lambda (lst)
    ; REQUIRES: lst is not empty
    ; ENSURES: result is the same as lst, except without the last item
    (if (null? (cdr lst))
	'()
	(cons (car lst)
	      (rdc (cdr lst))))))

(define last-item ; TYPE: (-> ((list T)) T)
  (lambda (ls)
    ; REQUIRES: ls is not empty
    ; ENSURES: result is the last item of ls
    (cond
      ((null? (cdr ls)) (car ls))
      (else (last-item (cdr ls))))))