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 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
|
include ../Makefile-generic
ACL2 = ../../saved_acl2
BASICS = app append base10-digit-charp coerce consless-listp combine \
explode-atom explode-nonnegative-integer flatten \
intern-in-package-of-symbol list-fix nat-listp nthcdr \
partition pos-listp repeat revappend reverse sign-byte signed-byte-listp \
string-append sum-list take unsigned-byte-listp z-listp
IO = update-state open-input-channels open-input-channel close-input-channel \
read-byte read-char peek-char read-object \
file-measure read-file-bytes read-file-characters read-ints \
nthcdr-bytes take-bytes
UNICODE = uchar utf8-table35 utf8-table36 utf8-encode utf8-decode read-utf8
BOOKS = $(BASICS) $(IO) $(UNICODE)
app.cert: app.lisp
app.cert: list-fix.cert
app.cert: take.cert
app.cert: nthcdr.cert
# app.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
append.cert: append.lisp
# append.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
base10-digit-charp.cert: base10-digit-charp.lisp
coerce.cert: coerce.lisp
consless-listp.cert: consless-listp.lisp
consless-listp.cert: app.cert
combine.cert: combine.lisp
combine.cert: sign-byte.cert
combine.cert: unsigned-byte-listp.cert
combine.cert: signed-byte-listp.cert
explode-atom.cert: explode-atom.lisp
explode-atom.cert: base10-digit-charp.cert
explode-atom.cert: explode-nonnegative-integer.cert
explode-nonnegative-integer.cert: explode-nonnegative-integer.lisp
explode-nonnegative-integer.cert: revappend.cert
explode-nonnegative-integer.cert: base10-digit-charp.cert
# explode-nonnegative-integer.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/floor-mod/floor-mod.cert
flatten.cert: flatten.lisp
flatten.cert: app.cert
flatten.cert: consless-listp.cert
intern-in-package-of-symbol.cert: intern-in-package-of-symbol.lisp
list-fix.cert: list-fix.lisp
nat-listp.cert: nat-listp.lisp
nat-listp.cert: app.cert
nthcdr.cert: nthcdr.lisp
# nthcdr.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
partition.cert: partition.lisp
partition.cert: flatten.cert
partition.cert: sum-list.cert
partition.cert: z-listp.cert
partition.cert: nthcdr.cert
# partition.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic/top-with-meta.cert
pos-listp.cert: pos-listp.lisp
pos-listp.cert: app.cert
repeat.cert: repeat.lisp
repeat.cert: take.cert
revappend.cert: revappend.lisp
# revappend.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
reverse.cert: reverse.lisp
reverse.cert: revappend.cert
reverse.cert: coerce.cert
sign-byte.cert: sign-byte.lisp
signed-byte-listp.cert: signed-byte-listp.lisp
signed-byte-listp.cert: unsigned-byte-listp.cert
# signed-byte-listp.cert: $(ACL2_SYSTEM_BOOKS)/ihs/logops-lemmas.cert
# signed-byte-listp.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
# signed-byte-listp.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/floor-mod/floor-mod.cert
string-append.cert: string-append.lisp
string-append.cert: append.cert
string-append.cert: coerce.cert
sum-list.cert: sum-list.lisp
sum-list.cert: nat-listp.cert
take.cert: take.lisp
# take.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
unsigned-byte-listp.cert: unsigned-byte-listp.lisp
unsigned-byte-listp.cert: take.cert
unsigned-byte-listp.cert: nat-listp.cert
unsigned-byte-listp.cert: repeat.cert
# unsigned-byte-listp.cert: $(ACL2_SYSTEM_BOOKS)/ihs/logops-lemmas.cert
# unsigned-byte-listp.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
# unsigned-byte-listp.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/floor-mod/floor-mod.cert
z-listp.cert: z-listp.lisp
z-listp.cert: app.cert
update-state.cert: update-state.lisp
open-input-channels.cert: open-input-channels.lisp
open-input-channel.cert: open-input-channel.lisp
open-input-channel.cert: update-state.cert
open-input-channel.cert: open-input-channels.cert
open-input-channel.cert: explode-nonnegative-integer.cert
open-input-channel.cert: intern-in-package-of-symbol.cert
open-input-channel.cert: coerce.cert
# open-input-channel.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
close-input-channel.cert: close-input-channel.lisp
close-input-channel.cert: update-state.cert
close-input-channel.cert: open-input-channels.cert
read-byte.cert: read-byte.lisp
read-byte.cert: update-state.cert
read-byte.cert: open-input-channels.cert
read-byte.cert: unsigned-byte-listp.cert
read-byte.cert: signed-byte-listp.cert
read-char.cert: read-char.lisp
read-char.cert: update-state.cert
read-char.cert: open-input-channels.cert
peek-char.cert: peek-char.lisp
peek-char.cert: update-state.cert
peek-char.cert: open-input-channels.cert
read-object.cert: read-object.lisp
read-object.cert: update-state.cert
read-object.cert: open-input-channels.cert
file-measure.cert: file-measure.lisp
file-measure.cert: update-state.cert
file-measure.cert: open-input-channels.cert
read-file-bytes.cert: read-file-bytes.lisp
read-file-bytes.cert: file-measure.cert
read-file-bytes.cert: unsigned-byte-listp.cert
read-file-bytes.cert: open-input-channel.cert
read-file-bytes.cert: close-input-channel.cert
read-file-bytes.cert: read-byte.cert
read-file-characters.cert: read-file-characters.lisp
read-file-characters.cert: file-measure.cert
read-file-characters.cert: open-input-channel.cert
read-file-characters.cert: read-char.cert
read-file-characters.cert: close-input-channel.cert
read-ints.cert: read-ints.lisp
read-ints.cert: read-byte.cert
read-ints.cert: unsigned-byte-listp.cert
read-ints.cert: signed-byte-listp.cert
read-ints.cert: sign-byte.cert
read-ints.cert: combine.cert
# read-ints.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
nthcdr-bytes.cert: nthcdr-bytes.lisp
nthcdr-bytes.cert: read-byte.cert
nthcdr-bytes.cert: read-file-bytes.cert
take-bytes.cert: take-bytes.lisp
take-bytes.cert: read-byte.cert
take-bytes.cert: read-file-bytes.cert
take-bytes.cert: nthcdr-bytes.cert
uchar.cert: uchar.lisp
utf8-table35.cert: utf8-table35.lisp
utf8-table35.cert: uchar.cert
utf8-table35.cert: unsigned-byte-listp.cert
utf8-table35.cert: signed-byte-listp.cert
utf8-table36.cert: utf8-table36.lisp
utf8-table36.cert: uchar.cert
utf8-table36.cert: unsigned-byte-listp.cert
utf8-table36.cert: signed-byte-listp.cert
utf8-encode.cert: utf8-encode.lisp
utf8-encode.cert: utf8-table35.cert
utf8-encode.cert: utf8-table36.cert
utf8-encode.cert: append.cert
utf8-encode.cert: signed-byte-listp.cert
utf8-decode.cert: utf8-decode.lisp
utf8-decode.cert: uchar.cert
utf8-decode.cert: utf8-table35.cert
utf8-decode.cert: utf8-table36.cert
utf8-decode.cert: utf8-encode.cert
utf8-decode.cert: partition.cert
utf8-decode.cert: nthcdr.cert
utf8-decode.cert: signed-byte-listp.cert
utf8-decode.cert: revappend.cert
# utf8-decode.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
read-utf8.cert: read-utf8.lisp
read-utf8.cert: utf8-decode.cert
read-utf8.cert: take-bytes.cert
read-utf8.cert: open-input-channel.cert
read-utf8.cert: close-input-channel.cert
read-utf8.cert: signed-byte-listp.cert
# read-utf8.cert: $(ACL2_SYSTEM_BOOKS)/arithmetic-3/bind-free/top.cert
|