1(INCLUDE-BOOK "problem-set-1-answers") 2 3; NOTE: Only the forms above are evaluated (as opposed the ones below, 4; which merely are read) when translating to ML. On a related note: 5; the following IN-PACKAGE form is for use by a2ml, but all forms in 6; this file assume that the current package is actually "ACL2". 7 8(IN-PACKAGE "M1") 9 10(DEFUN M1::NEXT-INST (M1::S) (M1::NTH (M1::PC M1::S) (M1::PROGRAM M1::S))) 11 12(DEFUN M1::EXECUTE-ICONST (M1::INST M1::S) 13 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 14 (M1::LOCALS M1::S) 15 (M1::PUSH (M1::ARG1 M1::INST) 16 (M1::STACK M1::S)) 17 (M1::PROGRAM M1::S))) 18 19(DEFUN M1::EXECUTE-ILOAD (M1::INST M1::S) 20 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 21 (M1::LOCALS M1::S) 22 (M1::PUSH (M1::NTH (M1::ARG1 M1::INST) 23 (M1::LOCALS M1::S)) 24 (M1::STACK M1::S)) 25 (M1::PROGRAM M1::S))) 26 27(DEFUN 28 M1::EXECUTE-IADD (M1::INST M1::S) 29 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 30 (M1::LOCALS M1::S) 31 (M1::PUSH (BINARY-+ (M1::TOP (M1::POP (M1::STACK M1::S))) 32 (M1::TOP (M1::STACK M1::S))) 33 (M1::POP (M1::POP (M1::STACK M1::S)))) 34 (M1::PROGRAM M1::S))) 35 36(DEFUN M1::EXECUTE-ISTORE (M1::INST M1::S) 37 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 38 (M1::UPDATE-NTH (M1::ARG1 M1::INST) 39 (M1::TOP (M1::STACK M1::S)) 40 (M1::LOCALS M1::S)) 41 (M1::POP (M1::STACK M1::S)) 42 (M1::PROGRAM M1::S))) 43 44(DEFUN 45 M1::EXECUTE-ISUB (M1::INST M1::S) 46 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 47 (M1::LOCALS M1::S) 48 (M1::PUSH (BINARY-+ (M1::TOP (M1::POP (M1::STACK M1::S))) 49 (UNARY-- (M1::TOP (M1::STACK M1::S)))) 50 (M1::POP (M1::POP (M1::STACK M1::S)))) 51 (M1::PROGRAM M1::S))) 52 53(DEFUN 54 M1::EXECUTE-IMUL (M1::INST M1::S) 55 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 56 (M1::LOCALS M1::S) 57 (M1::PUSH (BINARY-* (M1::TOP (M1::POP (M1::STACK M1::S))) 58 (M1::TOP (M1::STACK M1::S))) 59 (M1::POP (M1::POP (M1::STACK M1::S)))) 60 (M1::PROGRAM M1::S))) 61 62(DEFUN M1::EXECUTE-GOTO (M1::INST M1::S) 63 (M1::MAKE-STATE (BINARY-+ (M1::ARG1 M1::INST) 64 (M1::PC M1::S)) 65 (M1::LOCALS M1::S) 66 (M1::STACK M1::S) 67 (M1::PROGRAM M1::S))) 68 69(DEFUN M1::EXECUTE-IFLE (M1::INST M1::S) 70 (M1::MAKE-STATE (IF (NOT (< '0 (M1::TOP (M1::STACK M1::S)))) 71 (BINARY-+ (M1::ARG1 M1::INST) 72 (M1::PC M1::S)) 73 (BINARY-+ '1 (M1::PC M1::S))) 74 (M1::LOCALS M1::S) 75 (M1::POP (M1::STACK M1::S)) 76 (M1::PROGRAM M1::S))) 77 78(DEFUN 79 M1::DO-INST (M1::INST M1::S) 80 (IF (EQUAL (M1::OP-CODE M1::INST) 81 'M1::ICONST) 82 (M1::EXECUTE-ICONST M1::INST M1::S) 83 (IF (EQUAL (M1::OP-CODE M1::INST) 84 'M1::ILOAD) 85 (M1::EXECUTE-ILOAD M1::INST M1::S) 86 (IF (EQUAL (M1::OP-CODE M1::INST) 87 'M1::ISTORE) 88 (M1::EXECUTE-ISTORE M1::INST M1::S) 89 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::IADD) 90 (M1::EXECUTE-IADD M1::INST M1::S) 91 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::ISUB) 92 (M1::EXECUTE-ISUB M1::INST M1::S) 93 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::IMUL) 94 (M1::EXECUTE-IMUL M1::INST M1::S) 95 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::GOTO) 96 (M1::EXECUTE-GOTO M1::INST M1::S) 97 (IF (EQUAL (M1::OP-CODE M1::INST) 'M1::IFLE) 98 (M1::EXECUTE-IFLE M1::INST M1::S) 99 M1::S))))))))) 100 101(DEFUN M1::STEP (M1::S) (M1::DO-INST (M1::NEXT-INST M1::S) M1::S)) 102 103(DEFUN M1::RUN (M1::SCHED M1::S) 104 (IF (ENDP M1::SCHED) 105 M1::S 106 (M1::RUN (CDR M1::SCHED) 107 (M1::STEP M1::S)))) 108 109(DEFTHM M1::FACTORIAL-EXAMPLE-0 110 (EQUAL (M1::RUN '(0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 111 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 112 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 113 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 114 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) 115 (M1::MAKE-STATE '0 116 '(5 0) 117 'NIL 118 '((M1::ICONST 1) 119 (M1::ISTORE 1) 120 (M1::ILOAD 0) 121 (M1::IFLE 10) 122 (M1::ILOAD 0) 123 (M1::ILOAD 1) 124 (M1::IMUL) 125 (M1::ISTORE 1) 126 (M1::ILOAD 0) 127 (M1::ICONST 1) 128 (M1::ISUB) 129 (M1::ISTORE 0) 130 (M1::GOTO -10) 131 (M1::ILOAD 1) 132 (M1::HALT)))) 133 '(14 (0 120) 134 (120) 135 ((M1::ICONST 1) 136 (M1::ISTORE 1) 137 (M1::ILOAD 0) 138 (M1::IFLE 10) 139 (M1::ILOAD 0) 140 (M1::ILOAD 1) 141 (M1::IMUL) 142 (M1::ISTORE 1) 143 (M1::ILOAD 0) 144 (M1::ICONST 1) 145 (M1::ISUB) 146 (M1::ISTORE 0) 147 (M1::GOTO -10) 148 (M1::ILOAD 1) 149 (M1::HALT))))) 150 151(DEFUN M1::IFACT-LOOP-SCHED (M1::N) 152 (IF (ZP M1::N) 153 (M1::REPEAT '0 '4) 154 (M1::APP (M1::REPEAT '0 '11) 155 (M1::IFACT-LOOP-SCHED (BINARY-+ '-1 M1::N))))) 156 157(DEFUN M1::IFACT-SCHED (M1::N) 158 (M1::APP (M1::REPEAT '0 '2) 159 (M1::IFACT-LOOP-SCHED M1::N))) 160 161(DEFUN M1::! (M1::N) 162 (IF (ZP M1::N) 163 '1 164 (BINARY-* M1::N (M1::! (BINARY-+ '-1 M1::N))))) 165 166(DEFUN 167 M1::TEST-IFACT (M1::N) 168 (M1::TOP (M1::STACK (M1::RUN (M1::IFACT-SCHED M1::N) 169 (M1::MAKE-STATE '0 170 (CONS M1::N (CONS '0 'NIL)) 171 'NIL 172 '((M1::ICONST 1) 173 (M1::ISTORE 1) 174 (M1::ILOAD 0) 175 (M1::IFLE 10) 176 (M1::ILOAD 0) 177 (M1::ILOAD 1) 178 (M1::IMUL) 179 (M1::ISTORE 1) 180 (M1::ILOAD 0) 181 (M1::ICONST 1) 182 (M1::ISUB) 183 (M1::ISTORE 0) 184 (M1::GOTO -10) 185 (M1::ILOAD 1) 186 (M1::HALT))))))) 187 188(DEFTHM M1::FACTORIAL-EXAMPLE-1 (EQUAL (M1::TEST-IFACT '5) (M1::! '5))) 189 190(DEFTHM M1::FACTORIAL-EXAMPLE-2 191 (EQUAL (M1::TEST-IFACT '1000) 192 (M1::! '1000))) 193 194(DEFUN M1::EVEN-SCHED (M1::I) 195 (IF (ZP M1::I) 196 (M1::REPEAT '0 '4) 197 (IF (EQUAL M1::I '1) 198 (M1::REPEAT '0 '8) 199 (M1::APP (M1::REPEAT '0 '11) 200 (M1::EVEN-SCHED (BINARY-+ '-2 M1::I)))))) 201 202(DEFUN M1::TEST-EVEN (M1::I) 203 (M1::TOP (M1::STACK (M1::RUN (M1::EVEN-SCHED M1::I) 204 (M1::MAKE-STATE '0 205 (CONS M1::I 'NIL) 206 'NIL 207 '((M1::ILOAD 0) 208 (M1::IFLE 12) 209 (M1::ILOAD 0) 210 (M1::ICONST 1) 211 (M1::ISUB) 212 (M1::IFLE 6) 213 (M1::ILOAD 0) 214 (M1::ICONST 2) 215 (M1::ISUB) 216 (M1::ISTORE 0) 217 (M1::GOTO -10) 218 (M1::ICONST 0) 219 (M1::HALT) 220 (M1::ICONST 1) 221 (M1::HALT))))))) 222 223(DEFTHM M1::TEST-EVEN-THEOREM 224 (IF (EQUAL (M1::TEST-EVEN '18) '1) 225 (IF (EQUAL (M1::TEST-EVEN '19) '0) 226 (IF (EQUAL (M1::TEST-EVEN '235) '0) 227 (EQUAL (M1::TEST-EVEN '234) '1) 228 'NIL) 229 'NIL) 230 'NIL)) 231 232(DEFUN M1::COLLECT-AT-END (LIST M1::E) 233 (IF (M1::MEMBER M1::E LIST) 234 LIST (M1::APP LIST (CONS M1::E 'NIL)))) 235 236(DEFTHM M1::NTH-NIL (EQUAL (M1::NTH M1::N 'NIL) 'NIL)) 237 238(DEFTHM M1::ACL2-COUNT-NTH 239 (IMPLIES (CONSP LIST) 240 (< (ACL2-COUNT (M1::NTH M1::N LIST)) 241 (ACL2-COUNT LIST)))) 242 243(DEFUN M1::COLLECT-VARS-IN-EXPR 244 (M1::VARS M1::EXPR) 245 (IF (ATOM M1::EXPR) 246 (IF (SYMBOLP M1::EXPR) 247 (M1::COLLECT-AT-END M1::VARS M1::EXPR) 248 M1::VARS) 249 (M1::COLLECT-VARS-IN-EXPR 250 (M1::COLLECT-VARS-IN-EXPR M1::VARS (M1::NTH '0 M1::EXPR)) 251 (M1::NTH '2 M1::EXPR)))) 252 253(MUTUAL-RECURSION 254 (DEFUN M1::COLLECT-VARS-IN-STMT* 255 (M1::VARS M1::STMT-LIST) 256 (IF (ENDP M1::STMT-LIST) 257 M1::VARS 258 (M1::COLLECT-VARS-IN-STMT* 259 (M1::COLLECT-VARS-IN-STMT M1::VARS (CAR M1::STMT-LIST)) 260 (CDR M1::STMT-LIST)))) 261 (DEFUN 262 M1::COLLECT-VARS-IN-STMT 263 (M1::VARS M1::STMT) 264 (IF (EQUAL (M1::NTH '1 M1::STMT) 'M1::=) 265 (M1::COLLECT-VARS-IN-EXPR 266 (M1::COLLECT-AT-END M1::VARS (M1::NTH '0 M1::STMT)) 267 (M1::NTH '2 M1::STMT)) 268 (IF (EQUAL (M1::NTH '0 M1::STMT) 'M1::WHILE) 269 (M1::COLLECT-VARS-IN-STMT* 270 (M1::COLLECT-VARS-IN-EXPR M1::VARS (M1::NTH '1 M1::STMT)) 271 (CDR (CDR M1::STMT))) 272 (IF (EQUAL (M1::NTH '0 M1::STMT) 273 'M1::RETURN) 274 (M1::COLLECT-VARS-IN-EXPR M1::VARS (M1::NTH '1 M1::STMT)) 275 M1::VARS))))) 276 277(DEFUN M1::OP! (M1::OP) 278 (IF (EQUAL M1::OP '+) 279 '((M1::IADD)) 280 (IF (EQUAL M1::OP '-) 281 '((M1::ISUB)) 282 (IF (EQUAL M1::OP '*) 283 '((M1::IMUL)) 284 '((M1::ILLEGAL)))))) 285 286(DEFUN M1::ILOAD! (M1::VARS M1::VAR) 287 (CONS (CONS 'M1::ILOAD 288 (CONS (M1::INDEX M1::VAR M1::VARS) 289 'NIL)) 290 'NIL)) 291 292(DEFUN M1::ICONST! (M1::N) (CONS (CONS 'M1::ICONST (CONS M1::N 'NIL)) 'NIL)) 293 294(DEFUN M1::EXPR! (M1::VARS M1::EXPR) 295 (IF (ATOM M1::EXPR) 296 (IF (SYMBOLP M1::EXPR) 297 (M1::ILOAD! M1::VARS M1::EXPR) 298 (M1::ICONST! M1::EXPR)) 299 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '0 M1::EXPR)) 300 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '2 M1::EXPR)) 301 (M1::OP! (M1::NTH '1 M1::EXPR)))))) 302 303(DEFUN M1::IFLE! (M1::OFFSET) 304 (CONS (CONS 'M1::IFLE (CONS M1::OFFSET 'NIL)) 305 'NIL)) 306 307(DEFUN M1::GOTO! (M1::OFFSET) 308 (CONS (CONS 'M1::GOTO (CONS M1::OFFSET 'NIL)) 309 'NIL)) 310 311(DEFUN 312 M1::WHILE! (M1::TEST-CODE M1::BODY-CODE) 313 (M1::APP 314 M1::TEST-CODE 315 (M1::APP 316 (M1::IFLE! (BINARY-+ '2 (M1::LEN M1::BODY-CODE))) 317 (M1::APP 318 M1::BODY-CODE 319 (M1::GOTO! (UNARY-- (BINARY-+ (M1::LEN M1::TEST-CODE) 320 (BINARY-+ '1 321 (M1::LEN M1::BODY-CODE))))))))) 322 323(DEFUN M1::TEST! (M1::VARS M1::TEST) 324 (IF (EQUAL (M1::NTH '1 M1::TEST) '>) 325 (IF (EQUAL (M1::NTH '2 M1::TEST) '0) 326 (M1::EXPR! M1::VARS (M1::NTH '0 M1::TEST)) 327 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '0 M1::TEST)) 328 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '2 M1::TEST)) 329 '((M1::ISUB))))) 330 '((M1::ILLEGAL)))) 331 332(DEFUN M1::ISTORE! (M1::VARS M1::VAR) 333 (CONS (CONS 'M1::ISTORE 334 (CONS (M1::INDEX M1::VAR M1::VARS) 335 'NIL)) 336 'NIL)) 337 338(MUTUAL-RECURSION 339 (DEFUN M1::STMT*! (M1::VARS M1::STMT-LIST) 340 (IF (ENDP M1::STMT-LIST) 341 'NIL 342 (M1::APP (M1::STMT! M1::VARS (CAR M1::STMT-LIST)) 343 (M1::STMT*! M1::VARS (CDR M1::STMT-LIST))))) 344 (DEFUN M1::STMT! (M1::VARS M1::STMT) 345 (IF (EQUAL (M1::NTH '1 M1::STMT) 'M1::=) 346 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '2 M1::STMT)) 347 (M1::ISTORE! M1::VARS (M1::NTH '0 M1::STMT))) 348 (IF (EQUAL (M1::NTH '0 M1::STMT) 'M1::WHILE) 349 (M1::WHILE! (M1::TEST! M1::VARS (M1::NTH '1 M1::STMT)) 350 (M1::STMT*! M1::VARS (CDR (CDR M1::STMT)))) 351 (IF (EQUAL (M1::NTH '0 M1::STMT) 352 'M1::RETURN) 353 (M1::APP (M1::EXPR! M1::VARS (M1::NTH '1 M1::STMT)) 354 '((M1::HALT))) 355 '((M1::ILLEGAL))))))) 356 357(DEFUN M1::COMPILE (M1::FORMALS M1::STMT-LIST) 358 (M1::STMT*! (M1::COLLECT-VARS-IN-STMT* M1::FORMALS M1::STMT-LIST) 359 M1::STMT-LIST)) 360 361(DEFTHM M1::EXAMPLE-COMPILATION-1 362 (EQUAL (M1::COMPILE '(M1::N) 363 '((M1::A M1::= 1) 364 (M1::WHILE (M1::N > 0) 365 (M1::A M1::= (M1::N * M1::A)) 366 (M1::N M1::= (M1::N - 1))) 367 (M1::RETURN M1::A))) 368 '((M1::ICONST 1) 369 (M1::ISTORE 1) 370 (M1::ILOAD 0) 371 (M1::IFLE 10) 372 (M1::ILOAD 0) 373 (M1::ILOAD 1) 374 (M1::IMUL) 375 (M1::ISTORE 1) 376 (M1::ILOAD 0) 377 (M1::ICONST 1) 378 (M1::ISUB) 379 (M1::ISTORE 0) 380 (M1::GOTO -10) 381 (M1::ILOAD 1) 382 (M1::HALT)))) 383 384(DEFTHM M1::EXAMPLE-COMPILATION-2 385 (EQUAL (M1::COMPILE '(M1::N M1::K) 386 '((M1::A M1::= 0) 387 (M1::WHILE (M1::N > M1::K) 388 (M1::A M1::= (M1::A + 1)) 389 (M1::N M1::= (M1::N - 1))) 390 (M1::RETURN M1::A))) 391 '((M1::ICONST 0) 392 (M1::ISTORE 2) 393 (M1::ILOAD 0) 394 (M1::ILOAD 1) 395 (M1::ISUB) 396 (M1::IFLE 10) 397 (M1::ILOAD 2) 398 (M1::ICONST 1) 399 (M1::IADD) 400 (M1::ISTORE 2) 401 (M1::ILOAD 0) 402 (M1::ICONST 1) 403 (M1::ISUB) 404 (M1::ISTORE 0) 405 (M1::GOTO -12) 406 (M1::ILOAD 2) 407 (M1::HALT)))) 408 409(DEFTHM 410 M1::EXAMPLE-EXECUTION-1 411 (EQUAL 412 (M1::TOP 413 (M1::STACK 414 (M1::RUN 415 (M1::REPEAT '0 '1000) 416 (M1::MAKE-STATE '0 417 '(5 0) 418 'NIL 419 (M1::COMPILE '(M1::N) 420 '((M1::A M1::= 1) 421 (M1::WHILE (M1::N > 0) 422 (M1::A M1::= (M1::N * M1::A)) 423 (M1::N M1::= (M1::N - 1))) 424 (M1::RETURN M1::A))))))) 425 '120)) 426 427(DEFTHM 428 M1::EXAMPLE-EXECUTION-2 429 (EQUAL 430 (M1::TOP 431 (M1::STACK 432 (M1::RUN 433 (M1::REPEAT '0 '1000) 434 (M1::MAKE-STATE '0 435 '(10 4 0) 436 'NIL 437 (M1::COMPILE '(M1::N M1::K) 438 '((M1::A M1::= 0) 439 (M1::WHILE (M1::N > M1::K) 440 (M1::A M1::= (M1::A + 1)) 441 (M1::N M1::= (M1::N - 1))) 442 (M1::RETURN M1::A))))))) 443 '6)) 444 445(INCLUDE-BOOK "arithmetic-3/extra/top-ext" :DIR :SYSTEM) 446 447(DEFTHM M1::STACKS 448 (IF (EQUAL (M1::TOP (M1::PUSH M1::X M1::S)) 449 M1::X) 450 (IF (EQUAL (M1::POP (M1::PUSH M1::X M1::S)) 451 M1::S) 452 (IF (EQUAL (M1::TOP (CONS M1::X M1::S)) 453 M1::X) 454 (EQUAL (M1::POP (CONS M1::X M1::S)) 455 M1::S) 456 'NIL) 457 'NIL) 458 'NIL)) 459 460(DEFTHM 461 M1::STATES 462 (IF 463 (EQUAL (M1::PC (M1::MAKE-STATE M1::PC 464 M1::LOCALS M1::STACK M1::PROGRAM)) 465 M1::PC) 466 (IF 467 (EQUAL (M1::LOCALS (M1::MAKE-STATE M1::PC 468 M1::LOCALS M1::STACK M1::PROGRAM)) 469 M1::LOCALS) 470 (IF 471 (EQUAL (M1::STACK (M1::MAKE-STATE M1::PC 472 M1::LOCALS M1::STACK M1::PROGRAM)) 473 M1::STACK) 474 (IF 475 (EQUAL (M1::PROGRAM (M1::MAKE-STATE M1::PC 476 M1::LOCALS M1::STACK M1::PROGRAM)) 477 M1::PROGRAM) 478 (IF 479 (EQUAL (M1::PC (CONS M1::PC M1::X)) 480 M1::PC) 481 (IF 482 (EQUAL (M1::LOCALS (CONS M1::PC (CONS M1::LOCALS M1::X))) 483 M1::LOCALS) 484 (IF 485 (EQUAL (M1::STACK (CONS M1::PC 486 (CONS M1::LOCALS (CONS M1::STACK M1::X)))) 487 M1::STACK) 488 (EQUAL (M1::PROGRAM 489 (CONS M1::PC 490 (CONS M1::LOCALS 491 (CONS M1::STACK (CONS M1::PROGRAM M1::X))))) 492 M1::PROGRAM) 493 'NIL) 494 'NIL) 495 'NIL) 496 'NIL) 497 'NIL) 498 'NIL) 499 'NIL)) 500 501(DEFTHM M1::STEP-OPENER 502 (IMPLIES (CONSP (M1::NEXT-INST M1::S)) 503 (EQUAL (M1::STEP M1::S) 504 (M1::DO-INST (M1::NEXT-INST M1::S) 505 M1::S)))) 506 507(DEFTHM M1::RUN-APP 508 (EQUAL (M1::RUN (M1::APP M1::A M1::B) M1::S) 509 (M1::RUN M1::B (M1::RUN M1::A M1::S)))) 510 511(DEFTHM M1::RUN-OPENER 512 (IF (EQUAL (M1::RUN 'NIL M1::S) M1::S) 513 (EQUAL (M1::RUN (CONS M1::TH M1::SCHED) M1::S) 514 (M1::RUN M1::SCHED (M1::STEP M1::S))) 515 'NIL)) 516 517(DEFTHM M1::NTH-ADD1! 518 (IMPLIES (NATP M1::N) 519 (EQUAL (M1::NTH (BINARY-+ '1 M1::N) LIST) 520 (M1::NTH M1::N (CDR LIST))))) 521 522(DEFTHM M1::NTH-UPDATE-NTH 523 (IMPLIES (IF (NATP M1::I) (NATP M1::J) 'NIL) 524 (EQUAL (M1::NTH M1::I (M1::UPDATE-NTH M1::J M1::V LIST)) 525 (IF (EQUAL M1::I M1::J) 526 M1::V (M1::NTH M1::I LIST))))) 527 528(DEFTHM 529 M1::UPDATE-NTH-UPDATE-NTH-1 530 (IMPLIES (IF (NATP M1::I) 531 (IF (NATP M1::J) 532 (NOT (EQUAL M1::I M1::J)) 533 'NIL) 534 'NIL) 535 (EQUAL (M1::UPDATE-NTH M1::I 536 M1::V (M1::UPDATE-NTH M1::J M1::W LIST)) 537 (M1::UPDATE-NTH M1::J M1::W 538 (M1::UPDATE-NTH M1::I M1::V LIST))))) 539 540(DEFTHM M1::UPDATE-NTH-UPDATE-NTH-2 541 (EQUAL (M1::UPDATE-NTH M1::I 542 M1::V (M1::UPDATE-NTH M1::I M1::W LIST)) 543 (M1::UPDATE-NTH M1::I M1::V LIST))) 544 545(DEFUN M1::! (M1::N) 546 (IF (ZP M1::N) 547 '1 548 (BINARY-* M1::N (M1::! (BINARY-+ '-1 M1::N))))) 549 550(DEFUN M1::IFACT (M1::N M1::A) 551 (IF (ZP M1::N) 552 M1::A 553 (M1::IFACT (BINARY-+ '-1 M1::N) 554 (BINARY-* M1::N M1::A)))) 555 556(DEFUN M1::IFACT-LOOP-SCHED (M1::N) 557 (IF (ZP M1::N) 558 (M1::REPEAT '0 '4) 559 (M1::APP (M1::REPEAT '0 '11) 560 (M1::IFACT-LOOP-SCHED (BINARY-+ '-1 M1::N))))) 561 562(DEFUN M1::IFACT-SCHED (M1::N) 563 (M1::APP (M1::REPEAT '0 '2) 564 (M1::IFACT-LOOP-SCHED M1::N))) 565 566(DEFUN 567 M1::TEST-IFACT (M1::N) 568 (M1::TOP (M1::STACK (M1::RUN (M1::IFACT-SCHED M1::N) 569 (M1::MAKE-STATE '0 570 (CONS M1::N (CONS '0 'NIL)) 571 'NIL 572 '((M1::ICONST 1) 573 (M1::ISTORE 1) 574 (M1::ILOAD 0) 575 (M1::IFLE 10) 576 (M1::ILOAD 0) 577 (M1::ILOAD 1) 578 (M1::IMUL) 579 (M1::ISTORE 1) 580 (M1::ILOAD 0) 581 (M1::ICONST 1) 582 (M1::ISUB) 583 (M1::ISTORE 0) 584 (M1::GOTO -10) 585 (M1::ILOAD 1) 586 (M1::HALT))))))) 587 588(DEFTHM M1::TEST-IFACT-EXAMPLES 589 (IF (EQUAL (M1::TEST-IFACT '5) (M1::! '5)) 590 (IF (EQUAL (M1::TEST-IFACT '10) (M1::! '10)) 591 (EQUAL (M1::TEST-IFACT '100) 592 (M1::! '100)) 593 'NIL) 594 'NIL)) 595 596(DEFTHM 597 M1::IFACT-LOOP-LEMMA 598 (IMPLIES (IF (NATP M1::N) (NATP M1::A) 'NIL) 599 (EQUAL (M1::RUN (M1::IFACT-LOOP-SCHED M1::N) 600 (M1::MAKE-STATE '2 601 (CONS M1::N (CONS M1::A 'NIL)) 602 M1::STACK 603 '((M1::ICONST 1) 604 (M1::ISTORE 1) 605 (M1::ILOAD 0) 606 (M1::IFLE 10) 607 (M1::ILOAD 0) 608 (M1::ILOAD 1) 609 (M1::IMUL) 610 (M1::ISTORE 1) 611 (M1::ILOAD 0) 612 (M1::ICONST 1) 613 (M1::ISUB) 614 (M1::ISTORE 0) 615 (M1::GOTO -10) 616 (M1::ILOAD 1) 617 (M1::HALT)))) 618 (M1::MAKE-STATE '14 619 (CONS '0 620 (CONS (M1::IFACT M1::N M1::A) 'NIL)) 621 (M1::PUSH (M1::IFACT M1::N M1::A) 622 M1::STACK) 623 '((M1::ICONST 1) 624 (M1::ISTORE 1) 625 (M1::ILOAD 0) 626 (M1::IFLE 10) 627 (M1::ILOAD 0) 628 (M1::ILOAD 1) 629 (M1::IMUL) 630 (M1::ISTORE 1) 631 (M1::ILOAD 0) 632 (M1::ICONST 1) 633 (M1::ISUB) 634 (M1::ISTORE 0) 635 (M1::GOTO -10) 636 (M1::ILOAD 1) 637 (M1::HALT)))))) 638 639(DEFTHM 640 M1::IFACT-LEMMA 641 (IMPLIES (NATP M1::N) 642 (EQUAL (M1::RUN (M1::IFACT-SCHED M1::N) 643 (M1::MAKE-STATE '0 644 (CONS M1::N (CONS M1::A 'NIL)) 645 M1::STACK 646 '((M1::ICONST 1) 647 (M1::ISTORE 1) 648 (M1::ILOAD 0) 649 (M1::IFLE 10) 650 (M1::ILOAD 0) 651 (M1::ILOAD 1) 652 (M1::IMUL) 653 (M1::ISTORE 1) 654 (M1::ILOAD 0) 655 (M1::ICONST 1) 656 (M1::ISUB) 657 (M1::ISTORE 0) 658 (M1::GOTO -10) 659 (M1::ILOAD 1) 660 (M1::HALT)))) 661 (M1::MAKE-STATE '14 662 (CONS '0 663 (CONS (M1::IFACT M1::N '1) 'NIL)) 664 (M1::PUSH (M1::IFACT M1::N '1) 665 M1::STACK) 666 '((M1::ICONST 1) 667 (M1::ISTORE 1) 668 (M1::ILOAD 0) 669 (M1::IFLE 10) 670 (M1::ILOAD 0) 671 (M1::ILOAD 1) 672 (M1::IMUL) 673 (M1::ISTORE 1) 674 (M1::ILOAD 0) 675 (M1::ICONST 1) 676 (M1::ISUB) 677 (M1::ISTORE 0) 678 (M1::GOTO -10) 679 (M1::ILOAD 1) 680 (M1::HALT)))))) 681 682(DEFTHM M1::IFACT-IS-FACTORIAL 683 (IMPLIES (IF (NATP M1::N) (NATP M1::A) 'NIL) 684 (EQUAL (M1::IFACT M1::N M1::A) 685 (BINARY-* (M1::! M1::N) M1::A)))) 686 687(DEFTHM 688 M1::IFACT-CORRECT 689 (IMPLIES (NATP M1::N) 690 (EQUAL (M1::RUN (M1::IFACT-SCHED M1::N) 691 (M1::MAKE-STATE '0 692 (CONS M1::N (CONS M1::A 'NIL)) 693 M1::STACK 694 '((M1::ICONST 1) 695 (M1::ISTORE 1) 696 (M1::ILOAD 0) 697 (M1::IFLE 10) 698 (M1::ILOAD 0) 699 (M1::ILOAD 1) 700 (M1::IMUL) 701 (M1::ISTORE 1) 702 (M1::ILOAD 0) 703 (M1::ICONST 1) 704 (M1::ISUB) 705 (M1::ISTORE 0) 706 (M1::GOTO -10) 707 (M1::ILOAD 1) 708 (M1::HALT)))) 709 (M1::MAKE-STATE '14 710 (CONS '0 (CONS (M1::! M1::N) 'NIL)) 711 (M1::PUSH (M1::! M1::N) M1::STACK) 712 '((M1::ICONST 1) 713 (M1::ISTORE 1) 714 (M1::ILOAD 0) 715 (M1::IFLE 10) 716 (M1::ILOAD 0) 717 (M1::ILOAD 1) 718 (M1::IMUL) 719 (M1::ISTORE 1) 720 (M1::ILOAD 0) 721 (M1::ICONST 1) 722 (M1::ISUB) 723 (M1::ISTORE 0) 724 (M1::GOTO -10) 725 (M1::ILOAD 1) 726 (M1::HALT)))))) 727 728(DEFTHM 729 M1::IFACT-CORRECT-COROLLARY-1 730 (IMPLIES 731 (NATP M1::N) 732 (EQUAL 733 (M1::TOP 734 (M1::STACK (M1::RUN (M1::IFACT-SCHED M1::N) 735 (M1::MAKE-STATE '0 736 (CONS M1::N (CONS M1::A 'NIL)) 737 M1::STACK 738 '((M1::ICONST 1) 739 (M1::ISTORE 1) 740 (M1::ILOAD 0) 741 (M1::IFLE 10) 742 (M1::ILOAD 0) 743 (M1::ILOAD 1) 744 (M1::IMUL) 745 (M1::ISTORE 1) 746 (M1::ILOAD 0) 747 (M1::ICONST 1) 748 (M1::ISUB) 749 (M1::ISTORE 0) 750 (M1::GOTO -10) 751 (M1::ILOAD 1) 752 (M1::HALT)))))) 753 (M1::! M1::N)))) 754 755(DEFTHM 756 M1::IFACT-CORRECT-COROLLARY-2 757 (IMPLIES 758 (NATP M1::N) 759 (EQUAL 760 (M1::TOP 761 (M1::STACK 762 (M1::RUN 763 (M1::IFACT-SCHED M1::N) 764 (M1::MAKE-STATE '0 765 (CONS M1::N (CONS M1::A 'NIL)) 766 M1::STACK 767 (M1::COMPILE '(M1::N) 768 '((M1::A M1::= 1) 769 (M1::WHILE (M1::N > 0) 770 (M1::A M1::= (M1::N * M1::A)) 771 (M1::N M1::= (M1::N - 1))) 772 (M1::RETURN M1::A))))))) 773 (M1::! M1::N)))) 774 775(DEFTHM M1::EXAMPLE-MODIFY-1 776 (EQUAL (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 777 (M1::LOCALS M1::S) 778 (M1::PUSH (M1::ARG1 M1::INST) 779 (M1::STACK M1::S)) 780 (M1::PROGRAM M1::S)) 781 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 782 (M1::LOCALS M1::S) 783 (M1::PUSH (M1::ARG1 M1::INST) 784 (M1::STACK M1::S)) 785 (M1::PROGRAM M1::S)))) 786 787(DEFTHM M1::EXAMPLE-MODIFY-2 788 (EQUAL (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 789 (M1::UPDATE-NTH (M1::ARG1 M1::INST) 790 (M1::TOP (M1::STACK M1::S)) 791 (M1::LOCALS M1::S)) 792 (M1::POP (M1::STACK M1::S)) 793 (M1::PROGRAM M1::S)) 794 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 795 (M1::UPDATE-NTH (M1::ARG1 M1::INST) 796 (M1::TOP (M1::STACK M1::S)) 797 (M1::LOCALS M1::S)) 798 (M1::POP (M1::STACK M1::S)) 799 (M1::PROGRAM M1::S)))) 800 801(DEFTHM M1::EXAMPLE-MODIFY-3 802 (EQUAL (M1::MAKE-STATE (BINARY-+ (M1::ARG1 M1::INST) 803 (M1::PC M1::S)) 804 (M1::LOCALS M1::S) 805 (M1::STACK M1::S) 806 (M1::PROGRAM M1::S)) 807 (M1::MAKE-STATE (BINARY-+ (M1::ARG1 M1::INST) 808 (M1::PC M1::S)) 809 (M1::LOCALS M1::S) 810 (M1::STACK M1::S) 811 (M1::PROGRAM M1::S)))) 812 813(DEFUN M1::PATTERN-BINDINGS 814 (M1::VARS M1::ARG-EXPRESSIONS) 815 (IF (ENDP M1::VARS) 816 'NIL 817 (CONS (CONS (CAR M1::VARS) 818 (CONS (CAR M1::ARG-EXPRESSIONS) 'NIL)) 819 (M1::PATTERN-BINDINGS (CDR M1::VARS) 820 (CDR M1::ARG-EXPRESSIONS))))) 821 822(DEFTHM M1::EXAMPLE-SEMANTICS-1 823 (EQUAL ((LAMBDA (M1::C M1::-PC- M1::-LOCALS- 824 M1::-STACK- M1::-PROGRAM- M1::S) 825 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 826 (M1::LOCALS M1::S) 827 (M1::PUSH M1::C M1::-STACK-) 828 (M1::PROGRAM M1::S))) 829 (M1::ARG1 M1::INST) 830 (M1::PC M1::S) 831 (M1::LOCALS M1::S) 832 (M1::STACK M1::S) 833 (M1::PROGRAM M1::S) 834 M1::S) 835 (M1::MAKE-STATE (BINARY-+ '1 (M1::PC M1::S)) 836 (M1::LOCALS M1::S) 837 (M1::PUSH (M1::ARG1 M1::INST) 838 (M1::STACK M1::S)) 839 (M1::PROGRAM M1::S)))) 840 841(DEFUN M1::CONCAT-SYMBOLS (M1::PART1 M1::PART2) 842 (INTERN-IN-PACKAGE-OF-SYMBOL 843 (COERCE (M1::APP (COERCE (SYMBOL-NAME M1::PART1) 'LIST) 844 (COERCE (SYMBOL-NAME M1::PART2) 'LIST)) 845 'STRING) 846 'M1::RUN)) 847 848(DEFUN M1::MAKE-DEFUN 849 (M1::NAME M1::ARGS M1::DCL M1::BODY) 850 (IF M1::DCL 851 (CONS 'DEFUN 852 (CONS M1::NAME 853 (CONS M1::ARGS 854 (CONS M1::DCL (CONS M1::BODY 'NIL))))) 855 (CONS 'DEFUN 856 (CONS M1::NAME 857 (CONS M1::ARGS (CONS M1::BODY 'NIL)))))) 858