<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
;;; type inference for Scheme programs
;;; AUTHOR: Gary T. Leavens, using code originally by Mary Feeley

;------------------------------------------------------------------------------
;
; Error handling.

(define fail ; TYPE: datum -> poof
  (lambda msg
    ; EFFECT: print the error message
    (error "error:" msg)))

;-----------------------------------------------------------------------------
;
; The unifier.

(define *failure* 'unification-failure)

(load-quietly-from-lib "unify.ss")

;------------------------------------------------------------------------------
;
; An environment is an object that associates variables to values.
; They are represented by association lists.

(define env-empty ; TYPE: -> env
  (lambda ()
    ; ENSURES: result is an empty environment
    '()))

(define env-update ; TYPE: variable, datum, env -> env
  (lambda (var val env)
    ; ENSURES: result is a copy of env but with var associated to val
    (cons (cons var val) env)))

(define env-join  ; TYPE: env, env -> env
  (lambda (env1 env2)
    ; ENSURES: result is a new environment containing the bindings
    ; in env1 and env2 (env1 has precedence)
    (append env1 env2)))

(define env-bound? ; TYPE: variable, env -> boolean
  (lambda (var env)
    ; ENSURES: result is true iff the variable is bound in env
    (assq var env)))

(define env-value  ; TYPE: variable, env -> datum
  (lambda (var env)
    ; REQUIRES: var has an association in env
    ; ENSURES: result is the value associated to var in env
    (cdr (assq var env))))

;------------------------------------------------------------------------------
;
; Variables are represented by symbols starting with a "?" (e.g. ?a)

(define variable? ; TYPE: datum -> boolean
  (lambda (x)
    (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #\?))))

(define new-variable ; TYPE: -> variable
  (let ((variable-count 0))
    (lambda ()
      (set! variable-count (+ variable-count 1))
      (string->symbol (string-append "?" (number->string variable-count))))))

;------------------------------------------------------------------------------

(define instance  ; TYPE: type expr, generic variable list -> type expr
  (lambda (x prefix)
    ; ENSURES: result is an instance of x with new variables
    ; in place of the generic variables in prefix
    (letrec ((new ; TYPE: type expr, env, (type expr, env -> type expr)
	          ;                  -> type expr
	       (lambda (x env success)
		 (cond ((and (variable? x) (generic? x prefix))
			(if (env-bound? x env)
			    (success (env-value x env) env)
			    (let ((var (new-variable)))
			      (success var (env-update x var env)))))
		       ((pair? x)
			(new (car x) env
			  (lambda (a env)
			    (new (cdr x) env
			      (lambda (b env)
				(success (cons a b) env))))))
		       (else
			 (success x env))))))
      (new x (env-empty) (lambda (a env) a)))))

(define generic?  ; TYPE: variable, generic variables list -> boolean
  (lambda (var prefix)
    ; ENSURES: result is true iff the variable var is generic in prefix
    (cond ((null? prefix)
	   #t)
	  ((and (eq? (cadar prefix) var) (not (eq? (caar prefix) 'let)))
	   #f)
	  (else
	    (generic? var (cdr prefix))))))

;------------------------------------------------------------------------------

(define global-var-types
  '(
     (+        . (-> number number number))
     (-        . (-> number number number))
     (*        . (-> number number number))
     (/        . (-> number number number))
     (<        . (-> number number boolean))
     (>        . (-> number number boolean))     
     (<=       . (-> number number boolean))
     (=        . (-> number number boolean))
     (>=       . (-> number number boolean))
     (add1     . (-> number number))
     (sub1     . (-> number number))      
     (zero?    . (-> number boolean))

     (eq?      . (-> symbol symbol boolean))
     (eqv?     . (-> boolean boolean boolean))     ; too conservative...
     (equal?   . (-> ?a ?b boolean))        ; not quite right...

     (cons     . (-> ?a (list ?a) (list ?a)))
     (car      . (-> (list ?a) ?a))
     (cdr      . (-> (list ?a) (list ?a)))
     (caar     . (-> (list (list ?a)) ?a))    
     (cadr     . (-> (list ?a) ?a))
     (cdar     . (-> (list (list ?a)) (list ?a)))
     (cddr     . (-> (list ?a) (list ?a)))
     (set-car! . (-> (list ?a) ?a void))
     (set-cdr! . (-> (list ?a) (list ?a) void))
     (length   . (-> (list ?a) number))
     (list-ref . (-> (list ?a) number ?a))
     (append   . (-> (list ?a) (list ?a) (list ?a)))
     (reverse  . (-> (list ?a) (list ?a)))
     (map      . (-> (-> ?a ?b) (list ?a) (list ?b)))
     (for-each . (-> (-> ?a void) (list ?a) void))     

     (null?    . (-> ?a boolean))
     (pair?    . (-> ?a boolean))
     (boolean? . (-> ?a boolean))
     (symbol?  . (-> ?a boolean))     
     (procedure? . (-> ?a boolean))     
     (number?  . (-> ?a boolean))
     (integer? . (-> ?a boolean))      
     (real?    . (-> ?a boolean))      
     (string?    . (-> ?a boolean))
     (vector?    . (-> ?a boolean))
     
     (not      . (-> boolean boolean))
     (or       . (-> boolean boolean boolean))
     (and      . (-> boolean boolean boolean))
     (call/cc  . (-> (-> (-> ?a ?b) ?c) ?a))
     (apply    . (-> (-> ?a ?b) (list ?a) ?b)) ; works for monadic procs only
     (write    . (-> ?a void))
     (writeln  . (-> ?a void))     ; works for one argument only
     (display  . (-> ?a void))
     (newline  . (-> void))
     (read     . (-> ?a))

     (string-append . (-> string string string))
     (string=? . (-> string string boolean))
     (string-ci=? . (-> string string boolean))
     (string-length . (-> string string number))     
     (substring . (-> string number number))     
     (symbol->string . (-> symbol string))      

     (list->vector . (-> (list ?a) (vector ?a)))
     (make-vector . (-> number ?a (vector ?a)))
     (vector-generator . (-> (-> number ?a) (-> number (vector ?a))))
     (vector-length . (-> (vector ?a) number ?a))
     (vector-ref . (-> (vector ?a) number ?a))
     (vector-set! . (-> (vector ?a) number ?a void))


     (caaar    . (-> (list (list (list ?a))) ?a))
     (caadr    . (-> (list (list ?a)) ?a))
     (cadar    . (-> (list (list ?a)) ?a))     
     (caddr    . (-> (list ?a) ?a))
     (cdaar    . (-> (list (list (list ?a))) (list ?a)))     
     (cdadr    . (-> (list (list ?a)) (list ?a)))
     (cddar    . (-> (list (list ?a)) (list ?a)))
     (cdddr    . (-> (list ?a) (list ?a)))     

     (caaaar    . (-> (list (list (list (list ?a)))) ?a))
     (caaadr    . (-> (list (list (list ?a))) ?a))
     (caadar    . (-> (list (list (list ?a))) ?a))     
     (caaddr    . (-> (list (list ?a)) ?a))
     (cadaar    . (-> (list (list (list ?a))) ?a))
     (cadadr    . (-> (list (list ?a)) ?a))
     (caddar    . (-> (list (list ?a)) ?a))
     (cadddr    . (-> (list ?a) ?a))     
     (cdaaar    . (-> (list (list (list (list ?a)))) (list ?a)))
     (cdaadr    . (-> (list (list (list ?a))) (list ?a)))
     (cdadar    . (-> (list (list (list ?a))) (list ?a)))     
     (cdaddr    . (-> (list (list ?a)) (list ?a)))
     (cddaar    . (-> (list (list (list ?a))) (list ?a)))     
     (cddadr    . (-> (list (list ?a)) (list ?a)))
     (cdddar    . (-> (list (list ?a)) (list ?a)))
     (cddddr    . (-> (list ?a) (list ?a)))     

     (negative?  . (-> number boolean))
     (positive?  . (-> number boolean))
     (abs        . (-> number number))
     (ceiling    . (-> number number))
     (floor      . (-> number number))
     (truncate   . (-> number number))     
     (round      . (-> number number))     
     (expt       . (-> number number number))
     (sqrt       . (-> number number))
     (max        . (-> number number number))     
     (min        . (-> number number number))     
     (exp        . (-> number number))
     (log        . (-> number number))          
     (sin        . (-> number number))     
     (cos        . (-> number number))     
     (asin       . (-> number number))     
     (acos       . (-> number number))
     (tan        . (-> number number))     
     (atan       . (-> number number))     
     (quotient   . (-> number number number))     
     (remainder  . (-> number number number))     
     (modulo  . (-> number number number))     

     (char>?   . (-> char char boolean))
     (char<?   . (-> char char boolean))
     (char<=?  . (-> char char boolean))
     (char=?   . (-> char char boolean))
     (char>=?  . (-> char char boolean))
     (char>?   . (-> char char boolean))
   )
)

(define constant-type ; TYPE: datum -> type expr
  (lambda (x)
    ; ENSURES: result is the type of the Scheme constant x
    (cond ((number? x)                'number)
	  ((char? x)                  'char)
	  ((string? x)                'string)
	  ((boolean? x)               'boolean)
	  ((symbol? x)                'symbol)	
	  ((null? x)                  '(list ?a))
	  ((pair? x)
	   ; the following only deals properly with flat lists
	   (let ((element-type (constant-type (car x))))
	     (for-each (lambda (y)
			 (if (not (equal? (constant-type y) element-type))
			     (set! element-type 'datum)))
	       (cdr x))
	     (list 'list element-type)))
	  ((vector? x)
	   (if (= (vector-length x) 0)
	       '(vector ?a)
	       (let ((element-type (constant-type (vector-ref x 0))))
		 (vector-for-each
		   (lambda (y)
		     (if (not (equal? (constant-type y) element-type))
			 (set! element-type 'datum)))
		   x 1)
		 (list 'vector element-type))))
	  (else (fail "unknown constant type")))))

(define vector-for-each
  ; TYPE: all T . (T -> void), (vector of T), number -> void
  (lambda (f v start)
    ; EFFECT: apply f to each element of v, starting at index start
    ;         and going towards larger indexes
    (let ((size (vector-length v)))
      (letrec ((helper ; TYPE: integer -> void
		 (lambda (i)
		   (if (not (= i size))
		       (begin
			 (f (vector-ref v i))
			 (helper (+ 1 i)))))))
	(helper start)))))
  
(define quoted-constant-type ; TYPE: datum -> type expr
  (lambda (x)
    (if (eq? x '())
	'(list ?a) ; patch because #f = ()
	(constant-type x))))

(define type ; TYPE: s-expression -> type expr
  (lambda (f)
    ; ENSURES: result is the type of expression f
    (let ((e (env-empty)))
      (letrec
	((j ; TYPE: generic variables list, s-expression -> type expr
	   (lambda (p f)
	     ; ENSURES: result is the type of f, once variables in e
	     ;          are substituted for the variables in result
	     ; This is algorithm 'j' from Robin Milner's paper
	     (cond
	       ((symbol? f)
		(if (env-bound? f p)
		    (let ((x (env-value f p)))
		      (let ((kind (car x))
			    (type (cadr x)))
			(if (eq? kind 'let) (instance type p) type)))
		    (let ((glbl-binding (assq f global-var-types)))
		      (if (null? glbl-binding)
			  (fail (string-append
				  "unknown global name: "
				  (symbol->string f)))
			  (instance (cdr glbl-binding) (env-empty))))))
	       ((not (pair? f))
		(instance (constant-type f) (env-empty)))
	       ((eq? (car f) 'quote)
		(instance (quoted-constant-type (cadr f)) (env-empty)))
	       ((eq? (car f) 'if)
		(let ((pre (j p (cadr f)))
		      (con (j p (caddr f)))
		      (alt (j p (cadddr f))))
		  (set! e (unify con alt (unify pre 'boolean e)))
		  con))
	       ((eq? (car f) 'lambda)
		(let ((parms (map (lambda (x) (new-variable)) (cadr f))))
		  (let ((body (j (env-join
				   (map2 (lambda (x y) (list x 'lambda y))
					(cadr f)
					parms)
				   p)
				 (caddr f))))
		    (cons '-> (append parms (list body))))))
	       ((eq? (car f) 'let)
		(let ((p-let (env-join (map (lambda (x)
					      (list (car x)
						    'let
						    (j p (cadr x))))
					    (cadr f))
				       p)))
		  (j p-let (caddr f))))
	       ((eq? (car f) 'letrec)
		(let* ((p-rec (map (lambda (x)
					   (list (car x)
						 'lambda (new-variable)))
					 (cadr f)))
		       (p* (env-join p-rec p)))
		  (for-each
		    (lambda (x)
		      (let ((val (j p* (cadr x))))
			(set! e
			      (unify (cadr (env-value (car x) p*))
				     val
				     e))))
		    (cadr f))
		  (let ((p-rec2  ; env with letrec vars let-bound to types
			 (map
			  (lambda (x)
			    (list (car x)
				  'let
				  (env-value (caddr x) e)))
			  p-rec)))
		    (j (env-join p-rec2 p)
		       (caddr f)))))
	       ((and (pair? (car f)) (eq? (caar f) 'lambda))
		(j p (list 'let (map2 list (cadar f) (cdr f)) (caddar f))))
	       (else
		 (let ((result (new-variable))
		       (oper (j p (car f)))
		       (args (map (lambda (x) (j p x)) (cdr f))))
		   (set! e (unify oper
				  (cons '-> (append args (list result)))
				  e))
		   result))))))
	(let ((t (j (env-empty) f)))
	  (let ((expanded-type (subst-bindings e t)))
	    (if (eq? *failure* expanded-type)
		(fail "type error (or your expression is too hard)")
		expanded-type)))))))

(define map2 ; TYPE: (-> ((-> (S T) U) (list S) (list T)) (list U))
  (lambda (proc ls1 ls2)
    ; REQUIRES: ls1 and ls2 have same length.
    ; ENSURES: the result is a list, its items come from the result of
    ;          proc operating on corresponding items in ls1 and ls2.
    (if (null? ls1) '()
	(cons (proc (car ls1) (car ls2))
	      (map2 proc (cdr ls1) (cdr ls2))))))