;;; $Id: tc-output-type-expr.scm,v 1.11 2006/02/10 00:44:13 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.

;;; Output type expressions, as reported to the user in messages:
;;;
;;;   <type-expr> ::= <monomorphic-type>
;;;            | <polymorphic-type>
;;;   <monomorphic-type> ::= <basic-type>
;;;            | <function-type>
;;;            | <intersection-type>
;;;            | <type-predicate-for-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" "typedscm")

(provide tc:output-type-expr?
	 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? (type-predicate-for tc:output-type-expr))
(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) 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" "typedscm"))

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

(define tc:output-type-expr?
  (lambda (d)
    (or (tc:output-type-expr-basic-type? d)
	(tc:output-type-expr-function-type? d)
	(tc:output-type-expr-intersection-type? d)
	(tc:output-type-expr-type-predicate-for-type? d)
	(tc:output-type-expr-variant-record-type? d)
	(tc:output-type-expr-applied-type? d)
	(tc:output-type-expr-polymorphic-type? d))))

(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)
    (has-type-trusted
      boolean
      (and (list? d)
	   (= (length d) 3)
	   (eq? (car d) '->)
	   (list? (cadr d))))))

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

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

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

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

(define tc:output-type-expr-applied-type?
   (lambda (d)
     (has-type-trusted
       boolean
       (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)
    (has-type-trusted
      boolean
      (and (list? d)
	   (= (length d) 3)
	   (eq? (car d) 'forall)))))

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

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

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

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

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

(define tc:make-applied-output-type-expr
  (lambda (name typ)
    (has-type datum (cons name typ))))

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

(define tc:output-type-expr->basic-type
  (lambda (t)
    (if (tc:output-type-expr-basic-type? t)
	(has-type-trusted symbol 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)
	(has-type-trusted (list-of datum) (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 (has-type-trusted (list-of datum) 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)
	(has-type-trusted (list-of datum) (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 (has-type-trusted (list-of datum) 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)
	(has-type-trusted (list-of datum) (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)
	(has-type-trusted symbol (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 (has-type-trusted (list-of datum) 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)
	(has-type-trusted (list-of symbol) (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 (has-type-trusted (list-of datum) 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
    (has-type-trusted
      boolean
      (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)
    (has-type datum (cons variant-name field-type-bindings))))

(define tc:output-variant-type-decl->variant-name
  (lambda (vtd)
    (if (tc:output-variant-type-decl? vtd)
	(has-type-trusted symbol (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)
	(has-type-trusted (list-of datum) (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)
    (has-type-trusted
      boolean
      (and (list? d)
	   (= (length d) 2)))))

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

(define tc:output-field-type-binding->field-name
  (lambda (ftb)
    (if (tc:output-variant-type-decl? ftb)
	(has-type-trusted symbol (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)
	(has-type-trusted datum (cadr ftb))
	(error
	 "tc:output-field-type-binding->type called with non-field-type-binding argument"
	 ftb))))

) ;; end module