* Improve constraint simplification logic in comp-cstr.el
* lisp/emacs-lisp/comp-cstr.el (with-comp-cstr-accessors): Simplify. (comp-cstr-empty-p): New Funchion. (comp-split-pos-neg): Minor. (comp-normalize-typeset): Logic update. (comp-union-typesets): Minor. (comp-intersect-two-typesets): New functio. (comp-intersect-typesets): Logic update. (comp-range-union, comp-range-intersection): Minor. (comp-cstr-union-homogeneous, comp-cstr-union-1-no-mem) (comp-cstr-intersection-homogeneous) (comp-cstr-intersection-no-mem, comp-cstr-negation) (comp-type-spec-to-cstr, comp-cstr-to-type-spec): Logic update. * lisp/emacs-lisp/comp-cstr.el (with-comp-cstr-accessors): Simplify.
This commit is contained in:
Andrea Corallo
parent
a0c0daf7a1
commit
48d43f579e
1 changed files with 130 additions and 112 deletions
|
|
@ -100,14 +100,14 @@ Integer values are handled in the `range' slot.")
|
||||||
"Define some quick accessor to reduce code vergosity in BODY."
|
"Define some quick accessor to reduce code vergosity in BODY."
|
||||||
(declare (debug (form body))
|
(declare (debug (form body))
|
||||||
(indent defun))
|
(indent defun))
|
||||||
`(cl-macrolet ((typeset (&rest x)
|
`(cl-macrolet ((typeset (x)
|
||||||
`(comp-cstr-typeset ,@x))
|
`(comp-cstr-typeset ,x))
|
||||||
(valset (&rest x)
|
(valset (x)
|
||||||
`(comp-cstr-valset ,@x))
|
`(comp-cstr-valset ,x))
|
||||||
(range (&rest x)
|
(range (x)
|
||||||
`(comp-cstr-range ,@x))
|
`(comp-cstr-range ,x))
|
||||||
(neg (&rest x)
|
(neg (x)
|
||||||
`(comp-cstr-neg ,@x)))
|
`(comp-cstr-neg ,x)))
|
||||||
,@body))
|
,@body))
|
||||||
|
|
||||||
(defun comp-cstr-copy (cstr)
|
(defun comp-cstr-copy (cstr)
|
||||||
|
|
@ -118,6 +118,13 @@ Integer values are handled in the `range' slot.")
|
||||||
:range (copy-tree (range cstr))
|
:range (copy-tree (range cstr))
|
||||||
:neg (copy-tree (neg cstr)))))
|
:neg (copy-tree (neg cstr)))))
|
||||||
|
|
||||||
|
(defsubst comp-cstr-empty-p (cstr)
|
||||||
|
"Return t if CSTR is equivalent to the `nil' type specifier or nil otherwise."
|
||||||
|
(with-comp-cstr-accessors
|
||||||
|
(and (null (typeset cstr))
|
||||||
|
(null (valset cstr))
|
||||||
|
(null (range cstr)))))
|
||||||
|
|
||||||
(defun comp-cstrs-homogeneous (cstrs)
|
(defun comp-cstrs-homogeneous (cstrs)
|
||||||
"Check if constraints CSTRS are all homogeneously negated or non-negated.
|
"Check if constraints CSTRS are all homogeneously negated or non-negated.
|
||||||
Return `pos' if they are all positive, `neg' if they are all
|
Return `pos' if they are all positive, `neg' if they are all
|
||||||
|
|
@ -142,7 +149,7 @@ Return them as multiple value."
|
||||||
collect cstr into negatives
|
collect cstr into negatives
|
||||||
else
|
else
|
||||||
collect cstr into positives
|
collect cstr into positives
|
||||||
finally (cl-return (cl-values positives negatives))))
|
finally return (cl-values positives negatives)))
|
||||||
|
|
||||||
|
|
||||||
;;; Value handling.
|
;;; Value handling.
|
||||||
|
|
@ -168,7 +175,8 @@ Return them as multiple value."
|
||||||
|
|
||||||
(defun comp-normalize-typeset (typeset)
|
(defun comp-normalize-typeset (typeset)
|
||||||
"Sort TYPESET and return it."
|
"Sort TYPESET and return it."
|
||||||
(cl-sort typeset (lambda (x y)
|
(cl-sort (cl-remove-duplicates typeset)
|
||||||
|
(lambda (x y)
|
||||||
(string-lessp (symbol-name x)
|
(string-lessp (symbol-name x)
|
||||||
(symbol-name y)))))
|
(symbol-name y)))))
|
||||||
|
|
||||||
|
|
@ -224,22 +232,30 @@ Return them as multiple value."
|
||||||
do (setf last x)
|
do (setf last x)
|
||||||
finally (when last
|
finally (when last
|
||||||
(push last res)))
|
(push last res)))
|
||||||
finally (cl-return (comp-normalize-typeset
|
finally return (comp-normalize-typeset res))
|
||||||
(cl-remove-duplicates res))))
|
|
||||||
(comp-cstr-ctxt-union-typesets-mem comp-ctxt))))
|
(comp-cstr-ctxt-union-typesets-mem comp-ctxt))))
|
||||||
|
|
||||||
|
(defun comp-intersect-two-typesets (t1 t2)
|
||||||
|
"Intersect typesets T1 and T2."
|
||||||
|
(with-comp-cstr-accessors
|
||||||
|
(cl-loop
|
||||||
|
for types in (list t1 t2)
|
||||||
|
for other-types in (list t2 t1)
|
||||||
|
append
|
||||||
|
(cl-loop
|
||||||
|
for type in types
|
||||||
|
when (cl-some (lambda (x)
|
||||||
|
(comp-subtype-p type x))
|
||||||
|
other-types)
|
||||||
|
collect type))))
|
||||||
|
|
||||||
(defun comp-intersect-typesets (&rest typesets)
|
(defun comp-intersect-typesets (&rest typesets)
|
||||||
"Intersect types present into TYPESETS."
|
"Intersect types present into TYPESETS."
|
||||||
(when-let ((ty (apply #'append typesets)))
|
(unless (cl-some #'null typesets)
|
||||||
(if (> (length ty) 1)
|
(if (= (length typesets) 1)
|
||||||
(cl-reduce
|
(car typesets)
|
||||||
(lambda (x y)
|
(comp-normalize-typeset
|
||||||
(let ((st (comp-common-supertype-2 x y)))
|
(cl-reduce #'comp-intersect-two-typesets typesets)))))
|
||||||
(cond
|
|
||||||
((eq st x) (list y))
|
|
||||||
((eq st y) (list x)))))
|
|
||||||
ty)
|
|
||||||
(comp-normalize-typeset ty))))
|
|
||||||
|
|
||||||
|
|
||||||
;;; Integer range handling
|
;;; Integer range handling
|
||||||
|
|
@ -289,7 +305,7 @@ Return them as multiple value."
|
||||||
(when (= nest 1)
|
(when (= nest 1)
|
||||||
(push `(,(comp-range-1+ low) . ,i) res))
|
(push `(,(comp-range-1+ low) . ,i) res))
|
||||||
(cl-decf nest)
|
(cl-decf nest)
|
||||||
finally (cl-return (reverse res))))
|
finally return (reverse res)))
|
||||||
|
|
||||||
(defun comp-range-intersection (&rest ranges)
|
(defun comp-range-intersection (&rest ranges)
|
||||||
"Combine integer intervals RANGES by intersecting."
|
"Combine integer intervals RANGES by intersecting."
|
||||||
|
|
@ -321,7 +337,7 @@ Return them as multiple value."
|
||||||
(push `(,low . ,i)
|
(push `(,low . ,i)
|
||||||
res))
|
res))
|
||||||
(cl-decf nest)
|
(cl-decf nest)
|
||||||
finally (cl-return (reverse res))))
|
finally return (reverse res)))
|
||||||
|
|
||||||
(defun comp-range-negation (range)
|
(defun comp-range-negation (range)
|
||||||
"Negate range RANGE."
|
"Negate range RANGE."
|
||||||
|
|
@ -373,7 +389,11 @@ All SRCS constraints must be homogeneously negated or non-negated.
|
||||||
DST is returned."
|
DST is returned."
|
||||||
(apply #'comp-cstr-union-homogeneous-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-neg dst)
|
||||||
|
(when srcs
|
||||||
|
(comp-cstr-neg (car srcs)))
|
||||||
|
|
||||||
|
(comp-cstr-range dst)
|
||||||
(when (cl-notany (lambda (x)
|
(when (cl-notany (lambda (x)
|
||||||
(comp-subtype-p 'integer x))
|
(comp-subtype-p 'integer x))
|
||||||
(comp-cstr-typeset dst))
|
(comp-cstr-typeset dst))
|
||||||
|
|
@ -399,25 +419,26 @@ DST is returned."
|
||||||
;; or negated so we don't have to cons.
|
;; or negated so we don't have to cons.
|
||||||
(when-let ((res (comp-cstrs-homogeneous srcs)))
|
(when-let ((res (comp-cstrs-homogeneous srcs)))
|
||||||
(apply #'comp-cstr-union-homogeneous dst srcs)
|
(apply #'comp-cstr-union-homogeneous dst srcs)
|
||||||
(setf (neg dst) (eq res 'neg))
|
|
||||||
(cl-return-from comp-cstr-union-1-no-mem dst))
|
(cl-return-from comp-cstr-union-1-no-mem dst))
|
||||||
|
|
||||||
;; Some are negated and some are not
|
;; Some are negated and some are not
|
||||||
(cl-multiple-value-bind (positives negatives) (comp-split-pos-neg srcs)
|
(cl-multiple-value-bind (positives negatives) (comp-split-pos-neg srcs)
|
||||||
(let* ((pos (apply #'comp-cstr-union-homogeneous
|
(let* ((pos (apply #'comp-cstr-union-homogeneous
|
||||||
(make-comp-cstr) positives))
|
(make-comp-cstr) positives))
|
||||||
;; We use neg as result as *most* of times this will be
|
;; We'll always use neg as result as this is almost
|
||||||
;; negated.
|
;; always necessary for describing open intervals
|
||||||
|
;; resulting from negated constraints.
|
||||||
(neg (apply #'comp-cstr-union-homogeneous
|
(neg (apply #'comp-cstr-union-homogeneous
|
||||||
(make-comp-cstr :neg t) negatives)))
|
(make-comp-cstr :neg t) negatives)))
|
||||||
;; Type propagation.
|
;; Type propagation.
|
||||||
(when (and (typeset pos)
|
(when (and (typeset pos)
|
||||||
;; When every pos type is not a subtype of some neg ones.
|
;; When every pos type is a subtype of some neg ones.
|
||||||
(cl-every (lambda (x)
|
(cl-every (lambda (x)
|
||||||
(cl-some (lambda (y)
|
(cl-some (lambda (y)
|
||||||
(not (and (not (eq x y))
|
(comp-subtype-p x y))
|
||||||
(comp-subtype-p x y))))
|
(append (typeset neg)
|
||||||
(typeset neg)))
|
(when (range neg)
|
||||||
|
'(integer)))))
|
||||||
(typeset pos)))
|
(typeset pos)))
|
||||||
;; This is a conservative choice, ATM we can't represent such
|
;; This is a conservative choice, ATM we can't represent such
|
||||||
;; a disjoint set of types unless we decide to add a new slot
|
;; a disjoint set of types unless we decide to add a new slot
|
||||||
|
|
@ -452,30 +473,14 @@ DST is returned."
|
||||||
(cl-nset-difference (valset neg) (valset pos)))))
|
(cl-nset-difference (valset neg) (valset pos)))))
|
||||||
|
|
||||||
;; Range propagation
|
;; Range propagation
|
||||||
(if (and range
|
|
||||||
(or (range pos)
|
|
||||||
(range neg)))
|
|
||||||
(if (or (valset neg) (typeset neg))
|
|
||||||
(setf (range neg)
|
(setf (range neg)
|
||||||
(if (memq 'integer (typeset neg))
|
(when range
|
||||||
(comp-range-negation (range pos))
|
|
||||||
(comp-range-negation
|
(comp-range-negation
|
||||||
(comp-range-union (range pos)
|
|
||||||
(comp-range-negation (range neg))))))
|
|
||||||
;; When possibile do not return a negated cstr.
|
|
||||||
(setf (typeset dst) (typeset pos)
|
|
||||||
(valset dst) (valset pos)
|
|
||||||
(range dst) (unless (memq 'integer (typeset dst))
|
|
||||||
(comp-range-union
|
(comp-range-union
|
||||||
(comp-range-negation (range neg))
|
(comp-range-negation (range neg))
|
||||||
(range pos)))
|
(range pos)))))
|
||||||
(neg dst) nil)
|
|
||||||
(cl-return-from comp-cstr-union-1-no-mem dst))
|
|
||||||
(setf (range neg) ()))
|
|
||||||
|
|
||||||
(if (and (null (typeset neg))
|
(if (comp-cstr-empty-p neg)
|
||||||
(null (valset neg))
|
|
||||||
(null (range neg)))
|
|
||||||
(setf (typeset dst) (typeset pos)
|
(setf (typeset dst) (typeset pos)
|
||||||
(valset dst) (valset pos)
|
(valset dst) (valset pos)
|
||||||
(range dst) (range pos)
|
(range dst) (range pos)
|
||||||
|
|
@ -510,49 +515,57 @@ DST is returned."
|
||||||
All SRCS constraints must be homogeneously negated or non-negated.
|
All SRCS constraints must be homogeneously negated or non-negated.
|
||||||
DST is returned."
|
DST is returned."
|
||||||
|
|
||||||
;; Value propagation.
|
(with-comp-cstr-accessors
|
||||||
(setf (comp-cstr-valset dst)
|
(when (cl-some #'comp-cstr-empty-p srcs)
|
||||||
;; TODO sort.
|
(setf (valset dst) nil
|
||||||
(let ((values (cl-loop for src in srcs
|
(range dst) nil
|
||||||
for v = (comp-cstr-valset src)
|
(typeset dst) nil)
|
||||||
when v
|
|
||||||
collect v)))
|
|
||||||
(when values
|
|
||||||
(cl-reduce (lambda (x y)
|
|
||||||
(cl-intersection x y :test #'equal))
|
|
||||||
values))))
|
|
||||||
|
|
||||||
;; Range propagation.
|
|
||||||
(when (cl-some #'identity (mapcar #'comp-cstr-range srcs))
|
|
||||||
(if (comp-cstr-valset dst)
|
|
||||||
(progn
|
|
||||||
(setf (comp-cstr-valset dst) nil
|
|
||||||
(comp-cstr-range dst) nil
|
|
||||||
(comp-cstr-typeset dst) nil)
|
|
||||||
(cl-return-from comp-cstr-intersection-homogeneous dst))
|
(cl-return-from comp-cstr-intersection-homogeneous dst))
|
||||||
;; TODO memoize?
|
|
||||||
(setf (comp-cstr-range dst)
|
(setf (neg dst) (when srcs
|
||||||
(apply #'comp-range-intersection
|
(neg (car srcs))))
|
||||||
(mapcar #'comp-cstr-range srcs)))))
|
|
||||||
|
|
||||||
;; Type propagation.
|
;; Type propagation.
|
||||||
(setf (comp-cstr-typeset dst)
|
(setf (typeset dst)
|
||||||
(if (or (comp-cstr-range dst) (comp-cstr-valset dst))
|
|
||||||
(cl-loop
|
|
||||||
with type-val = (cl-remove-duplicates
|
|
||||||
(append (mapcar #'type-of
|
|
||||||
(comp-cstr-valset dst))
|
|
||||||
(when (comp-cstr-range dst)
|
|
||||||
'(integer))))
|
|
||||||
for type in (apply #'comp-intersect-typesets
|
|
||||||
(mapcar #'comp-cstr-typeset srcs))
|
|
||||||
when (and type (not (member type type-val)))
|
|
||||||
do (setf (comp-cstr-valset dst) nil
|
|
||||||
(comp-cstr-range dst) nil)
|
|
||||||
(cl-return nil))
|
|
||||||
(apply #'comp-intersect-typesets
|
(apply #'comp-intersect-typesets
|
||||||
(mapcar #'comp-cstr-typeset srcs))))
|
(mapcar #'comp-cstr-typeset srcs)))
|
||||||
dst)
|
|
||||||
|
;; Value propagation.
|
||||||
|
(setf (valset dst)
|
||||||
|
(comp-normalize-valset
|
||||||
|
(cl-loop
|
||||||
|
for src in srcs
|
||||||
|
append
|
||||||
|
(cl-loop
|
||||||
|
for val in (valset src)
|
||||||
|
;; If (member value) is subtypep of all other sources then
|
||||||
|
;; is good to be colleted.
|
||||||
|
when (cl-every (lambda (s)
|
||||||
|
(or (memq val (valset s))
|
||||||
|
(cl-some (lambda (type)
|
||||||
|
(cl-typep val type))
|
||||||
|
(typeset s))))
|
||||||
|
(remq src srcs))
|
||||||
|
collect val))))
|
||||||
|
|
||||||
|
;; Range propagation.
|
||||||
|
(setf (range dst)
|
||||||
|
;; Do range propagation only if the destination typeset
|
||||||
|
;; doesn't cover it already.
|
||||||
|
(unless (cl-some (lambda (type)
|
||||||
|
(comp-subtype-p 'integer type))
|
||||||
|
(typeset dst))
|
||||||
|
(apply #'comp-range-intersection
|
||||||
|
(cl-loop
|
||||||
|
for src in srcs
|
||||||
|
;; Collect effective ranges.
|
||||||
|
collect (or (range src)
|
||||||
|
(when (cl-some (lambda (s)
|
||||||
|
(comp-subtype-p 'integer s))
|
||||||
|
(typeset src))
|
||||||
|
'((- . +))))))))
|
||||||
|
|
||||||
|
dst))
|
||||||
|
|
||||||
(cl-defun comp-cstr-intersection-no-mem (dst &rest srcs)
|
(cl-defun comp-cstr-intersection-no-mem (dst &rest srcs)
|
||||||
"Combine SRCS by intersection set operation setting the result in DST.
|
"Combine SRCS by intersection set operation setting the result in DST.
|
||||||
|
|
@ -566,8 +579,9 @@ DST is returned."
|
||||||
(neg dst) nil)
|
(neg dst) nil)
|
||||||
(cl-return-from comp-cstr-intersection-no-mem dst)))
|
(cl-return-from comp-cstr-intersection-no-mem dst)))
|
||||||
(when-let ((res (comp-cstrs-homogeneous srcs)))
|
(when-let ((res (comp-cstrs-homogeneous srcs)))
|
||||||
(apply #'comp-cstr-intersection-homogeneous dst srcs)
|
(if (eq res 'neg)
|
||||||
(setf (neg dst) (eq res 'neg))
|
(apply #'comp-cstr-union-homogeneous dst srcs)
|
||||||
|
(apply #'comp-cstr-intersection-homogeneous dst srcs))
|
||||||
(cl-return-from comp-cstr-intersection-no-mem dst))
|
(cl-return-from comp-cstr-intersection-no-mem dst))
|
||||||
|
|
||||||
;; Some are negated and some are not
|
;; Some are negated and some are not
|
||||||
|
|
@ -575,7 +589,7 @@ DST is returned."
|
||||||
(let* ((pos (apply #'comp-cstr-intersection-homogeneous
|
(let* ((pos (apply #'comp-cstr-intersection-homogeneous
|
||||||
(make-comp-cstr) positives))
|
(make-comp-cstr) positives))
|
||||||
(neg (apply #'comp-cstr-intersection-homogeneous
|
(neg (apply #'comp-cstr-intersection-homogeneous
|
||||||
(make-comp-cstr :neg t) negatives)))
|
(make-comp-cstr) negatives)))
|
||||||
|
|
||||||
;; In case pos is not relevant return directly the content
|
;; In case pos is not relevant return directly the content
|
||||||
;; of neg.
|
;; of neg.
|
||||||
|
|
@ -613,12 +627,8 @@ DST is returned."
|
||||||
do (setf found t))))
|
do (setf found t))))
|
||||||
|
|
||||||
(setf (range pos)
|
(setf (range pos)
|
||||||
(if (memq 'integer (typeset pos))
|
|
||||||
(progn
|
|
||||||
(setf (typeset pos) (delq 'integer (typeset pos)))
|
|
||||||
(comp-range-negation (range neg)))
|
|
||||||
(comp-range-intersection (range pos)
|
(comp-range-intersection (range pos)
|
||||||
(comp-range-negation (range neg)))))
|
(comp-range-negation (range neg))))
|
||||||
|
|
||||||
;; Return a non negated form.
|
;; Return a non negated form.
|
||||||
(setf (typeset dst) (typeset pos)
|
(setf (typeset dst) (typeset pos)
|
||||||
|
|
@ -668,11 +678,12 @@ DST is returned."
|
||||||
(defun comp-cstr-negation (dst src)
|
(defun comp-cstr-negation (dst src)
|
||||||
"Negate SRC setting the result in DST.
|
"Negate SRC setting the result in DST.
|
||||||
DST is returned."
|
DST is returned."
|
||||||
(setf (comp-cstr-typeset dst) (comp-cstr-typeset src)
|
(with-comp-cstr-accessors
|
||||||
(comp-cstr-valset dst) (comp-cstr-valset src)
|
(setf (typeset dst) (typeset src)
|
||||||
(comp-cstr-range dst) (comp-cstr-range src)
|
(valset dst) (valset src)
|
||||||
(comp-cstr-neg dst) (not (comp-cstr-neg src)))
|
(range dst) (range src)
|
||||||
dst)
|
(neg dst) (not (neg src)))
|
||||||
|
dst))
|
||||||
|
|
||||||
(defun comp-cstr-negation-make (src)
|
(defun comp-cstr-negation-make (src)
|
||||||
"Negate SRC and return a new constraint."
|
"Negate SRC and return a new constraint."
|
||||||
|
|
@ -686,10 +697,14 @@ FN non-nil indicates we are parsing a function lambda list."
|
||||||
(if fn
|
(if fn
|
||||||
x
|
x
|
||||||
(error "Invalid `%s` in type specifier" x)))
|
(error "Invalid `%s` in type specifier" x)))
|
||||||
|
('nil
|
||||||
|
(make-comp-cstr :typeset ()))
|
||||||
('fixnum
|
('fixnum
|
||||||
(comp-irange-to-cstr `(,most-negative-fixnum . ,most-positive-fixnum)))
|
(comp-irange-to-cstr `(,most-negative-fixnum . ,most-positive-fixnum)))
|
||||||
('boolean
|
('boolean
|
||||||
(comp-type-spec-to-cstr '(member t nil)))
|
(comp-type-spec-to-cstr '(member t nil)))
|
||||||
|
('integer
|
||||||
|
(comp-irange-to-cstr '(- . +)))
|
||||||
('null (comp-value-to-cstr nil))
|
('null (comp-value-to-cstr nil))
|
||||||
((pred atom)
|
((pred atom)
|
||||||
(comp-type-to-cstr type-spec))
|
(comp-type-to-cstr type-spec))
|
||||||
|
|
@ -742,6 +757,9 @@ FN non-nil indicates we are parsing a function lambda list."
|
||||||
(setf range (cl-loop for (l . h) in range
|
(setf range (cl-loop for (l . h) in range
|
||||||
for low = (if (integerp l) l '*)
|
for low = (if (integerp l) l '*)
|
||||||
for high = (if (integerp h) h '*)
|
for high = (if (integerp h) h '*)
|
||||||
|
if (and (eq low '*) (eq high '*))
|
||||||
|
collect 'integer
|
||||||
|
else
|
||||||
collect `(integer ,low , high))
|
collect `(integer ,low , high))
|
||||||
valset (cl-remove-duplicates valset))
|
valset (cl-remove-duplicates valset))
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue