· 7 years ago · Jan 18, 2019, 07:46 PM
1;;; Experiments in polymorphic function type instantiation with improve Fusion types.
2(defpackage #:fusion
3 (:use #:cl))
4
5(require "alexandria")
6
7(in-package #:fusion)
8
9(defconstant v 'v
10 "Symbol for the implicitly constrained value in a constraint.")
11
12(defconstant top 'top
13 "Symbol for the toplevel implicitly constrained value in a synthesised constraint..")
14
15(defconstant @- '@-
16 "Function symbol to refer to function arguments")
17
18(defconstant @+ '@+
19 "Function symbol to refer to function results")
20
21(defvar *counter*)
22(declaim (type (and unsigned-byte fixnum) *counter*))
23
24(defpackage #:fresh
25 (:use)
26 (:export . #.(loop for i below 100 append
27 (loop for prefix in '(#:v #:b #:e #:k)
28 collect (make-symbol (format nil "~A~A" prefix i))))))
29
30(defun fresh (&optional (prefix '#:v))
31 (prog1
32 (let ((name (intern (format nil "~A~A" prefix *counter*)
33 (load-time-value (find-package '#:fresh)))))
34 ;; the plist is initally empty, and no one should be using our
35 ;; internal package.
36 (unless (symbol-plist name)
37 ;; Populate the symbol's plist with a preparsed version of the identifier.
38 ;; We set the prefix to ^foo because cl-smt will then print that as just 'foo',
39 ;; without any package prefix.
40 (setf (get name :prefix) (intern
41 (concatenate 'string
42 "^" (string-downcase
43 (symbol-name prefix)))
44 (load-time-value (find-package '#:fresh)))
45 (get name :counter) *counter*))
46 name)
47 (incf *counter*)))
48
49(defun rename-fresh-variables-to-smtlib (expression)
50 (typecase expression
51 (list (mapcar #'rename-fresh-variables-to-smtlib expression))
52 (symbol (if (eql (symbol-package expression)
53 (load-time-value (find-package '#:fresh)))
54 ;; (_ :key index) is a valid SMT LIB identifier
55 `(_ ,(get expression :prefix) ,(get expression :counter))
56 expression))
57 (t expression)))
58
59;;; Monomorphic type language
60(defstruct (mono-type
61 (:constructor nil)))
62
63(defstruct (mono-function
64 (:include mono-type)
65 (:constructor mono-function (arguments results)))
66 (arguments (error "Missing arguments") :type list #|mono-type|# :read-only t)
67 (results (error "Missing results") :type list #|mono-type|# :read-only t))
68
69;; This stands in for lists, and other ADTs that act as
70;; non-deterministic sources of types.
71(defstruct (mono-box
72 (:include mono-type)
73 (:constructor mono-box (contents)))
74 (contents (error "Missing contents") :type mono-type :read-only t))
75
76(defstruct (mono-base
77 (:include mono-type)
78 (:constructor mono-base (sort &optional (constraint 'true))))
79 (sort (error "Missing sort") :type symbol :read-only t)
80 (constraint 'true :type (or symbol list) :read-only t))
81
82;;; Polymorphic type language
83(defstruct (poly-type
84 (:constructor nil)))
85
86(defstruct (poly-function
87 (:include poly-type)
88 (:constructor poly-function (arguments results)))
89 (arguments (error "Missing arguments") :type list #|poly-type|# :read-only t)
90 (results (error "Missing results") :type list #|poly-type|# :read-only t))
91
92(defstruct (poly-box
93 (:include poly-type)
94 (:constructor poly-box (contents)))
95 (contents (error "Missing contents") :type poly-type :read-only t))
96
97(defstruct (poly-var
98 (:include poly-type)
99 (:constructor poly-var (&optional (name (fresh)))))
100 (name (fresh) :type symbol :read-only t))
101
102;;; poly-base are used to:
103;;; 1. make sure a poly-var matches against a base type (sort = *, constraint = nil)
104;;; checked in skeleton-matches-polytype-p
105;;; 2. make sure a poly-var matches against a specific base type (sort != *)
106;;; checked in skeleton-matches-polytype-p
107;;; 3. make sure arguments match a certain constraint (constrain them)
108;;; that's done in flow-constraints-for-polytype, where we add constraints for
109;;; each binding and return types from both the polytype and the arguments.
110;;; N.B., while this preserve the goal that the instantiated monotype be a subtype
111;;; of the polytype, it does not guarantee that the arguments fit the instantiated
112;;; mono function type. We must still check subtyping.
113;;; 4. override the constraint on a return type (set it to the poly-base's constraint).
114;;; that's done in %synthesise-skeleton.
115;;; Why do we want to exactly set the return type?
116;;; a return type is equivalent to the argument type for a function passed as an
117;;; argument (think CPS). Clearly, for a funarg's argument, we want to widen the
118;;; argument type to contain the poly-base's constraint (otherwise, we might accept
119;;; a funarg that's too strict for the polymorphic function). Moreover, if the
120;;; polymorphic function was typechecked with that constraint, there's no use in
121;;; having the funarg's argument be wider than necessary. Similarly, if the
122;;; polymorphic checked with that constraint on a return type, there's no reason
123;;; to weaken the constraint.
124;;; N.B., we still have to check that any funarg fits this constraint.
125(defstruct (poly-base
126 (:include poly-var)
127 (:constructor poly-base (&optional (name (fresh)) (sort '*) constraint)))
128 ;; * means no sort defined.
129 (sort '* :type symbol :read-only t)
130 ;; nil means no constraint.
131 (constraint nil :type (or symbol null list) :read-only t))
132
133;;; Skeleton type language. It's the same as the polymorphic types,
134;;; except that we have no generic type variable, and base types have
135;;; a unique name, and track which tvar they flow into (and how).
136(defstruct (skel-type
137 (:constructor nil)))
138
139(defstruct (skel-function
140 (:include skel-type)
141 (:constructor skel-function (arguments results)))
142 (arguments (error "Missing arguments") :type list #|skel-type|# :read-only t)
143 (results (error "Missing results") :type list #|skel-type|# :read-only t))
144
145(defstruct (skel-box
146 (:include skel-type)
147 (:constructor skel-box (contents)))
148 (contents (error "Missing contents") :type skel-type :read-only t))
149
150(defstruct (skel-base
151 (:include skel-type)
152 (:constructor skel-base (sort variance
153 &key (name (fresh '#:b)) (eqv (fresh '#:e)))))
154 (sort (error "Missing sort") :type (and symbol (not (eql *))) :read-only t)
155 (name (fresh '#:b) :type symbol :read-only t)
156 (variance (error "Missing variance") :type (member - +) :read-only t)
157 ;; equivalence class.
158 (eqv (fresh '#:e) :type symbol :read-only t))
159
160(defun invert-variance (variance &optional (flip t))
161 (if flip
162 (ecase variance
163 (- '+)
164 (+ '-))
165 variance))
166
167;;; Create skeleton from pattern and argument monotypes.
168(defgeneric %generate-skeleton (monotype variance)
169 (:documentation "Generate a fresh skeleton that matches monotype."))
170
171(defun generate-skeleton (monotype)
172 (%generate-skeleton monotype '+))
173
174(defmethod %generate-skeleton (monotype variance)
175 (error "Bad argument"))
176
177(defmethod %generate-skeleton ((monotype mono-function) variance)
178 (skel-function (mapcar (lambda (monotype)
179 (%generate-skeleton monotype (invert-variance variance)))
180 (mono-function-arguments monotype))
181 (mapcar (lambda (monotype)
182 (%generate-skeleton monotype variance))
183 (mono-function-results monotype))))
184
185(defmethod %generate-skeleton ((monotype mono-box) variance)
186 ;; Assume boxes are covariant.
187 (skel-box (%generate-skeleton (mono-box-contents monotype) variance)))
188
189(defmethod %generate-skeleton ((monotype mono-base) variance)
190 (skel-base (mono-base-sort monotype) variance))
191
192;;; Copy skeleton to match new variance. If root variance is +,
193;;; nothing to do, otherwise, must flip everything.
194(defvar *root-variance*)
195(declaim (type (member + -) *root-variance*))
196
197(defgeneric %instantiate-skeleton (skeleton))
198
199(defun instantiate-skeleton (skeleton *root-variance*)
200 (%instantiate-skeleton skeleton))
201
202(defmethod %instantiate-skeleton ((skeleton skel-function))
203 (skel-function (mapcar #'%instantiate-skeleton
204 (skel-function-arguments skeleton))
205 (mapcar #'%instantiate-skeleton
206 (skel-function-arguments skeleton))))
207
208(defmethod %instantiate-skeleton ((skeleton skel-box))
209 (skel-box (%instantiate-skeleton (skel-box-contents skeleton))))
210
211(defmethod %instantiate-skeleton ((skeleton skel-base))
212 (skel-base (skel-base-sort skeleton)
213 (invert-variance (skel-base-variance skeleton)
214 (eql *root-variance* '-))
215 :name (fresh '#:b)
216 :eqv (skel-base-eqv skeleton)))
217
218;;; Convert polytype into skeleton by making sure the prefix of the tree matches,
219;;; and variables are instantiated as necessary.
220(defconstant +failed-extension+ '+failed-extension+
221 "Catch tag for failed extension to skeleton.")
222
223(defvar *skeleton-cache*)
224(declaim (type hash-table *skeleton-cache*))
225
226(defun lists-of-same-length-p (x y)
227 (loop while (or x y)
228 do (unless (and x y)
229 (return nil))
230 (pop x)
231 (pop y)
232 finally (return t)))
233
234(assert (lists-of-same-length-p '(1 2) '(2 3)))
235(assert (not (lists-of-same-length-p '(1 2) '(2))))
236
237(defgeneric %extend-polytype (pattern monotype variance))
238
239(defun extend-polytype (pattern monotype variance *skeleton-cache*)
240 (%extend-polytype pattern monotype variance))
241
242(defmethod %extend-polytype (pattern monotype variance)
243 (throw +failed-extension+
244 (format nil "Missing case ~A ~A ~A~%" pattern monotype variance)))
245
246(defmethod %extend-polytype ((pattern poly-function) (monotype mono-function)
247 variance)
248 (unless (and (lists-of-same-length-p
249 (poly-function-arguments pattern)
250 (mono-function-arguments monotype))
251 (lists-of-same-length-p
252 (poly-function-results pattern)
253 (mono-function-results monotype)))
254 (throw +failed-extension+ "Function type mismatch"))
255 (skel-function (mapcar (lambda (pattern monotype)
256 (%extend-polytype pattern monotype
257 (invert-variance variance)))
258 (poly-function-arguments pattern)
259 (mono-function-arguments monotype))
260 (mapcar (lambda (pattern monotype)
261 (%extend-polytype pattern monotype variance))
262 (poly-function-results pattern)
263 (mono-function-results monotype))))
264
265(defmethod %extend-polytype ((pattern poly-box) (monotype mono-box) variance)
266 (skel-box (%extend-polytype (poly-box-contents pattern)
267 (mono-box-contents monotype)
268 variance)))
269
270(defmethod %extend-polytype ((pattern poly-var) (monotype mono-type) variance)
271 (let* ((key (poly-var-name pattern))
272 (skeleton (or (gethash key *skeleton-cache*)
273 (setf (gethash key *skeleton-cache*)
274 (generate-skeleton monotype)))))
275 (instantiate-skeleton skeleton variance)))
276
277;;; instantiate a return type from the type pattern captures above.
278(defgeneric %instantiate-return-type (pattern variance))
279
280(defun instantiate-return-type (pattern cache)
281 (let ((*skeleton-cache* cache))
282 (%instantiate-return-type pattern '+)))
283
284(defmethod %instantiate-return-type ((pattern poly-function) variance)
285 (skel-function (mapcar (lambda (pattern)
286 (%instantiate-return-type pattern (invert-variance variance)))
287 (poly-function-arguments pattern))
288 (mapcar (lambda (pattern)
289 (%instantiate-return-type pattern variance))
290 (poly-function-results pattern))))
291
292(defmethod %instantiate-return-type ((pattern poly-box) variance)
293 (skel-box (%instantiate-return-type (poly-box-contents pattern)
294 variance)))
295
296(defmethod %instantiate-return-type ((pattern poly-var) variance)
297 (instantiate-skeleton
298 (or (gethash (poly-var-name pattern) *skeleton-cache*)
299 (and (poly-base-p pattern)
300 (skel-base (poly-base-sort pattern) '+))
301 (throw +failed-extension+ "Unbound type variable in return type."))
302 variance))
303
304;;; Use the machinery above to create a skeleton function type from a
305;;; polymorphic function pattern and a set of arguments.
306(defun propagate-to-skeleton (pattern arguments)
307 (check-type pattern poly-function)
308 (assert (every #'mono-type-p arguments))
309 (unless (lists-of-same-length-p (poly-function-arguments pattern)
310 arguments)
311 (format *error-output* "Mismatching argument lists for ~A / ~A.~%"
312 pattern arguments)
313 (return-from propagate-to-skeleton nil))
314
315 (let ((error
316 (catch +failed-extension+
317 (let ((cache (make-hash-table)))
318 (return-from propagate-to-skeleton
319 (values (skel-function (mapcar (lambda (pattern monotype)
320 (extend-polytype pattern monotype '- cache))
321 (poly-function-arguments pattern)
322 arguments)
323 (mapcar (lambda (pattern)
324 (instantiate-return-type pattern cache))
325 (poly-function-results pattern)))
326 cache))))))
327 (format *error-output*
328 "Failed to propagate to skeleton for ~A / ~A: ~A~%"
329 pattern arguments error)
330 nil))
331
332(let ((*counter* 0))
333 (assert
334 (equalp
335 (propagate-to-skeleton
336 (poly-function `(,(poly-var 'v0))
337 `(,(poly-var 'v0)))
338 `(,(mono-box (mono-base 'integer))))
339 (skel-function `(,(skel-box (skel-base
340 'integer '-
341 :name 'fresh:b2
342 :eqv 'fresh:e1)))
343 `(,(skel-box (skel-base
344 'integer '+
345 :name 'fresh:b3
346 :eqv 'fresh:e1)))))))
347
348;;; Compare a skeleton with a monotype.
349(defgeneric %skeleton-matches-monotype-p (skeleton monotype))
350
351(defun skeleton-matches-monotype-p (skeleton arguments)
352 (check-type skeleton skel-function)
353 (assert (every #'mono-type-p arguments))
354 (and (lists-of-same-length-p (skel-function-arguments skeleton)
355 arguments)
356 (every #'%skeleton-matches-monotype-p
357 (skel-function-arguments skeleton)
358 arguments)))
359
360(defmethod %skeleton-matches-monotype-p (skeleton monotype)
361 (format *error-output* "Missing case for ~A ~A~%" skeleton monotype)
362 nil)
363
364(defmethod %skeleton-matches-monotype-p ((skeleton skel-function)
365 (monotype mono-function))
366 (flet ((lists-match-p (skeletons monotypes)
367 (and (lists-of-same-length-p skeletons monotypes)
368 (every #'%skeleton-matches-monotype-p skeletons monotypes))))
369 (and (lists-match-p (skel-function-arguments skeleton)
370 (mono-function-arguments monotype))
371 (lists-match-p (skel-function-results skeleton)
372 (mono-function-results monotype)))))
373
374(defmethod %skeleton-matches-monotype-p ((skeleton skel-box)
375 (monotype mono-box))
376 (%skeleton-matches-monotype-p (skel-box-contents skeleton)
377 (mono-box-contents monotype)))
378
379(defmethod %skeleton-matches-monotype-p ((skeleton skel-base)
380 (monotype mono-base))
381 (eql (skel-base-sort skeleton)
382 (mono-base-sort monotype)))
383
384;;; Compare a skeleton with a polytype.
385
386;;; While the skeleton mostly matches the polytype by construction, we
387;;; have to check that poly-base only match skel-base.
388(defgeneric %polytype-matches-skeleton-p (polytype skeleton))
389
390(defun skeleton-matches-polytype-p (skeleton polytype)
391 (check-type skeleton skel-function)
392 (check-type polytype poly-function)
393 (%polytype-matches-skeleton-p polytype skeleton))
394
395(defmethod %polytype-matches-skeleton-p (polytype skeleton)
396 (format *error-output* "Missing case for ~A ~A~%" polytype skeleton)
397 nil)
398
399(defmethod %polytype-matches-skeleton-p ((polytype poly-var) (skeleton skel-type))
400 t)
401
402(defmethod %polytype-matches-skeleton-p ((polytype poly-function)
403 (skeleton skel-function))
404 (flet ((lists-match-p (polytypes skeletons)
405 (and (lists-of-same-length-p polytypes skeletons)
406 (every #'%polytype-matches-skeleton-p polytypes skeletons))))
407 (and (lists-match-p (poly-function-arguments polytype)
408 (skel-function-arguments skeleton))
409 (lists-match-p (poly-function-results polytype)
410 (skel-function-results skeleton)))))
411
412(defmethod %polytype-matches-skeleton-p ((polytype poly-box)
413 (skeleton skel-box))
414 (%polytype-matches-skeleton-p (poly-box-contents polytype)
415 (skel-box-contents skeleton)))
416
417(defmethod %polytype-matches-skeleton-p ((polytype poly-base)
418 (skeleton skel-base))
419 (or (eql (poly-base-sort polytype) '*)
420 (eql (poly-base-sort polytype) (skel-base-sort skeleton))))
421
422;;; Representation for bound values of a base type.
423
424;;; The scope itself is represented as a dynamically bound cons list
425;;; for simplicity. This does mean that going up-scope is linear
426;;; time, but it shouldn't be an issue in practice ;)
427(defstruct scope-level
428 (arguments (make-array 8 :adjustable t :fill-pointer 0)
429 :type vector
430 :read-only t)
431 (results (make-array 8 :adjustable t :fill-pointer 0)
432 :type vector
433 :read-only t))
434
435(defvar *environment* '())
436(declaim (type (or null (cons scope-level)) *environment*))
437
438(defconstant +failed-lookup+ '+failed-lookup+)
439
440(defun lookup (form environment)
441 (destructuring-bind (operator index &optional (depth 0)) form
442 (let* ((level (or (elt environment depth)
443 (throw +failed-lookup+ "No such depth")))
444 (vector (ecase operator
445 (@- (scope-level-arguments level))
446 (@+ (scope-level-results level)))))
447 (when (>= index (length vector))
448 (throw +failed-lookup+ "No such index"))
449 (or (elt vector index)
450 (throw +failed-lookup+ "No base value bound at index.")))))
451
452;;; Representation for globalised side constraints, and their flow
453;;; into/out of type variables.
454(defstruct (global-constraint
455 (:constructor global-constraint (key dependencies expression)))
456 (key (error "Missing key") :type skel-base :read-only t)
457 (dependencies (error "Missing dependencies")
458 :type list #|skel-base|#
459 :read-only t)
460 (expression (error "Missing constraint expression")
461 :type (or symbol list)
462 :read-only t))
463
464(defstruct skel-base-constraints
465 ;; List of skel-base that polymorphically flow in this equivalenc class.
466 ;; We have to generate a constraint; for each such argument flowing in.
467 (polymorphic-flows-in '() :type list)
468 ;; All skel-base that flow into this equivalence class (sources of values).
469 (flow-in (make-array 8 :adjustable t :fill-pointer 0) :read-only t)
470 ;; All skel-base that flow out of this equivalence class (source of constraints),
471 (flow-out (make-array 8 :adjustable t :fill-pointer 0) :read-only t))
472
473;;; Convert a constraint with de bruijn indices to an expression that
474;;; refers directly to the skel-base bound to each index.
475(defun %listify-dependencies (dependencies)
476 (sort (alexandria:hash-table-keys dependencies)
477 #'string< :key #'skel-base-name))
478
479(defun globalise-constraint (key constraint environment)
480 (check-type key skel-base)
481 (check-type environment list)
482 ;; The environment maps de bruijn indices to `skel-base` instances or nil.
483 (let ((dependencies (make-hash-table)))
484 (labels ((walk (form)
485 (etypecase form
486 ((cons (member @- @+))
487 (let ((dependency (lookup form environment)))
488 (setf (gethash dependency dependencies) dependency)))
489 (list
490 (mapcar #'walk form))
491 (t
492 form))))
493 (let ((expression (walk constraint)))
494 (global-constraint key
495 (%listify-dependencies dependencies)
496 expression)))))
497
498;;; Utility to accumulate constraints.
499(defvar *skel-base-flow-constraints*) ; skel-base-eqv -> skel-base-constraints
500(declaim (type hash-table *skel-base-flow-constraints*))
501
502(defun accumulate-flow-constraint (constraint skeleton
503 &optional (environment *environment*))
504 (check-type skeleton skel-base)
505 (let* ((global-constraint (globalise-constraint skeleton constraint environment))
506 (flow-map *skel-base-flow-constraints*)
507 (flow-set (or (gethash (skel-base-eqv skeleton) flow-map)
508 (setf (gethash (skel-base-eqv skeleton) flow-map)
509 (make-skel-base-constraints)))))
510 (ecase (skel-base-variance skeleton)
511 (- ;; value flows into this type.
512 (vector-push-extend global-constraint (skel-base-constraints-flow-in flow-set)))
513 (+
514 (vector-push-extend global-constraint (skel-base-constraints-flow-out flow-set)))))
515 nil)
516
517(defun note-polymorphic-argument-type (skeleton)
518 (check-type skeleton skel-base)
519 (let* ((flow-map *skel-base-flow-constraints*)
520 (flow-set (or (gethash (skel-base-eqv skeleton) flow-map)
521 (setf (gethash (skel-base-eqv skeleton) flow-map)
522 (make-skel-base-constraints)))))
523 (push skeleton (skel-base-constraints-polymorphic-flows-in flow-set))
524 nil))
525
526(defvar *flow-constraints-in-return-value*)
527(declaim (type boolean *flow-constraints-in-return-value*))
528
529(defgeneric note-polymorphic-arguments-in-skeleton (skeleton))
530
531(defmethod note-polymorphic-arguments-in-skeleton :around (skeleton)
532 (when *flow-constraints-in-return-value*
533 (call-next-method)))
534
535(defmethod note-polymorphic-arguments-in-skeleton ((skeleton skel-function))
536 (map nil #'note-polymorphic-arguments-in-skeleton
537 (skel-function-arguments skeleton))
538 (map nil #'note-polymorphic-arguments-in-skeleton
539 (skel-function-results skeleton)))
540
541(defmethod note-polymorphic-arguments-in-skeleton ((skeleton skel-box))
542 (note-polymorphic-arguments-in-skeleton (skel-box-contents skeleton)))
543
544(defmethod note-polymorphic-arguments-in-skeleton ((skeleton skel-base))
545 (when (eql '- (skel-base-variance skeleton))
546 (note-polymorphic-argument-type skeleton)))
547
548;;; Accumulate subtyping constraints for a polytype into a skeleton.
549;;; Assume the skeleton already matches the polytype.
550(defgeneric %flow-constraints-for-polytype (polytype skeleton))
551
552(defun flow-constraints-for-polytype (polytype skeleton)
553 (check-type polytype poly-function)
554 (check-type skeleton skel-function)
555 (assert (null *environment*))
556 (let* ((level (make-scope-level))
557 (*environment* (list level)))
558 (let ((*flow-constraints-in-return-value* nil))
559 (loop
560 for polytype in (poly-function-arguments polytype)
561 for skeleton in (skel-function-arguments skeleton)
562 do (%flow-constraints-for-polytype polytype skeleton)
563 (vector-push-extend (and (skel-base-p skeleton)
564 skeleton)
565 (scope-level-arguments level))))
566 (let ((*flow-constraints-in-return-value* t))
567 (loop
568 for polytype in (poly-function-results polytype)
569 for skeleton in (skel-function-results skeleton)
570 do (%flow-constraints-for-polytype polytype skeleton)
571 (vector-push-extend (and (skel-base-p skeleton)
572 skeleton)
573 (scope-level-results level))))))
574
575(defmethod %flow-constraints-for-polytype (polytype skeleton)
576 (error "Mismatching polytype / skeleton: ~A ~A~%" polytype skeleton))
577
578(defmethod %flow-constraints-for-polytype ((polytype poly-function)
579 (skeleton skel-function))
580 (let* ((level (make-scope-level))
581 (*environment* (cons level *environment*)))
582 (loop
583 for polytype in (poly-function-arguments polytype)
584 for skeleton in (skel-function-arguments skeleton)
585 do (%flow-constraints-for-polytype polytype skeleton)
586 (vector-push-extend (and (skel-base-p skeleton)
587 skeleton)
588 (scope-level-arguments level)))
589 (loop
590 for polytype in (poly-function-results polytype)
591 for skeleton in (skel-function-results skeleton)
592 do (%flow-constraints-for-polytype polytype skeleton)
593 (vector-push-extend (and (skel-base-p skeleton)
594 skeleton)
595 (scope-level-results level)))))
596
597(defmethod %flow-constraints-for-polytype ((polytype poly-box)
598 (skeleton skel-box))
599 (%flow-constraints-for-polytype (poly-box-contents polytype)
600 (skel-box-contents skeleton)))
601
602(defmethod %flow-constraints-for-polytype ((polytype poly-var)
603 (skeleton skel-type))
604 (note-polymorphic-arguments-in-skeleton skeleton))
605
606(defmethod %flow-constraints-for-polytype ((polytype poly-base)
607 (skeleton skel-base))
608 ;; We only flow information from poly base types in argument position.
609 ;; return values are handled in %synthesise-skeleton.
610 (when (eql '+ (skel-base-variance skeleton))
611 (return-from %flow-constraints-for-polytype))
612 (when *flow-constraints-in-return-value*
613 (note-polymorphic-argument-type skeleton))
614 ;; sort was already checked to match.
615 (let ((constraint (poly-base-constraint polytype)))
616 (when constraint ; NIL means no constraint
617 (accumulate-flow-constraint constraint skeleton))))
618
619;;; Accumulate subtyping constraints for monotype arguments going to a
620;;; skeleton.
621(defgeneric %flow-constraints-for-monotype (monotype skeleton))
622
623(defun flow-constraints-for-monotype-arguments (skeleton monotypes)
624 (check-type skeleton skel-function)
625 (assert (every #'mono-type-p monotypes))
626 (assert (null *environment*))
627 (let* ((level (make-scope-level))
628 (*environment* (list level)))
629 (loop
630 for skeleton in (skel-function-arguments skeleton)
631 for monotype in monotypes
632 do (%flow-constraints-for-monotype monotype skeleton)
633 (vector-push-extend (and (skel-base-p skeleton)
634 skeleton)
635 (scope-level-arguments level)))))
636
637(defmethod %flow-constraints-for-monotype (monotype skeleton)
638 (error "Mismatching monotype / skeleton ~A ~A~%" monotype skeleton))
639
640(defmethod %flow-constraints-for-monotype ((monotype mono-function)
641 (skeleton skel-function))
642 (let* ((level (make-scope-level))
643 (*environment* (cons level *environment*)))
644 (loop
645 for monotype in (mono-function-arguments monotype)
646 for skeleton in (skel-function-arguments skeleton)
647 do (%flow-constraints-for-monotype monotype skeleton)
648 (vector-push-extend (and (skel-base-p skeleton)
649 skeleton)
650 (scope-level-arguments level)))
651 (loop
652 for monotype in (mono-function-results monotype)
653 for skeleton in (skel-function-results skeleton)
654 do (%flow-constraints-for-monotype monotype skeleton)
655 (vector-push-extend (and (skel-base-p skeleton)
656 skeleton)
657 (scope-level-results level)))))
658
659(defmethod %flow-constraints-for-monotype ((monotype mono-box)
660 (skeleton skel-box))
661 (%flow-constraints-for-monotype (mono-box-contents monotype)
662 (skel-box-contents skeleton)))
663
664(defmethod %flow-constraints-for-monotype ((monotype mono-base)
665 (skeleton skel-base))
666 (accumulate-flow-constraint (mono-base-constraint monotype)
667 skeleton))
668
669;;; Populate polymorphic argument types
670;;;
671;;; In a function like `(a -> b) -> (a -> b)`, no (known) value flows
672;;; into `a`. Be maximally permissive by letting the constraint for
673;;; the returned function's argument (and every other polymorphically
674;;; bound argument) satisfy the condition for every site that can
675;;; receive an `a` (to which `a` flows out), nothing more.
676(defun %populate-polymorphic-argument-type (constraints)
677 (check-type constraints skel-base-constraints)
678 (unless (skel-base-constraints-polymorphic-flows-in constraints)
679 (return-from %populate-polymorphic-argument-type))
680 (let ((dependencies (make-hash-table))
681 (conditions '()))
682 ;; No need to try and filter away constraints that come from the polytype:
683 ;; we don't collect those when they're flowing out of the type.
684 (loop for condition across (skel-base-constraints-flow-out constraints)
685 do (loop for dependency in (global-constraint-dependencies condition)
686 do (setf (gethash dependency dependencies) dependencies))
687 (push (global-constraint-expression condition) conditions))
688 (let* ((dependencies (%listify-dependencies dependencies))
689 (condition (cond ((null conditions)
690 'true)
691 ((null (rest conditions))
692 (first conditions))
693 (t
694 `(and ,@(nreverse conditions))))))
695 (loop for polymorphic-argument
696 in (skel-base-constraints-polymorphic-flows-in constraints)
697 do (vector-push-extend (global-constraint
698 polymorphic-argument dependencies condition)
699 (skel-base-constraints-flow-in constraints)))
700 nil)))
701
702;;; Accumulate all globalised flow side constraints for base type variables
703;;; in the skeleton.
704(defun flow-constraints (skeleton polytype monotypes)
705 (check-type skeleton skel-function)
706 (check-type polytype poly-function)
707 (assert (every #'mono-type-p monotypes))
708 (let ((*skel-base-flow-constraints* (make-hash-table)))
709 (flow-constraints-for-polytype polytype skeleton)
710 (flow-constraints-for-monotype-arguments skeleton monotypes)
711 (maphash (lambda (k constraints)
712 (declare (ignore k))
713 (%populate-polymorphic-argument-type constraints))
714 *skel-base-flow-constraints*)
715 *skel-base-flow-constraints*))
716
717;;; Convert a globalised condition to a local one, given the current
718;;; reverse de bruijn mapping.
719
720;;; alist from skel-base -> location, (operator index depth), if in scope. The
721;;; depth is reversed from the usual de bruijn scheme.
722(defvar *global-skel-base-map*)
723
724;;; same thing, but these bindings are always safe to use.
725(defvar *safe-skel-base-map*)
726(declaim (type list *global-skel-base-map* *safe-skel-base-map*))
727
728;;; current scoping depth. We recover the source-level de bruijn index by
729;;; subtracting a binding's global depth from the current depth.
730(defvar *current-depth*)
731(declaim (type (and fixnum (integer -1)) *current-depth*))
732
733(defvar *synthesising-results*)
734
735(defun find-binding (skeleton safe-only)
736 "Returns an expression to refer to skeleton, or nil."
737 (check-type skeleton skel-base)
738 (check-type *current-depth* unsigned-byte)
739 (let ((entry (or (cdr (assoc skeleton *safe-skel-base-map*))
740 (and (not safe-only)
741 (cdr (assoc skeleton *global-skel-base-map*))))))
742 (and entry
743 (destructuring-bind (operator index depth) entry
744 (assert (<= depth *current-depth*))
745 (let ((relative-depth (- *current-depth* depth)))
746 `(,operator ,index ,@(and (plusp relative-depth)
747 `(,relative-depth))))))))
748
749(defvar *occur-check-set*)
750
751(defun %localise-condition (condition &key safe-only)
752 "Converts a condition to use local bindings, in the current environment.
753
754 If safe-only is true, only use safe, toplevel bindings."
755 (check-type condition global-constraint)
756 (let ((binding-for-condition-source (find-binding
757 (global-constraint-key condition)
758 safe-only)))
759 (when binding-for-condition-source
760 (return-from %localise-condition `(= v ,binding-for-condition-source))))
761 (let ((dependency-map (make-hash-table)) ; skel-base -> de bruijn expression
762 (values-to-synthesise '())) ; alist var name -> skel-base
763 (loop for dependency in (global-constraint-dependencies condition)
764 for binding = (find-binding dependency safe-only)
765 when binding
766 do (setf (gethash dependency dependency-map) binding))
767 (labels ((walk (form)
768 (etypecase form
769 (skel-base
770 (or (gethash form dependency-map)
771 (let ((name (fresh '#:v)))
772 (push (cons name form) values-to-synthesise)
773 name)))
774 (list
775 (mapcar #'walk form))
776 (atom form))))
777 (let ((root-expression (walk (global-constraint-expression condition))))
778 (if (not values-to-synthesise)
779 root-expression
780 (labels
781 ((bind-existentials (to-bind)
782 (if (null to-bind)
783 `(let ((,v ,top))
784 ,root-expression)
785 (destructuring-bind ((name . skeleton) . to-bind) to-bind
786 (let ((sort (skel-base-sort skeleton))
787 (possible-values (%synthesise-value skeleton))
788 (body (bind-existentials to-bind)))
789 `(exists ((,name ,sort))
790 ,(if (eql possible-values 'true)
791 body
792 `(and (let ((,v ,name))
793 ,possible-values)
794 ,body))))))))
795 (let* ((key (skel-base-eqv (global-constraint-key condition)))
796 (must-mark (not (gethash key *occur-check-set*))))
797 (prog2
798 (when must-mark
799 ;; when called from a toplevel synthesis function, populate
800 ;; the occur check table here.
801 (setf (gethash key *occur-check-set*) t))
802 `(let ((,top ,v))
803 ,(bind-existentials (nreverse values-to-synthesise)))
804 (when must-mark
805 (setf (gethash key *occur-check-set*) nil))))))))))
806
807(defun %synthesise-value (skeleton)
808 "Returns an expression that conservatively describes the set of all
809 values that might be bound to skeleton."
810 (check-type skeleton skel-base)
811 (let ((eqv-class (skel-base-eqv skeleton)))
812 (cond ((gethash eqv-class *occur-check-set*)
813 ;; If there's a circular dependency, assume any value of the base type
814 ;; can flow in. This is safe, if coarse.
815 ;;
816 ;; XXX: let the types unroll more than once? Would we need to rethink
817 ;; the naming scheme for temp variables?
818 (format *error-output* "Breaking circular dependency for ~A.~%" skeleton)
819 'true)
820 (t
821 (prog2 (setf (gethash eqv-class *occur-check-set*) t)
822 (let* ((constraints
823 (or (gethash eqv-class *skel-base-flow-constraints*)
824 (error "Eqv class ~A not found for ~A."
825 eqv-class skeleton)))
826 (localised-conditions
827 (map 'list
828 (lambda (condition)
829 (let ((binding (find-binding
830 (global-constraint-key condition)
831 t)))
832 (if binding
833 `(= ,v ,binding)
834 (%localise-condition condition :safe-only t))))
835 (skel-base-constraints-flow-in constraints))))
836 (cond ((null localised-conditions)
837 (format *error-output* "No value flowing in?")
838 'false)
839 ((null (rest localised-conditions))
840 (first localised-conditions))
841 (t
842 `(or ,@localised-conditions))))
843 (setf (gethash eqv-class *occur-check-set*) nil))))))
844
845;;; Find the tightest condition for each skel-base.
846;;;
847;;; We don't simply take all constraints ever attached to this
848;;; equivalence set in order to get tighter conditions on live
849;;; bindings.
850;;;
851;;; If the variance is -, we're generating a condition for a bound
852;;; value. The only reason we'll have more than one condition for this
853;;; binding is if both the polytype and the monotype have conditions
854;;; on it. In that case, we accept anything that satisfies both
855;;; conditions. For example, if the polytype has a side constraint
856;;; that a given argument must accept any `Int` (i.e., constraint =
857;;; true), then we must any `Int` in the synthesised monotype.
858;;; Otherwise, the synthesised type would not be a subtype of the poly
859;;; type, and that would be bad.
860;;;
861;;; If the variance is +, we're generating the description for a
862;;; return value. That value could be anything that we ever received
863;;; of that type, so we OR together the conditions for every binding.
864(defun %synthesise-argument-condition (skeleton constraints)
865 (check-type skeleton skel-base)
866 (let ((constraints (skel-base-constraints-flow-in constraints))
867 (conditions '()))
868 (loop for constraint across constraints
869 for key = (global-constraint-key constraint)
870 when (eql key skeleton)
871 do (push constraint conditions))
872 (cond ((null conditions) nil)
873 ((null (rest conditions))
874 (%localise-condition (first conditions)))
875 (t
876 `(and ,@(mapcar #'%localise-condition (nreverse conditions)))))))
877
878;;; XXX. When we're actually synthesising a funarg's arguments, we're
879;;; only generating a subtyping constraint to check against the
880;;; monotypes. As such, it's always safe to widen the condition by
881;;; only allowing the use of safe bindings.
882(defun %synthesise-return-condition (constraints)
883 (let* ((groups (loop
884 ;; group conditions by key. conditions for the same key
885 ;; constrain the same binding and may be ANDed.
886 with dst = (make-hash-table)
887 for constraint across (skel-base-constraints-flow-in constraints)
888 do (push constraint (gethash (global-constraint-key constraint)
889 dst))
890 finally (return dst)))
891 (conditions (loop for group being the hash-values of groups
892 collect
893 (let ((localised (mapcar (lambda (condition)
894 (%localise-condition condition
895 :safe-only t))
896 group)))
897 (if (null (rest localised))
898 (first localised)
899 `(and ,@localised))))))
900 (cond ((null conditions)
901 (format *error-output*
902 "Why are we generating a polymorphic type with no value going in?")
903 'false)
904 ((null (rest conditions))
905 (first conditions))
906 (t
907 `(or ,@conditions)))))
908
909(defun %synthesise-condition (skeleton)
910 "Constructs a tight condition with local bindings for the skel-base."
911 (check-type skeleton skel-base)
912 (let* ((eqv-class (skel-base-eqv skeleton))
913 (constraints (or (gethash eqv-class *skel-base-flow-constraints*)
914 (error "Eqv class ~A not found for ~A."
915 eqv-class skeleton))))
916 (ecase (skel-base-variance skeleton)
917 (- (or (%synthesise-argument-condition skeleton constraints)
918 (error "Polymorphic argument not detected?")))
919 (+ (%synthesise-return-condition constraints)))))
920
921;;; Synthesise the full function monotype for a skeleton.
922(defgeneric %synthesise-skeleton (skeleton polytype))
923
924(defvar *populate-bindings*)
925
926(defun synthesise-skeleton (skeleton polytype flow-constraints)
927 (check-type skeleton skel-function)
928 (check-type polytype poly-function)
929 (check-type flow-constraints hash-table)
930 (let ((*skel-base-flow-constraints* flow-constraints)
931 (*global-skel-base-map* '())
932 (*safe-skel-base-map* '())
933 (*current-depth* -1)
934 (*populate-bindings* t)
935 (*occur-check-set* (make-hash-table)))
936 (%synthesise-skeleton skeleton polytype)))
937
938(defmethod %synthesise-skeleton ((skeleton skel-function) polytype)
939 (check-type polytype (or null poly-function poly-var))
940 (let ((*current-depth* (1+ *current-depth*))
941 (*global-skel-base-map* *global-skel-base-map*)
942 (*safe-skel-base-map* *safe-skel-base-map*)
943 (arguments (skel-function-arguments skeleton))
944 (polyargs (and (poly-function-p polytype)
945 (poly-function-arguments polytype)))
946 (results (skel-function-results skeleton))
947 (polyresults (and (poly-function-p polytype)
948 (poly-function-results polytype))))
949 (mono-function (loop
950 for i upfrom 0
951 for skeleton in arguments
952 for polytype = (pop polyargs)
953 ;; Don't recursively populate bindings in
954 ;; funargs: it doesn't make sense to refer to
955 ;; refer their arguments from their arguments.
956 for monotype = (let ((*populate-bindings* nil))
957 (%synthesise-skeleton skeleton polytype))
958 collect monotype
959 when (skel-base-p skeleton)
960 do (let ((binding (list skeleton '@- i *current-depth*)))
961 (if *populate-bindings*
962 (push binding *safe-skel-base-map*)
963 (push binding *global-skel-base-map*))))
964 (loop
965 for i upfrom 0
966 for skeleton in results
967 for polytype = (pop polyresults)
968 for monotype = (%synthesise-skeleton skeleton polytype)
969 collect monotype
970 when (skel-base-p skeleton)
971 do (let ((binding (list skeleton '@+ i *current-depth*)))
972 (if *populate-bindings*
973 (push binding *safe-skel-base-map*)
974 (push binding *global-skel-base-map*)))))))
975
976(defmethod %synthesise-skeleton ((skeleton skel-box) polytype)
977 (check-type polytype (or null poly-box poly-var))
978 (mono-box (%synthesise-skeleton (skel-box-contents skeleton)
979 (and (poly-box-p polytype)
980 (poly-box-contents polytype)))))
981
982(defmethod %synthesise-skeleton ((skeleton skel-base) polytype)
983 (mono-base (skel-base-sort skeleton)
984 ;; If a the polymorphic function specifies a return type, take
985 ;; the override.
986 (or (and (poly-base-p polytype)
987 (eql (skel-base-variance skeleton) '+)
988 (poly-base-constraint polytype))
989 (%synthesise-condition skeleton))))
990
991;;; Instantiate the monotype for a polymorphic function and monotyped arguments.
992(defun instantiate-polymorphic-call (function arguments)
993 (check-type function poly-function)
994 (assert (every #'mono-type-p arguments))
995 ;; XXX: save the mapping from propagate-to-skeleton if we want to
996 ;;monomorphise with codegen.
997 (let* ((*counter* 0)
998 (skeleton (or (propagate-to-skeleton function arguments)
999 (progn
1000 (format *error-output* "Failed to create skeleton.")
1001 (return-from instantiate-polymorphic-call nil)))))
1002 #+debug
1003 (format t "skeleton:~%~A~%" skeleton)
1004 (unless (skeleton-matches-monotype-p skeleton arguments)
1005 (format *error-output* "Skeleton does not match arguments.")
1006 (return-from instantiate-polymorphic-call nil))
1007 (unless (skeleton-matches-polytype-p skeleton function)
1008 (format *error-output* "Skeleton does not match polymorphic pattern.")
1009 (return-from instantiate-polymorphic-call nil))
1010 (let ((constraints (flow-constraints skeleton function arguments)))
1011 #+debug
1012 (format t "constraints:~%~A~%" (alexandria:hash-table-alist constraints))
1013 (synthesise-skeleton skeleton function constraints))))
1014
1015;; See what happens with
1016;; (A -> B) -> (B -> C) -> A -> C.
1017(assert (equalp
1018 (instantiate-polymorphic-call
1019 (poly-function `(,(poly-function `(,(poly-var 'a))
1020 `(,(poly-var 'b)))
1021 ,(poly-function `(,(poly-var 'b))
1022 `(,(poly-var 'c))))
1023 `(,(poly-function `(,(poly-var 'a))
1024 `(,(poly-var 'c)))))
1025 `(,(mono-function `(,(mono-base 'integer `(>= v 0)))
1026 `(,(mono-base 'integer `(= ,v (+ (@- 0) 1)))))
1027 ,(mono-function `(,(mono-base 'integer))
1028 `(,(mono-base 'integer `(= ,v (- (@- 0) 1)))))))
1029 ;; Expected:
1030 ;; (x={int: v >= 0} -> {int: v = x + 1})
1031 ;; -> (y={int: v >= 1} -> {int: v = y - 1})
1032 ;; -> z={int: v >= 0} -> {int: v = z + 1 - 1}
1033 (mono-function
1034 `(,(mono-function `(,(mono-base 'integer `(>= v 0)))
1035 `(,(mono-base 'integer `(= v (+ (@- 0) 1)))))
1036 ,(mono-function `(,(mono-base 'integer `(let ((top v))
1037 (exists ((fresh:v12 integer))
1038 (and
1039 (let ((v fresh:v12))
1040 (>= v 0))
1041 (let ((v top))
1042 (= v (+ fresh:v12 1))))))))
1043 `(,(mono-base 'integer `(= v (- (@- 0) 1))))))
1044 `(,(mono-function `(,(mono-base 'integer
1045 `(>= v 0)))
1046 `(,(mono-base 'integer
1047 `(let ((top v))
1048 (exists ((fresh:v13 integer))
1049 (and
1050 (let ((v fresh:v13))
1051 (let ((top v))
1052 (exists ((fresh:v14 integer))
1053 (and
1054 (let ((v fresh:v14))
1055 (= v (@- 0)))
1056 (let ((v top))
1057 (= v (+ fresh:v14 1)))))))
1058 (let ((v top))
1059 (= v (- fresh:v13 1)))))))))))))
1060
1061;; try this for looping.
1062#+nil
1063(instantiate-polymorphic-call
1064 (poly-function `(,(poly-box (poly-base 'a)) ; reduce
1065 ,(poly-base 'b)
1066 ,(poly-function `(,(poly-base 'a) ,(poly-base 'b))
1067 `(,(poly-base 'b))))
1068 `(,(poly-base 'b)))
1069 `(,(mono-box (mono-base 'integer `(>= v 1)))
1070 ,(mono-base 'integer `(= v 0))
1071 ,(mono-function `(,(mono-base 'integer `(>= v 1))
1072 ,(mono-base 'integer `(>= v 0)))
1073 `(,(mono-base 'integer `(and (= v (+ (@- 0) (@- 1)))
1074 (> v (@- 1))
1075 (>= v (@- 0))))))))
1076#+nil
1077#s(mono-function
1078 :arguments (#s(mono-box
1079 :contents #s(mono-base :sort integer :constraint (>= v 1)))
1080 #s(mono-base :sort integer :constraint (= v 0))
1081 #s(mono-function
1082 :arguments (#s(mono-base :sort integer :constraint (>= v 1))
1083 #s(mono-base
1084 :sort integer
1085 :constraint (or (= v (@- 1 1))
1086 (let ((top v))
1087 (exists
1088 ((fresh:v10 integer))
1089 (and
1090 (let ((v fresh:v10))
1091 (>= v 1))
1092 (exists
1093 ((fresh:v11 integer))
1094 (exists
1095 ((fresh:v12 integer))
1096 (exists
1097 ((fresh:v13 integer))
1098 (and
1099 (let ((v fresh:v13))
1100 (>= v 1))
1101 (let ((v top))
1102 (and
1103 (= v
1104 (+ fresh:v10
1105 fresh:v11))
1106 (> v fresh:v12)
1107 (>= v
1108 fresh:v13)))))))))))))
1109 :results (#s(mono-base
1110 :sort integer
1111 :constraint (and (= v (+ (@- 0) (@- 1)))
1112 (> v (@- 1)) (>= v (@- 0)))))))
1113 :results (#s(mono-base
1114 :sort integer
1115 :constraint (or (= v (@- 1))
1116 (let ((top v))
1117 (exists ((fresh:v14 integer))
1118 (and
1119 (let ((v fresh:v14))
1120 (>= v 1))
1121 (exists ((fresh:v15 integer))
1122 (exists ((fresh:v16 integer))
1123 (exists ((fresh:v17 integer))
1124 (and
1125 (let ((v fresh:v17))
1126 (>= v 1))
1127 (let ((v top))
1128 (and (= v (+ fresh:v14 fresh:v15))
1129 (> v fresh:v16)
1130 (>= v fresh:v17))))))))))))))