fast-coerce - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "arithmetic/top-with-meta" :dir :system))

local

(local (include-book "data-structures/list-defthms" :dir :system))

fast-coerce-aux1function

(defund fast-coerce-aux1
  (x i len)
  (declare (type string x)
    (type (signed-byte 30) i)
    (type (signed-byte 30) len)
    (xargs :guard (and (stringp x)
        (natp i)
        (natp len)
        (= len (length x))
        (<= i len))
      :measure (nfix (- (nfix len) (nfix i)))))
  (if (mbe :logic (zp (- (nfix len) (nfix i)))
      :exec (= (the-fixnum i) (the-fixnum len)))
    nil
    (cons (the character
        (char (the string x) (the (signed-byte 30) i)))
      (fast-coerce-aux1 x
        (the-fixnum (+ (the-fixnum 1)
            (mbe :logic (nfix i) :exec (the-fixnum i))))
        (the-fixnum len)))))

fast-coerce-aux2function

(defund fast-coerce-aux2
  (x i len)
  (declare (type string x)
    (type integer i)
    (type integer len)
    (xargs :guard (and (stringp x)
        (natp i)
        (natp len)
        (= len (length x))
        (<= i len))
      :guard-debug t
      :measure (nfix (- (nfix len) (nfix i)))))
  (if (mbe :logic (zp (- (nfix len) (nfix i)))
      :exec (= (the integer i) (the integer len)))
    nil
    (cons (char x i)
      (fast-coerce-aux2 x
        (+ (the integer 1)
          (mbe :logic (nfix i) :exec (the integer i)))
        len))))

local

(local (defthm lemma
    (implies (and (natp i) (< i (len x)))
      (equal (cons (nth i x) (cdr (nthcdr i x))) (nthcdr i x)))))

local

(local (defthm lemma2
    (equal (nthcdr i (cdr x)) (cdr (nthcdr i x)))))

local

(local (defthm lemma3
    (implies (and (stringp x) (natp i) (<= i (length x)))
      (equal (fast-coerce-aux2 x i (len (coerce x 'list)))
        (nthcdr i (coerce x 'list))))
    :hints (("Goal" :in-theory (enable fast-coerce-aux2)))))

local

(local (defthm fast-coerce-aux2-equiv
    (equal (fast-coerce-aux1 x i len)
      (fast-coerce-aux2 x i len))
    :hints (("Goal" :in-theory (enable fast-coerce-aux2 fast-coerce-aux1)))))

fast-coercefunction

(defun fast-coerce
  (x y)
  (declare (xargs :guard (case y (list (stringp x)) (string (character-listp x)))))
  (mbe :logic (coerce x y)
    :exec (if (eq y 'list)
      (let ((length (length x)))
        (if (< (the integer length) (the integer 536870912))
          (fast-coerce-aux1 (the string x)
            (the (signed-byte 30) 0)
            (the (signed-byte 30) length))
          (fast-coerce-aux2 (the string x)
            (the integer 0)
            (the integer length))))
      (coerce x y))))