arrays

(defun def-array-set-fn
  (name stobj field update length guard fix check)
  (let* ((length (or length
         (intern-in-package-of-symbol (concatenate 'string (symbol-name field) "-LENGTH")
           field))) (update (or update
          (intern-in-package-of-symbol (concatenate 'string "UPDATE-" (symbol-name field) "I")
            field)))
      (fast-name (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-FAST")
          name)))
    `(progn (definline ,NAME
        (idx x ,STOBJ)
        (declare (xargs :guard (and (natp idx) ,GUARD) :stobjs ,STOBJ))
        (mbe :logic (,UPDATE (nfix idx) ,FIX ,STOBJ)
          :exec (if (and (< idx (,LENGTH ,STOBJ)) ,CHECK)
            (,UPDATE idx x ,STOBJ)
            (ec-call (,UPDATE idx x ,STOBJ)))))
      (definline ,FAST-NAME
        (idx x ,STOBJ)
        (declare (xargs :guard (and (natp idx) (< idx (,LENGTH ,STOBJ)) ,GUARD)
            :stobjs ,STOBJ))
        (mbe :logic (,UPDATE (nfix idx) ,FIX ,STOBJ)
          :exec ,(IF (EQUAL CHECK ''T)
     `(,UPDATE IDX X ,STOBJ)
     `(IF ,CHECK
          (,UPDATE IDX X ,STOBJ)
          (EC-CALL (,UPDATE IDX X ,STOBJ)))))))))

(defun def-slot-set-fn
  (name stobj field update guard fix check)
  (let* ((update (or update
         (intern-in-package-of-symbol (concatenate 'string "UPDATE-" (symbol-name field))
           field))))
    `(definline ,NAME
      (x ,STOBJ)
      (declare (xargs :guard ,GUARD :stobjs ,STOBJ))
      (mbe :logic (,UPDATE ,FIX ,STOBJ)
        :exec (if ,CHECK
          (,UPDATE x ,STOBJ)
          (ec-call (,UPDATE x ,STOBJ)))))))