Skip to content
Browse files

Added special type constructor forall.

  • Loading branch information...
1 parent 5f60ce3 commit ea90adc457980fbb9c7c443993a340a40b120cb9 @Ralith Ralith committed Apr 20, 2012
Showing with 47 additions and 13 deletions.
  1. +28 −7 src/specials.lisp
  2. +13 −6 src/types.lisp
  3. +6 −0 src/values.lisp
35 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)
(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?")))
19 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
6 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)

0 comments on commit ea90adc

Please sign in to comment.
Something went wrong with that request. Please try again.