acl2-books-source 4.3-3 / usr / share / acl2-4.3 / books / unicode / open-input-channels.lisp

;; Processing Unicode Files with ACL2
;; Copyright (C) 2005-2006 by Jared Davis <jared@cs.utexas.edu>
;;
;; This program is free software; you can redistribute it and/or modify it
;; under the terms of the GNU General Public License as published by the Free
;; Software Foundation; either version 2 of the License, or (at your option)
;; any later version.
;;
;; This program is distributed in the hope that it will be useful but WITHOUT
;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
;; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
;; more details.
;;
;; You should have received a copy of the GNU General Public License along with
;; this program; if not, write to the Free Software Foundation, Inc., 59 Temple
;; Place - Suite 330, Boston, MA 02111-1307, USA.

(in-package "ACL2")

; The open input channels table is the logical fiction that supports our
; ability to read from files.  When a file is opened, it is added to this
; table.  When it is read from, we consult this table to find its contents and
; update the table to consume one object of input.  When it is closed, this
; table must be updated to handle the closure.  The table itself is just an
; object that satisfies open-channels-p, and it is easy to show that calling
; open-input-channels on a state returns an object of this form.

(defthm open-input-channels-ok
  (implies (state-p1 state)
           (open-channels-p (open-input-channels state))))

(defthm ordered-symbol-alistp-of-open-input-channels
  (implies (state-p1 state)
           (ordered-symbol-alistp (open-input-channels state))))



; We typically update this table by using the function add-pair.  We will find
; several lemmas about this function to be useful.  First, we give a very nice
; little rewrite rule that shows that add-pair does indeed act as we would
; expect with respect to assoc-equal.  (Note that we canonicalize all uses of
; assoc-eq and assoc to their assoc-equal form, so this will cover those cases
; as well after rewriting.)

(defthm add-pair-assoc-equal
  (equal (assoc-equal key1 (add-pair key2 val alist))
         (if (equal key1 key2)
             (cons key2 val)
           (assoc-equal key1 alist))))



; In order to prove that an update to our open channels list preserves the
; basic open-channels-p property, we will need to show that such updates
; satisfy both ordered-symbol-alistp and open-channel-listp.  We introduce the
; lemmas below towards this purpose.

(defthm add-pair-ordered-symbol-alistp
  (implies (ordered-symbol-alistp list)
           (equal (ordered-symbol-alistp (add-pair key val list))
                  (symbolp key))))

(defthm delete-assoc-eq-ordered-symbol-alistp
  (implies (ordered-symbol-alistp list)
           (ordered-symbol-alistp (delete-assoc-eq key list))))

(defthm add-pair-open-channel-listp
  (implies (open-channel-listp list)
           (equal (open-channel-listp (add-pair key val list))
                  (open-channel1 val))))

(defthm delete-assoc-eq-open-channel-listp
  (implies (open-channel-listp list)
           (open-channel-listp (delete-assoc-eq key list))))

(defthm add-pair-open-channels-p
  (implies (open-channels-p list)
           (equal (open-channels-p (add-pair key val list))
                  (and (symbolp key)
                       (open-channel1 val)))))

(defthm delete-assoc-eq-open-channels-p
  (implies (open-channels-p list)
           (open-channels-p (delete-assoc-eq key list))))



; If we grab something out of the open channels list, what can we say about it?
; Well, by looking at the definition of open-channel-listp, the most obvious
; thing to do is to prove that it is an open-channel1, and then to prove
; properties about such objects instead of having to reason about assoc'ing
; into an open channel list all the time.  Towards this end, we will show that
; if we find a channel in an open-channels-p list, it is an open-channel1, and
; if we have an open-channel1, we know that its contents are a typed list of
; the correct type.

(defthm open-channels-assoc
  (implies (and (open-channels-p x)
                (assoc-equal channel x))
           (open-channel1 (cdr (assoc-equal channel x)))))

(defthm open-channel1-contents-type
  (implies (open-channel1 x)
           (typed-io-listp (cdr x) (cadar x))))



; Now, here is a lemma that we'll use to show that our reading operations
; preserve open-channel1.  The form (cons (car x) (cddr x)) below is a basic
; operation which preserves the header of an open channel's contents, while
; eliminating the first element of its contents.  Here we show that this usage
; preserves open-channel1.

(defthm open-channel1-advance
  (implies (open-channel1 x)
           (open-channel1 (cons (car x) (cddr x)))))



; All of our reading operations require that we have an open input channel of
; the right type, i.e., that (open-input-channel-p1 channel type state) is true
; of our state.  What can we conclude given that this holds for some state?
; First off, we know that looking up the channel in the open-input-channels
; list will be successful.  Secondly, we know that the type of the channel
; returned will be the same as type in our call to open-input-channel-p1.

; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.]
; (local (defthm assoc-eq-is-assoc-equal
;          (equal (assoc-eq a x)
;                 (assoc-equal a x))))

(defthm assoc-open-input-channels-exists
  (implies (open-input-channel-p1 channel type state)
           (assoc-equal channel (open-input-channels state))))

(defthm assoc-open-input-channels-type
  (implies (open-input-channel-p1 channel type state)
           (equal (cadadr (assoc-equal channel (open-input-channels state)))
                  type)))



; We can go further and say that given an open input channel and a state,
; the contents of the channel are a typed io list of the correct type.

(defthm assoc-open-input-channels-contents
  (implies (and (state-p1 state)
                (open-input-channel-p1 channel type state))
           (typed-io-listp (cddr (assoc-equal channel (open-input-channels state)))
                           type))
  :hints(("Goal" :use (:instance open-input-channels-ok))))



; We're now ready for a really ugly but important lemma.  This is the core
; operation that read-byte$, read-char$, and read-object use in order to
; "consume" an object from their input streams.  We show that when they do
; this, they still have an open-channels-p.

(defthm add-pair-open-channels
  (implies (and (state-p1 state)
                (open-input-channel-p1 channel type state)
                (symbolp channel))
           (open-channels-p
            (add-pair channel
                      (cons (cadr (assoc-equal channel
                                               (open-input-channels state)))
                            (cdddr (assoc-equal channel
                                                (open-input-channels state))))
                      (open-input-channels state))))
  :hints(("Goal" :in-theory (disable open-input-channels
                                     open-channels-p))))





(defthm equal-of-update-open-input-channels-with-state
  (implies (state-p1 state)
           (equal (equal (update-open-input-channels x state) state)
                  (equal x (open-input-channels state))))
  :hints(("Goal" :in-theory (enable update-open-input-channels
                                    open-input-channels
                                    state-p1))))

(defthm equal-of-add-pair-with-channels
  (implies (ordered-symbol-alistp channels)
           (equal (equal (add-pair channel x channels) channels)
                  (equal (assoc-equal channel channels)
                         (cons channel x))))
  :hints(("Goal"
          :in-theory (enable ordered-symbol-alistp add-pair)
          :induct (add-pair channel x channels))))