]> git.eshelyaron.com Git - emacs.git/commitdiff
Initial support for union of negated constraints
authorAndrea Corallo <akrl@sdf.org>
Wed, 2 Dec 2020 21:47:00 +0000 (22:47 +0100)
committerAndrea Corallo <akrl@sdf.org>
Sat, 5 Dec 2020 18:01:03 +0000 (19:01 +0100)
* 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.

lisp/emacs-lisp/comp-cstr.el
test/lisp/emacs-lisp/comp-cstr-tests.el

index 6397bccdae59c8937c69c6f3cff8baf531570492..a18099670758bb655e74663ec1b1c739640b7ebf 100644 (file)
@@ -239,23 +239,26 @@ Integer values are handled in the `range' slot.")
 
 (defun comp-range-negation (range)
   "Negate range RANGE."
-  (cl-loop
-   with res = ()
-   with last-h = '-
-   for (l . h) in range
-   unless (eq l '-)
+  (if (null range)
+      '((- . +))
+    (cl-loop
+     with res = ()
+     with last-h = '-
+     for (l . h) in range
+     unless (eq l '-)
      do (push `(,(comp-range-1+ last-h) . ,(1- l)) res)
-   do (setf last-h h)
-   finally
-   (unless (eq '+ last-h)
-     (push `(,(1+ last-h) . +) res))
-   (cl-return (reverse res))))
+     do (setf last-h h)
+     finally
+     (unless (eq '+ last-h)
+       (push `(,(1+ last-h) . +) res))
+     (cl-return (reverse res)))))
 
 \f
-;;; Entry points.
+;;; Union specific code.
 
-(defun comp-cstr-union-no-range (dst &rest srcs)
-  "As `comp-cstr-union' but escluding the irange component."
+(defun comp-cstr-union-homogeneous-no-range (dst &rest srcs)
+  "As `comp-cstr-union' but escluding the irange component.
+All SRCS constraints must be homogeneously negated or non-negated."
 
   ;; Type propagation.
   (setf (comp-cstr-typeset dst)
@@ -277,10 +280,11 @@ Integer values are handled in the `range' slot.")
 
   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.
+All SRCS constraints must be homogeneously negated or non-negated.
 DST is returned."
-  (apply #'comp-cstr-union-no-range dst srcs)
+  (apply #'comp-cstr-union-homogeneous-no-range dst srcs)
   ;; Range propagation.
   (setf (comp-cstr-range dst)
         (when (cl-notany (lambda (x)
@@ -291,6 +295,105 @@ DST is returned."
                  (mapcar #'comp-cstr-range srcs))))
   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)
+
+\f
+;;; 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)
   "Combine SRCS by union set operation and return a new constraint."
   (apply #'comp-cstr-union (make-comp-cstr) srcs))
index 541533601b10b93b6f52c9a8c94c33a1b645761c..5c119c6ba3e0f42d183bf2dc4e40a5332b1da39a 100644 (file)
     ((and (integer -1 3) (integer 3 5)) . (integer 3 3))
     ((and (integer -1 4) (integer 3 5)) . (integer 3 4))
     ((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.")
 
 (defmacro comp-cstr-synthesize-tests ()