;;; $Id: tc-type-translate.scm,v 1.31 2006/02/14 02:27:28 leavens Exp $
;;; Copyright (C) 2006 Iowa State University
;;;
;;; This file is part of Typedscm.
;;;
;;; This library is free software; you can redistribute it and/or
;;; modify it under the terms of the GNU Lesser General Public License
;;; as published by the Free Software Foundation; either version 2.1,
;;; of the License, or (at your option) any later version.
;;;
;;; This library is distributed in the hope that it will be useful,
;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;;; Lesser General Public License for more details.
;;;
;;; You should have received a copy of the GNU Lesser General Public
;;; License along with Typedscm; see the file LesserGPL.txt.  If not,
;;; write to the Free Software Foundation, Inc., 51 Franklin St, Fifth
;;; Floor, Boston, MA 02110-1301 USA.

;;; Translation from the internal type format to the external format,
;;; with nested arguments, and better variable names for types.
;;; AUTHORS: Curtis Clifton and Gary T. Leavens
;;;          Adapted by Brian Dorn

(module tc-type-translate (lib "typedscm.ss" "typedscm")

(provide tc:type-unparse tc:type-parse
	 tc:input-type-parse)

(deftype tc:type-unparse (-> (tc:type-expr) tc:output-type-expr))
(deftype tc:type-parse (-> (tc:output-type-expr) tc:type-expr))
(deftype tc:input-type-parse (-> (tc:input-type-exp) tc:type-expr))

(require (lib "tc-types.scm" "typedscm")
	 (lib "tc-output-type-expr.scm" "typedscm")
	 (lib "tc-scheme-abstract-syntax.scm" "typedscm"))

(define tc:type-unparse
  (lambda (typ)
    ;; ENSURES: result is typ with argument types nested, and with
    ;;          type variables translated into letters if possible.
    (cond
     ((tc:variable-type-expr? typ)
      (tc:make-polymorphic-output-type-expr
       '(T)
       (tc:make-basic-output-type-expr 'T)))
     (else
      (let* ((vars (tc:type-vars typ))
	     (better-names (tc:better-variable-list-for vars)))
	(if (null? vars)
	    (tc:nest-args typ)
	    (tc:make-polymorphic-output-type-expr
	     better-names
	     (tc:better-variables (tc:nest-args typ) vars better-names))))))))

(deftype tc:union (-> ((list-of symbol) (list-of symbol)) (list-of symbol)))
(define tc:union
  (lambda (s1 s2)
    ;;   REQUIRES: s1 and s2 have no duplicates
    ;;   ENSURES: result has the elements of s1 and s2,
    ;;   	 but no duplicates
    ;; ALSO:
    ;;   REQUIRES: s1 has duplicates or s2 has duplicates 
    ;;   ENSURES: result has the elements of s1 and s2
    (cond
     ((null? s1) s2)
     ((memq (car s1) s2) (tc:union (cdr s1) s2))
     (else (cons (car s1) (tc:union (cdr s1) s2))))))

(deftype tc:unionAll (-> ((list-of (list-of symbol))) (list-of symbol)))
(define tc:unionAll
  (lambda (ss)
    ;; REQUIRES: each element of ss has no duplicates
    ;; ENSURES: result has the elements of the elements of ss,
    ;;         but no duplicates
    (if (null? ss)
	'()
	(tc:union (car ss) (tc:unionAll (cdr ss))))))

(deftype tc:type-vars (-> (tc:type-expr) (list-of symbol)))
(define tc:type-vars
  (lambda (typ)
    ;; ENSURES: result is a list symbols corresponding to the
    ;;          type variables in typ,
    ;;          and no element of result occurs twice in result
    (cond
     ((tc:variable-type-expr? typ)
      (list (tc:uniq-sym->symbol (tc:variable-type-expr->uniq-sym typ))))
     ((tc:non-variable-basic-type-expr? typ) '())
     ((tc:function-type-expr? typ)
      (tc:union
       (tc:unionAll (map tc:type-vars
			 (tc:function-type-expr->arg-types typ)))
       (tc:type-vars
	(tc:function-type-expr->result-type typ))))
     ((tc:intersection-type-expr? typ)
      (tc:unionAll (map tc:type-vars
			(tc:intersection-type-expr->conjoined-types typ))))
     ((tc:type-predicate-for-type-expr? typ)
      (tc:type-vars (tc:type-predicate-for-type-expr->type typ)))

     ((tc:variant-record-type-expr? typ)
      (tc:unionAll (map tc:type-vars
			(tc:variant-record-type-expr->variants typ))))
     
     ((tc:variant-type-expr? typ)
      (tc:unionAll (map tc:type-vars
			(tc:variant-type-expr->fields typ))))
     
     ((tc:field-type-binding-type-expr? typ)
      (tc:type-vars (tc:field-type-binding-type-expr->type typ)))
     
     ((tc:applied-type-expr? typ)
      (tc:union (tc:type-vars (tc:applied-type-expr->operator-type typ))
		(tc:unionAll
		 (map tc:type-vars
		      (tc:applied-type-expr->operand-types typ)))))
     ((tc:error-type-expr? typ) '())
     ((tc:declaration-type-expr? typ)
      '()
      ;; modules are not first-class
      ;; (tc:unionAll (map (lambda (binding)
      ;;                     (tc:type-vars (tc:binding->type-expr binding)))
      ;;                   (tc:env-vals (tc:declaration-type-expr->env typ))))
      )
     (else
      (error
       "tc:type-vars called with unknown type expression:"
       typ)))))

(deftype tc:better-variable-list-for
  (-> ((list-of symbol)) (list-of symbol)))
(define tc:better-variable-list-for
  (let* ((reversed-preferred-order
	 (reverse
	  '(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)))
	 (num-of-preferred (length reversed-preferred-order)))
  (lambda (vars)
    ;; ENSURES: result is a list of the same length as vars
    ;;          with better variable names.
    (let ((len (length vars)))
      (cond
       ((= 1 len) '(T))
       ((<= len num-of-preferred)
	(reverse (list-tail reversed-preferred-order
			    (- num-of-preferred len))))
       (else 
        (append (reverse reversed-preferred-order)
		(list-tail vars (- len num-of-preferred)))))))))
    
(deftype tc:better-variables
  (-> (tc:output-type-expr (list-of symbol) (list-of symbol))
      tc:output-type-expr))
(define tc:better-variables
  (lambda (typ vars better-names)
    ;; REQUIRES (length vars) = (length better-names)
    ;; ENSURES: result is typ with each occurrence of vars replaced
    ;;          with a better-name, until the better names run out...
    (if (null? vars)
	typ
	(tc:better-variables (tc:substq-all-output (car better-names)
						   (car vars)
						   typ)
			     (cdr vars)
			     (cdr better-names)))))

(deftype tc:nest-args (-> (tc:type-expr) tc:output-type-expr))
(define tc:nest-args
  (lambda (typ)
    ;; ENSURES: result is an tc:output-type-expr equivalent to typ,
    ;;          except that it will look monomorphic.
    (cond
     ((tc:variable-type-expr? typ)
      (tc:make-basic-output-type-expr
       (tc:uniq-sym->symbol (tc:variable-type-expr->uniq-sym typ))))
     ((tc:non-variable-basic-type-expr? typ)
      (tc:make-basic-output-type-expr (tc:basic-type-expr->symbol typ)))
     ((tc:function-type-expr? typ)
      (tc:make-function-output-type-expr
       (map tc:nest-args (tc:function-type-expr->arg-types typ))
       (tc:nest-args (tc:function-type-expr->result-type typ))))
     ((tc:intersection-type-expr? typ)
      (tc:make-intersection-output-type-expr
       (map tc:nest-args (tc:intersection-type-expr->conjoined-types typ))))
     ((tc:type-predicate-for-type-expr? typ)
      (tc:make-type-predicate-for-output-type-expr
       (tc:nest-args (tc:type-predicate-for-type-expr->type typ))))
     ((tc:variant-record-type-expr? typ)          
      (tc:make-variant-record-output-type-expr
       (map tc:nest-variant-type-args
	    (tc:variant-record-type-expr->variants typ))))
     ((tc:applied-type-expr? typ)
      (tc:make-applied-output-type-expr
       (tc:output-type-expr->basic-type
	(tc:nest-args (tc:applied-type-expr->operator-type typ)))
       (map tc:nest-args (tc:applied-type-expr->operand-types typ))))
     ((tc:declaration-type-expr? typ)
      (tc:make-basic-output-type-expr 'module))
     ((tc:error-type-expr? typ)
       (tc:make-basic-output-type-expr 'error))
     ((tc:variant-type-expr? typ)
      (error "tc:nest-args called with bare variant-type-expr:" typ))
     ((tc:field-type-binding-type-expr? typ)
      (error "tc:nest-args called with bare field-type-binding-type-expr:"
	     typ))
     (else
      (error "tc:nest-args called with unknown type expression:" typ))
     )))

(deftype tc:nest-variant-type-args
  (-> (tc:type-expr) tc:output-variant-type-decl))
(define tc:nest-variant-type-args
  (lambda (typ)
    (cond
     ((tc:variant-type-expr? typ)
      (tc:make-output-variant-type-decl
       (tc:variant-type-expr->variant-name typ)
       (map tc:nest-field-type-binding-args
	    (tc:variant-type-expr->fields typ))))
     (else
      (error
       "tc:nest-variant-type-args called with non-variant type expression:"
       typ)))))

(deftype tc:nest-field-type-binding-args
  (-> (tc:type-expr) tc:output-field-type-binding))
(define tc:nest-field-type-binding-args
  (lambda (typ)
    (cond
     ((tc:field-type-binding-type-expr? typ)
      (tc:make-output-field-type-binding
       (tc:field-type-binding-type-expr->field-name typ)
       (tc:nest-args
	(tc:field-type-binding-type-expr->type typ))))
     (else
      (error
       "tc:nest-field-type-binding-args called with non-variant type expression:"
       typ)))))

(define tc:type-parse
  (lambda (typ)
    ;; ENSURES: result is typ with argument types unnested, and with
    ;;          type formals translated into type variables.
    (if (not (tc:output-type-expr-polymorphic-type? typ))
	(tc:unnest-args typ)
	(let ((type-formals (tc:output-type-expr->type-formals typ)))
	  (tc:unnest-args
	   (tc:worse-variables
	    (tc:output-type-expr->monomorphic-type typ)
	    type-formals
	    (tc:worse-variable-list-for type-formals)))))))

(deftype tc:worse-variable-list-for
  (-> ((list-of symbol)) (list-of symbol)))
(define tc:worse-variable-list-for
    (lambda (vars)
    ;; ENSURES: result is a list of the same length as vars
    ;;          with internal variable names.
    (let ((len (length vars)))
      ;; Ingore preferred names for now....
      (map tc:logicalvar->name (tc:new-lv-list len)))))

(deftype tc:worse-variables 
  (-> (tc:output-type-expr (list-of symbol) (list-of symbol))
      tc:output-type-expr))
(define tc:worse-variables
  (lambda (typ vars worse-names)
    ;; REQUIRES: (length vars) = (length worse-names)
    ;; ENSURES: result is typ with each occurrence of a symbol in vars
    ;;          that is not a tc:variable? replaced with a worse-name
    (cond
     ((null? vars) typ)
     ((tc:variable? (car vars))
      ;; don't need to do anything, it's already a variable
      (tc:worse-variables typ (cdr vars) (cdr worse-names)))
     (else
      (tc:worse-variables
       (tc:substq-all-output (car worse-names) (car vars) typ)
       (cdr vars)
       (cdr worse-names))))))

(deftype tc:substq-all-output 
  (-> (symbol symbol tc:output-type-expr) tc:output-type-expr))
(define tc:substq-all-output
  (lambda (new old typ)
    (letrec
	((substq
	  (lambda (typ)
	    ;; ENSURES: result is typ with all occurrences
	    ;;          of old replaced by new
	    (cond
	     ((tc:output-type-expr-basic-type? typ)
	      (if (eq? old (tc:output-type-expr->basic-type typ))
		  (tc:make-basic-output-type-expr new)
		  typ))
	     ((tc:output-type-expr-function-type? typ)
	      (tc:make-function-output-type-expr
	       (map substq (tc:output-type-expr->function-arg-types typ))
	       (substq (tc:output-type-expr->function-result-type typ))))
	     ((tc:output-type-expr-intersection-type? typ)
	      (tc:make-intersection-output-type-expr
	       (map substq (tc:output-type-expr->conjoined-types typ))))
	     ((tc:output-type-expr-type-predicate-for-type? typ)
	      (tc:make-type-predicate-for-output-type-expr
	       (substq (tc:output-type-expr->for-type typ))))
	     ((tc:output-type-expr-variant-record-type? typ)
 	      (tc:make-variant-record-output-type-expr
	       (map substq-variant (tc:output-type-expr->variants typ))))
	     ((tc:output-type-expr-applied-type? typ)
	      (tc:make-applied-output-type-expr
	       (tc:output-type-expr->basic-type
		(substq (tc:make-basic-output-type-expr
			 (tc:output-type-expr->operator typ))))
	       (map substq (tc:output-type-expr->operands typ))))
	     ((tc:output-type-expr-polymorphic-type? typ)
	      (let ((formals (tc:output-type-expr->type-formals typ)))
		(if (memq old (tc:output-type-expr->type-formals typ))
		    typ
		    (tc:make-polymorphic-output-type-expr
		     formals
		     (substq (tc:output-type-expr->monomorphic-type typ))))))
	     (else
	      (error
	       "tc:substq-all-output called with unknown type expression:"
	       typ)))))
	 (substq-variant
	  (lambda (vtd)
	    (tc:make-output-variant-type-decl
	     (tc:output-variant-type-decl->variant-name vtd)
	     (map substq-field-type-binding
		  (tc:output-variant-type-decl->field-type-bindings vtd)))))
	 (substq-field-type-binding
	  (lambda (ftb)
	    (tc:make-output-field-type-binding
	     (tc:output-field-type-binding->field-name ftb)
	     (substq (tc:output-field-type-binding->type ftb))))))
      (substq typ))))

(deftype tc:unnest-args (-> (tc:output-type-expr) tc:type-expr))
(define tc:unnest-args
  (letrec
      ((unnest-variant-type-decl
	(lambda (vtd)
	  (tc:make-variant-type-expr
	   (tc:output-variant-type-decl->variant-name vtd)
	   (map unnest-field-type-binding
		(tc:output-variant-type-decl->field-type-bindings vtd)))))
       (unnest-field-type-binding
	(lambda (ftb)
	  (tc:make-field-type-binding-type-expr
	   (tc:output-field-type-binding->field-name ftb)
	   (tc:unnest-args
	    (tc:output-field-type-binding->type ftb))))))
    (lambda (typ)
      ;; ENSURES: result is a tc:type-expr equivalent to typ
      (cond
       ((tc:output-type-expr-basic-type? typ)
	(let ((name (tc:output-type-expr->basic-type typ)))
	  (if (tc:variable? name)
	      (tc:make-variable-type-expr name)
	      (tc:make-basic-type-expr name))))
       ((tc:output-type-expr-function-type? typ)
	(tc:make-function-type-expr
	 (map tc:unnest-args (tc:output-type-expr->function-arg-types typ))
	 (tc:unnest-args (tc:output-type-expr->function-result-type typ))))
       ((tc:output-type-expr-intersection-type? typ)
	(tc:make-intersection-type-expr
	 (map tc:unnest-args (tc:output-type-expr->conjoined-types typ))))
       ((tc:output-type-expr-type-predicate-for-type? typ)
	(tc:make-type-predicate-for-type-expr
	 (tc:unnest-args (tc:output-type-expr->for-type typ))))
       ((tc:output-type-expr-variant-record-type? typ)
	(tc:make-variant-record-type-expr
	 (map unnest-variant-type-decl (tc:output-type-expr->variants typ))))
       ((tc:output-type-expr-applied-type? typ)
	(tc:make-applied-type-expr
	 (tc:unnest-args (tc:make-basic-output-type-expr
			  (tc:output-type-expr->operator typ)))
	 (map tc:unnest-args (tc:output-type-expr->operands typ))))
       ((tc:output-type-expr-polymorphic-type? typ)
	(tc:unnest-args (tc:output-type-expr->monomorphic-type typ)))
       (else (error "tc:unnest-args called with unknown type expression:" typ))
       ))))

(deftype tc:input-type-exp-poof? (-> (tc:input-type-exp) boolean))
(define tc:input-type-exp-poof?
  (lambda (ete)
    (cases tc:input-type-exp ete
      (tc:basic-input-type-exp (position identifier) (eq? identifier 'poof))
      (else (error "tc:input-type-exp-poof? bad record:" ete)))))

(deftype tc:input-type-exp-datum? (-> (tc:input-type-exp) boolean))
(define tc:input-type-exp-datum?
  (lambda (ete)
    (cases tc:input-type-exp ete
      (tc:basic-input-type-exp (position identifier) (eq? identifier 'datum))
      (else (error "tc:input-type-exp-datum? bad record:" ete)))))

(define tc:input-type-parse
  (lambda (typ)
    (cases tc:input-type-exp typ
      (tc:polymorphic-input-type-exp
       (position type-formals monomorphic-type)
       (tc:input-to-type-expr
	(tc:worse-input-variables monomorphic-type type-formals)))
      (else
       (tc:input-to-type-expr typ)))))

(deftype tc:input-to-type-expr
  (-> (tc:input-type-exp) tc:type-expr))
(define tc:input-to-type-expr
  (letrec
      ((tc:variant-type-decl-input-to-type-expr
	(has-type
	 (-> (tc:variant-type-decl-record)
	     tc:type-expr)
	 (lambda (vtd)
	   (cases tc:variant-type-decl-record vtd
	     (tc:variant-type-decl (position variant-name fields)
	       (tc:make-variant-type-decl-type-expr
		variant-name
		(map tc:field-type-binding-input-to-type-expr fields)))
	     (else
	      (error
	       "tc:variant-type-decl-input-to-type-expr called with non-tc:variant-type-decl-record:"
	       vtd))))))
       (tc:field-type-binding-input-to-type-expr
	(has-type
	 (-> (tc:field-type-binding-record)
	     tc:type-expr)
	 (lambda (ftb)
	   (cases tc:field-type-binding-record ftb
	     (tc:field-type-binding (position field-name type)
	       (tc:make-field-type-binding-type-expr
		field-name
		(tc:input-to-type-expr type)))
	     (else
	      (error
	       "tc:field-type-binding-input-to-type-expr called with non-tc:field-type-binding-record:"
	       ftb)))))))
    (lambda (typ)
      ;; ENSURES: result is a tc:type-expr equivalent to typ
      ;;          but without a position
      (cases tc:input-type-exp typ
        (tc:basic-input-type-exp (position identifier)
	  (if (tc:variable? identifier)
	      (tc:make-variable-type-expr identifier)
	      (tc:make-basic-type-expr identifier)))
	(tc:function-input-type-exp (position arg-types result-type)
          (tc:make-function-type-expr
	   (map tc:input-to-type-expr arg-types)
	   (tc:input-to-type-expr result-type)))
	(tc:varargs-function-input-type-exp
	 (position arg-types repeated-type result-type)
	 (tc:make-function-type-expr
	  (append (map tc:input-to-type-expr arg-types)
		  (list (tc:input-to-type-expr repeated-type)
			(tc:make-basic-type-expr '...)))
	  (tc:input-to-type-expr result-type)))
	(tc:intersection-input-type-exp (position conjoined-types)
         (tc:make-intersection-type-expr
	  (map tc:input-to-type-expr conjoined-types)))
	(tc:type-predicate-for-input-type-exp (position type)
         (tc:make-type-predicate-for-type-expr
	  (tc:input-to-type-expr type)))
	(tc:variant-record-input-type-exp (position variants)
         (tc:make-variant-record-type-expr
	  (map tc:variant-type-decl-input-to-type-expr variants)))
	(tc:applied-input-type-exp (position operator operand-types)
	 (tc:make-applied-type-expr
	  (tc:make-basic-type-expr operator)
	  (map tc:input-to-type-expr operand-types)))
	(tc:polymorphic-input-type-exp (position type-formals monomorphic-type)
	 (error "tc:input-to-type-expr called with a polymorphic type"))
	(tc:translated-input-type-exp (position type-expr)
				      (test-type tc:type-expr? type-expr))
	(else
	 (error "tc:input-to-type-expr has missing case for:" typ))
	))))

(deftype tc:worse-input-variables 
  (-> (tc:input-type-exp (list-of symbol)) tc:input-type-exp))
(define tc:worse-input-variables
  (lambda (typ vars)
    ;; ENSURES: result is typ with all occurrences of vars typ
    ;;          replaced by "worse" variable names
    (letrec
	((helper
	  (has-type
	   (-> (tc:input-type-exp (list-of symbol) (list-of symbol))
	       tc:input-type-exp)
	   (lambda (typ vars worse-names)
	     ;; REQUIRES: (length vars) = (length worse-names)
	     ;; ENSURES: result is typ with each occurrence of a symbol in vars
	     ;;          replaced with a worse-name
	     (cond
	      ((null? vars) typ)
	      (else
	       (helper (tc:substq-all-input (car worse-names) (car vars) typ)
		       (cdr vars)
		       (cdr worse-names))))))))
      (helper typ vars (tc:worse-variable-list-for vars)))))

(deftype tc:substq-all-input 
  (-> (symbol symbol tc:input-type-exp) tc:input-type-exp))
(define tc:substq-all-input
  (lambda (new old typ)
    (letrec
	((substq
	  (has-type
	     (-> (tc:input-type-exp) tc:input-type-exp)
	     (lambda (typ)
	       ;; ENSURES: result is typ
	       ;; with all free occurrences of old replaced by new
	       (cases tc:input-type-exp typ
		 (tc:basic-input-type-exp (position identifier)
	           (if (eq? old identifier)
		       (tc:basic-input-type-exp position new)
		       typ))
		 (tc:function-input-type-exp (position arg-types result-type)
	           (tc:function-input-type-exp
		    position
		    (map substq arg-types)
		    (substq result-type)))
		 (tc:varargs-function-input-type-exp
		  (position arg-types repeated-type result-type)
		  (tc:varargs-function-input-type-exp
		   position
		   (map substq arg-types)
		   (substq repeated-type)
		   (substq result-type)))
		 (tc:intersection-input-type-exp (position conjoined-types)
                  (tc:intersection-input-type-exp
		   position
		   (map substq conjoined-types)))
		 (tc:type-predicate-for-input-type-exp (position type)
                  (tc:type-predicate-for-input-type-exp
		   position
		   (substq type)))
		 (tc:variant-record-input-type-exp (position variants)
                  (tc:variant-record-input-type-exp
		   position
		   (map variant-substq variants)))
		 (tc:applied-input-type-exp (position operator operand-types)
                  (tc:applied-input-type-exp
		   position
		   operator
		   (map substq operand-types)))
		 (tc:polymorphic-input-type-exp
		  (position type-formals monomorphic-type)
		  (if (memq old type-formals)
		      typ
		      (tc:polymorphic-input-type-exp
		       position type-formals
		       (substq monomorphic-type))))
		 (tc:translated-input-type-exp (position type-expr)
	           (tc:translated-input-type-exp
		    position
		    (substq-type-expr (test-type tc:type-expr? type-expr))))
		 (else
		  (error "substq in tc:substq-all-input has missing case for:"
			 typ))
		 ))))
	 (variant-substq
	  (lambda (vtd)
	    (cases tc:variant-type-decl-record vtd
	      (tc:variant-type-decl (position variant-name fields)
		(tc:variant-type-decl
		 position
		 variant-name
		 (map field-type-binding-substq fields)))
	      (else
	       (error "variant-substq in tc:substq-all-input called with non-tc:variant-type-decl-record:"
		      vtd)))))
	 (field-type-binding-substq
	  (lambda (ftb)
	    (cases tc:field-type-binding-record ftb
	      (tc:field-type-binding (position field-name type)
		(tc:field-type-binding
		 position
		 field-name
		 (substq type)))
	      (else
	       (error "field-type-binding-substq in tc:substq-all-input called with non-tc:field-type-binding-record:"
		      ftb)))))
         (substq-type-expr
          (lambda (te)
            (cases tc:type-expr te
              (tc:function-type-expr (arg-types result-type)
                 (tc:function-type-expr
                    (map substq-type-expr arg-types)
                    (substq-type-expr result-type)))
	     (tc:intersection-type-expr (conjoined-types)
                 (tc:intersection-type-expr
                  (map substq-type-expr conjoined-types)))
	     (tc:type-predicate-for-type-expr (type)
		(tc:type-predicate-for-type-expr (substq-type-expr type)))
	     (tc:variant-record-type-expr (variants)
		(tc:variant-record-type-expr
                 (map substq-type-expr variants)))
	     (tc:applied-type-expr (operator-type operand-types)
	        (tc:applied-type-expr
                 (substq-type-expr operator-type)
                 (map substq-type-expr operand-types)))
	     (tc:variable-type-expr (lvar)
	        (if (eq? old (tc:logicalvar->name lvar))
		       (tc:variable-type-expr (tc:symbol->logicalvar new))
		       te))
	     (tc:declaration-type-expr (pi)
		(tc:declaration-type-expr
                 (tc:env-map
                  (lambda (key binding)
                    (tc:bind-type-expr
                     (tc:binding->binder binding)
                     (substq-type-expr (tc:binding->type-expr binding))))     
                  pi)))
	     (tc:variant-type-expr (variant-name fields)
		(tc:variant-type-expr
                 variant-name
                 (map substq-type-expr fields)))
	     (tc:field-type-binding-type-expr (field-name type)
		(tc:field-type-binding-type-expr
                 field-name
                 (substq-type-expr type)))
	     (else te))))
         )
      (substq typ))))

) ;; end module