read-string-tests

other

(in-package "ACL2")

include-book

(include-book "read-string")

test-okmacro

(defmacro test-ok
  (str expect)
  `(make-event (b* (((mv errmsg objects state) (read-string ',STR nil)) ((when (and (not errmsg) (equal objects ',EXPECT))) (value '(value-triple :success))))
      (er soft
        'test-ok
        "Test failed for ~s0: expect ~x1 but got ~x2; msg is ~@3"
        ',STR
        ',EXPECT
        objects
        (or errmsg "NIL")))))

test-failmacro

(defmacro test-fail
  (str)
  `(make-event (b* (((mv errmsg objects state) (read-string ',STR nil)) ((when errmsg) (value '(value-triple :success))))
      (er soft
        'test-fail
        "Test failed for ~s0: expect FAIL but got ~x1."
        ',STR
        objects))))

other

(test-ok "" nil)

other

(test-ok "1 2 3" (1 2 3))

other

(test-ok "#x10 "foo"" (16 "foo"))

other

(test-ok "#ux_1_0_0" (256))

other

(test-ok "(append x y z)" ((append x y z)))

other

(test-ok "*foo*" (*foo*))

other

(test-ok "#\a " (#\a))

other

(test-ok "#\Page " (#\))

other

(test-ok "#\a" (#\a))

other

(test-ok "#\Page" (#\))

other

(test-fail "3.5")

other

(test-fail "#wtf ")

other

(test-fail "#Return ")

other

(test-ok "a" (a))

other

(test-ok "acl2::a" (a))

other

(test-ok "std::foo" (foo))

other

(defttag :more-tests)

other

(progn! (in-package "STD"))

other

(test-ok "a" (a))

other

(test-ok "acl2::a" (a))

other

(test-ok "std::foo" (foo))

Included Books