1(*****************************************************************************) 2(* This file defines a type of s-expressions and various constants and *) 3(* functions on this type (t, nil, car, cdr, cons etc). *) 4(* *) 5(* See Holmakefile for how this file is used *) 6(* *) 7(* One goal is to construct a model of ACL2 by proving the axioms in *) 8(* axioms.lisp. *) 9(* *) 10(* File originally written by Mike Gordon and Matt Kaufmann; *) 11(* now maintained by Mike Gordon. *) 12(* *) 13(*****************************************************************************) 14 15 16(****************************************************************************** 17* Load theories 18******************************************************************************) 19quietdec := true; 20map 21 load 22 ["complex_rationalTheory", "sexp"]; 23open complex_rationalTheory sexp; 24Globals.checking_const_names := false; 25quietdec := false; 26 27(*****************************************************************************) 28(* Start new theory "sexp" *) 29(*****************************************************************************) 30val _ = new_theory "sexp"; 31 32(*****************************************************************************) 33(* Define s-expressions. *) 34(*****************************************************************************) 35 36(*****************************************************************************) 37(* Introduce mnemonic abbreviations to indicate use of type ``:string`` *) 38(*****************************************************************************) 39val _ = type_abbrev("packagename", ``:string``); 40val _ = type_abbrev("name", ``:string``); 41 42(*****************************************************************************) 43(* ACL2 S-expressions defined as a HOL datatype. *) 44(* Definition below adapted from Mark Staples' code. *) 45(*****************************************************************************) 46val _ = Hol_datatype 47 `sexp = ACL2_SYMBOL of packagename => name (* only curried for style *) 48 | ACL2_STRING of string 49 | ACL2_CHARACTER of char 50 | ACL2_NUMBER of complex_rational 51 | ACL2_PAIR of sexp => sexp`; (* only curried for style *) 52 53(*****************************************************************************) 54(* Each ACL2 function or constant is given a name of the form "pkg::nam". *) 55(* Since "::" is not handled by the HOL parser (and there are also many *) 56(* other character sequences that HOL can't parse occurring in ACL2 *) 57(* names) we also provide a HOL friendly name which is overloaded onto the *) 58(* ACL2 name. For example the ACL2 name "ACL2::BAD-ATOM<=" is given the *) 59(* HOL friendly name "bad_atom_less_equal". *) 60(*****************************************************************************) 61 62(*****************************************************************************) 63(* Overload "cons" onto ``ACL2_PAIR`` rather than make a definition, so *) 64(* that cons behaves like a constructor and so can be used in patterns in *) 65(* definitions (e.g. see definition of car below). *) 66(*****************************************************************************) 67 68(*****************************************************************************) 69(* Overload short mnemonic names onto the sexp datatype constructors. *) 70(*****************************************************************************) 71val _ = declare_names ("ACL2_PAIR", "cons"); 72val _ = declare_names ("ACL2_SYMBOL", "sym"); 73val _ = declare_names ("ACL2_NUMBER", "num"); 74val _ = declare_names ("ACL2_STRING", "str"); 75val _ = declare_names ("ACL2_CHARACTER", "chr"); 76 77(*****************************************************************************) 78(* Introduce some constants to abbreviate common package names. *) 79(*****************************************************************************) 80val ACL2_def = Define `ACL2 = "ACL2"` 81and COMMON_LISP_def = Define `COMMON_LISP = "COMMON-LISP"` 82and KEYWORD_def = Define `KEYWORD = "KEYWORD"` 83and ACL2_OUTPUT_CHANNEL_def = Define `ACL2_OUTPUT_CHANNEL = "ACL2-OUTPUT-CHANNEL"`; 84 85val _ = 86 add_string_abbrevs 87 [("ACL2", lhs(concl ACL2_def )), 88 ("COMMON-LISP", lhs(concl COMMON_LISP_def)), 89 ("KEYWORD", lhs(concl KEYWORD_def)), 90 ("ACL2-OUTPUT-CHANNEL", lhs(concl ACL2_OUTPUT_CHANNEL_def)) 91 ]; 92 93 94(*****************************************************************************) 95(* Definition of primitive constants and functions. *) 96(*****************************************************************************) 97val nil_def = 98 acl2Define "COMMON-LISP::NIL" `nil = sym "COMMON-LISP" "NIL"`; 99 100val t_def = 101 acl2Define "COMMON-LISP::T" `t = sym "COMMON-LISP" "T"`; 102 103val quote_def = 104 acl2Define "COMMON-LISP::QUOTE" `quote = sym "COMMON-LISP" "QUOTE"`; 105 106(*****************************************************************************) 107(* From axioms.lisp *) 108(* *) 109(* ; (equal x x) = T *) 110(* *) 111(* ; x/=y -> (equal x y) = NIL *) 112(* *) 113(* *) 114(* equal *) 115(* *) 116(* ; *1* definition (not helpful): *) 117(* (defun-*1* equal (x y) *) 118(* (equal x y)) *) 119(*****************************************************************************) 120val equal_def = 121 acl2Define "COMMON-LISP::EQUAL" 122 `equal (x:sexp) (y:sexp) = if x = y then t else nil`; 123 124(*****************************************************************************) 125(* stringp *) 126(* *) 127(* ; *1* definition (not helpful): *) 128(* (defun-*1* stringp (x) *) 129(* (stringp x)) *) 130(*****************************************************************************) 131val stringp_def = 132 acl2Define "COMMON-LISP::STRINGP" 133 `(stringp(str x) = t) /\ (stringp _ = nil)`; 134 135(*****************************************************************************) 136(* characterp *) 137(* *) 138(* ; *1* definition (not helpful): *) 139(* (defun-*1* characterp (x) *) 140(* (characterp x)) *) 141(*****************************************************************************) 142val characterp_def = 143 acl2Define "COMMON-LISP::CHARACTERP" 144 `(characterp(chr x) = t) /\ (characterp _ = nil)`; 145 146(*****************************************************************************) 147(* Construct a fraction then a rational from numerator and denominator *) 148(*****************************************************************************) 149val rat_def = Define `rat n d = abs_rat(abs_frac(n,d))`; 150 151(*****************************************************************************) 152(* Construct a complex from four integers: an/ad + (bn/bd)i. *) 153(*****************************************************************************) 154val cpx_def = 155 Define `cpx an ad bn bd = num(com (rat an ad) (rat bn bd))`; 156 157(*****************************************************************************) 158(* Construct a complex from an integer: n |--> n/1 + (0/1)i. *) 159(*****************************************************************************) 160val int_def = Define `int n = cpx n 1 0 1`; 161 162(*****************************************************************************) 163(* Construct a complex from a natural number: n |--> int n. *) 164(*****************************************************************************) 165val nat_def = Define `nat n = int(& n)`; 166 167(*****************************************************************************) 168(* acl2-numberp *) 169(* *) 170(* ; *1* definition (not helpful): *) 171(* (defun-*1* acl2-numberp (x) *) 172(* (numberp x)) *) 173(*****************************************************************************) 174val acl2_numberp_def = 175 acl2Define "ACL2::ACL2-NUMBERP" 176 `(acl2_numberp(num x) = t) /\ (acl2_numberp _ = nil)`; 177 178(*****************************************************************************) 179(* binary-+ *) 180(* *) 181(* ; *1* definition: *) 182(* (defun-*1* binary-+ (x y) *) 183(* (the number *) 184(* (if (numberp x) *) 185(* (if (numberp y) *) 186(* (+ (the number x) (the number y)) *) 187(* (gv binary-+ (x y) x)) *) 188(* (gv binary-+ (x y) *) 189(* (if (numberp y) *) 190(* y *) 191(* 0))))) *) 192(* *) 193(* ; Hand-optimized ACL2: *) 194(* (defun-*1* binary-+ (x y) *) 195(* (+ (if (numberp x) x 0) *) 196(* (if (numberp y) y 0))) *) 197(*****************************************************************************) 198val add_def = 199 acl2Define "ACL2::BINARY-+" 200 `(add (num x) (num y) = num(x+y)) /\ 201 (add (num x) _ = num x) /\ 202 (add _ (num y) = num y) /\ 203 (add _ _ = int 0)`; 204 205(*****************************************************************************) 206(* [Note: space added between "(" and "*" to avoid confusing ML!] *) 207(* *) 208(* binary-* *) 209(* *) 210(* ; *1* definition: *) 211(* (defun-*1* binary-* (x y) *) 212(* (the number *) 213(* (if (numberp x) *) 214(* (if (numberp y) *) 215(* ( * x y) *) 216(* (gv binary-* (x y) 0)) *) 217(* (gv binary-* (x y) 0)))) *) 218(*****************************************************************************) 219val mult_def = 220 acl2Define "ACL2::BINARY-*" 221 `(mult (num x) (num y) = num(x*y)) /\ 222 (mult _ _ = int 0)`; 223 224(*****************************************************************************) 225(* ; *1* definition (not very helpful):: *) 226(* (defun-*1* < (x y) *) 227(* (if (and (rationalp x) *) 228(* (rationalp y)) *) 229(* (< (the rational x) (the rational y)) *) 230(* (gv < (x y) *) 231(* (let ((x1 (if (numberp x) x 0)) *) 232(* (y1 (if (numberp y) y 0))) *) 233(* (or (< (realpart x1) (realpart y1)) *) 234(* (and (= (realpart x1) (realpart y1)) *) 235(* (< (imagpart x1) (imagpart y1)))))))) *) 236(*****************************************************************************) 237val less_def = 238 acl2Define "COMMON-LISP::<" 239 `(less (num(com xr xi)) (num(com yr yi)) = 240 if xr < yr 241 then t 242 else (if xr = yr then (if xi < yi then t else nil) else nil)) 243 /\ 244 (less _ (num(com yr yi)) = 245 if rat_0 < yr 246 then t 247 else (if rat_0 = yr then (if rat_0 < yi then t else nil) else nil)) 248 /\ 249 (less (num(com xr xi)) _ = 250 if xr < rat_0 251 then t 252 else (if xr = rat_0 then (if xi < rat_0 then t else nil) else nil)) 253 /\ 254 (less _ _ = nil)`; 255 256(*****************************************************************************) 257(* unary-- *) 258(* *) 259(* ; *1* definition: *) 260(* (defun-*1* unary-- (x) *) 261(* (the number *) 262(* (if (numberp x) *) 263(* (- x) *) 264(* (gv unary-- (x) 0)))) *) 265(*****************************************************************************) 266val unary_minus_def = 267 acl2Define "ACL2::UNARY--" 268 `(unary_minus(num x) = num(COMPLEX_SUB com_0 x)) /\ 269 (unary_minus _ = int 0)`; 270 271(*****************************************************************************) 272(* unary-/ *) 273(* *) 274(* ; *1* definition: *) 275(* (defun-*1* unary-/ (x) *) 276(* (the number *) 277(* (if (and (numberp x) (not (= x 0))) *) 278(* (/ x) *) 279(* (gv unary-/ (x) 0)))) *) 280(* *) 281(* ; Hand-optimized ACL2: *) 282(* (defun-*1* unary-/ (x) *) 283(* (if (and (numberp x) (not (equal x 0))) *) 284(* (/ x) *) 285(* 0)) *) 286(*****************************************************************************) 287val reciprocal_def = 288 acl2Define "ACL2::UNARY-/" 289 `(reciprocal (num x) = 290 if x = com_0 then int 0 else num(COMPLEX_RECIPROCAL x)) 291 /\ 292 (reciprocal _ = int 0)`; 293 294(*****************************************************************************) 295(* consp *) 296(* *) 297(* ; *1* definition (not helpful): *) 298(* (defun-*1* consp (x) *) 299(* (consp x)) *) 300(* *) 301(*****************************************************************************) 302val consp_def = 303 acl2Define "COMMON-LISP::CONSP" 304 `(consp(cons x y) = t) /\ (consp _ = nil)`; 305 306(*****************************************************************************) 307(* car *) 308(* *) 309(* ; *1* definition: *) 310(* (defun-*1* car (x) *) 311(* (cond *) 312(* ((consp x) *) 313(* (car x)) *) 314(* ((null x) *) 315(* nil) *) 316(* (t (gv car (x) nil)))) *) 317(* *) 318(* ; Hand-optimized ACL2: *) 319(* (defun-*1* car (x) *) 320(* (if (consp x) (car x) nil)) *) 321(*****************************************************************************) 322val car_def = 323 acl2Define "COMMON-LISP::CAR" 324 `(car(cons x _) = x) /\ (car _ = nil)`; 325 326(*****************************************************************************) 327(* cdr *) 328(* *) 329(* ; *1* definition: *) 330(* (defun-*1* cdr (x) *) 331(* (cond *) 332(* ((consp x) *) 333(* (cdr x)) *) 334(* ((null x) *) 335(* nil) *) 336(* (t (gv cdr (x) nil)))) *) 337(* *) 338(* ; Hand-optimized ACL2: *) 339(* (defun-*1* cdr (x) *) 340(* (if (consp x) (cdr x) nil)) *) 341(*****************************************************************************) 342val cdr_def = 343 acl2Define "COMMON-LISP::CDR" 344 `(cdr(cons _ y) = y) /\ (cdr _ = nil)`; 345 346(*****************************************************************************) 347(* realpart *) 348(* *) 349(* ; *1* definition: *) 350(* (defun-*1* realpart (x) *) 351(* (if (numberp x) *) 352(* (realpart x) *) 353(* (gv realpart (x) 0))) *) 354(*****************************************************************************) 355val realpart_def = 356 acl2Define "COMMON-LISP::REALPART" 357 `(realpart(num(com a b)) = num(com a rat_0)) /\ 358 (realpart _ = int 0)`; 359 360(*****************************************************************************) 361(* imagpart *) 362(* *) 363(* ; *1* definition: *) 364(* (defun-*1* imagpart (x) *) 365(* (if (numberp x) *) 366(* (imagpart x) *) 367(* (gv imagpart (x) 0))) *) 368(*****************************************************************************) 369val imagpart_def = 370 acl2Define "COMMON-LISP::IMAGPART" 371 `(imagpart(num(com a b)) = num(com b rat_0)) /\ 372 (imagpart _ = int 0)`; 373 374(*****************************************************************************) 375(* rationalp *) 376(* *) 377(* ; *1* definition (not helpful): *) 378(* (defun-*1* rationalp (x) *) 379(* (rationalp x)) *) 380(*****************************************************************************) 381val rationalp_def = 382 acl2Define "COMMON-LISP::RATIONALP" 383 `(rationalp(num(com a b)) = if b = rat_0 then t else nil) /\ 384 (rationalp _ = nil)`; 385 386(*****************************************************************************) 387(* complex-rationalp *) 388(* *) 389(* ; *1* definition: *) 390(* (defun-*1* complex-rationalp (x) *) 391(* (complexp x)) *) 392(* *) 393(* Complex-rationalp holds only of numbers that are not rational, i.e., *) 394(* have a non-zero imaginary part. Here is the ACL2 documentation for *) 395(* COMPLEX-RATIONALP, followed by the doc for COMPLEX (pointed to by the *) 396(* former, and perhaps also useful for you). *) 397(* *) 398(* *) 399(* COMPLEX-RATIONALP recognizes complex rational numbers *) 400(* *) 401(* *) 402(* Examples: *) 403(* (complex-rationalp 3) ; nil, as 3 is rational, not complex rational*) 404(* (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3 *) 405(* (complex-rationalp t) ; nil *) 406(* (complex-rationalp #c(3 1)) ; t, as #c(3 1) is the complex number 3 + i *) 407(*****************************************************************************) 408val complex_rationalp_def = 409 acl2Define "ACL2::COMPLEX-RATIONALP" 410 `(complex_rationalp(num(com a b)) = if b = rat_0 then nil else t) 411 /\ 412 (complex_rationalp _ = nil)`; 413 414(*****************************************************************************) 415(* complex *) 416(* *) 417(* ; *1* definition: *) 418(* (defun-*1* complex (x y) *) 419(* (complex (the rational (if (rationalp x) x (gv complex (x y) 0))) *) 420(* (the rational (if (rationalp y) y (gv complex (x y) 0))))) *) 421(* *) 422(* *) 423(* COMPLEX create an ACL2 number *) 424(* *) 425(* *) 426(* Examples: *) 427(* (complex x 3) ; x + 3i, where i is the principal square root of -1 *) 428(* (complex x y) ; x + yi *) 429(* (complex x 0) ; same as x, for rational numbers x *) 430(* *) 431(* *) 432(* The function complex takes two rational number arguments and returns an *) 433(* ACL2 number. This number will be of type (complex rational) [as defined *) 434(* in the Common Lisp language], except that if the second argument is *) 435(* zero, then complex returns its first argument. The function *) 436(* complex-rationalp is a recognizer for complex rational numbers, i.e. for *) 437(* ACL2 numbers that are not rational numbers. *) 438(* *) 439(* The reader macro #C (which is the same as #c) provides a convenient way *) 440(* for typing in complex numbers. For explicit rational numbers x and y, *) 441(* #C(x y) is read to the same value as (complex x y). *) 442(* *) 443(* The functions realpart and imagpart return the real and imaginary parts *) 444(* (respectively) of a complex (possibly rational) number. So for example, *) 445(* (realpart #C(3 4)) = 3, (imagpart #C(3 4)) = 4, (realpart 3/4) = 3/4, *) 446(* and (imagpart 3/4) = 0. *) 447(* *) 448(* The following built-in axiom may be useful for reasoning about complex *) 449(* numbers. *) 450(* *) 451(* (defaxiom complex-definition *) 452(* (implies (and (real/rationalp x) *) 453(* (real/rationalp y)) *) 454(* (equal (complex x y) *) 455(* (+ x ( * #c(0 1) y)))) *) 456(* :rule-classes nil) *) 457(* *) 458(* *) 459(* A completion axiom that shows what complex returns on arguments *) 460(* violating its guard (which says that both arguments are rational *) 461(* numbers) is the following. *) 462(* *) 463(* (equal (complex x y) *) 464(* (complex (if (rationalp x) x 0) *) 465(* (if (rationalp y) y 0))) *) 466(*****************************************************************************) 467val complex_def = 468 acl2Define "COMMON-LISP::COMPLEX" 469 `(complex (num(com xr xi)) (num(com yr yi)) = 470 num(com (if (xi = rat_0) then xr else rat_0) 471 (if (yi = rat_0) then yr else rat_0))) 472 /\ 473 (complex (num(com xr xi)) _ = 474 num(com (if (xi = rat_0) then xr else rat_0) rat_0)) 475 /\ 476 (complex _ (num(com yr yi)) = 477 num(com rat_0 (if (yi = rat_0) then yr else rat_0))) 478 /\ 479 (complex _ _ = int 0)`; 480 481(*****************************************************************************) 482(* integerp *) 483(* *) 484(* ; *1* definition (not helpful): *) 485(* (defun-*1* integerp (x) *) 486(* (integerp x)) *) 487(*****************************************************************************) 488val integerp_def = 489 acl2Define "COMMON-LISP::INTEGERP" 490 `(integerp(num n) = if IS_INT n then t else nil) /\ 491 (integerp _ = nil)`; 492 493(*****************************************************************************) 494(* numerator *) 495(* *) 496(* ; *1* definition:: *) 497(* (defun-*1* numerator (x) *) 498(* (if (rationalp x) *) 499(* (numerator x) *) 500(* (gv numerator (x) 0))) *) 501(* *) 502(* ; Hand-optimized ACL2: *) 503(* (defun-*1* numerator (x) *) 504(* (if (rationalp x) *) 505(* (numerator x) *) 506(* 0)) *) 507(*****************************************************************************) 508val numerator_def = 509 acl2Define "COMMON-LISP::NUMERATOR" 510 `(numerator(num(com a b)) = 511 if b = rat_0 then int(reduced_nmr a) else int 0) 512 /\ 513 (numerator _ = int 0)`; 514 515(*****************************************************************************) 516(* denominator *) 517(* *) 518(* ; *1* definition:: *) 519(* (defun-*1* denominator (x) *) 520(* (if (rationalp x) *) 521(* (denominator x) *) 522(* (gv denominator (x) 1))) *) 523(* *) 524(* ; Hand-optimized ACL2: *) 525(* (defun-*1* denominator (x) *) 526(* (if (rationalp x) *) 527(* (denominator x) *) 528(* 1)) *) 529(*****************************************************************************) 530val denominator_def = 531 acl2Define "COMMON-LISP::DENOMINATOR" 532 `(denominator(num(com a b)) = 533 if b = rat_0 then int(reduced_dnm a) else int 1) 534 /\ 535 (denominator _ = int 1)`; 536 537(*****************************************************************************) 538(* char-code *) 539(* *) 540(* ; *1* definition *) 541(* (defun-*1* char-code (x) *) 542(* (if (characterp x) *) 543(* (char-code x) *) 544(* (gv char-code (x) 0))): *) 545(*****************************************************************************) 546val char_code_def = 547 acl2Define "COMMON-LISP::CHAR-CODE" 548 `(char_code(chr c) = int (&(ORD c))) /\ 549 (char_code _ = int 0)`; 550 551(*****************************************************************************) 552(* code-char *) 553(* *) 554(* ; *1* definition: *) 555(* (defun-*1* code-char (x) *) 556(* (if (and (integerp x) *) 557(* (>= x 0) *) 558(* (< x 256)) *) 559(* (code-char x) *) 560(* (gv code-char (x) (code-char 0)))) *) 561(*****************************************************************************) 562val code_char_def = 563 acl2Define "COMMON-LISP::CODE-CHAR" 564 `(code_char(num(com a b)) = 565 if IS_INT(com a b) /\ (0 <= reduced_nmr a) /\ (reduced_nmr a < 256) 566 then chr(CHR (Num(reduced_nmr a))) 567 else chr(CHR 0)) 568 /\ 569 (code_char _ = chr(CHR 0))`; 570 571(*****************************************************************************) 572(* From axioms.lisp *) 573(* *) 574(* ; (if NIL y z) = z *) 575(* *) 576(* ; x/=NIL -> (if x y z) = y *) 577(* *) 578(* if *) 579(* *) 580(* ; *1* definition (not helpful): *) 581(* (defun-*1* if (x y z) *) 582(* (error "We just can't stand having a non-lazy IF around. *) 583(* But we attempted ~%~ to call the executable counterpart *) 584(* of IF on argument list ~s." *) 585(* (list x y z))) *) 586(* *) 587(* Can't overload "if" onto ``ACL2_IF`` because of HOL's *) 588(* `if ... then ... else` construct. Using "ite" instead. *) 589(*****************************************************************************) 590val ite_def = 591 acl2Define "COMMON-LISP::IF" 592 `ite x (y:sexp) (z:sexp) = if x = nil then z else y`; 593 594(*****************************************************************************) 595(* If f : 'a -> sexp then list_to_sexp f : num list : 'a list -> sexp. *) 596(* *) 597(* For example: *) 598(* *) 599(* |- list_to_sexp num [1; 2; 3] = *) 600(* cons (num 1) (cons (num 2) (cons (num 3) (sym "COMMON-LISP" "NIL"))) *) 601(*****************************************************************************) 602val list_to_sexp_def = 603 Define 604 `(list_to_sexp f [] = nil) /\ 605 (list_to_sexp f (x::l) = cons (f x) (list_to_sexp f l))`; 606 607(*****************************************************************************) 608(* coerce *) 609(* *) 610(* ; First, we nee to translate this ACL2 definition: *) 611(* *) 612(* (defun make-character-list (x) *) 613(* (cond ((atom x) nil) *) 614(* ((characterp (car x)) *) 615(* (cons (car x) (make-character-list (cdr x)))) *) 616(* (t *) 617(* (cons (code-char 0) (make-character-list (cdr x)))))) *) 618(* *) 619(* ; We also require HOL functions coerce_string_to_list and *) 620(* ; coerce_list_to_string (not written here) that coerce a string (e.g., *) 621(* ; "abc") to an SEXP list (e.g., cons 'a' (cons 'b' (cons 'c' nil))) *) 622(* ; and vice-versa, respectively. *) 623(* *) 624(* ; *1* definition (not very helpful): *) 625(* (defun-*1* coerce (x y) *) 626(* (cond *) 627(* ((equal y 'list) *) 628(* (if (stringp x) *) 629(* (coerce x 'list) *) 630(* (gv coerce (x y) nil))) *) 631(* ((character-listp x) *) 632(* (if (equal y 'string) *) 633(* (coerce x 'string) *) 634(* (gv coerce (x y) (coerce x 'string)))) *) 635(* (t *) 636(* (gv coerce (x y) *) 637(* (coerce (make-character-list x) 'string))))) *) 638(*****************************************************************************) 639 640(*****************************************************************************) 641(* (defun make-character-list (x) *) 642(* (cond ((atom x) nil) *) 643(* ((characterp (car x)) *) 644(* (cons (car x) (make-character-list (cdr x)))) *) 645(* (t *) 646(* (cons (code-char 0) (make-character-list (cdr x)))))) *) 647(*****************************************************************************) 648val make_character_list_def = 649 Define 650 `(make_character_list(cons (chr c) y) = 651 (cons (chr c) (make_character_list y))) 652 /\ 653 (make_character_list(cons x y) = 654 (cons (code_char(int 0)) (make_character_list y))) 655 /\ 656 (make_character_list _ = nil)`; 657 658(*****************************************************************************) 659(* "abc" |--> (cons (chr #"a") (cons (chr #"b") (cons (chr #"c") nil))) *) 660(* *) 661(* list_to_sexp maps a function down a HOL list and then conses up an *) 662(* s-expression from the resulting list. For example: *) 663(* *) 664(* list_to_sexp chr [a; b; c] = *) 665(* cons (chr a) (cons (chr b) (cons (chr c) (sym "COMMON-LISP" "NIL"))) *) 666(* *) 667(* EXPLODE explodes a HOL string into a HOL list of characters. *) 668(*****************************************************************************) 669val coerce_string_to_list_def = 670 Define 671 `coerce_string_to_list s = list_to_sexp chr (EXPLODE s)`; 672 673(*****************************************************************************) 674(* (cons (chr #"a") (cons (chr #"b") (cons (chr #"c") nil))) |--> "abc" *) 675(* *) 676(* STRING : char->string->string is HOL's string-cons function. *) 677(*****************************************************************************) 678val coerce_list_to_string_def = 679 Define 680 `(coerce_list_to_string(cons (chr c) y) = 681 STRING c (coerce_list_to_string y)) 682 /\ 683 (coerce_list_to_string _ = "")`; 684 685val coerce_def = 686 acl2Define "COMMON-LISP::COERCE" 687 `(coerce (str s) y = 688 if y = sym "COMMON-LISP" "LIST" 689 then coerce_string_to_list s 690 else str "") 691 /\ 692 (coerce (cons a x) y = 693 if y = sym "COMMON-LISP" "LIST" 694 then nil 695 else str(coerce_list_to_string(make_character_list(cons a x)))) 696 /\ 697 (coerce _ y = if y = sym "COMMON-LISP" "LIST" then nil else str "")`; 698 699(*****************************************************************************) 700(* The following function represents an ACL2 package system, but is not *) 701(* itself an ACL2 primitive; rather, it is used in the translation (see *) 702(* for example intern-in-package-of-symbol). *) 703(* *) 704(* BASIC_INTERN : string -> string -> SEXP *) 705(* *) 706(* An ACL2 data structure is available to help with the definition of *) 707(* BASIC_INTERN. For example, after evaluation of (defpkg "FOO" '(a *) 708(* b)), the form (known-package-alist state) evaluates to the following *) 709(* (which I have abbreviated, omitting irrelevant or not-useful info). *) 710(* Note that each package is associated with a list of imported *) 711(* symbols. For example, "FOO" imports two symbols, represented in HOL *) 712(* as (sym "ACL2" "A") and (sym "ACL2" "B"). *) 713(* *) 714(* (("FOO" (A B) ...) *) 715(* ("ACL2-USER" (& *ACL2-EXPORTS* ...)) *) 716(* ("ACL2-PC" NIL ...) *) 717(* ("ACL2-INPUT-CHANNEL" NIL NIL NIL) *) 718(* ("ACL2-OUTPUT-CHANNEL" NIL NIL NIL) *) 719(* ("ACL2" (&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH* ...) NIL NIL) *) 720(* ("COMMON-LISP" NIL NIL NIL) *) 721(* ("KEYWORD" NIL NIL NIL)) *) 722(* *) 723(* Let us turn now to the definition of BASIC_INTERN. *) 724(* *) 725(* If pkg_name is the name of a known package and symbol_name is the *) 726(* name of a symbol imported into that package from some other package, *) 727(* named old_pkg, then: *) 728(* *) 729(* BASIC_INTERN symbol_name pkg_name = (sym old_pkg symbol_name) *) 730(* *) 731(* For example, given the package system shown above, *) 732(* BASIC_INTERN "A" "FOO" = (sym "ACL2" "A"). *) 733(* *) 734(* Otherwise, if pkg_name is the name of a known package (from the ACL2 *) 735(* data structure as shown above), then: *) 736(* *) 737(* BASIC_INTERN symbol_name pkg_name = (sym pkg_name symbol_name) *) 738(* *) 739(* Finally, if pkg_name is not the name of a known package, we return *) 740(* an arbitrary value. *) 741(*****************************************************************************) 742 743(*****************************************************************************) 744(* ACL2_PACKAGE_ALIST contains a list of triples *) 745(* *) 746(* (symbol-name , known-pkg-name , actual-pkg-name) *) 747(* *) 748(* The idea is that when symbol-name is interned into known-pkg-name, the *) 749(* resulting symbol's package name is actual-pkg-name. That is, the *) 750(* symbol with name symbol-name and package-name actual-pkg-name is *) 751(* imported into package known-pkg-name. *) 752(*****************************************************************************) 753 754(*****************************************************************************) 755(* Building a term directly out of a slurped in ACL2 package structure *) 756(* (e.g. kpa-v2-9-3.ml) breaks the HOL compiler. We therefore fold in the *) 757(* abbreviations below (this idea due to Konrad). It is strange that *) 758(* rewriting the big term is no problem, but compiling it breaks. *) 759(*****************************************************************************) 760val ACL2_CL_def = Define `ACL2_CL = ("ACL2", "COMMON-LISP")`; 761val ACL2_USER_def = Define `ACL2_USER = ("ACL2-USER" , "ACL2")`; 762val ACL_USER_CL_def = Define `ACL2_USER_CL = ("ACL2-USER" , "COMMON-LISP")`; 763 764(*****************************************************************************) 765(* Convert imported ACL2 package structure: *) 766(* *) 767(* [ *) 768(* ("&", "ACL2-USER", "ACL2"), *) 769(* ("*ACL2-EXPORTS*", "ACL2-USER", "ACL2"), *) 770(* ... *) 771(* ("VALUES", "ACL2", "COMMON-LISP"), *) 772(* ("ZEROP", "ACL2", "COMMON-LISP") *) 773(* ] *) 774(* *) 775(* to corresponding term, then fold in ACL2_CL_def, ACL2_USER_def and *) 776(* ACL_USER_CL_def using REWRITE_CONV, then extract the simplified term. *) 777(* Used to define ACL2_PACKAGE_ALIST *) 778(*****************************************************************************) 779 780fun make_package_structure_term l = 781 rhs 782 (concl 783 (REWRITE_CONV 784 (map GSYM [ACL2_CL_def,ACL2_USER_def,ACL_USER_CL_def]) 785 (mk_list 786 (map 787 (fn (s1,s2,s3) => 788 mk_pair(fromMLstring s1, mk_pair(fromMLstring s2, fromMLstring s3))) 789 l, 790 ``:string # string # string``)))); 791 792val ACL2_PACKAGE_STRUCTURE = ref([] : (string * string * string)list); 793 794use (Globals.HOLDIR ^ "/examples/acl2/ml/kpa-v2-9-3.ml"); 795 796val ACL2_PACKAGE_ALIST = 797 time 798 Define 799 `ACL2_PACKAGE_ALIST = 800 ^(make_package_structure_term (!ACL2_PACKAGE_STRUCTURE))`; 801 802(*****************************************************************************) 803(* - LOOKUP y [(x1,y1,z1);...;(xn,yn,zn)] x = zi if x=xi and y=yi *) 804(* (scan from left) *) 805(* - LOOKUP y [(x1,y1,z1);...;(xn,yn,zn)] x = y if (x=/=xi or y=/=yi) *) 806(* for any i *) 807(*****************************************************************************) 808val LOOKUP_def = 809 Define 810 `(LOOKUP y [] _ = y) 811 /\ 812 (LOOKUP y ((x1,y1,z1)::a) x = 813 if (x=x1) /\ (y=y1) then z1 else LOOKUP y a x)`; 814 815val BASIC_INTERN_def = 816 Define 817 `BASIC_INTERN sym_name pkg_name = 818 sym (LOOKUP pkg_name ACL2_PACKAGE_ALIST sym_name) sym_name`; 819 820(*****************************************************************************) 821(* symbolp *) 822(* *) 823(* ; *1* definition (not helpful): *) 824(* (defun-*1* symbolp (x) *) 825(* (symbolp x)) *) 826(*****************************************************************************) 827val symbolp_def = 828 acl2Define "COMMON-LISP::SYMBOLP" 829 `(symbolp (sym p n) = 830 if (BASIC_INTERN n p = sym p n) /\ ~(p = "") then t else nil) 831 /\ 832 (symbolp _ = nil)`; 833 834(*****************************************************************************) 835(* bad-atom<= *) 836(* *) 837(* ; For us, bad atoms are objects that look like symbols but whose *) 838(* ; combination of package name and symbol name are impossible for the *) 839(* ; given package system. *) 840(* *) 841(* ; *1* definition (not helpful): *) 842(* (defun-*1* bad-atom<= (x y) *) 843(* (cond ((and (bad-atom x) (bad-atom y)) *) 844(* *) 845(* ; The following should never happen. *) 846(* *) 847(* (error "We have called (the executable counterpart of) *) 848(* bad-atom<= on ~ ~s and ~s, but bad-atom<= *) 849(* has no Common Lisp definition." *) 850(* x y)) *) 851(* (t (gv bad-atom<= (x y) nil)))) *) 852(*****************************************************************************) 853 854(*****************************************************************************) 855(* Pick a well-founded relation on s-expressions *) 856(*****************************************************************************) 857val SEXP_WF_LESS_def = 858 Define `SEXP_WF_LESS = @R:sexp->sexp->bool. WF R`; 859 860(*****************************************************************************) 861(* ACL2_BAD_ATOM_LESS x y iff x is less then y in the well-founded relation *) 862(*****************************************************************************) 863val bad_atom_less_equal_def = 864 acl2Define "ACL2::BAD-ATOM<=" 865 `bad_atom_less_equal x y = if SEXP_WF_LESS x y then t else nil`; 866 867(*****************************************************************************) 868(* symbol-name *) 869(* *) 870(* ; *1* definition: *) 871(* (defun-*1* symbol-name (x) *) 872(* (if (symbolp x) *) 873(* (symbol-name x) *) 874(* (gv symbol-name (x) ""))) *) 875(*****************************************************************************) 876val symbol_name_def = 877 acl2Define "COMMON-LISP::SYMBOL-NAME" 878 `(symbol_name (sym p n) = ite (symbolp (sym p n)) (str n) (str "")) 879 /\ 880 (symbol_name _ = (str ""))`; 881 882(*****************************************************************************) 883(* symbol-package-name *) 884(* *) 885(* ; *1* definition: *) 886(* (defun-*1* symbol-package-name (x) *) 887(* (if (symbolp x) *) 888(* (symbol-package-name x) *) 889(* (gv symbol-package-name (x) ""))) *) 890(*****************************************************************************) 891val symbol_package_name_def = 892 acl2Define "ACL2::SYMBOL-PACKAGE-NAME" 893 `(symbol_package_name (sym p n) = 894 ite (symbolp (sym p n)) (str p) (str "")) 895 /\ 896 (symbol_package_name _ = (str ""))`; 897 898(*****************************************************************************) 899(* pkg-witness *) 900(* *) 901(* ; *1* definition (not very helpful): *) 902(* (defun-*1* pkg-witness (pkg) *) 903(* (if (stringp pkg) *) 904(* (if (find-non-hidden-package-entry *) 905(* pkg (known-package-alist *the-live-state* )) *) 906(* (intern *pkg-witness-name* pkg) *) 907(* (throw-raw-ev-fncall (list 'pkg-witness-er pkg))) *) 908(* (gv pkg-witness (pkg) nil))) *) 909(* *) 910(* ; Here, we treat the ACL2 constant *pkg-witness-name* as its value, *) 911(* ; the string "PKG-WITNESS" -- in fact, ACL2 treates constants *) 912(* ; (defconst events) much as it treats macros, in the sense that they *) 913(* ; are eliminated when passing to internal terms. *) 914(* *) 915(* ; Note that ACL2 refuses to parse (pkg-witness pkg) unless pkg is an *) 916(* ; explicit string naming a package already known to ACL2. *) 917(*****************************************************************************) 918val pkg_witness_def = 919 acl2Define "ACL2::PKG-WITNESS" 920 `pkg_witness (str x) = 921 let s = BASIC_INTERN "PKG-WITNESS" x in ite (symbolp s) s nil`; 922 923(*****************************************************************************) 924(* intern-in-package-of-symbol *) 925(* *) 926(* ; *1* definition:: *) 927(* (defun-*1* intern-in-package-of-symbol (x y) *) 928(* (if (and (stringp x) *) 929(* (symbolp y)) *) 930(* (intern x (symbol-package y)) *) 931(* (gv intern (x y) nil))) *) 932(* *) 933(* ; Hand-optimized ACL2: *) 934(* (defun-*1* intern-in-package-of-symbol (x y) *) 935(* (if (and (stringp x) *) 936(* (symbolp y)) *) 937(* (intern x (symbol-package y)) *) 938(* nil)) *) 939(*****************************************************************************) 940val intern_in_package_of_symbol_def = 941 acl2Define "ACL2::INTERN-IN-PACKAGE-OF-SYMBOL" 942 `(intern_in_package_of_symbol (str x) (sym p n) = 943 ite (symbolp (sym p n)) (BASIC_INTERN x p) nil) 944 /\ 945 (intern_in_package_of_symbol _ _ = nil)`; 946 947(*****************************************************************************) 948(* Auxiliary definitions. *) 949(*****************************************************************************) 950 951(*****************************************************************************) 952(* |= t, where t:sexp, means t is a theorem of ACL2 *) 953(*****************************************************************************) 954val _ = set_fixity "|=" (Prefix 11); (* Give "|=" weak precedence *) 955 956val ACL2_TRUE_def = 957 xDefine "ACL2_TRUE" 958 `(|= p) = (ite (equal p nil) nil t = t)`; 959 960val _ = export_acl2_theory(); 961 962compile_theory(); 963