;;; $Id: type-check-type-expr.def,v 1.5 1999/06/23 16:57:22 leavens Exp $

trustme!				; pair representation of bindings
					; confuses the type checker

(defrep type-expr datum)
(defrep binding (pair symbol type-expr))
(defrep uniq-sym symbol)

(deftype tc:type-expr? (-> (datum) boolean))
(deftype tc:variable-type-expr? (-> (type-expr) boolean))
(deftype tc:basic-type-expr? (-> (type-expr) boolean))
(deftype tc:non-variable-basic-type-expr? (-> (type-expr) boolean))
(deftype tc:poof-type-expr? (-> (type-expr) boolean))
(deftype tc:datum-type-expr? (-> (type-expr) boolean))
(deftype tc:dots-type-expr? (-> (type-expr) boolean))
(deftype tc:function-type-expr? (-> (type-expr) boolean))
(deftype tc:varargs-function-type-expr? (-> (type-expr) boolean))
(deftype tc:and-type-expr? (-> (type-expr) boolean))
(deftype tc:applied-type-expr? (-> (type-expr) boolean))
(deftype tc:make-variable-type-expr (-> (symbol) type-expr))
(deftype tc:variable-type-expr-new-level (-> (type-expr number) type-expr))
(deftype tc:new-variable-type-expr (-> () type-expr))
(deftype tc:make-basic-type-expr (-> (symbol) type-expr))
(deftype tc:make-function-type-expr
  (-> ((list type-expr) type-expr) type-expr))
(deftype tc:make-and-type-expr (-> ((list type-expr)) type-expr))
(deftype tc:make-applied-type-expr (-> (type-expr (list type-expr)) type-expr))
(deftype tc:variable-type-expr->name (-> (type-expr) symbol))
(deftype tc:variable-type-expr->level (-> (type-expr) number))
(deftype tc:variable-type-expr->uniq-sym (-> (type-expr) uniq-sym))
(deftype tc:uniq-sym->variable-type-expr (-> (uniq-sym) type-expr))
(deftype tc:basic-type-expr->symbol (-> (type-expr) symbol))
(deftype tc:function-type-expr->arg-types (-> (type-expr) (list type-expr)))
(deftype tc:function-type-expr->result-type (-> (type-expr) type-expr))
(deftype tc:and-type-expr->conjoined-types (-> (type-expr) (list type-expr)))
(deftype tc:applied-type-expr->operator-type (-> (type-expr) type-expr))
(deftype tc:applied-type-expr->operand-types (-> (type-expr) (list type-expr)))
(deftype tc:parse-type-expr (-> (datum) type-expr))
(deftype tc:occurs-in-type-expr? (-> (type-expr) (-> (type-expr) boolean)))
(deftype tc:type-expr-uniquify
  (and (-> (type-expr) type-expr)
       (-> ((pair type-expr type-expr)) (pair type-expr type-expr))))
(deftype tc:type-expr-instance (-> (type-expr) type-expr))
(deftype tc:variable-type-expr-eq? (-> (type-expr type-expr) boolean))
(deftype tc:basic-type-expr-eq? (-> (type-expr type-expr) boolean))

(deftype tc:binding? (-> (datum) boolean))
(deftype tc:bind-type-expr (-> (symbol type-expr) binding))
(deftype tc:bound? (-> (symbol binding) boolean))
(deftype tc:binding->type-expr (-> (binding) type-expr))
(deftype tc:binding->binder (-> (binding) symbol))
