• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
      • Open-channel-lemmas
      • Std/io/read-char$
      • Std/io/read-object
      • Std/io/open-output-channel
      • Unsound-read
      • Read-string
      • Read-bytes$
      • File-measure
      • Read-bytes$-n
      • Std/io/read-byte$
      • Std/io/open-input-channel
      • Read-file-lines-no-newlines
      • Print-compressed
      • Nthcdr-bytes
      • Read-file-lines
      • Std/io/close-output-channel
      • Read-file-characters
      • Read-file-bytes
      • Print-legibly
      • Std/io/close-input-channel
      • Read-file-objects
      • Logical-story-of-io
      • Take-bytes
      • Std/io/peek-char$
      • Read-file-characters-rev
      • Read-file-as-string
      • Std/io/write-byte$
      • Std/io/set-serialize-character
      • Std/io/print-object$
      • Std/io/princ$
      • Std/io/read-file-into-string
      • *file-types*
    • Oslib
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/io

File-measure

A measure for admitting functions that read from files.

Signature: (file-measure channel state-state) returns a natural number.

• channel may be any symbol but is typically an open input channel.
• state-state is typically the ACL2 state.

This is a logic-mode function, but its logical definition is tricky; see logical-story-of-io. The basic gist is that it returns how many objects are left in the channel and hence how many functions can still be read.

This function is only meant to be used to admit functions, and cannot be executed on the real ACL2 state.

Definitions and Theorems

Function: file-measure

(defun file-measure (channel state-state)
 (declare (xargs :guard (and (symbolp channel)
                             (state-p1 state-state))))
 (+
  (len (cddr (assoc-equal channel
                          (open-input-channels state-state))))
  (if
   (consp (cddr (assoc-equal channel
                             (open-input-channels state-state))))
   (if
    (cdr
      (last (cddr (assoc-equal channel
                               (open-input-channels state-state)))))
    1
    0)
   (if (cddr (assoc-equal channel
                          (open-input-channels state-state)))
       1
     0))))

Theorem: file-measure-of-read-byte$-weak

(defthm file-measure-of-read-byte$-weak
  (<= (file-measure channel
                    (mv-nth 1 (read-byte$ channel state)))
      (file-measure channel state))
  :rule-classes (:rewrite :linear))

Theorem: file-measure-of-read-byte$-strong

(defthm file-measure-of-read-byte$-strong
  (implies (mv-nth 0 (read-byte$ channel state))
           (< (file-measure channel
                            (mv-nth 1 (read-byte$ channel state)))
              (file-measure channel state)))
  :rule-classes (:rewrite :linear))

Theorem: file-measure-of-read-byte$-rw

(defthm file-measure-of-read-byte$-rw
  (implies
       (mv-nth 0 (read-byte$ channel state))
       (equal (file-measure channel
                            (mv-nth 1 (read-byte$ channel state)))
              (+ -1 (file-measure channel state)))))

Theorem: file-measure-of-read-char$-weak

(defthm file-measure-of-read-char$-weak
  (<= (file-measure channel
                    (mv-nth 1 (read-char$ channel state)))
      (file-measure channel state))
  :rule-classes (:rewrite :linear))

Theorem: file-measure-of-read-char$-strong

(defthm file-measure-of-read-char$-strong
  (implies (mv-nth 0 (read-char$ channel state))
           (< (file-measure channel
                            (mv-nth 1 (read-char$ channel state)))
              (file-measure channel state)))
  :rule-classes (:rewrite :linear))

Theorem: file-measure-of-read-char$-rw

(defthm file-measure-of-read-char$-rw
  (implies
       (mv-nth 0 (read-char$ channel state))
       (equal (file-measure channel
                            (mv-nth 1 (read-char$ channel state)))
              (1- (file-measure channel state)))))

Theorem: file-measure-of-read-object-weak

(defthm file-measure-of-read-object-weak
  (<= (file-measure channel
                    (mv-nth 2 (read-object channel state)))
      (file-measure channel state))
  :rule-classes (:rewrite :linear))

Theorem: file-measure-of-read-object-rw

(defthm file-measure-of-read-object-rw
  (implies
       (not (mv-nth 0 (read-object channel state)))
       (equal (file-measure channel
                            (mv-nth 2 (read-object channel state)))
              (1- (file-measure channel state)))))

Theorem: file-measure-of-read-object-strong

(defthm file-measure-of-read-object-strong
  (implies (not (mv-nth 0 (read-object channel state)))
           (< (file-measure channel
                            (mv-nth 2 (read-object channel state)))
              (file-measure channel state)))
  :rule-classes (:rewrite :linear))

Theorem: file-measure-type

(defthm file-measure-type
  (natp (file-measure channel state))
  :rule-classes :type-prescription)