From ea90adc457980fbb9c7c443993a340a40b120cb9 Mon Sep 17 00:00:00 2001
From: Benjamin Saunders <besaunde@sfu.ca>
Date: Fri, 20 Apr 2012 14:20:02 -0700
Subject: [PATCH] Added special type constructor forall.

---
 src/specials.lisp | 35 ++++++++++++++++++++++++++++-------
 src/types.lisp    | 19 +++++++++++++------
 src/values.lisp   |  6 ++++++
 3 files changed, 47 insertions(+), 13 deletions(-)

diff --git a/src/specials.lisp b/src/specials.lisp
index 082bd5c..1431e20 100644
--- a/src/specials.lisp
+++ b/src/specials.lisp
@@ -1,5 +1,25 @@
 (in-package #:bitlisp)
 
+(defmacro def-type-special (name self (&rest args) (env &rest resolver) constructor)
+  (with-gensyms (sym)
+    `(let* ((,sym (make-bl-symbol ,name))
+            (,self (make-special-tycon :name ,sym)))
+       (bind *primitives-env* :type ,sym ,self)
+       (setf (special-tycon-resolver ,self) (lambda (,env ,@args) ,@resolver)
+             (special-tycon-constructor ,self) (lambda ,args ,@constructor)))))
+
+(def-type-special "forall" self (vars constraints type)
+    (env (let ((subenv (make-subenv env)))
+           (let ((tyvars (loop :repeat (length vars)
+                               :collect (make-instance 'tyvar))))
+             (mapc (curry #'bind subenv :type) vars tyvars)
+             (list self tyvars
+                   (mapcar (rcurry #'constraint-eval subenv)
+                           constraints)
+                   (infer-kinds (type-resolve type subenv))))))
+    ((declare (ignore vars))
+     (values (type-construct type) constraints)))
+
 (defmacro defspecial (name self (&rest args)
                       (env &body resolver)
                       (&body inferrer)
@@ -120,9 +140,9 @@
 (defspecial "def-as" self (declared-type name value)
     (env
       (let* ((subenv (make-subenv env))
-             (scheme (let ((ty (type-construct (infer-kinds (type-resolve-free declared-type subenv)))))
-                       ;; TODO: Allow constraints to be specified
-                       (quantify (free-vars ty) nil ty)))
+             (scheme
+               (multiple-value-bind (ty preds) (type-eval declared-type env)
+                 (quantify (free-vars ty) preds ty)))
              (var (make-instance 'value
                                  :name name :env env
                                  :value-type scheme)))
@@ -204,10 +224,11 @@
                       (llvm remote-binding) val))))))))
 
 (defspecial "the" self (type value)
-    (env (list self (type-eval type env) (resolve value env)))
-    ((multiple-value-bind (form preds subst) (infer-expr value)
-       (values form preds
-               (subst-compose subst (unify (form-type form) type)))))
+    (env (list self (type-resolve type env) (resolve value env)))
+    ((multiple-value-bind (form val-preds subst) (infer-expr value)
+       (multiple-value-bind (ty ty-preds) (type-construct type)
+         (values form (nconc ty-preds val-preds)
+                 (subst-compose subst (unify (form-type form) ty))))))
     (m b ty
       (declare (ignore m b ty type value))
       (error "What's this doing here?")))
diff --git a/src/types.lisp b/src/types.lisp
index 2be239f..c71fea3 100644
--- a/src/types.lisp
+++ b/src/types.lisp
@@ -182,7 +182,11 @@
     (integer code)
     ((or bl-symbol string) (or (lookup code :type env)
                                (error "~A names no type binding!" code)))
-    (list (mapcar (rcurry #'type-resolve env) code))))
+    (list (let ((ctor (type-resolve (first code) env)))
+            (typecase ctor
+              (special-tycon (apply (special-tycon-resolver ctor)
+                                    env (rest code)))
+              (t (cons ctor (mapcar (rcurry #'type-resolve env) (rest code)))))))))
 
 (defun type-resolve-free (code &optional (env *primitives-env*))
   "Like type-resolve, but binds free variables. Kind inference must be done on the result."
@@ -193,15 +197,18 @@
                                      (make-instance 'tyvar))))
     (list (mapcar (rcurry #'type-resolve-free env) code))))
 
-(defun type-construct (resolved &optional (env *primitives-env*))
+(defun type-construct (resolved)
   (etypecase resolved
     ((or integer bl-type) resolved)
-    (list (destructuring-bind (constructor &rest args)
-              (mapcar (rcurry #'type-construct env) resolved)
-            (apply #'tyapply constructor args)))))
+    (list (unless (null resolved)
+            (destructuring-bind (constructor &rest args) resolved
+              (typecase constructor
+                (special-tycon (apply (special-tycon-constructor constructor)
+                                      args))
+                (t (apply #'tyapply (mapcar #'type-construct resolved)))))))))
 
 (defun type-eval (code &optional (env *primitives-env*))
-  (type-construct (type-resolve code env) env))
+  (type-construct (type-resolve code env)))
 
 (defun constraint-eval (code &optional (env *primitives-env*))
   (destructuring-bind (interface &rest args) code
diff --git a/src/values.lisp b/src/values.lisp
index 2c38e1c..f7b4d9f 100644
--- a/src/values.lisp
+++ b/src/values.lisp
@@ -6,6 +6,12 @@
   (print-unreadable-object (value stream :type t)
     (princ (special-op-name value) stream)))
 
+(defstruct special-tycon name resolver constructor)
+
+(defmethod print-object ((value special-tycon) stream)
+  (print-unreadable-object (value stream :type t)
+    (princ (special-op-name value) stream)))
+
 (defclass value ()
   ((name :initarg :name :reader name)
    (env :initarg :env :reader env)