Filtering...

defdata-testing

books/acl2s/defdata-testing
other
(in-package "ACL2S")
other
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil)
other
(include-book "acl2s/base-theory" :dir :system :ttags :all)
other
(include-book "acl2s/custom" :dir :system :ttags :all)
other
(include-book "acl2s/acl2s-sigs" :dir :system :ttags :all)
other
(acl2s-defaults :set cgen-single-test-timeout
  0)
other
(must-succeed (thm (implies (natp n)
      (booleanp (nth-boolean-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (natp (nth-nat-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (posp (nth-pos-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (negp (nth-neg-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (non-pos-integerp (nth-non-pos-integer-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (non-0-integerp (nth-non-0-integer-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (integerp (nth-integer-builtin n)))))
other
(must-succeed (thm (implies (and (natp n)
        (integerp lo)
        (integerp hi)
        (<= lo hi))
      (and (integerp (nth-integer-between n lo hi))
        (<= lo
          (nth-integer-between n lo hi))
        (>= hi
          (nth-integer-between n lo hi))))))
other
(must-succeed (test? (implies (natp n)
      (pos-ratiop (nth-pos-ratio-builtin n)))))
other
(must-succeed (test? (implies (natp n)
      (neg-ratiop (nth-neg-ratio-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (neg-rationalp (nth-neg-rational-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (pos-rationalp (nth-pos-rational-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (non-neg-rationalp (nth-non-neg-rational-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (non-pos-rationalp (nth-non-pos-rational-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (non-0-rationalp (nth-non-0-rational-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (rationalp (nth-rational-builtin n)))))
other
(must-succeed (test? (implies (and (natp n)
        (rationalp lo)
        (rationalp hi)
        (<= lo hi))
      (and (rationalp (nth-rational-between n lo hi))
        (<= lo
          (nth-rational-between n lo hi))
        (>= hi
          (nth-rational-between n lo hi))))))
other
(must-succeed (thm (implies (natp n)
      (stringp (nth-string-builtin n)))))
other
(must-succeed (test? (implies (natp n)
      (standard-stringp (nth-standard-string-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (symbolp (nth-symbol-builtin n)))))
other
(must-succeed (thm (implies (natp n)
      (characterp (nth-character-builtin n)))))
other
(must-succeed (test? (implies (natp n)
      (in (nth-alpha-num-character n)
        *alpha-num-chars*))))
other
(must-succeed (thm (implies (natp n)
      (character-listp (nth-character-list-builtin n)))))
other
(must-succeed (test? (implies (natp n)
      (standard-char-listp (nth-standard-char-list-builtin n)))))
other
(defdata one 1)
other
(defdata loi (listof int))
other
(defdata r1
  (record (a . loi)))
other
(defdata data (listof nat))
other
(defdata receiver-state
  (record (received . data)))
other
(definec bax
  (rs :data)
  :receiver-state (receiver-state rs))
other
(property (rs :data)
  (receiver-statep (receiver-state rs)))
other
(property (rs :receiver-state a b c :all)
  (equal (mget :received (msets rs
        :received a
        :received b
        :received c))
    c))
other
(must-fail (defdata-alias r2 r1))
other
(must-succeed (test? (=> (^ (intp lo)
        (intp hi)
        (natp n)
        (<= lo hi))
      (^ (<= lo
          (geometric-int-between lo hi n))
        (>= hi
          (geometric-int-between lo hi n))))))
other
(must-succeed (test? (=> (^ (rationalp lo)
        (rationalp hi)
        (natp n)
        (<= lo hi))
      (^ (<= lo
          (geometric-rat-between lo hi n))
        (>= hi
          (geometric-rat-between lo hi n))))))
other
(must-succeed (test? (=> (^ (intp lo)
        (intp hi)
        (<= lo hi))
      (b* (((mv mid1 mid2) (int-midpoints lo hi)))
        (^ (<= lo mid1)
          (>= hi mid2))))))
other
(must-succeed (test? (=> (^ (rationalp lo)
        (rationalp hi)
        (<= lo hi))
      (b* (((mv mid1 mid2) (rat-midpoints lo hi)))
        (^ (<= lo mid1)
          (>= hi mid2))))))
other
(defdata receiver-state
  (record (received . data)))
other
(defdata value-type int)
other
(defdata read-request
  (list 'read-request))
other
(defdata read-response
  (list 'read-response value-type))
other
(defdata write-request
  (list 'write-request value-type))
other
(defdata write-response
  (list 'write-response))
other
(defdata repl-request
  (list 'repl-request nat value-type))
other
(defdata repl-response
  (list 'repl-response))
other
(defdata operation
  (oneof read-request
    read-response
    write-request
    write-response
    repl-request
    repl-response))
other
(check (operationp (list 'read-request)))
other
(check (operationp (list 'read-response 1)))
other
(check (operationp (list 'write-request 1)))
other
(check (operationp (list 'write-response)))
other
(check (operationp (list 'repl-request 1 2)))
other
(check (operationp (list 'repl-response)))
other
(check (write-requestp '(write-request 3)))
other
(defdata name (map nat nat))
other
(defdata d2 (map loi loi))
other
(defdata lloi (listof loi))
other
(defdata d3 (map lloi lloi))
other
(defdata d4 (map loi lloi))
other
(defdata d5 (map lloi loi))
other
(defdata d6
  (record (a . loi)
    (b . int)
    (c . non-neg-rational)))
other
(defdata d7 (map d6 d6))
other
(must-fail (defdata zero 0))
zeeropfunction
(defun zeerop
  (x)
  (declare (xargs :guard t))
  (equal x 0))
other
(defdata zeero 0)
other
(must-fail (defdata zero 0))
zeeeropfunction
(defun zeeerop
  (x)
  (declare (xargs :guard (acl2-numberp x)))
  (equal x 0))
other
(must-fail (defdata zeeero 0))
other
(defdata ds1 (enum '(1 2 3 1 2 3)))
other
(defdata ds2 (or 1 2 3 1 2 3))
other
(defdata ds3 (or 1 2 3 1 2 3 int))
other
(defdata ds4 1)
other
(defdata ds5 'x)
other
(defdata ds6 int)
other
(defdata ds7 (or 1 nil))
other
(check= (defdata-domain-size ds1) 3)
other
(check= (defdata-domain-size ds2) 3)
other
(check= (defdata-domain-size ds3)
  'infinite)
other
(check= (defdata-domain-size ds4) 1)
other
(check= (defdata-domain-size ds5) 1)
other
(check= (defdata-domain-size ds6) 1)
other
(check= (defdata-domain-size ds7) 2)
other
(defdata ds8
  (record (a . int)
    (b . tl)))
other
(property (x y :ds8)
  :h (^ (== (ds8-a x) (ds8-a y))
    (== (ds8-b x) (ds8-b y)))
  (== x y))