|
|
|---|
|
|
|
|---|
Reading expressions in the ACL2 read-eval-print loop
The ACL2 read-eval-print loop reads expressions much like they are
read in any Common Lisp read-eval-print loop. For example, you may use the
single tick symbol (') for
ACL2-specific reader macros include its reading of expressions in a
specified package (using
See set-iprint for how to make ACL2 print expressions like
Strictly speaking, there is nothing special about how the reader handles keywords in the input. But see keyword-commands for how ACL2 may interpret a top-level keyword command.
We conclude this topic with a log that illustrates features discussed above. Comments of the form {{..}} have been inserted manually.
ACL2 !>(defconst *c* (+ 3 4)) Summary Form: ( DEFCONST *C* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *C* ACL2 !>'(a #.*c* 17) ;{{See :doc sharp-dot-reader. ; Notice that #.*c* is read as the value of *c*, thus, ; as 7 rather than as (+ 3 4).}} (A 7 17) ACL2 !>'(a #.(+ 5 6) 17) ;{{But this is not legal in ACL2, as #. must be followed by ; a known constant symbol.}} *********************************************** ************ ABORTING from raw Lisp *********** ********** (see :DOC raw-lisp-error) ********** Error: ACL2 supports #. syntax only for #.*a*, where *a* has been defined by DEFCONST. Thus the form #.(+ 5 6) is illegal. *********************************************** ;{{Additional output here has been omitted in this log.}} ACL2 !>(defpkg "FOO" nil) Summary Form: ( DEFPKG "FOO" ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) "FOO" ACL2 !>#!foo'(a b c) ;{{See :doc sharp-bang-reader. The prefix "#!foo" causes ; the s-expression after it to be read into the "FOO" package.}} (FOO::A FOO::B FOO::C) ACL2 !>#x100a ;{{As in Common Lisp, "#x" causes the digits after it to be read in hex.}} 4106 ACL2 !>#ux10_0a ;{{The "#u" prefix allows underscores in the numeral after it. Those ; underscores are ignored, but can improve readability.}} 4106 ACL2 !>(set-iprint t) ;{{See :DOC set-print. This causes "#@1#" below to be printed.}} ACL2 Observation in SET-IPRINT: Iprinting has been enabled. ACL2 !>(set-evisc-tuple (evisc-tuple 3 ; print-level 4 ; print-length nil ; alist nil ; hiding-cars ) :sites :ld) ;{{Abbreviate the printing of top-level evaluation results. ; See :doc set-evisc-tuple.}} (:LD) ACL2 !>(make-list 10) (NIL NIL NIL NIL . #@1#) ACL2 !>'#@1# ;{{Note that the reader replaces #@1# with the value that was stored there.}} (NIL NIL NIL NIL . #@2#) ACL2 !>(without-evisc '(NIL NIL NIL NIL . #@1#)) ;{{See :doc without-evisc.}} (NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL) ACL2 !>(set-evisc-tuple nil :sites :ld) (:LD) ACL2 !>(let ((x '(3 4))) `(a b ,x c)) ;{{As in Common Lisp, backquote can be escaped by comma.}} (A B (3 4) C) ACL2 !>(let ((x '(3 4))) `(a b ,@x c)) ;{{As in Common Lisp, backquote can be escaped by comma-atsign, which ; splices its value into the list.}} (A B 3 4 C) ACL2 !>