;;; $Id: tc-output-type-expr.scm,v 1.4 2005/03/28 22:03:06 leavens Exp $
;;;
;;; Output type expressions, as reported to the user in messages:
;;;
;;;   <type-expr> ::= <monomorphic-type>
;;;            | <polymorphic-type>
;;;   <monomorphic-type> ::= <basic-type>
;;;            | <function-type>
;;;            | <intersection-type>
;;;            | <applied>
;;;            | <variant-record-type>
;;;            | <polymorphic-type>
;;;   <basic-type> ::= an <identifier>
;;;   <function-type> ::= ( -> ( {<type>}* ) <type> )    ;; parens around args
;;;                     | ( -> ( {<type>}* <type> ... ) <type> )
;;;   <intersection-type> ::= ( all-of {<type>}+ )
;;;   <applied> ::= ( <identifier> {<type>}+ )
;;;   <type-predicate-for-type> ::= ( type-predicate-for <type-expr> )
;;;   <variant-record-type> ::= ( variant-record {<variant-type-decl>}+ )
;;;   <polymorphic-type> ( forall ( <type-formals> ) <monomorphic-type> )
;;;   <type-formals> ::= ( {<identifier>}* )
;;;                    | ( {<identifier>}* . <identifier> )
;;;
;;;   <variant-type-decl>  ::= ( <identifier> {<field-type-binding>}* )
;;;   <field-type-binding> ::= ( <identifier> <type> )

(module tc-output-type-expr (lib "typedscm.ss" "lib342")

(provide tc:output-type-expr-basic-type? tc:output-type-expr-poof?
	 tc:output-type-expr-datum? tc:output-type-expr-dots?
	 tc:output-type-expr-function-type?
	 tc:output-type-expr-varargs-function-type?
	 tc:output-type-expr-intersection-type?
	 tc:output-type-expr-type-predicate-for-type?
	 tc:output-type-expr-variant-record-type?
	 tc:output-type-expr-polymorphic-type?
	 tc:output-type-expr-applied-type?
	 tc:make-basic-output-type-expr tc:make-function-output-type-expr
	 tc:make-intersection-output-type-expr
	 tc:make-type-predicate-for-output-type-expr
	 tc:make-variant-record-output-type-expr
	 tc:make-applied-output-type-expr tc:make-polymorphic-output-type-expr
	 tc:output-type-expr->basic-type
	 tc:output-type-expr->function-arg-types
	 tc:output-type-expr->function-result-type
	 tc:output-type-expr->conjoined-types
	 tc:output-type-expr->operator tc:output-type-expr->operands
	 tc:output-type-expr->type-formals tc:output-type-expr->for-type
	 tc:output-type-expr->variants tc:output-type-expr->monomorphic-type
	 tc:occurs-in-output-type-expr?

	 tc:output-variant-type-decl? tc:make-output-variant-type-decl
	 tc:output-variant-type-decl->variant-name
	 tc:output-variant-type-decl->field-type-bindings

	 tc:output-field-type-binding? tc:make-output-field-type-binding
	 tc:output-field-type-binding->field-name
	 tc:output-field-type-binding->type
	 )

(deftype tc:output-type-expr-basic-type? (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-poof? (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-datum? (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-dots? (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-function-type?
  (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-varargs-function-type?
  (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-intersection-type?
  (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-type-predicate-for-type?
  (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-variant-record-type?
  (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-polymorphic-type?
  (-> (tc:output-type-expr) boolean))
(deftype tc:output-type-expr-applied-type? (-> (tc:output-type-expr) boolean))
(deftype tc:make-basic-output-type-expr (-> (symbol) tc:output-type-expr))
(deftype tc:make-function-output-type-expr
  (-> ((list-of tc:output-type-expr) tc:output-type-expr) tc:output-type-expr))
(deftype tc:make-intersection-output-type-expr
  (-> ((list-of tc:output-type-expr)) tc:output-type-expr))
(deftype tc:make-type-predicate-for-output-type-expr
  (-> (tc:output-type-expr) tc:output-type-expr))
(deftype tc:make-variant-record-output-type-expr
  (-> ((list-of tc:output-variant-type-decl)) tc:output-type-expr))
(deftype tc:make-applied-output-type-expr
  (-> (symbol (list-of tc:output-type-expr)) tc:output-type-expr))
(deftype tc:make-polymorphic-output-type-expr
  (-> ((list-of symbol) (list-of tc:output-type-expr)) tc:output-type-expr))
(deftype tc:output-type-expr->basic-type
  (-> (tc:output-type-expr) symbol))
(deftype tc:output-type-expr->function-arg-types
  (-> (tc:output-type-expr) (list-of tc:output-type-expr)))
(deftype tc:output-type-expr->function-result-type
  (-> (tc:output-type-expr) tc:output-type-expr))
(deftype tc:output-type-expr->conjoined-types
  (-> (tc:output-type-expr) (list-of tc:output-type-expr)))
(deftype tc:output-type-expr->operator
  (-> (tc:output-type-expr) symbol))
(deftype tc:output-type-expr->operands
  (-> (tc:output-type-expr) (list-of tc:output-type-expr)))
(deftype tc:output-type-expr->type-formals
  (-> (tc:output-type-expr) (list-of symbol)))
(deftype tc:output-type-expr->for-type
  (-> (tc:output-type-expr) tc:output-type-expr))
(deftype tc:output-type-expr->variants
  (-> (tc:output-type-expr) (list-of tc:output-variant-type-decl)))
(deftype tc:output-type-expr->monomorphic-type
  (-> (tc:output-type-expr) tc:output-type-expr))
(deftype tc:occurs-in-output-type-expr?
  (-> (symbol tc:output-type-expr) boolean))

(deftype tc:output-variant-type-decl?
  (type-predicate-for tc:output-variant-type-decl))
(deftype tc:make-output-variant-type-decl
  (-> (symbol (list-of tc:output-field-type-binding))
      tc:output-variant-type-decl))
(deftype tc:output-variant-type-decl->variant-name
  (-> (tc:output-variant-type-decl) symbol))
(deftype tc:output-variant-type-decl->field-type-bindings
  (-> (tc:output-variant-type-decl) (list-of tc:output-field-type-binding)))

(deftype tc:output-field-type-binding?
  (type-predicate-for tc:output-field-type-binding))
(deftype tc:make-output-field-type-binding
  (-> (symbol tc:output-type-expr) tc:output-field-type-binding))
(deftype tc:output-field-type-binding->field-name
  (-> (tc:output-field-type-binding) symbol))
(deftype tc:output-field-type-binding->type
  (-> (tc:output-field-type-binding) tc:output-type-expr))

(require (lib "tc-util.scm" "lib342"))

(defrep (tc:output-type-expr datum)
        (tc:output-variant-type-decl datum)
        (tc:output-field-type-binding datum))

(define tc:output-type-expr-basic-type?
  (lambda (d)
    (symbol? d)))

(define tc:output-type-expr-poof?
  (lambda (d)
    (eq? d 'poof)))

(define tc:output-type-expr-datum?
  (lambda (d)
    (eq? d 'datum)))

(define tc:output-type-expr-dots?
  (lambda (d)
    (eq? d '...)))

(define tc:output-type-expr-function-type?
  (lambda (d)
    (and (list? d)
	 (= (length d) 3)
	 (eq? (car d) '->)
	 (list? (cadr d)))))

(define tc:output-type-expr-varargs-function-type?
  (lambda (d)
    (and (tc:output-type-expr-function-type? d)
	 (member '... (cadr d)))))

(define tc:output-type-expr-intersection-type?
  (lambda (d)
    (and (list? d)
	 (>= (length d) 2)
	 (eq? (car d) 'all-of))))

(define tc:output-type-expr-type-predicate-for-type?
  (lambda (d)
    (and (list? d)
	 (= (length d) 2)
	 (eq? (car d) 'type-predicate-for))))

(define tc:output-type-expr-variant-record-type?
  (lambda (d)
    (and (list? d)
	 (>= (length d) 2)
	 (eq? (car d) 'variant-record))))

(define tc:output-type-expr-applied-type?
   (lambda (d)
     (and (list? d)
	  (>= (length d) 2)
	  (symbol? (car d))
	  (not (eq? (car d) '->))
	  (not (eq? (car d) 'and-of))
	  (not (eq? (car d) 'forall)))))

(define tc:output-type-expr-polymorphic-type?
  (lambda (d)
    (and (list? d)
	 (= (length d) 3)
	 (eq? (car d) 'forall))))

(define tc:make-basic-output-type-expr
  (lambda (s) s))

(define tc:make-function-output-type-expr
  (lambda (arg-types result-type)
    (list '-> arg-types result-type)))

(define tc:make-intersection-output-type-expr
  (lambda (arg-types)
    (cons 'all-of arg-types)))

(define tc:make-type-predicate-for-output-type-expr
  (lambda (type)
    (list 'type-predicate-for type)))

(define tc:make-variant-record-output-type-expr
  (lambda (variant-decls)
    (cons 'variant-record variant-decls)))

(define tc:make-applied-output-type-expr
  cons)

(define tc:make-polymorphic-output-type-expr
  (lambda (type-formals monomorphic-type)
    (list 'forall type-formals monomorphic-type)))

(define tc:output-type-expr->basic-type
  (lambda (t)
    (if (tc:output-type-expr-basic-type? t)
	t
	(error "tc:output-type-expr->basic-type called with non-basic-type argument"
	       t))))

(define tc:output-type-expr->function-arg-types
  (lambda (t)
    (if (tc:output-type-expr-function-type? t)
	(cadr t)
	(error
	 "tc:output-type-expr->function-arg-types called with non-function type argument"
	 t))))

(define tc:output-type-expr->function-result-type
  (lambda (t)
    (if (tc:output-type-expr-function-type? t)
	(caddr t)
	(error
	 "tc:output-type-expr->function-result-type called with non-function type argument "
	 t))))

(define tc:output-type-expr->conjoined-types
  (lambda (t)
    (if (tc:output-type-expr-intersection-type? t)
	(cdr t)
	(error
	 "tc:output-type-expr->conjoined-types called with non-intersection-type argument"
	 t))))

(define tc:output-type-expr->for-type
  (lambda (t)
    (if (tc:output-type-expr-type-predicate-for-type? t)
	(cadr t)
	(error
	 "tc:output-type-expr->for-type called with non-type-predicate-for-type argument"
	 t))))

(define tc:output-type-expr->variants
  (lambda (t)
    (if (tc:output-type-expr-variant-record-type? t)
	(cdr t)
	(error
	 "tc:output-type-expr->variants called with non-variant-record-type argument"
	 t))))

(define tc:output-type-expr->operator
  (lambda (t)
    (if (tc:output-type-expr-applied-type? t)
	(car t)
	(error
	 "tc:output-type-expr->operator called with non-applied type argument"
	 t))))

(define tc:output-type-expr->operands
  (lambda (t)
    (if (tc:output-type-expr-applied-type? t)
	(cdr t)
	(error
	 "tc:output-type-expr->operands called with non-applied type argument"
	 t))))

(define tc:output-type-expr->type-formals
  (lambda (t)
    (if (tc:output-type-expr-polymorphic-type? t)
	(cadr t)
	(error
	 "tc:output-type-expr->type-formals called with non-polymorphic type argument"
	 t))))

(define tc:output-type-expr->monomorphic-type
  (lambda (t)
    (if (tc:output-type-expr-polymorphic-type? t)
	(caddr t)
	(error
	 "tc:output-type-expr->type-formals called with non-polymorphic type argument"
	 t))))

(define tc:occurs-in-output-type-expr?
  (lambda (sym typ2)
    ;; EFFECT: determines if sym occurs free in typ2
    (or
     (equal? sym typ2)
     (and (tc:output-type-expr-function-type? typ2)
	  (or (tc:some (lambda (t) (tc:occurs-in-output-type-expr? sym t))
		       (tc:output-type-expr->function-arg-types typ2))
	      (tc:occurs-in-output-type-expr?
	       sym
	       (tc:output-type-expr->function-result-type typ2))))
     (and (tc:output-type-expr-intersection-type? typ2)
	  (tc:some (lambda (t) (tc:occurs-in-output-type-expr? sym t))
		   (tc:output-type-expr->conjoined-types typ2)))
     (and (tc:output-type-expr-type-predicate-for-type? typ2)
	  (tc:occurs-in-output-type-expr?
	   sym
	   (tc:output-type-expr->for-type typ2)))
     (and (tc:output-type-expr-variant-record-type? typ2)
	  (tc:some (lambda (t) (tc:occurs-in-output-variant-decl? sym t))
		   (tc:output-type-expr->variants typ2)))
     (and (tc:output-type-expr-applied-type? typ2)
	  (or (equal? sym (tc:output-type-expr->operator typ2))
	      (tc:some (lambda (t) (tc:occurs-in-output-type-expr? sym t))
		       (tc:output-type-expr->operands typ2))))
     (and (tc:output-type-expr-polymorphic-type? typ2)
	  (not (memq sym (tc:output-type-expr->type-formals typ2)))
	  (tc:occurs-in-output-type-expr?
	   sym 
	   (tc:output-type-expr->monomorphic-type typ2)))
	  )))


(define tc:occurs-in-output-variant-decl?
  (lambda (sym vtd)
    ;; EFFECT: determines if sym occurs free in vtd
    (tc:some (lambda (ftb) (tc:occurs-in-output-field-type-binding? sym ftb))
	     (tc:output-variant-type-decl->field-type-bindings vtd))))

(define tc:occurs-in-output-field-type-binding?
  (lambda (sym ftb)
    ;; EFFECT: determines if sym occurs free in ftb
    (tc:occurs-in-output-type-expr?
     sym
     (tc:output-field-type-binding->type ftb))))
     
(define tc:output-variant-type-decl?
  (lambda (d)
    (and (list? d)
	 (not (null? d)))))

(define tc:make-output-variant-type-decl
  (lambda (variant-name field-type-bindings)
    (cons variant-name field-type-bindings)))

(define tc:output-variant-type-decl->variant-name
  (lambda (vtd)
    (if (tc:output-variant-type-decl? vtd)
	(car vtd)
	(error
	 "tc:output-variant-type-decl->variant-name called with non-variant-type-decl argument"
	 vtd))))

(define tc:output-variant-type-decl->field-type-bindings
  (lambda (vtd)
    (if (tc:output-variant-type-decl? vtd)
	(cdr vtd)
	(error
	 "tc:output-variant-type-decl->field-type-bindings called with non-variant-type-decl argument"
	 vtd))))

(define tc:output-field-type-binding?
  (lambda (d)
    (and (list? d)
	 (= (length d) 2))))

(define tc:make-output-field-type-binding
  (lambda (field-name type)
    (list field-name type)))

(define tc:output-field-type-binding->field-name
  (lambda (ftb)
    (if (tc:output-variant-type-decl? ftb)
	(car ftb)
	(error
	 "tc:output-field-type-binding->field-name called with non-field-type-binding argument"
	 ftb))))

(define tc:output-field-type-binding->type
  (lambda (ftb)
    (if (tc:output-variant-type-decl? ftb)
	(cadr ftb)
	(error
	 "tc:output-field-type-binding->type called with non-field-type-binding argument"
	 ftb))))

) ;; end module