;;; $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))