defintrange

(defmacro defintrange1
  (name min max)
  (declare (xargs :guard (symbolp name)))
  `(make-event (b* ((pkg (current-package state)) (m (type-metadata-table (w state)))
        (a (type-alias-table (w state)))
        (th1 (make-sym ',ACL2S::NAME 'thm1 pkg))
        (th2 (make-sym ',ACL2S::NAME 'thm2 pkg))
        (th3 (make-sym ',ACL2S::NAME 'thm3 pkg))
        (namep (make-symbl `(,',ACL2S::NAME p) pkg))
        (type (cond ((equal ,MIN 0) 'nat)
            ((< 0 ,MIN) 'pos)
            ((<= ,MAX 0) 'neg)
            (t 'integer)))
        (pred (make-symbl `(,TYPE p) pkg))
        (rng `(and (,ACL2S::PRED a)
            (<= ,,MIN a)
            (< a ,,MAX)))
        (type-of-type (type-of-type ',ACL2S::NAME m a))
        (alias? (not (equal type-of-type ',ACL2S::NAME))))
      (value (if alias?
          '(value-triple :invisible)
          `(progn (defdata-subtype ,',ACL2S::NAME ,TYPE :strictp t)
            (defthm ,ACL2S::TH1
              (implies (,ACL2S::NAMEP a) ,ACL2S::RNG)
              :rule-classes ((:forward-chaining)))
            (defthm ,ACL2S::TH2
              (implies ,ACL2S::RNG (,ACL2S::NAMEP a))
              :rule-classes ((:rewrite :backchain-limit-lst 1)))
            (defthm ,ACL2S::TH3
              (equal (,ACL2S::NAMEP a) ,ACL2S::RNG)
              :rule-classes :compound-recognizer)
            (in-theory (disable ,ACL2S::NAMEP))))))))

(defmacro defintrange
  (name min max)
  "Define a datatype that includes all integers [min..max), i.e., >= min and < max"
  (declare (xargs :guard (symbolp name)))
  `(progn (defdata ,ACL2S::NAME
      (range integer (,MIN <= _ < ,MAX)))
    (defintrange1 ,ACL2S::NAME ,MIN ,MAX)))

(defmacro defnatrange
  (name max)
  "Define a datatype that includes all nats < max"
  (declare (xargs :guard (symbolp name)))
  `(defintrange ,ACL2S::NAME 0 ,MAX))