;;; comp-cstr.el --- native compiler constraint library -*- lexical-binding: t -*-

;; Copyright (C) 2020-2023 Free Software Foundation, Inc.

;; Author: Andrea Corallo <acorallo@gnu.org>
;; Keywords: lisp
;; Package: emacs

;; This file is part of GNU Emacs.

;; GNU Emacs is free software: you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.

;; GNU Emacs is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs.  If not, see <https://www.gnu.org/licenses/>.

;;; Commentary:

;; Constraint library in use by the native compiler.

;; In LIMPLE each non immediate value is represented by a `comp-mvar'.
;; The part concerning the set of all values the `comp-mvar' can
;; assume is described into its constraint `comp-cstr'.  Each
;; constraint consists in a triplet: type-set, value-set, range-set.
;; This file provide set operations between constraints (union
;; intersection and negation) plus routines to convert from and to a
;; CL like type specifier.

;;; Code:

(require 'cl-lib)
(require 'cl-macs)

(defconst comp--typeof-builtin-types (mapcar (lambda (x)
                                               (append x '(t)))
                                             cl--typeof-types)
  ;; TODO can we just add t in `cl--typeof-types'?
  "Like `cl--typeof-types' but with t as common supertype.")

(cl-defstruct (comp-cstr (:constructor comp-type-to-cstr
                                       (type &aux
					     (null (eq type 'null))
                                             (integer (eq type 'integer))
					     (typeset (if (or null integer)
							  nil
							(list type)))
					     (valset (when null
						       '(nil)))
                                             (range (when integer
                                                      '((- . +))))))
                         (:constructor comp-value-to-cstr
                                       (value &aux
                                              (integer (integerp value))
                                              (valset (unless integer
                                                        (list value)))
                                              (range (when integer
                                                       `((,value . ,value))))
                                              (typeset ())))
                         (:constructor comp-irange-to-cstr
                                       (irange &aux
                                               (range (list irange))
                                               (typeset ())))
                         (:copier nil))
  "Internal representation of a type/value constraint."
  (typeset '(t) :type list
           :documentation "List of possible types the mvar can assume.
Each element cannot be a subtype of any other element of this slot.")
  (valset () :type list
          :documentation "List of possible values the mvar can assume.
Integer values are handled in the `range' slot.")
  (range () :type list
         :documentation "Integer interval.")
  (neg nil :type boolean
       :documentation "Non-nil if the constraint is negated"))

(cl-defstruct comp-cstr-f
  "Internal constraint representation for a function."
  (args () :type list
        :documentation "List of `comp-cstr' for its arguments.")
  (ret nil :type (or comp-cstr comp-cstr-f)
       :documentation "Returned value."))

(defun comp--cl-class-hierarchy (x)
  "Given a class name `x' return its hierarchy."
  `(,@(cl--class-allparents (cl--struct-get-class x))
    ;; FIXME: AFAICT, `comp--all-classes' will also find those struct types
    ;; which use :type and can thus be either `vector' or `cons' (the latter
    ;; isn't `atom').
    atom
    t))

(defun comp--all-classes ()
  "Return all non built-in type names currently defined."
  (let (res)
    (mapatoms (lambda (x)
                (when (cl-find-class x)
                  (push x res)))
              obarray)
    res))

(defun comp--compute-typeof-types ()
  (append comp--typeof-builtin-types
          (mapcar #'comp--cl-class-hierarchy (comp--all-classes))))

(defun comp--compute--pred-type-h ()
  (cl-loop with h = (make-hash-table :test #'eq)
	   for class-name in (comp--all-classes)
           for pred = (get class-name 'cl-deftype-satisfies)
           when pred
             do (puthash pred class-name h)
	   finally return h))

(cl-defstruct comp-cstr-ctxt
  (typeof-types (comp--compute-typeof-types)
                :type list
                :documentation "Type hierarchy.")
  (pred-type-h (comp--compute--pred-type-h)
               :type hash-table
               :documentation "Hash pred -> type.")
  (union-typesets-mem (make-hash-table :test #'equal) :type hash-table
                      :documentation "Serve memoization for
`comp-union-typesets'.")
  ;; TODO we should be able to just cons hash this.
  (common-supertype-mem (make-hash-table :test #'equal) :type hash-table
                        :documentation "Serve memoization for
`comp-common-supertype'.")
  (subtype-p-mem (make-hash-table :test #'equal) :type hash-table
                 :documentation "Serve memoization for
`comp-cstr-ctxt-subtype-p-mem'.")
  (union-1-mem-no-range (make-hash-table :test #'equal) :type hash-table
                        :documentation "Serve memoization for
`comp-cstr-union-1'.")
  (union-1-mem-range (make-hash-table :test #'equal) :type hash-table
                     :documentation "Serve memoization for
`comp-cstr-union-1'.")
  (intersection-mem (make-hash-table :test #'equal) :type hash-table
                    :documentation "Serve memoization for
`intersection-mem'."))

(defun comp-cstr-ctxt-update-type-slots (ctxt)
  "Update the type related slots of CTXT.
This must run after byte compilation in order to account for user
defined types."
  (setf (comp-cstr-ctxt-typeof-types ctxt)
        (comp--compute-typeof-types))
  (setf (comp-cstr-ctxt-pred-type-h ctxt)
        (comp--compute--pred-type-h)))

(defmacro with-comp-cstr-accessors (&rest body)
  "Define some quick accessor to reduce code vergosity in BODY."
  (declare (debug (form body))
           (indent defun))
  `(cl-macrolet ((typeset (x)
                          `(comp-cstr-typeset ,x))
                 (valset (x)
                         `(comp-cstr-valset ,x))
                 (range (x)
                        `(comp-cstr-range ,x))
                 (neg (x)
                      `(comp-cstr-neg ,x)))
     ,@body))

(defun comp-cstr-copy (cstr)
  "Return a deep copy of CSTR."
  (with-comp-cstr-accessors
    (make-comp-cstr :typeset (copy-sequence (typeset cstr))
                    :valset (copy-sequence (valset cstr))
                    :range (copy-tree (range cstr))
                    :neg (neg cstr))))

(defsubst comp-cstr-shallow-copy (dst src)
  "Copy the content of SRC into DST."
  (with-comp-cstr-accessors
    (setf (range dst) (range src)
          (valset dst) (valset src)
          (typeset dst) (typeset src)
          (neg dst) (neg src))))

(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))
         (null (neg cstr)))))

(defsubst comp-cstr-null-p (cstr)
  "Return t if CSTR is equivalent to the `null' type specifier, nil otherwise."
  (with-comp-cstr-accessors
    (and (null (typeset cstr))
         (null (range cstr))
         (null (neg cstr))
         (equal (valset cstr) '(nil)))))

(defun comp-cstrs-homogeneous (cstrs)
  "Check if constraints CSTRS are all homogeneously negated or non-negated.
Return `pos' if they are all positive, `neg' if they are all
negated or nil otherwise."
  (cl-loop
   for cstr in cstrs
   unless (comp-cstr-neg cstr)
     count t into n-pos
   else
     count t into n-neg
   finally
   (cond
    ((zerop n-neg) (cl-return 'pos))
    ((zerop n-pos) (cl-return 'neg)))))

(defun comp-split-pos-neg (cstrs)
  "Split constraints CSTRS into non-negated and negated.
Return them as multiple value."
  (cl-loop
   for cstr in cstrs
   if (comp-cstr-neg cstr)
     collect cstr into negatives
   else
     collect cstr into positives
   finally return (cl-values positives negatives)))

;; So we can load comp-cstr.el and comp.el in non native compiled
;; builds.
(defvar comp-ctxt nil)

(defvar comp-cstr-one (comp-value-to-cstr 1)
  "Represent the integer immediate one.")

(defvar comp-cstr-t (comp-type-to-cstr t)
  "Represent the superclass t.")

\f
;;; Value handling.

(defun comp-normalize-valset (valset)
  "Sort and remove duplicates from VALSET then return it."
  (cl-sort (cl-remove-duplicates valset :test #'eq)
           (lambda (x y)
             (cond
              ((and (symbolp x) (symbolp y))
               (string< x y))
              ((and (symbolp x) (not (symbolp y)))
               t)
              ((and (not (symbolp x)) (symbolp y))
               nil)
              (t
               (< (sxhash-equal x)
                  (sxhash-equal y)))))))

(defun comp-union-valsets (&rest valsets)
  "Union values present into VALSETS."
  (comp-normalize-valset (cl-reduce #'cl-union valsets)))

(defun comp-intersection-valsets (&rest valsets)
  "Union values present into VALSETS."
  (comp-normalize-valset (cl-reduce #'cl-intersection valsets)))

\f
;;; Type handling.

(defun comp--sym-lessp (x y)
  "Like `string-lessp' but for symbol names."
  (string-lessp (symbol-name x)
                (symbol-name y)))

(defun comp--direct-supertype (type)    ;FIXME: There can be several!
  "Return the direct supertype of TYPE."
  (declare (obsolete comp--direct-supertype "30.1"))
  (cl-loop
   named outer
   for i in (comp-cstr-ctxt-typeof-types comp-ctxt)
   do (cl-loop for (j y) on i
                   when (eq j type)
                     do (cl-return-from outer y))))

(defun comp--direct-supertypes (type)
  "Return the direct supertypes of TYPE."
  (let ((supers (comp-supertypes type)))
    (cl-assert (eq type (car supers)))
    (cl-loop
     with notdirect = nil
     with direct = nil
     for parent in (cdr supers)
     unless (memq parent notdirect)
     do (progn
          (push parent direct)
          (setq notdirect (append notdirect (comp-supertypes parent))))
     finally return direct)))

(defsubst comp-subtype-p (type1 type2)
  "Return t if TYPE1 is a subtype of TYPE2 or nil otherwise."
  (let ((types (cons type1 type2)))
    (or (gethash types (comp-cstr-ctxt-subtype-p-mem comp-ctxt))
        (puthash types
                 (memq type2 (comp-supertypes type1))
                 (comp-cstr-ctxt-subtype-p-mem comp-ctxt)))))

(defun comp--normalize-typeset0 (typeset)
  ;; For every type search its supertypes.  If all the subtypes of a
  ;; supertype are presents remove all of them, add the identified
  ;; supertype and restart.
  ;; FIXME: The intention is to return a 100% equivalent but simpler
  ;; typeset, but this is only the case when the supertype is abstract
  ;; and "final/closed" (i.e. can't have new subtypes).
  (when typeset
    (while (eq 'restart
               (cl-loop
                named main
                for sup in (cl-remove-duplicates
                            (apply #'append
                                   (mapcar #'comp--direct-supertypes typeset)))
                for subs = (comp--direct-subtypes sup)
                when (and (length> subs 1) ;;FIXME: Why?
                          ;; Every subtype of `sup` is a subtype of
                          ;; some element of `typeset`?
                          ;; It's tempting to just check (member x typeset),
                          ;; but think of the typeset (marker number),
                          ;; where `sup' is `integer-or-marker' and `sub'
                          ;; is `integer'.
                          (cl-every (lambda (sub)
                                      (cl-some (lambda (type)
                                                 (comp-subtype-p sub type))
                                               typeset))
                                    subs))
                do (progn
                     (setq typeset (cons sup (cl-set-difference typeset subs)))
                     (cl-return-from main 'restart)))))
    typeset))

(defun comp-normalize-typeset (typeset)
  "Sort TYPESET and return it."
  (cl-sort (comp--normalize-typeset0 (cl-remove-duplicates typeset)) #'comp--sym-lessp))

(defun comp--direct-subtypes (type)
  "Return all the direct subtypes of TYPE."
  ;; TODO: memoize.
  (let ((subtypes ()))
    (dolist (j (comp-cstr-ctxt-typeof-types comp-ctxt))
      (let ((occur (memq type j)))
        (when occur
          (while (not (eq j occur))
            (let ((candidate (pop j)))
              (when (and (not (memq candidate subtypes))
                         (memq type (comp--direct-supertypes candidate)))
                (push candidate subtypes)))))))
    (cl-sort subtypes #'comp--sym-lessp)))

(defun comp--intersection (list1 list2)
  "Like `cl-intersection` but preserves the order of one of its args."
  (if (equal list1 list2) list1
    (let ((res nil))
      (while list2
	(if (memq (car list2) list1)
	    (push (car list2) res))
	(pop list2))
      (nreverse res))))

(defun comp-supertypes (type)
  "Return the ordered list of supertypes of TYPE."
  ;; FIXME: We should probably keep the results in
  ;; `comp-cstr-ctxt-typeof-types' (or maybe even precompute them
  ;; and maybe turn `comp-cstr-ctxt-typeof-types' into a hash-table).
  ;; Or maybe we shouldn't keep structs and defclasses in it,
  ;; and just use `cl--class-allparents' when needed (and refuse to
  ;; compute their direct subtypes since we can't know them).
  (cl-loop
   named loop
   with above
   for lane in (comp-cstr-ctxt-typeof-types comp-ctxt)
   do (let ((x (memq type lane)))
        (cond
         ((null x) nil)
         ((eq x lane) (cl-return-from loop x)) ;A base type: easy case.
         (t (setq above
                  (if above (comp--intersection x above) x)))))
   finally return above))

(defun comp-union-typesets (&rest typesets)
  "Union types present into TYPESETS."
  (or (gethash typesets (comp-cstr-ctxt-union-typesets-mem comp-ctxt))
      (puthash typesets
               (cl-loop
                ;; List of (TYPE . SUPERTYPES)", ordered from
                ;; "most general" to "least general"
                with typess = (sort (mapcar #'comp-supertypes
                                            (apply #'append typesets))
                                    (lambda (l1 l2)
                                      (<= (length l1) (length l2))))
                with res = '()
                for types in typess
                ;; Don't keep this type if it's a subtype of one of
                ;; the other types.
                unless (comp--intersection types res)
                do (push (car types) res)
                finally return (comp-normalize-typeset res))
               (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)
  "Intersect types present into TYPESETS."
  (unless (cl-some #'null typesets)
    (if (length= typesets 1)
        (car typesets)
      (comp-normalize-typeset
       (cl-reduce #'comp-intersect-two-typesets typesets)))))

\f
;;; Integer range handling

(defsubst comp-star-or-num-p (x)
  (or (numberp x) (eq '* x)))

(defsubst comp-range-1+ (x)
  (if (symbolp x)
      x
    (1+ x)))

(defsubst comp-range-1- (x)
  (if (symbolp x)
      x
    (1- x)))

(defsubst comp-range-+ (x y)
  (pcase (cons x y)
    ((or '(+ . -) '(- . +)) '??)
    ((or `(- . ,_) `(,_ . -)) '-)
    ((or `(+ . ,_) `(,_ . +)) '+)
    (_ (+ x y))))

(defsubst comp-range-- (x y)
  (pcase (cons x y)
    ((or '(+ . +) '(- . -)) '??)
    ('(+ . -) '+)
    ('(- . +) '-)
    ((or `(+ . ,_) `(,_ . -)) '+)
    ((or `(- . ,_) `(,_ . +)) '-)
    (_ (- x y))))

(defsubst comp-range-< (x y)
  (cond
   ((eq x '+) nil)
   ((eq x '-) t)
   ((eq y '+) t)
   ((eq y '-) nil)
   (t (< x y))))

(defsubst comp-cstr-smallest-in-range (range)
  "Smallest entry in RANGE."
  (caar range))

(defsubst comp-cstr-greatest-in-range (range)
  "Greater entry in RANGE."
  (cdar (last range)))

(defun comp-range-union (&rest ranges)
  "Combine integer intervals RANGES by union set operation."
  (cl-loop
   with all-ranges = (apply #'append ranges)
   with lows = (mapcar (lambda (x)
                         (cons (comp-range-1- (car x)) 'l))
                       all-ranges)
   with highs = (mapcar (lambda (x)
                          (cons (cdr x) 'h))
                        all-ranges)
   with nest = 0
   with low = nil
   with res = ()
   for (i . x) in (cl-sort (nconc lows highs) #'comp-range-< :key #'car)
   if (eq x 'l)
   do
   (when (zerop nest)
     (setf low i))
   (cl-incf nest)
   else
   do
   (when (= nest 1)
     (push `(,(comp-range-1+ low) . ,i) res))
   (cl-decf nest)
   finally return (reverse res)))

(defun comp-range-intersection (&rest ranges)
  "Combine integer intervals RANGES by intersecting."
  (cl-loop
   with all-ranges = (apply #'append ranges)
   with n-ranges = (length ranges)
   with lows = (mapcar (lambda (x)
                         (cons (car x) 'l))
                       all-ranges)
   with highs = (mapcar (lambda (x)
                          (cons (cdr x) 'h))
                        all-ranges)
   with nest = 0
   with low = nil
   with res = ()
   for (i . x) in (cl-sort (nconc lows highs) #'comp-range-< :key #'car)
   initially (when (cl-some #'null ranges)
               ;; Intersecting with a null range always results in a
               ;; null range.
               (cl-return '()))
   if (eq x 'l)
   do
   (cl-incf nest)
   (when (= nest n-ranges)
     (setf low i))
   else
   do
   (when (= nest n-ranges)
     (push `(,low . ,i)
           res))
   (cl-decf nest)
   finally return (reverse res)))

(defun comp-range-negation (range)
  "Negate range RANGE."
  (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)))))

(defsubst comp-cstr-set-cmp-range (dst old-dst ext-range)
  "Support range comparison functions."
  (with-comp-cstr-accessors
    (if ext-range
        (setf (typeset dst) (when (cl-some (lambda (x)
                                             (comp-subtype-p 'float x))
                                           (typeset old-dst))
                                '(float))
              (valset dst) ()
              (range dst) (if (range old-dst)
                              (comp-range-intersection (range old-dst)
                                                       ext-range)
                            ext-range)
              (neg dst) nil)
      (comp-cstr-shallow-copy dst old-dst))))

(defmacro comp-cstr-set-range-for-arithm (dst src1 src2 &rest range-body)
  ;; Prevent some code duplication for `comp-cstr-add-2'
  ;; `comp-cstr-sub-2'.
  (declare (debug (range-body))
           (indent defun))
  `(with-comp-cstr-accessors
     (if (or (neg src1) (neg src2))
         (setf (typeset ,dst) '(number))
       (when-let ((r1 (range ,src1))
                  (r2 (range ,src2)))
         (let* ((l1 (comp-cstr-smallest-in-range r1))
                (l2 (comp-cstr-smallest-in-range r2))
                (h1 (comp-cstr-greatest-in-range r1))
                (h2 (comp-cstr-greatest-in-range r2)))
           (setf (typeset ,dst) (when (cl-some (lambda (x)
                                                 (comp-subtype-p 'float x))
                                               (append (typeset src1)
                                                       (typeset src2)))
                                  '(float))
                 (range ,dst) ,@range-body))))))

(defun comp-cstr-add-2 (dst src1 src2)
  "Sum SRC1 and SRC2 into DST."
  (comp-cstr-set-range-for-arithm dst src1 src2
    `((,(comp-range-+ l1 l2) . ,(comp-range-+ h1 h2)))))

(defun comp-cstr-sub-2 (dst src1 src2)
  "Subtract SRC1 and SRC2 into DST."
  (comp-cstr-set-range-for-arithm dst src1 src2
    (let ((l (comp-range-- l1 h2))
          (h (comp-range-- h1 l2)))
      (if (or (eq l '??) (eq h '??))
          '((- . +))
        `((,l . ,h))))))

\f
;;; Union specific code.

(defun comp-cstr-union-homogeneous-no-range (dst &rest srcs)
  "As `comp-cstr-union' but excluding the irange component.
All SRCS constraints must be homogeneously negated or non-negated."

  ;; Type propagation.
  (setf (comp-cstr-typeset dst)
        (apply #'comp-union-typesets (mapcar #'comp-cstr-typeset srcs)))

  ;; Value propagation.
  (setf (comp-cstr-valset dst)
        (comp-normalize-valset
         (cl-loop
          with values = (mapcar #'comp-cstr-valset srcs)
          ;; TODO sort.
          for v in (cl-remove-duplicates (apply #'append values)
                                         :test #'equal)
          ;; We propagate only values those types are not already
          ;; into typeset.
          when (cl-notany (lambda (x)
                            (comp-subtype-p (type-of v) x))
                          (comp-cstr-typeset dst))
          collect v)))

  dst)

(defun comp-cstr-union-homogeneous (range dst &rest srcs)
  "Combine SRCS by union set operation setting the result in DST.
Do range propagation when RANGE is non-nil.
All SRCS constraints must be homogeneously negated or non-negated.
DST is returned."
  (apply #'comp-cstr-union-homogeneous-no-range dst srcs)
  ;; Range propagation.
  (setf (comp-cstr-neg dst)
        (when srcs
          (comp-cstr-neg (car srcs)))

        (comp-cstr-range dst)
        (when (cl-notany (lambda (x)
                           (comp-subtype-p 'integer x))
                         (comp-cstr-typeset dst))
          (if range
              (apply #'comp-range-union
                     (mapcar #'comp-cstr-range srcs))
            '((- . +)))))
  dst)

(cl-defun comp-cstr-union-1-no-mem (range &rest srcs)
  "Combine SRCS by union set operation setting the result in DST.
Do range propagation when RANGE is non-nil.
Non memoized version of `comp-cstr-union-1'.
DST is returned."
  (with-comp-cstr-accessors
    (let ((dst (make-comp-cstr)))
      (cl-flet ((give-up ()
                         (setf (typeset dst) '(t)
                               (valset dst) ()
                               (range dst) ()
                               (neg dst) nil)
                         (cl-return-from comp-cstr-union-1-no-mem dst)))

        ;; Check first if we are in the simple case of all input non-negate
        ;; or negated so we don't have to cons.
        (when-let ((res (comp-cstrs-homogeneous srcs)))
          (apply #'comp-cstr-union-homogeneous range dst srcs)
          (cl-return-from comp-cstr-union-1-no-mem dst))

        ;; Some are negated and some are not
        (cl-multiple-value-bind (positives negatives) (comp-split-pos-neg srcs)
          (let* ((pos (apply #'comp-cstr-union-homogeneous range
                             (make-comp-cstr) positives))
                 ;; We'll always use neg as result as this is almost
                 ;; always necessary for describing open intervals
                 ;; resulting from negated constraints.
                 (neg (apply #'comp-cstr-union-homogeneous range
                             (make-comp-cstr :neg t) negatives)))
            ;; Type propagation.
            (when (and (typeset pos)
                       ;; When every pos type is a subtype of some neg ones.
                       (cl-every (lambda (x)
                                   (cl-some (lambda (y)
                                              (comp-subtype-p x y))
                                            (append (typeset neg)
                                                    (when (range neg)
                                                      '(integer)))))
                                 (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' or adopt something like
              ;; `intersection-type' `union-type' in SBCL.  Keep it
              ;; "simple" for now.
              (give-up))

            ;; When every neg type is a subtype of some pos one.
            ;; In case return pos.
            (when (and (typeset neg)
                       (cl-every (lambda (x)
                                   (cl-some (lambda (y)
                                              (comp-subtype-p x y))
                                            (append (typeset pos)
                                                    (when (range pos)
                                                      '(integer)))))
                                 (typeset neg)))
              (comp-cstr-shallow-copy dst pos)
              (setf (neg dst) nil)
              (cl-return-from comp-cstr-union-1-no-mem dst))

            ;; Verify disjoint condition between positive types and
            ;; negative types coming from values, in case give-up.
            (let ((neg-value-types (nconc (mapcar #'type-of (valset neg))
                                          (when (range neg)
                                            '(integer)))))
              (when (cl-some (lambda (x)
                               (cl-some (lambda (y)
                                          (and (not (eq y x))
                                               (comp-subtype-p y x)))
                                        neg-value-types))
                             (typeset pos))
                (give-up)))

            ;; Value propagation.
            (cond
             ((and (valset pos) (valset neg)
                   (equal (comp-union-valsets (valset pos) (valset neg))
                          (valset pos)))
              ;; Pos is a superset of neg.
              (give-up))
             ((cl-some (lambda (x)
                         (cl-some (lambda (y)
                                    (comp-subtype-p y x))
                                  (mapcar #'type-of (valset pos))))
                       (typeset neg))
              (give-up))
             (t
              ;; pos is a subset or eq to neg
              (setf (valset neg)
                    (cl-nset-difference (valset neg) (valset pos)))))

            ;; Range propagation
            (when range
              ;; Handle apart (or (integer 1 1) (not (integer 1 1)))
              ;; like cases.
              (if (and (range pos) (range neg)
                       (equal (range pos) (range neg)))
                  (give-up)
                (setf (range neg)
                      (comp-range-negation
                       (comp-range-union
                        (comp-range-negation (range neg))
                        (range pos))))))

            (comp-cstr-shallow-copy dst (if (comp-cstr-empty-p neg)
                                            pos
                                          neg))))

        ;; (not null) => t
        (when (and (neg dst)
                   (null (typeset dst))
                   (null (valset dst))
                   (null (range dst)))
          (give-up)))

      dst)))

(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."
  (with-comp-cstr-accessors
    (let* ((mem-h (if range
                      (comp-cstr-ctxt-union-1-mem-range comp-ctxt)
                    (comp-cstr-ctxt-union-1-mem-no-range comp-ctxt)))
           (res (or (gethash srcs mem-h)
                    (puthash
                     (mapcar #'comp-cstr-copy srcs)
                     (apply #'comp-cstr-union-1-no-mem range srcs)
                     mem-h))))
      (comp-cstr-shallow-copy dst res)
      res)))

(cl-defun comp-cstr-intersection-homogeneous (dst &rest srcs)
  "Combine SRCS by intersection set operation setting the result in DST.
All SRCS constraints must be homogeneously negated or non-negated.
DST is returned."

  (with-comp-cstr-accessors
    (when (cl-some #'comp-cstr-empty-p srcs)
      (setf (valset dst) nil
            (range dst) nil
            (typeset dst) nil)
      (cl-return-from comp-cstr-intersection-homogeneous dst))

    (setf (neg dst) (when srcs
                      (neg (car srcs))))

    ;; Type propagation.
    (setf (typeset dst)
          (apply #'comp-intersect-typesets
                 (mapcar #'comp-cstr-typeset srcs)))

    ;; 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 (memql 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 (&rest srcs)
  "Combine SRCS by intersection set operation.
Non memoized version of `comp-cstr-intersection-no-mem'."
  (let ((dst (make-comp-cstr)))
    (with-comp-cstr-accessors
      (cl-flet ((return-empty ()
                              (setf (typeset dst) ()
                                    (valset dst) ()
                                    (range dst) ()
                                    (neg dst) nil)
                              (cl-return-from comp-cstr-intersection-no-mem dst)))
        (when-let ((res (comp-cstrs-homogeneous srcs)))
          (if (eq res 'neg)
              (apply #'comp-cstr-union-homogeneous t dst srcs)
            (apply #'comp-cstr-intersection-homogeneous dst srcs))
          (cl-return-from comp-cstr-intersection-no-mem dst))

        ;; Some are negated and some are not
        (cl-multiple-value-bind (positives negatives) (comp-split-pos-neg srcs)
          (let* ((pos (apply #'comp-cstr-intersection-homogeneous
                             (make-comp-cstr) positives))
                 (neg (apply #'comp-cstr-intersection-homogeneous
                             (make-comp-cstr) negatives)))

            ;; In case pos is not relevant return directly the content
            ;; of neg.
            (when (equal (typeset pos) '(t))
              (comp-cstr-shallow-copy dst neg)
              (setf (neg dst) t)

              ;; (not t) => nil
              (when (and (null (valset dst))
                         (null (range dst))
                         (neg dst)
                         (equal '(t) (typeset dst)))
                (setf (typeset dst) ()
                      (neg dst) nil))

              (cl-return-from comp-cstr-intersection-no-mem dst))

            (when (cl-some
                   (lambda (ty)
                     (memq ty (typeset neg)))
                   (typeset pos))
              (return-empty))

            ;; Some negated types are subtypes of some non-negated one.
            ;; Transform the corresponding set of types from neg to pos.
            (cl-loop
             for neg-type in (typeset neg)
             do (cl-loop
                 for pos-type in (copy-sequence (typeset pos))
                 when (and (not (eq neg-type pos-type))
                           (comp-subtype-p neg-type pos-type))
                   do (cl-loop
                       with found
                       for type in (comp-supertypes neg-type)
                       when found
                         collect type into res
                       when (eq type pos-type)
                         do (setf (typeset pos) (cl-union (typeset pos) res))
                            (cl-return)
                       when (eq type neg-type)
                         do (setf found t))))

            (setf (range pos)
                  (comp-range-intersection (range pos)
                                           (comp-range-negation (range neg)))
                  (valset pos)
                  (cl-set-difference (valset pos) (valset neg)))

            ;; Return a non negated form.
            (comp-cstr-shallow-copy dst pos)
            (setf (neg dst) nil)))
        dst))))

\f
;;; Entry points.

(defun comp-cstr-imm-vld-p (cstr)
  "Return t if one and only one immediate value can be extracted from CSTR."
  (with-comp-cstr-accessors
    (when (and (null (typeset cstr))
               (null (neg cstr)))
      (let* ((v (valset cstr))
             (r (range cstr))
             (valset-len (length v))
             (range-len (length r)))
        (if (and (= valset-len 1)
                 (= range-len 0))
            t
          (when (and (= valset-len 0)
                     (= range-len 1))
            (let* ((low (caar r))
                   (high (cdar r)))
              (and (integerp low)
                   (integerp high)
                   (= low high)))))))))

(defun comp-cstr-imm (cstr)
  "Return the immediate value of CSTR.
`comp-cstr-imm-vld-p' *must* be satisfied before calling
`comp-cstr-imm'."
  (declare (gv-setter
            (lambda (val)
              `(with-comp-cstr-accessors
                 (if (integerp ,val)
                     (setf (typeset ,cstr) nil
                           (range ,cstr) (list (cons ,val ,val)))
                   (setf (typeset ,cstr) nil
                         (valset ,cstr) (list ,val)))))))
  (with-comp-cstr-accessors
    (let ((v (valset cstr)))
      (if (length= v 1)
          (car v)
        (caar (range cstr))))))

(defun comp-cstr-fixnum-p (cstr)
  "Return t if CSTR is certainly a fixnum."
  (with-comp-cstr-accessors
    (when (null (neg cstr))
      (when-let (range (range cstr))
        (let* ((low (caar range))
               (high (cdar (last range))))
          (unless (or (eq low '-)
                      (< low most-negative-fixnum)
                      (eq high '+)
                      (> high most-positive-fixnum))
            t))))))

(defun comp-cstr-symbol-p (cstr)
  "Return t if CSTR is certainly a symbol."
  (with-comp-cstr-accessors
    (and (null (range cstr))
         (null (neg cstr))
         (or (and (null (valset cstr))
                  (equal (typeset cstr) '(symbol)))
             (and (or (null (typeset cstr))
                      (equal (typeset cstr) '(symbol)))
                  (cl-every #'symbolp (valset cstr)))))))

(defsubst comp-cstr-cons-p (cstr)
  "Return t if CSTR is certainly a cons."
  (with-comp-cstr-accessors
    (and (null (valset cstr))
         (null (range cstr))
         (null (neg cstr))
         (equal (typeset cstr) '(cons)))))

;; Move to comp.el?
(defsubst comp-cstr-cl-tag-p (cstr)
  "Return non-nil if CSTR is a CL tag."
  (with-comp-cstr-accessors
    (and (null (range cstr))
         (null (neg cstr))
         (null (typeset cstr))
         (length= (valset cstr) 1)
         (string-match (rx "cl-struct-" (group-n 1 (1+ not-newline)) "-tags")
                       (symbol-name (car (valset cstr)))))))

(defsubst comp-cstr-cl-tag (cstr)
  "If CSTR is a CL tag return its tag name."
  (with-comp-cstr-accessors
    (and (comp-cstr-cl-tag-p cstr)
         (intern (match-string 1 (symbol-name (car (valset cstr))))))))

(defun comp-cstr-= (dst op1 op2)
  "Constraint OP1 being = OP2 setting the result into DST."
  (with-comp-cstr-accessors
    (cl-flet ((relax-cstr (cstr)
                (setf cstr (copy-sequence cstr))
                ;; If can be any float extend it to all integers.
                (when (memq 'float (typeset cstr))
                  (setf (range cstr) '((- . +))))
                ;; For each float value that can be represented
                ;; precisely as an integer add the integer as well.
                (cl-loop
                 for v in (valset cstr)
                 do
                 (when-let* ((ok (floatp v))
                             (truncated (ignore-error overflow-error
                                          (truncate v)))
                             (ok (= v truncated)))
                   (push (cons truncated truncated) (range cstr))))
                (cl-loop
                 with vals-to-add
                 for (l . h) in (range cstr)
                 ;; If an integer range reduces to single value add
                 ;; its float value too.
                 if (eql l h)
                   do (push (float l) vals-to-add)
                 ;; Otherwise can be any float.
                 else
                   do (cl-pushnew 'float (typeset cstr))
                      (cl-return cstr)
                 finally (setf (valset cstr)
                               (append vals-to-add (valset cstr))))
                (when (memql 0.0 (valset cstr))
                  (cl-pushnew -0.0 (valset cstr)))
                (when (memql -0.0 (valset cstr))
                  (cl-pushnew 0.0 (valset cstr)))
                cstr))
      (comp-cstr-intersection dst (relax-cstr op1) (relax-cstr op2)))))

(defun comp-cstr-> (dst old-dst src)
  "Constraint DST being > than SRC.
SRC can be either a comp-cstr or an integer."
  (with-comp-cstr-accessors
    (let ((ext-range
           (if (integerp src)
               `((,(1+ src) . +))
             (when-let* ((range (range src))
                         (low (comp-cstr-smallest-in-range range))
                         (okay (integerp low)))
               `((,(1+ low) . +))))))
      (comp-cstr-set-cmp-range dst old-dst ext-range))))

(defun comp-cstr->= (dst old-dst src)
  "Constraint DST being >= than SRC.
SRC can be either a comp-cstr or an integer."
  (with-comp-cstr-accessors
    (let ((ext-range
           (if (integerp src)
               `((,src . +))
             (when-let* ((range (range src))
                         (low (comp-cstr-smallest-in-range range))
                         (okay (integerp low)))
               `((,low . +))))))
      (comp-cstr-set-cmp-range dst old-dst ext-range))))

(defun comp-cstr-< (dst old-dst src)
  "Constraint DST being < than SRC.
SRC can be either a comp-cstr or an integer."
  (with-comp-cstr-accessors
    (let ((ext-range
           (if (integerp src)
               `((- . ,(1- src)))
             (when-let* ((range (range src))
                         (low (comp-cstr-greatest-in-range range))
                         (okay (integerp low)))
               `((- . ,(1- low)))))))
      (comp-cstr-set-cmp-range dst old-dst ext-range))))

(defun comp-cstr-<= (dst old-dst src)
  "Constraint DST being > than SRC.
SRC can be either a comp-cstr or an integer."
  (with-comp-cstr-accessors
    (let ((ext-range
           (if (integerp src)
               `((- . ,src))
             (when-let* ((range (range src))
                         (low (comp-cstr-greatest-in-range range))
                         (okay (integerp low)))
               `((- . ,low))))))
      (comp-cstr-set-cmp-range dst old-dst ext-range))))

(defun comp-cstr-add (dst srcs)
  "Sum SRCS into DST."
  (comp-cstr-add-2 dst (cl-first srcs) (cl-second srcs))
  (cl-loop
   for src in (nthcdr 2 srcs)
   do (comp-cstr-add-2 dst dst src)))

(defun comp-cstr-sub (dst srcs)
  "Subtract SRCS into DST."
  (comp-cstr-sub-2 dst (cl-first srcs) (cl-second srcs))
  (cl-loop
   for src in (nthcdr 2 srcs)
   do (comp-cstr-sub-2 dst dst src)))

(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))

(defun comp-cstr-intersection (dst &rest srcs)
  "Combine SRCS by intersection set operation setting the result in DST.
DST is returned."
  (with-comp-cstr-accessors
    (let* ((mem-h (comp-cstr-ctxt-intersection-mem comp-ctxt))
           (res (or (gethash srcs mem-h)
                    (puthash
                     (mapcar #'comp-cstr-copy srcs)
                     (apply #'comp-cstr-intersection-no-mem srcs)
                     mem-h))))
      (comp-cstr-shallow-copy dst res)
      res)))

(defun comp-cstr-intersection-no-hashcons (dst &rest srcs)
  "Combine SRCS by intersection set operation setting the result in DST.
Non hash consed values are not propagated as values but rather
promoted to their types.
DST is returned."
  (with-comp-cstr-accessors
    (apply #'comp-cstr-intersection dst srcs)
    (if (and (neg dst)
             (valset dst)
             (cl-notevery #'symbolp (valset dst)))
        (setf (valset dst) ()
              (typeset dst) '(t)
              (range dst) ()
              (neg dst) nil)
      (let (strip-values strip-types)
        (cl-loop for v in (valset dst)
                 unless (symbolp v)
                   do (push v strip-values)
                      (push (type-of v) strip-types))
        (when strip-values
          (setf (typeset dst) (comp-union-typesets (typeset dst) strip-types)
                (valset dst) (cl-set-difference (valset dst) strip-values)))
        (cl-loop for (l . h) in (range dst)
                 when (or (bignump l) (bignump h))
                 do (setf (range dst) '((- . +)))
                    (cl-return))))
    dst))

(defun comp-cstr-intersection-make (&rest srcs)
  "Combine SRCS by intersection set operation and return a new constraint."
  (apply #'comp-cstr-intersection (make-comp-cstr) srcs))

(defun comp-cstr-negation (dst src)
  "Negate SRC setting the result in DST.
DST is returned."
  (with-comp-cstr-accessors
    (cond
     ((and (null (valset src))
           (null (range src))
           (null (neg src))
           (equal (typeset src) '(t)))
      (setf (typeset dst) ()
            (valset dst) ()
            (range dst) nil
            (neg dst) nil))
     ((and (null (valset src))
           (null (range src))
           (null (neg src))
           (null (typeset src)))
      (setf (typeset dst) '(t)
            (valset dst) ()
            (range dst) nil
            (neg dst) nil))
     (t
      (comp-cstr-shallow-copy dst src)
      (setf (neg dst) (not (neg src)))))
    dst))

(defun comp-cstr-value-negation (dst src)
  "Negate values in SRC setting the result in DST.
DST is returned."
  (with-comp-cstr-accessors
    (if (or (valset src) (range src))
        (setf (typeset dst) ()
              (valset dst) (valset src)
              (range dst) (range src)
              (neg dst) (not (neg src)))
      (setf (typeset dst) (typeset src)
            (valset dst) ()
            (range dst) ()))
    dst))

(defun comp-cstr-negation-make (src)
  "Negate SRC and return a new constraint."
  (comp-cstr-negation (make-comp-cstr) src))

(defun comp-type-spec-to-cstr (type-spec &optional fn)
  "Convert a type specifier TYPE-SPEC into a `comp-cstr'.
FN non-nil indicates we are parsing a function lambda list."
  (pcase type-spec
    ((and (or '&optional '&rest) x)
     (if fn
         x
       (error "Invalid `%s` in type specifier" x)))
    ('nil
     (make-comp-cstr :typeset ()))
    ('fixnum
     (comp-irange-to-cstr `(,most-negative-fixnum . ,most-positive-fixnum)))
    ('boolean
     (comp-type-spec-to-cstr '(member t nil)))
    ('integer
     (comp-irange-to-cstr '(- . +)))
    ('null (comp-value-to-cstr nil))
    ((pred atom)
     (comp-type-to-cstr type-spec))
    (`(or . ,rest)
     (apply #'comp-cstr-union-make
            (mapcar #'comp-type-spec-to-cstr rest)))
    (`(and . ,rest)
     (apply #'comp-cstr-intersection-make
            (mapcar #'comp-type-spec-to-cstr rest)))
    (`(not  ,cstr)
     (comp-cstr-negation-make (comp-type-spec-to-cstr cstr)))
    (`(integer ,(and (pred integerp) l) ,(and (pred integerp) h))
     (comp-irange-to-cstr `(,l . ,h)))
    (`(integer * ,(and (pred integerp) h))
     (comp-irange-to-cstr `(- . ,h)))
    (`(integer ,(and (pred integerp) l) *)
     (comp-irange-to-cstr `(,l . +)))
    (`(float ,(pred comp-star-or-num-p) ,(pred comp-star-or-num-p))
     ;; No float range support :/
     (comp-type-to-cstr 'float))
    (`(member . ,rest)
     (apply #'comp-cstr-union-make (mapcar #'comp-value-to-cstr rest)))
    (`(function ,args ,ret)
     (make-comp-cstr-f
      :args (mapcar (lambda (x)
                      (comp-type-spec-to-cstr x t))
                    args)
      :ret (comp-type-spec-to-cstr ret)))
    (_ (error "Invalid type specifier"))))

(defun comp--simple-cstr-to-type-spec (cstr)
  "Given a non comp-cstr-f CSTR return its type specifier."
  (let ((valset (comp-cstr-valset cstr))
        (typeset (comp-cstr-typeset cstr))
        (range (comp-cstr-range cstr))
        (negated (comp-cstr-neg cstr)))

    (when valset
      (when (memq nil valset)
        (if (memq t valset)
            (progn
              ;; t and nil are values, convert into `boolean'.
              (push 'boolean typeset)
              (setf valset (remove t (remove nil valset))))
          ;; Only nil is a value, convert it into a `null' type specifier.
          (setf valset (remove nil valset))
          (push 'null typeset))))

    ;; Form proper integer type specifiers.
    (setf range (cl-loop for (l . h) in range
                         for low = (if (integerp l) l '*)
                         for high = (if (integerp h) h '*)
                         if (and (eq low '*) (eq high '*))
                           collect 'integer
                         else
                           collect `(integer ,low , high))
          valset (cl-remove-duplicates valset))

    ;; Form the final type specifier.
    (let* ((types-ints (append typeset range))
           (res (cond
                 ((and types-ints valset)
                  `((member ,@valset) ,@types-ints))
                 (types-ints types-ints)
                 (valset `(member ,@valset))
                 (t
                  ;; Empty type specifier
                  nil)))
           (final
            (pcase res
              ((or `(member . ,rest)
                   `(integer ,(pred comp-star-or-num-p)
                             ,(pred comp-star-or-num-p)))
               (if rest
                   res
                 (car res)))
              ((pred atom) res)
              (`(,_first . ,rest)
               (if rest
                   `(or ,@res)
                 (car res))))))
      (if negated
          `(not ,final)
        final))))

(defun comp-cstr-to-type-spec (cstr)
  "Given CSTR return its type specifier."
  (cl-etypecase cstr
    (comp-cstr-f
     `(function
       ,(mapcar (lambda (x)
                  (cl-etypecase x
                    (comp-cstr (comp-cstr-to-type-spec x))
                    (symbol x)))
                (comp-cstr-f-args cstr))
       ,(comp--simple-cstr-to-type-spec (comp-cstr-f-ret cstr))))
    (comp-cstr
     (comp--simple-cstr-to-type-spec cstr))))

(provide 'comp-cstr)

;;; comp-cstr.el ends here