From 4e987026148fe65c323afbc93cd560c07bf06b3f Mon Sep 17 00:00:00 2001
From: Yale AI Dept <ai@nebula.cs.yale.edu>
Date: Wed, 14 Jul 1993 13:08:00 -0500
Subject: Import to github.

---
 type/type-decl.scm | 337 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 337 insertions(+)
 create mode 100644 type/type-decl.scm

(limited to 'type/type-decl.scm')

diff --git a/type/type-decl.scm b/type/type-decl.scm
new file mode 100644
index 0000000..790c0ca
--- /dev/null
+++ b/type/type-decl.scm
@@ -0,0 +1,337 @@
+;;; This deals with declarations (let & letrec).  The input is a list of
+;;; declarations (valdefs) which may contain recursive-decl-groups, as
+;;; introduced in dependency analysis.  This function alters the list
+;;; of non-generic type variables.  Expressions containing declarations
+;;; need to rebind the non-generic list around the decls and all expressions
+;;; within their scope.
+
+;;; This returns an updated decl list with recursive decl groups removed.
+
+(define (type-decls decls)
+  (cond ((null? decls)
+	 '())
+	((is-type? 'recursive-decl-group (car decls))
+	 (let ((d (recursive-decl-group-decls (car decls))))
+ 	   (type-recursive d)
+	   (append d (type-decls (cdr decls)))))
+	(else
+	 (type-non-recursive (car decls))
+	 (cons (car decls)
+	       (type-decls (cdr decls))))))
+
+;;; This typechecks a mutually recursive group of declarations (valdefs).
+;;; Generate a monomorphic variable for each declaration and unify it with
+;;; the lhs of the decl.  The variable all-vars collects all variables defined
+;;; by the declaration group.  Save the values of placeholders and ng-list
+;;; before recursing.
+
+;;; The type of each variable is marked as recursive.
+
+(define (type-recursive decls)
+  (let ((old-ng (dynamic *non-generic-tyvars*))
+	(old-placeholders (dynamic *placeholders*))
+	(all-vars '())
+	(new-tyvars '())
+	(decls+tyvars '()))
+    ;; on a type error set all types to `a' and give up.
+    (setf (dynamic *placeholders*) '())
+    (recover-type-error 
+       (lambda (r)
+	 (make-dummy-sigs decls)
+	 (setf (dynamic *dict-placeholders*) old-placeholders)
+	 (funcall r))
+       ;; Type the lhs of each decl and then mark each variable bound
+       ;; in the decl as recursive.
+       (dolist (d decls)
+        (fresh-type lhs-type
+	  (push lhs-type (dynamic *non-generic-tyvars*))
+	  (push lhs-type new-tyvars)
+	  (type-decl-lhs d lhs-type)
+	  (push (tuple d lhs-type) decls+tyvars))
+	(dolist (var-ref (collect-pattern-vars (valdef-lhs d)))
+	  (let ((var (var-ref-var var-ref)))
+	    (push var all-vars)
+	    (setf (var-type var)
+		  (make recursive-type (type (var-type var))
+			(placeholders '()))))))
+
+;;; This types the decl right hand sides.  Each rhs type is unified with the
+;;; tyvar corresponding to the lhs.  Before checking the signatures, the
+;;; ng-list is restored.  
+
+       (dolist (d decls+tyvars)
+	 (let ((rhs-type (type-decl-rhs (tuple-2-1 d)))
+	       (lhs-type (tuple-2-2 d)))
+	   (type-unify lhs-type rhs-type
+		 (type-mismatch (tuple-2-1 d)
+			  "Decl type mismatch" lhs-type rhs-type))))
+       (setf (dynamic *non-generic-tyvars*) old-ng)
+       (let ((sig-contexts (check-user-signatures all-vars)))
+
+;;; This generalizes the signatures of recursive decls.  First, the
+;;; context of the declaration group is computed.  Any tyvar in the
+;;; bodies with a non-empty context must appear in all signatures that
+;;; are non-ambiguous.
+	  
+	 (let* ((all-tyvars (collect-tyvars/l new-tyvars))
+		(overloaded-tyvars '()))
+	   (dolist (tyvar all-tyvars)
+	      (when (and (ntyvar-context tyvar) (not (non-generic? tyvar)))
+		 (push tyvar overloaded-tyvars)))
+	   (reconcile-sig-contexts overloaded-tyvars sig-contexts)
+	 ;; We should probably also emit a warning about inherently
+	 ;; ambiguous decls.
+	   (when (and overloaded-tyvars
+		      (apply-pattern-binding-rule? decls))
+		 (setf (dynamic *non-generic-tyvars*)
+		       (do-pattern-binding-rule
+			decls overloaded-tyvars old-ng))
+		 (setf overloaded-tyvars '()))
+	 ;; The next step is to compute the signatures of the defined
+	 ;; variables and to define all recursive placeholders.  When
+	 ;; there is no context the placeholders become simple var refs.
+	 ;; and the types are simply converted.
+	   (cond ((null? overloaded-tyvars)
+		  (dolist (var all-vars)
+		    (let ((r (var-type var)))
+		      (setf (var-type var) (recursive-type-type (var-type var)))
+		      (dolist (p (recursive-type-placeholders r))
+		        (setf (recursive-placeholder-exp p)
+			      (**var/def var)))
+		      (generalize-type var))))
+	 ;; When the declaration has a context things get very hairy.
+	 ;; First, grap the recursive placeholders before generalizing the
+	 ;; types.
+		 (else
+		  ;; Mark the overloaded tyvars as read-only.  This prevents
+		  ;; signature unification from changing the set of tyvars
+		  ;; defined in the mapping.
+		  (dolist (tyvar overloaded-tyvars)
+		     (setf (ntyvar-read-only? tyvar) '#t))
+		  (let ((r-placeholders '()))
+		    (dolist (var all-vars)
+		     (let ((rt (var-type var)))
+		      (dolist (p (recursive-type-placeholders rt))
+			(push p r-placeholders))
+		      (setf (var-type var) (recursive-type-type rt))))
+	 ;; Now compute a signature for each definition and do dictionary
+	 ;; conversion.  The var-map defines the actual parameter associated
+	 ;; with each of the overloaded tyvars.
+		    (let ((var-map (map (lambda (decl)
+					 (tuple (decl-var decl)
+					  (generalize-overloaded-type
+					   decl overloaded-tyvars)))
+					decls)))
+	 ;; Finally discharge each recursive placeholder.
+		      (dolist (p r-placeholders)
+			(let ((ref-to (recursive-placeholder-var p))
+			      (decl-from
+			       (search-enclosing-decls
+				 (recursive-placeholder-enclosing-decls p)
+				 decls)))
+			  (setf (recursive-placeholder-exp p)
+				(recursive-call-code decl-from ref-to var-map)))
+			)))))
+	   (setf (dynamic *placeholders*)
+		 (process-placeholders
+		  (dynamic *placeholders*) old-placeholders decls)))))))
+
+;;; Non-recursive decls are easier.  Save the placeholders, use a fresh type
+;;; for the left hand side, check signatures, and generalize.
+
+(define (type-non-recursive decl)
+ (remember-context decl
+  (fresh-type lhs-type
+    (let ((old-placeholders (dynamic *placeholders*))
+	  (all-vars (map (lambda (x) (var-ref-var x))
+			    (collect-pattern-vars (valdef-lhs decl)))))
+     (setf (dynamic *placeholders*) '())
+     (recover-type-error
+      (lambda (r)
+        (make-dummy-sigs (list decl))
+	(setf (dynamic *placeholders*) old-placeholders)
+        (funcall r))
+      (type-decl-lhs decl lhs-type)
+      (let ((rhs-type (type-decl-rhs decl)))
+	(type-unify lhs-type rhs-type
+           (type-mismatch decl
+	       "Decl type mismatch" lhs-type rhs-type)))
+      (check-user-signatures all-vars)
+      (let ((all-tyvars (collect-tyvars lhs-type))
+	    (overloaded-tyvars '()))
+	(dolist (tyvar all-tyvars)
+	  (when (ntyvar-context tyvar)
+	     (push tyvar overloaded-tyvars)))
+	(when (and overloaded-tyvars
+		   (apply-pattern-binding-rule? (list decl)))
+	 (setf (dynamic *non-generic-tyvars*)
+	   (do-pattern-binding-rule
+	    (list decl) overloaded-tyvars (dynamic *non-generic-tyvars*)))
+	 (setf overloaded-tyvars '()))
+	(if (null? overloaded-tyvars)
+	    (dolist (var all-vars)
+	      (generalize-type var))
+	    (generalize-overloaded-type decl '()))
+	(setf (dynamic *placeholders*)
+	      (process-placeholders
+	       (dynamic *placeholders*) old-placeholders (list decl)))))))))
+
+;;; These functions type check definition components.
+
+;;; This unifies the type of the lhs pattern with a type variable.
+
+(define (type-decl-lhs object type)
+ (dynamic-let ((*enclosing-decls* (cons object (dynamic *enclosing-decls*))))
+  (remember-context object
+   (type-check valdef lhs pat-type
+    (type-unify type pat-type #f)))))
+
+
+;;; This types the right hand side.  The *enclosing-decls* variable is
+;;; used to keep track of which decl the type checker is inside.  This
+;;; is needed for both defaulting (to find which module defaults apply)
+;;; and recursive types to keep track of the dictionary parameter variables
+;;; for recursive references.
+
+(define (type-decl-rhs object)
+ (dynamic-let ((*enclosing-decls* (cons object (dynamic *enclosing-decls*))))
+  (remember-context object
+   (type-check/unify-list valdef definitions res-type
+       (type-mismatch/list object
+	   "Right hand sides have different types")
+       res-type))))
+
+
+;;; This is similar to typing lambda.
+
+(define-type-checker single-fun-def
+  (fresh-monomorphic-types (length (single-fun-def-args object)) tyvars
+    (type-check/list single-fun-def args arg-types
+      (unify-list tyvars arg-types)
+      (type-check/decls single-fun-def where-decls
+        (type-check/unify-list single-fun-def rhs-list rhs-type
+           (type-mismatch/list object
+			"Bodies have incompatible types")
+	  (return-type object (**arrow/l-2 arg-types rhs-type)))))))
+
+
+;;; These functions are part of the generalization process.
+
+;;; This function processes user signature declarations for the set of
+;;; variables defined in a declaration.  Since unification of one signature
+;;; may change the type associated with a previously verified signature,
+;;; signature unification is done twice unless only one variable is
+;;; involved.  The context of the signatures is returned to compare
+;;; with the overall context of the declaration group.
+
+(define (check-user-signatures vars)
+  (cond ((null? (cdr vars))
+	 (let* ((var (car vars))
+		(sig (var-signature var)))
+	   (if (eq? sig '#f)
+	       '()
+	       (list (tuple var (check-var-signature var sig))))))
+	(else
+	 (let ((sigs '()))
+	   (dolist (var vars)
+	     (let ((sig (var-signature var)))
+	       (unless (eq? sig '#f)
+		 (check-var-signature var sig))))
+	   (dolist (var vars)
+	     (let ((sig (var-signature var)))
+	       (unless (eq? sig '#f)
+		 (push (tuple var (check-var-signature var sig)) sigs))))
+	   sigs))))
+
+
+(define (check-var-signature var sig)
+  (mlet (((sig-type sig-vars) (instantiate-gtype/newvars sig)))
+    (dolist (tyvar sig-vars)
+      (setf (ntyvar-read-only? tyvar) '#t))
+    (type-unify (remove-recursive-type (var-type var)) sig-type
+	     (signature-mismatch var))
+    (dolist (tyvar sig-vars)
+      (setf (ntyvar-read-only? tyvar) '#f))
+    sig-vars))
+  
+;;; Once the declaration context is computed, it must be compared to the
+;;; contexts given by the user.  All we need to check is that all tyvars
+;;; constrained in the user signatures are also in the decl-context.
+;;; All user supplied contexts are correct at this point - we just need
+;;; to see if some ambiguous portion of the context exists.
+
+;;; This error message needs work.  We need to present the contexts.
+
+(define (reconcile-sig-contexts overloaded-tyvars sig-contexts)
+  (dolist (sig sig-contexts)
+    (let ((sig-vars (tuple-2-2 sig)))
+      (dolist (d overloaded-tyvars)
+	(when (not (memq d sig-vars))
+	  (type-error
+"Declaration signature has insufficiant context in declaration~%~A~%"
+            (tuple-2-1 sig)))))))
+
+;;; This is used for noisy type inference
+
+(define (report-typing var)
+ (when (memq 'type (dynamic *printers*))
+  (let* ((name (symbol->string (def-name var))))
+    (when (not (or (string-starts? "sel-" name)
+		   (string-starts? "i-" name)
+		   (string-starts? "default-" name)
+		   (string-starts? "dict-" name)))
+      (format '#t "~A :: ~A~%" var (var-type var))))))
+
+;;; This is used during error recovery.  When a type error occurs, all
+;;; variables defined in the enclosing declaration are set to type `a'
+;;; and typing is resumed.
+
+(define (make-dummy-sigs decls)
+  (let ((dummy-type (make gtype (context '(()))
+			        (type (**gtyvar 0)))))
+    (dolist (d decls)
+      (dolist (var-ref (collect-pattern-vars (valdef-lhs d)))
+        (let ((var (var-ref-var var-ref)))
+	  (setf (var-type var) dummy-type))))))
+
+
+;;; This is used to generalize the variable signatures.  If there is
+;;; an attached signature, the signature is used.  Otherwise the ntype
+;;; is converted to a gtype.
+
+(define (generalize-type var)
+  (if (eq? (var-signature var) '#f)
+      (setf (var-type var) (ntype->gtype (var-type var)))
+      (setf (var-type var) (var-signature var)))
+  (report-typing var))
+      
+;;; For overloaded types, it is necessary to map the declaration context
+;;; onto the generalized type.  User signatures may provide different but
+;;; equivilant contexts for different declarations in a decl goup.
+
+;;; The overloaded-vars argument allows ambiguous contexts.  This is not
+;;; needed for non-recursive vars since the context cannot be ambiguous.
+
+(define (generalize-overloaded-type decl overloaded-vars)
+  (let* ((var (decl-var decl))
+	 (sig (var-signature var))
+	 (new-tyvars '()))
+    (cond ((eq? sig '#f)
+	   (mlet (((gtype tyvars)
+		   (ntype->gtype/env (var-type var) overloaded-vars)))
+	      (setf (var-type var) gtype)
+	      (setf new-tyvars tyvars)))
+	  (else
+	   (mlet (((ntype tyvars) (instantiate-gtype/newvars sig)))
+	     (unify ntype (var-type var))
+	     (setf (var-type var) sig)
+	     (setf new-tyvars (prune/l tyvars)))))
+    (report-typing var)
+    (dictionary-conversion/definition decl new-tyvars)
+    new-tyvars))
+
+(define (remove-recursive-type ty)
+  (if (recursive-type? ty)
+      (recursive-type-type ty)
+      ty))
+
-- 
cgit v1.2.3