1
Fork 0
mirror of git://git.sv.gnu.org/emacs.git synced 2025-12-15 18:40:39 -08:00

Initial support for union of negated constraints

* lisp/emacs-lisp/comp-cstr.el (comp-range-negation): New
	function.
	(comp-cstr-union-homogeneous-no-range): Rename from
	`comp-cstr-union-no-range'.
	(comp-cstr-union-homogeneous): Rename from `comp-cstr-union'.
	(comp-cstr-union-1): New function.
	(comp-cstr-union-no-range, comp-cstr-union): Rewrite in function
	of `comp-cstr-union-1'.
	* test/lisp/emacs-lisp/comp-cstr-tests.el
	(comp-cstr-typespec-tests-alist): Add a bunch of tests.
This commit is contained in:
Andrea Corallo 2020-12-02 22:47:00 +01:00
parent 1fb249f6db
commit 7c1d90a41d
2 changed files with 126 additions and 16 deletions

View file

@ -239,23 +239,26 @@ Integer values are handled in the `range' slot.")
(defun comp-range-negation (range) (defun comp-range-negation (range)
"Negate range RANGE." "Negate range RANGE."
(cl-loop (if (null range)
with res = () '((- . +))
with last-h = '- (cl-loop
for (l . h) in range with res = ()
unless (eq l '-) with last-h = '-
for (l . h) in range
unless (eq l '-)
do (push `(,(comp-range-1+ last-h) . ,(1- l)) res) do (push `(,(comp-range-1+ last-h) . ,(1- l)) res)
do (setf last-h h) do (setf last-h h)
finally finally
(unless (eq '+ last-h) (unless (eq '+ last-h)
(push `(,(1+ last-h) . +) res)) (push `(,(1+ last-h) . +) res))
(cl-return (reverse res)))) (cl-return (reverse res)))))
;;; Entry points. ;;; Union specific code.
(defun comp-cstr-union-no-range (dst &rest srcs) (defun comp-cstr-union-homogeneous-no-range (dst &rest srcs)
"As `comp-cstr-union' but escluding the irange component." "As `comp-cstr-union' but escluding the irange component.
All SRCS constraints must be homogeneously negated or non-negated."
;; Type propagation. ;; Type propagation.
(setf (comp-cstr-typeset dst) (setf (comp-cstr-typeset dst)
@ -277,10 +280,11 @@ Integer values are handled in the `range' slot.")
dst) dst)
(defun comp-cstr-union (dst &rest srcs) (defun comp-cstr-union-homogeneous (dst &rest srcs)
"Combine SRCS by union set operation setting the result in DST. "Combine SRCS by union set operation setting the result in DST.
All SRCS constraints must be homogeneously negated or non-negated.
DST is returned." DST is returned."
(apply #'comp-cstr-union-no-range dst srcs) (apply #'comp-cstr-union-homogeneous-no-range dst srcs)
;; Range propagation. ;; Range propagation.
(setf (comp-cstr-range dst) (setf (comp-cstr-range dst)
(when (cl-notany (lambda (x) (when (cl-notany (lambda (x)
@ -291,6 +295,105 @@ DST is returned."
(mapcar #'comp-cstr-range srcs)))) (mapcar #'comp-cstr-range srcs))))
dst) dst)
(cl-defun comp-cstr-union-1 (range dst &rest srcs)
"Combine SRCS by union set operation setting the result in DST.
Do range propagation when RANGE is non-nil.
DST is returned."
;; Check first if we are in the simple case of all input non-negate
;; or negated so we don't have to cons.
(cl-loop
for cstr in srcs
unless (comp-cstr-neg cstr)
count t into n-pos
else
count t into n-neg
finally
(when (or (zerop n-pos) (zerop n-neg))
(apply #'comp-cstr-union-homogeneous dst srcs)
(cl-return-from comp-cstr-union-1 dst)))
;; Some are negated and some are not
(cl-loop
for cstr in srcs
if (comp-cstr-neg cstr)
collect cstr into negatives
else
collect cstr into positives
finally
(let* ((pos (apply #'comp-cstr-union-homogeneous (make-comp-cstr) positives))
(neg (apply #'comp-cstr-union-homogeneous (make-comp-cstr) negatives)))
;; Type propagation.
(when (and (comp-cstr-typeset pos)
;; When some pos type is not a subtype of any neg ones.
(cl-every (lambda (x)
(cl-some (lambda (y)
(not (comp-subtype-p x y)))
(comp-cstr-typeset neg)))
(comp-cstr-typeset pos)))
;; This is a conservative choice, ATM we can't represent such a
;; disjoint set of types unless we decide to add a new slot
;; into `comp-cstr' list them all. This probably wouldn't
;; work for the future when we'll support also non-builtin
;; types.
(setf (comp-cstr-typeset dst) '(t)
(comp-cstr-valset dst) ()
(comp-cstr-range dst) ()
(comp-cstr-neg dst) nil)
(cl-return-from comp-cstr-union-1 dst))
;; Value propagation.
(setf (comp-cstr-valset neg)
(cl-nset-difference (comp-cstr-valset neg) (comp-cstr-valset pos)))
;; Range propagation
(when (and range
(or (comp-cstr-range pos)
(comp-cstr-range neg))
(cl-notany (lambda (x)
(comp-subtype-p 'integer x))
(comp-cstr-typeset pos)))
(if (or (comp-cstr-valset neg)
(comp-cstr-typeset neg))
(setf (comp-cstr-range neg)
(comp-range-union (comp-range-negation (comp-cstr-range pos))
(comp-cstr-range neg)))
;; When possibile do not return a negated cstr.
(setf (comp-cstr-typeset dst) ()
(comp-cstr-valset dst) ()
(comp-cstr-range dst) (comp-range-union
(comp-range-negation (comp-cstr-range neg))
(comp-cstr-range pos))
(comp-cstr-neg dst) nil)
(cl-return-from comp-cstr-union-1 dst)))
(if (and (null (comp-cstr-typeset neg))
(null (comp-cstr-valset neg))
(null (comp-cstr-range neg)))
(setf (comp-cstr-typeset dst) '(t)
(comp-cstr-valset dst) ()
(comp-cstr-range dst) ()
(comp-cstr-neg dst) nil)
(setf (comp-cstr-typeset dst) (comp-cstr-typeset neg)
(comp-cstr-valset dst) (comp-cstr-valset neg)
(comp-cstr-range dst) (comp-cstr-range neg)
(comp-cstr-neg dst) t))))
dst)
;;; Entry points.
(defun comp-cstr-union-no-range (dst &rest srcs)
"Combine SRCS by union set operation setting the result in DST.
Do not propagate the range component.
DST is returned."
(apply #'comp-cstr-union-1 nil dst srcs))
(defun comp-cstr-union (dst &rest srcs)
"Combine SRCS by union set operation setting the result in DST.
DST is returned."
(apply #'comp-cstr-union-1 t dst srcs))
(defun comp-cstr-union-make (&rest srcs) (defun comp-cstr-union-make (&rest srcs)
"Combine SRCS by union set operation and return a new constraint." "Combine SRCS by union set operation and return a new constraint."
(apply #'comp-cstr-union (make-comp-cstr) srcs)) (apply #'comp-cstr-union (make-comp-cstr) srcs))

View file

@ -78,7 +78,14 @@
((and (integer -1 3) (integer 3 5)) . (integer 3 3)) ((and (integer -1 3) (integer 3 5)) . (integer 3 3))
((and (integer -1 4) (integer 3 5)) . (integer 3 4)) ((and (integer -1 4) (integer 3 5)) . (integer 3 4))
((and (integer -1 5) nil) . nil) ((and (integer -1 5) nil) . nil)
((not symbol) . (not symbol))) ((not symbol) . (not symbol))
((or (member foo) (not (member foo bar))) . (not (member bar)))
((or (member foo bar) (not (member foo))) . t)
;; Intentionally conservative, see `comp-cstr-union'.
((or symbol (not sequence)) . t)
((or vector (not sequence)) . (not sequence))
((or (integer 1 10) (not (integer * 5))) . (integer 1 *))
((or symbol (integer 1 10) (not (integer * 5))) . (integer 1 *)))
"Alist type specifier -> expected type specifier.") "Alist type specifier -> expected type specifier.")
(defmacro comp-cstr-synthesize-tests () (defmacro comp-cstr-synthesize-tests ()