The answer in
comma-comma-at in Common Lisp helped me figure out what's going on. I'm just going to build upon that answer and apply to this question.
We here have two ways of reasoning about nested backquote forms. One way, which I will call the replacement interpretation, is simply that for a doubly nested backquote form, evaluation of that form is
- removing the outermost backtick character
- then replacing comma-following forms appearing at the same level as the outermost backquote with their evaluation results (See Using two backquotes and commas, Common Lisp for meaning of same level) (also, erase those commas)
- then replacing comma-at-following forms appearing at the same level as the outermost backquote by splicing their evaluation results into their spots (also, erase those comma-at)
The other way, which I will call the equivalency interpretation, is that I should reinterpret backquote forms with their equivalent non-backquote forms, as in the CLHS link, and that for a doubly nested backquote form, I should reinterpret the innermost backquote forms before reinterpreting the outermost backquote form.
Only thing that the replacement interpretation explicitly specifies is how to evaluate a backquote form. How a backquote form is equivalent to a non-backquote form is only indirectly specified as a consequence of how their evaluation works.
Only thing that the equivalency interpretation explicitly specifies is how a backquote form is equivalent to a non-backquote form. How a backquote form gets evaluated is only indirectly specified as a consequence of how their equivalent non-backquote forms evaluate.
The way SBCL evaluates Expression P is easily explained from the replacement interpretation. But it can also be explained from the equivalence interpretation. To see why, we first work through Example A and Example B.
some convention: I use ~ to mean "previous expression is equivalent to the next expression". I use ~> to mean "previous expression evaluates to or something equivalent to the next expression". By "equivalent to" I mean "may be interpreted to mean" in the sense as in the CLHS link.
Example A (a simple backquote form):
`(open ,@(list 'cat 'dog))
;; ~
(append (list `open)
(list 'cat 'dog)
nil)
;; ~
(append (list 'open)
(list 'cat 'dog)
nil)
;; ~>
(open cat dog)
Example B (when comma-at is in a deeper place):
`(beg (open ,@(list 'cat 'dog)))
;; ~
(append (list `beg)
(list `(open ,@(list 'cat 'dog)))
nil)
;; ~>
(beg (open cat dog))
Example C (expression P)
`(outer
`(inner ,@(no ,@(list 'cat 'dog))))
;; ~
`(outer
'(append
(list `inner)
(no ,@(list 'cat 'dog))
nil))
;; ~>
(outer
'(append
(list `inner)
(no cat dog)
nil))
;; ~
(outer
`(inner ,@(no cat dog)))
So the replacement interpretation is consistent with the equivalency interpretation so far.
Are the two interpretations compatible all the way? The replacement interpretation has some complications, and the equivalency interpretation seems to be part of CLHS, if I am reading the CLHS link right. So it seems that the equivalency interpretation is the real deal and the replacement interpretation is simply a convenient illusion.
What are complications of the replacement interpretation? I have gone through all doubly nested backquote examples from Backquote Appendix C with the replacement interpretation, and most of the examples (except four) show no complications. For most examples, replacement interpretation works and is consistent with real results.
The four examples that you get complications are:
,@',@
,',@
,,@
,@,@
For the first two, complication is that you must splice a list before a quote character. What does it mean to splice before a quote character? It means nothing. But if you think of 'something
as (quote something)
, then you can say that splicing a single element list before a quote character has a meaning, and that it means quoting that single element. If you patch up the replacement interpretation like that, it then gives results consistent with real results.
For the last two, complication is that you must splice a list before a comma character (or a comma-at). What does it mean to splice before a comma character? It means nothing. But if you say "let it mean simply splicing a list and then putting a comma (or comma-at) in front of each inserted element", then this patched up replacement interpretation gives results consistent with real result.
Emacs Lisp Note: For the last two, Emacs Lisp and Common Lisp give different results.
Common Lisp implementations Note: For comma-quote-comma-at, different implementations give different results according to this thread
I would stay away from using any of the four cases in my code.