file-measure

(in-package "ACL2")

(defsection file-measure
  :parents (std/io)
  :short "A measure for admitting functions that read from files."
  :long "<p><b>Signature:</b> @(call file-measure) returns a natural
number.</p>

<ul>

<li>@('channel') may be any symbol but is typically an open input channel.</li>

<li>@('state-state') is typically the ACL2 @(see state).</li>

</ul>

<p>This is a @(see logic)-mode function, but its logical definition is tricky;
see @(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.</p>

<p>This function is only meant to be used to admit functions, and cannot be
executed on the real ACL2 @(see state).</p>"
  (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))))
  (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))
  (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))
  (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)))))
  (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))
  (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))
  (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)))))
  (local (in-theory (enable read-acl2-oracle
        update-acl2-oracle
        put-global
        iprint-oracle-updates)))
  (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))
  (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)))))
  (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))
  (defthm file-measure-type
    (natp (file-measure channel state))
    :rule-classes :type-prescription))