1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
|
;; 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-pair-ordered-symbol-alistp
(implies (ordered-symbol-alistp list)
(ordered-symbol-alistp (delete-pair 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-pair-open-channel-listp
(implies (open-channel-listp list)
(open-channel-listp (delete-pair 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-pair-open-channels-p
(implies (open-channels-p list)
(open-channels-p (delete-pair 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.
(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))))
|