From 4e987026148fe65c323afbc93cd560c07bf06b3f Mon Sep 17 00:00:00 2001 From: Yale AI Dept Date: Wed, 14 Jul 1993 13:08:00 -0500 Subject: Import to github. --- type/unify.scm | 154 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 154 insertions(+) create mode 100644 type/unify.scm (limited to 'type/unify.scm') diff --git a/type/unify.scm b/type/unify.scm new file mode 100644 index 0000000..59248c9 --- /dev/null +++ b/type/unify.scm @@ -0,0 +1,154 @@ + +;;; File: type/unify.scm Author: John + +;;; This is the basic unification algorithm used in type checking. + +;;; Unification failure invokes the current type error handler + +;;; Start by removing instantiated type variables from the type. + +(define (unify type1 type2) + (unify-1 (prune type1) (prune type2))) + +;;; The only real tweak here is the read-only bit on type variables. +;;; The rule is that a RO tyvar can be unified only with a generic +;;; non-RO tyvar which has the same or more general context. + +;;; Aside from this, this is standard unification except that context +;;; propagation is needed when a tyvar with a non-empty context is +;;; instantiated. + +;;; If type2 is a tyvar and type1 is not they are switched. + +(define (unify-1 type1 type2) + (cond ((eq? type1 type2) ;; this catches variable to variable unify + 'OK) + ((ntyvar? type1) + (cond ((occurs-in-type type1 type2) + (type-error "Circular type: cannot unify ~A with ~A" + type1 type2)) + ((ntyvar-read-only? type1) + (cond ((or (not (ntyvar? type2)) (ntyvar-read-only? type2)) + (type-error + "Signature too general: cannot unify ~A with ~A" + type1 type2)) + (else + (unify-1 type2 type1)))) + ((and (ntyvar? type2) + (ntyvar-read-only? type2) + (non-generic? type1)) + (type-error + "Type signature cannot be used: monomorphic type variables present.")) + (else + (instantiate-tyvar type1 type2) + (let ((classes (ntyvar-context type1))) + (if (null? classes) + 'OK + (propagate-contexts/ntype type1 type2 classes)))))) + ((ntyvar? type2) + (unify-1 type2 type1)) + ((eq? (ntycon-tycon type1) (ntycon-tycon type2)) + (unify-list (ntycon-args type1) (ntycon-args type2))) + (else + (let ((etype1 (expand-ntype-synonym type1)) + (etype2 (expand-ntype-synonym type2))) + (if (same-tycon? (ntycon-tycon etype1) (ntycon-tycon etype2)) + (unify-list (ntycon-args etype1) (ntycon-args etype2)) + ;; This error message should probably show both the original + ;; and the expanded types for clarity. + (type-error + "Type conflict: type ~A does not match ~A" + etype1 etype2)))))) + + +(define-integrable (instantiate-tyvar tyvar val) + (setf (ntyvar-value tyvar) val)) + +;;; This is needed since interface files may leave multiple def's +;;; for the same tycon sitting around. + +(define (same-tycon? ty1 ty2) + (or (eq? ty1 ty2) + (and (eq? (def-name ty1) (def-name ty2)) + (eq? (def-module ty1) (def-module ty2))))) + + +;;; unifies two lists of types pairwise. Used for tycon args. + +(define (unify-list args1 args2) + (if (null? args1) + 'OK + (begin (unify-list (cdr args1) (cdr args2)) + (unify (car args1) (car args2))))) + +;;; combines a list of types into a single type. Used in constructs +;;; such as [x,y,z] and case expressions. + +(define (unify-list/single-type types) + (when (not (null? types)) + (let ((type (car types))) + (dolist (type2 (cdr types)) + (unify type type2))))) + +;;; This propagates the context from a just instantiated tyvar to the +;;; instantiated value. If the value is a tycon, instances must be +;;; looked up. If the value is a tyvar, the context is added to that of +;;; other tyvar. + +;;; This is used to back out of the unification on errors. This is a +;;; poor mans trail stack! Without this, error messages get very +;;; obscure. + +(define *instantiated-tyvar* '()) + +(define (propagate-contexts/ntype tyvar type classes) + (dynamic-let ((*instantiated-tyvar* tyvar)) + (propagate-contexts/inner type classes))) + +(define (propagate-contexts/inner type classes) + (let ((type (prune type))) + (if (ntyvar? type) + (if (ntyvar-read-only? type) + (if (context-implies? (ntyvar-context type) classes) + 'OK ; no need for context propagation here + (begin + (setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f) + (type-error "Signature context is too general"))) + (if (null? (ntyvar-context type)) + (setf (ntyvar-context type) classes) + (setf (ntyvar-context type) + (merge-contexts classes (ntyvar-context type))))) + (propagate-contexts-1 (expand-ntype-synonym type) classes)))) + +;;; The type has now been expanded. This propagates each class constraint +;;; in turn. + +(define (propagate-contexts-1 type classes) + (dolist (class classes) + (propagate-single-class type class))) + +;;; Now we have a single class & data type. Either an instance decl can +;;; be found or a type error should be signalled. Once the instance +;;; decl is found, contexts are propagated to the component types. + +(define (propagate-single-class type class) + (let ((instance (lookup-instance (ntycon-tycon type) class))) + (cond ((eq? instance '#f) + ;; This remove the instantiation which caused the type + ;; error - perhaps stop error propagation & make + ;; error message better. + (setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f) + (type-error "Type ~A is not in class ~A" type class)) + (else + ;; The instance contains a list of class constraints for + ;; each argument. This loop pairs the argument to the + ;; type constructor with the context required by the instance + ;; decl. + (dolist2 (classes (instance-gcontext instance)) + (arg (ntycon-args type)) + (propagate-contexts/inner arg classes))))) + 'OK) + +;;; The routines which handle contexts (merge-contexts and context-implies?) +;;; are in type-utils. The occurs check is also there. + -- cgit v1.2.3