Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: bitlisp/bitlisp
base: db17644003
...
head fork: bitlisp/bitlisp
compare: e64574cbaf
  • 5 commits
  • 5 files changed
  • 0 commit comments
  • 1 contributor
View
6 src/environments.lisp
@@ -42,7 +42,7 @@
(defun unbind (env symbol)
(remhash symbol (bindings env)))
-(defun resolve (env source)
+(defun resolve (source &optional (env *primitives-env*))
"Lower code into internal representations"
(etypecase source
(null nil)
@@ -53,9 +53,9 @@
(error "~A names no binding" source))))
(list
(destructuring-bind (operator &rest args) source
- (let ((op (resolve env operator)))
+ (let ((op (resolve operator env)))
(typecase op
;(macro (error "TODO: Macroexpansion"))
(special-op (apply (special-op-resolver op) env args))
- (t (cons op (mapcar (curry #'resolve env) args)))))))
+ (t (cons op (mapcar (rcurry #'resolve env) args)))))))
((or string integer single-float double-float) source)))
View
16 src/inference.lisp
@@ -7,17 +7,17 @@
(integer (let ((var (make-instance 'tyvar :kind 1)))
(values (make-form var lit)
(list (make-instance 'pred
- :iface (if (= lit 0)
- (or (lookup "AbelianGroup")
- (error "AbelianGroup undefined"))
- (or (lookup "Ring")
- (error "Ring undefined")))
+ :interface (if (= lit 0)
+ (or (lookup "AbelianGroup")
+ (error "AbelianGroup undefined"))
+ (or (lookup "Ring")
+ (error "Ring undefined")))
:args (list var))))))
(ratio (let ((var (make-instance 'tyvar :kind 1)))
(values (make-form var lit)
(list (make-instance 'pred
- :iface (or (lookup "DivisionRing")
- (error "DivisionRing undefined"))
+ :interface (or (lookup "DivisionRing")
+ (error "DivisionRing undefined"))
:args (list var))))))))
(defun infer-expr-seq (exprs)
@@ -58,7 +58,7 @@
(t (infer-literal expr))))
(defun infer-source (source)
- (infer-expr (resolve *primitives-env* source)))
+ (infer-expr (resolve source)))
(defun split-preds (fixed-vars quant-vars preds)
"(values deferred retained)"
View
8 src/specials.lisp
@@ -51,8 +51,8 @@
(defspecial "if" self (condition then else)
(env
- (list self (resolve env condition)
- (resolve env then) (resolve env else)))
+ (list self (resolve condition env)
+ (resolve then env) (resolve else env)))
((multiple-value-bind (cform cpreds csubst) (infer-expr condition)
(multiple-value-bind (tform tpreds tsubst) (infer-expr then)
(multiple-value-bind (eform epreds esubst) (infer-expr else)
@@ -90,7 +90,7 @@
(env
(let ((var (make-instance 'var :name name :env env)))
(bind env name var)
- (list self var (resolve env value))))
+ (list self var (resolve value env))))
((setf (var-type name) (to-scheme (make-instance 'tyvar :kind 1)))
(multiple-value-bind (vform vpreds vsubst)
(infer-expr value)
@@ -143,7 +143,7 @@
(llvm remote-binding) val))))))))
(defspecial "the" self (type value)
- (env (list self (type-eval type env) (resolve env 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)))))
View
85 src/types.lisp
@@ -141,28 +141,28 @@
(make-instance 'tyqual :context context :head head))
(defclass pred ()
- ((iface :initarg :iface :reader iface)
+ ((interface :initarg :interface :reader interface)
(args :initarg :args :reader args)))
(defmethod print-object ((p pred) stream)
(print-unreadable-object (p stream)
- (format stream "~A~{ ~A~}" (iface p) (args p))))
+ (format stream "~A~{ ~A~}" (interface p) (args p))))
(defmethod subst-apply (s (pred pred))
(make-instance 'pred
- :iface (iface pred)
+ :interface (interface pred)
:args (subst-apply s (args pred))))
(defmethod free-vars ((pred pred))
(free-vars (args pred)))
(defmethod bl-type= ((a pred) (b pred))
- (and (eq (iface a) (iface b))
+ (and (eq (interface a) (interface b))
(every #'bl-type= (args a) (args b))))
-(defun make-pred (iface &rest args)
+(defun make-pred (interface &rest args)
(make-instance 'pred
- :iface iface
+ :interface interface
:args args))
@@ -173,18 +173,30 @@
:args (append (args operator) args)))
(t (make-instance 'tyapp :operator operator :args args))))
-(defun type-eval (code &optional (env *primitives-env*))
+(defun type-resolve (code &optional (env *primitives-env*))
(etypecase code
- ((or integer tygen tyapp) code)
+ (integer code)
((or bl-symbol string) (lookup code env))
+ (list (mapcar (rcurry #'type-resolve env) code))))
+
+(defun type-construct (resolved &optional (env *primitives-env*))
+ (etypecase resolved
+ ((or integer bl-type) resolved)
(list (destructuring-bind (constructor &rest args)
- (mapcar (rcurry #'type-eval env) code)
+ (mapcar (rcurry #'type-construct env) resolved)
+ (assert (> (kind constructor) (length args))
+ (constructor)
+ "Cannot apply type of kind ~A to ~A arguments!"
+ (kind constructor) (length args))
(apply #'tyapply constructor args)))))
+(defun type-eval (code &optional (env *primitives-env*))
+ (type-construct (type-resolve code env) env))
+
(defun constraint-eval (code &optional (env *primitives-env*))
- (destructuring-bind (iface &rest args) code
+ (destructuring-bind (interface &rest args) code
(make-instance 'pred
- :iface (lookup iface env)
+ :interface (lookup interface env)
:args (mapcar (rcurry #'type-eval env) args))))
(defun make-ftype (arg-type return-type)
@@ -199,40 +211,41 @@
:args (list (first types)
(apply #'make-prodty (rest types)))))))
-(defclass iface ()
+(defclass interface ()
((name :initarg :name :reader name)
(supers :initarg :supers :reader supers
:documentation "List of predicates on signature vars")
- (signature :initarg :signature :reader signature
- :documentation "List of vars paramterized on")
- (impls :initarg :impls :accessor impls
- :documentation "List of qualified predicates")))
-
-(defmethod kind ((iface iface))
- (length (signature iface)))
-
-(defun add-impl (iface predicates &rest params)
- (check-type iface iface)
- (unless (= (kind iface) (length params))
+ (vars :initarg :vars :reader vars
+ :documentation "List of vars paramterized on")
+ (implementations :initarg :implementations :accessor implementations
+ :initform nil
+ :documentation "List of qualified predicates")))
+
+(defmethod kind ((interface interface))
+ (length (vars interface)))
+
+(defun add-impl (interface predicates &rest params)
+ (check-type interface interface)
+ (unless (= (kind interface) (length params))
(error "Implementation has wrong kind (~A) to implement ~A (kind ~A)"
- (length params) iface (kind iface)))
+ (length params) interface (kind interface)))
(let ((pred (make-instance 'pred
- :iface iface
+ :interface interface
:args params)))
(when (some (curry #'preds-overlap pred)
- (mapcar #'head (impls iface))))
+ (mapcar #'head (implementations interface))))
(push (make-instance 'tyqual
:context predicates
:head pred)
- (impls iface))))
+ (implementations interface))))
(defun preds-overlap (a b)
(handler-case (unify a b)
(simple-error nil)))
(defun by-super (pred)
- (let ((subst (mapcar #'cons (signature (iface pred)) (args pred))))
- (cons pred (mapcan #'by-super (subst-apply subst (supers (iface pred)))))))
+ (let ((subst (mapcar #'cons (vars (interface pred)) (args pred))))
+ (cons pred (mapcan #'by-super (subst-apply subst (supers (interface pred)))))))
(defun by-impl (pred)
(some (lambda (qual)
@@ -242,7 +255,7 @@
(mapcar (curry #'subst-apply subst)
(context qual))
nil)))
- (impls (iface pred))))
+ (implementations (interface pred))))
(defun entail (givens pred)
(or (some (compose (rcurry (curry #'member pred) :test #'bl-type=)
@@ -365,7 +378,7 @@
(defmethod instantiate (types (gentype pred))
(make-instance 'pred
- :iface (iface gentype)
+ :interface (interface gentype)
:args (instantiate types (args gentype))))
(defun fresh-instance (scheme)
@@ -373,3 +386,13 @@
(make-instance 'tyvar :kind (kind v)))
(vars scheme))
(inner-type scheme)))
+
+(defun infer-kinds (type &optional (arg-count 0))
+ "Takes a resolved type form and returns a (tyvar/tygen . kind) alist."
+ (assert (not (null type)))
+ (etypecase type
+ ((or tyvar tygen) (list (cons type (1+ arg-count))))
+ (list (apply #'nconc
+ (infer-kinds (first type) (length (rest type)))
+ (mapcar #'infer-kinds (rest type))))
+ ((or bl-type integer) nil)))
View
8 src/unification.lisp
@@ -41,9 +41,9 @@
(error "constructor mismatch")))
(defmethod unify ((a pred) (b pred))
- (if (eq (iface a) (iface b))
+ (if (eq (interface a) (interface b))
(unify (args a) (args b))
- (error "interface mismatch: ~A ≠ ~A" (iface a) (iface b))))
+ (error "interface mismatch: ~A ≠ ~A" (interface a) (interface b))))
(defmethod unify ((a integer) (b integer))
(if (= a b)
@@ -88,6 +88,6 @@
(error "constructor mismatch")))
(defmethod match ((a pred) (b pred))
- (if (eq (iface a) (iface b))
+ (if (eq (interface a) (interface b))
(match (args a) (args b))
- (error "interface mismatch: ~A ≠ ~A" (iface a) (iface b))))
+ (error "interface mismatch: ~A ≠ ~A" (interface a) (interface b))))

No commit comments for this range

Something went wrong with that request. Please try again.