Among other items:

  > 8. Add implicit (BLOCK DEFUN ...) around body of defuns
  >
  > (BLOCK function-name ...) is automatically added around the body of
  > defuns now; this enables (RETURN-FROM function-name ...) to be used.
  > It would be convenient for (BLOCK DEFUN ...) to be added as well, so
  > that (RETURN-FROM DEFUN ...) can be used.  This obviates the task of
  > editing RETURN-FROM forms when the name of the function is changed
  > and facilitates writing macros that produce defuns with RETURN-FROM
  > forms.

Making any symbol (apart from NIL) a special case for RETURN-FROM
seems inelegant.  Wouldn't it be better to have a macro called (say)
FRETURN which can be used only lexically within a function definition
(a DEFUN form, maybe a LAMBDA form as well) as if

  (defun foo (...)
    ...)

is implicitly

  (defun foo (...)
    (block #1=#:function
      (macrolet ((freturn (&optional value) `(return-from #1# ,value)))
        ...)))

In fact I was wrong to suggest LAMBDA forms since there might be
a macro that expands into a LAMBDA form which would shadow the
DEFUN and cause FRETURN to return not from the block intended by
the programmer.

As to FRETURN from DEFUN, here's an implementation in case
someone wants to try it out.

----- cut here -----
;;;; freturn        -*- Mode: lisp; Package: lux -*-
;;; Purpose: FRETURN returns from a function.
;;; Exports: DEFUN, FRETURN.
;;; Created: VaN [1999 Jul 23]
;;; Author: Vassil Nikolov <vniko...@poboxes.com>
;;; Warning: no warranty!

#|  Implementation:

  (lux:defun foo (...)
    [[ declaration... | doc-string ]]
    form...)

->

  (cl:defun foo (...)
    [[ declaration... | doc-string ]]
    (defun-body-block foo
      form...))

->

  (cl:defun foo (...)
    [[ declaration... | doc-string ]]
    (block #:foo
      (macrolet ((freturn (result) `(return-from #:foo ,result)))
        form...)))

|#

(cl:defpackage lisp-user-extensions
  (:nicknames lux)
  (:shadow defun)
  (:export defun freturn))
(cl:in-package lux)

;;; auxiliaries:

(cl:defun decl-or-doc-string-p (item tail)
  "Returns true if item is a declaration or a doc-string.
Used to process function bodies.  The second argument is
the rest of the body after item."
  (typecase item
    (cons (eql 'declare (first item)))  ;no check for malformed ones
    (string tail)  ;a string is not a doc-string if it comes last
    (otherwise nil)))

(cl:defun body-forms (defun-body)
  "Returns the sublist of defun-body that contains just the
forms (skipping any declarations and doc-string)."
  ;; Does not check if there are two or more doc-strings.
  ;; I could do here with a function that is to MEMBER-IF as
  ;; MAPLIST is to MAPCAR.
  (do ((l defun-body (rest l)))
      ((endp l) '())
    (unless (decl-or-doc-string-p (first l) (rest l))
      (return l))))

(defmacro defun-body-block (name &body defun-body-forms)
  "Wraps a block around a function body from which FRETURN
may be used to return."
  `(block ,name
     (macrolet ((freturn (&optional (result 'nil))
                  `(return-from ,',name ,result)))
       ,@defun-body-forms)))

;;; exports:

(defmacro freturn (&optional (result 'nil))
  "Returns from the immediately enclosing function definition
introduced by LUX:DEFUN.  Within (LUX:DEFUN FOO ...),
(FRETURN form) === (RETURN-FROM FOO form).
Rationale: if the name of the function changes, FRETURN forms
don't need to change."
  (declare (ignore result))
  (error "FRETURN may be used only within a DEFUN form."))

(defmacro defun (name lambda-list &body dds+forms)
  "This extends CL:DEFUN by allowing the use of LUX:FRETURN to return
from the function."
  (let ((block-name (make-symbol (symbol-name name)))
        (forms (body-forms dds+forms)))
    `(cl:defun ,name ,lambda-list
       ;; declarations and doc-string:
       ,@(ldiff dds+forms forms)
       ;; forms (this is silly but harmless if there are none):
       (defun-body-block ,block-name ,@forms))))

;;; eof.
----- end -----

 (defun foo (x)
   (+ (if (zerop x) (return-from foo 7) x) 3))

 (defun bar (z
   (+ (foo z) 2))

and then (by sloppy editing) grabbing the body and dropping it into

 (defun bar (z)
   (+ ((lambda (x) (+ (if (zerop x) (return-from foo 7) x) 3)) z)
      2))

and just compiling it with no errors.  This will flag a reminder that
you've moved to a new context and you need to identify the FOO boundary.
If you'd instead used the FRETURN idiom, you'd find 7, not 9, being
returned from BAR when z is 0 once you substituted things, and you'd
get no compilation warning about the fact that this was going to happen.

For the benefit of those who suggested there were no good uses for it.

FWIW, programming by cut-and-paste is always going to be at risk for a
multitude of "capture errors", so I'm not sure this is a valid
drawback to return-from.

Emacs, he explained to me, is powerful exactly because it simultaneously
allows access to multiple representations at the same time, tolerating
quick switching back and forth between "s-expression commands", "word
commands", "character commands",  "line commands", etc.  So I can go
"up a line" even though Lisp has no "line structure". Or I can go forward
an s-expression even though text has no s-expression structure.
This leads to a very concise language for describing edits.  Yes, it's
possible to have more rigid sexp-only or text-only tools do your editing,
but such tools are always going to have the problem that you can see an
"expression style" and cannot quickly use it because the more rigid tool
does not accomodate it, so you'll be forced to say something more clumsy.

I'd draw three parallels:

a) Godel's "Incompleteness" theorem.  

Bertrand Russell was trying to come up with a "Principia Mathematica,"
where some limited set of mathematical axioms could be used to
construct all the rest of the things that mathematics could prove.
That is, pretty much, the reductionist view where "If you come up with
a suitable set of perfect tools, you can build everything, and if you
have the right set of transitions, it's done perfectly."

Kurt Godel established that in any propositional system, there would
be true statements that could not be proven within the system's
context.

Thus, the idea is broken from a purely theoretical perspective.

I would suggest the connection that it may be *impossible* to create
an editor that *guarantees* that (for instance) an SGML document is
valid at every step.

b) ISO 9000 and "Dilbertian Managers"

Modern business enterprises have fallen into the same trap; they
figure that if you write up a suitable set of "Quality Management"
documents, whether ISO 900x or for "Malcolm Baldridge," you can, via
clearly defined procedures, prevent problems from occurring, and
thereby produce better results.

As with mathematics, where theorems sometimes prove useful results,
there *can* be merit to this, but, as Russell found, creating a
"Principia Manageria" is largely a fool's errand.  Scott Adams touched
the pulse of this when he created Dilbert and his coworkers.

Cases where managers that are technically illiterate hear from other
technically illiterate managers schemes for "preventing" programming
errors represent a good example of this.

Amaya isn't an example of this; it is an example of some researchers
trying out something that is academically interesting, but probably
not viable as a technology.

c) Mathematical programming and "relaxation methods."

One of the major classes of methods of solving mathematical
programming problems is that of Lagrangian relaxation, where the basic
idea is to take a problem that involves constraints and objectives,
and relax some of the constraints, transforming them into objectives.

This is particularly useful when you are trying to solve a problem
where you don't start with a feasible solution; you relax the problem
by saying "We'll assume that some initial value is good enough for
now, and then attach hefty costs to the violations of constraints so
as to encourage the solution scheme to move towards feasible
solutions."

In effect, this is what a good Lisp editor can do to help the
programmer; you can do whatever you like to the lines of text (which
can make the program incorrect, e.g. "infeasible"), but by providing
things like "intelligent" indentation and parenthesis counting, the
editor provides feedback to encourage the programmer to make the
program look "more correct," at least from a "syntax/form" point of
view.  (There is obviously no solution to the problem of writing
Stupid Code.)

  no, this is trivial to create.  having such an "editor" would make design
  of DTDs almost doable, since the "editor" would have to create a complete
  document for you and then let the user make branch decisions, showing
  which options were available at all times.  (what's not so trivial is
  making such an "editor" comfortable to use for humans.)

I find it works pretty well for putting together SGML documents.  I've
written some fairly large ones with it, mostly analysis and
requirements specs for some of the larger projects my employer has
undertaken.

It offers you a list of elements that are valid at any point in the
document, but does not force the document to be valid at all times.
For instance when putting together a varlist in Docbook documents, I
usually just put open and close tags in as I need them, as opposed to
creating a valid structure for the varlist and then filling it in.
psgml-mode lets me do that and makes it easy to close up the structure
as I pass thru it.  At various points the document is invalid, but it
does seem to follow my normal thought process for writing a document.

obLisp: I have some elisp code for inserting SGML templates into a
docoument.  The idea was to provide our HTML monkeys who usually work
with BBEDIT or something similiar a set of buttons for inserting large
hunks of HTML which they would then fill in.  To make it even easier
on them, I also have code which will insert the template with elisp
code embedded in it, so as they insert it, it asks them questions
about what should go where.  Overall psgml-mode is pretty sweet.

Unfortunately I expect that it is entirely unavailable now, as the
machines it ran on were even more of a dead-end than the other Lisp
machines.

(The drawing package on those machines was also very good.  The text
editor was rubbish though.)

In Maclisp, there was an s-expression editing tool called the
"kludgey binford editor" that edited s-expressions in a token-based way
where you could say teco-like commands that inserted and deleted and
moved over s-expressions, but it also let you just insert a single
paren and then go somewhere else and insert another paren (not necessarily
at the same level) and then you could do a command that asked that it
re-compute paren matches and it would rationalize the tree to make the
two parens you had inserted become "real parens" (that is, make the
tree work).  That's a cool accomodation to both structured and
non-structured.  I think it was probably the case that INTERLISP
had things like this its DWIM facility, but I never used it so don't know
for sure.  But Emacs was much better because it basically always manages
the general case and only imposes syntax requirements when you issue
a syntax-oriented command (like forward-sexp).  It's easy to make
"Save File" be a syntax-oriented command so you can't save ill-formed
buffers, but you don't have to make it so.

Amaya may guarantee the generation of "valid" HTML.  But if it's too
annoying to use, people won't use it, and will prefer some other tool
that is not so "guaranteed valid."

I think the art and science of language design is not about the easy
part of just defining things to have clear semantics; it's about the
software equivalent of worrying that users will confuse floppy disk
drives with coffee cup holders, and understanding that the entire
burden of avoiding that problem is not in just getting better
customers but really coming to grips with what people really do, not
what you wish they would do.  You're welcome to make your name
designing languages that don't acknowledge this truth, and I wish you
luck.  I have staked my career and reputation on the idea that
understanding and accepting what people really want to do is important
and not to be neglected.  Indeed, I believe that users often do things
that appear superficially stupid but that if you examine them with
more care you realize were not so foolish as they seem.  It's easy to
trivialize out the parts of something you see someone do that don't
fit your model, but sometimes those parts are the important ones.

the "Principia Mathematica" approach is wonderful, admirable and even
somewhat resembling lisp/scheme/forth.
with just a few primitives you build up a rich, closed world. even if
goedel smashed the completeness i don't care because this is just
philosophy. i don't need proofs about my world, self-consciousness, if
lisp is complete or not, if i'm complete ;) ... => obviously not.

if it's important i can prove it by using methods outside of the lisp or
editors or robots world.

to come to the editor:
it is too simple to give up saying that it is *impossible* because it
cannot be *proved*. halting problem and such. it can be proved but not
within the closed world assumption of either SGML or LISP or
whatssoever. a robot cannot proof its world view but it can reason and
do. it can be coded, it can process input and output to the best of its
world, that's the point. if it fails it must be rebooted :)

the editor cannot guarantee to stop or fall into an endless loop, but if
it stops it can be formally guaranteed that the input or output is
correct. you as meta reasoner can proof that. the editor does not care.

What Godel established was that P.M. could not be a *complete* work.

This does not establish that the study of mathematics is dumb because
you can't have The Complete Book Of Mathematics, only that trying to
have The Complete Book of Mathematics is impossible.

In keeping with an attempt to keep this relevant, the most precise
analogy is probably that it is not possible to create a program editor
that guarantees that all program written using it will terminate.

And from a more relevant standpoint, it seems to be a Pretty Difficult
Problem to build an editor that guarantees the syntactic correctness
of programs and all transformations thereof, whilst simultaneously
remaining *usable* by mere humans.

It seems to be more appropriate to build editors that don't maintain
such guarantees, but rather allow the programmer to make changes that
may temporarily "break" the code, but then provide tools that provide
maximum assistance to the user to help fix the problems.

Interesting, but I think your analogy is slightly off. Better might
be to equate the legal steps in the editor to theorems (or maybe even
better, rules of inference) in the proof system. Then you'd get a
statement like this:

  While it is certainly possible to create an editor that guarantees
  that an initially valid SGML document remains valid after every
  subsequent allowed editing step, Godel's Proof suggests that there
  will always be some valid SGML documents which it is impossible
  to create using such an editor.

-Rob

  in what way is a mathematical proof a _process_ that resembles editing?

  Gödel's Incompleteness Theorem isn't a trivial statement of a problem
  with all sorts of complex systems.  is very carefully constrained to say
  something about proofs _inside_ a complex system.  it is possible to
  prove any mathematical theorem, but you might have to add something from
  outside the system to accomplish it.  the incompleteness theorem states,
  as far as I have understood it, that no system is able to prove all its
  true statements within itself.  I find that intuitively evident, because
  "truth" is already a concept that is not contained fully by the system.
  of course, I live in a post-Gödel time and lots of stuff that was very
  far from intuitively evident at the time is intuitively evident today,
  thanks in to the trailblazing efforts of geniuses past.

  however, Gödel's Incompleteness theorem is perhaps the single most
  mis-popularized theorem from mathematics there is, probably because
  people still believe in the pre-Gödel idea that truth is contained by
  a system, such as and especially religions.

  the above statement from Rob Warnock sounds like New Age flirting with
  quantum physics to me.  it sounds profound because what it flirts with is
  profound, while it's really just unfounded and confused opinion.

  in other words: I'd really like to see some evidence that there exists a
  valid string in a regular syntax that cannot be produced by the grammar.

* Erik Naggum
|
| the incompleteness theorem states, as far as I have understood it,
| that no system is able to prove all its true statements within
| itself.

This is almost exactly my understanding as well, with two additions:

  - there is a complexity limit for such systems beneath which you can
    prove all true statements

  - you can extend the system to a point where you can prove all true
    statements, but then the system will contain inconsistencies

It is also worth noting that Gödel only proved this in a specific case
and never generalized the theorem to cover all formal systems.
However, as far as I know, no mathematicians at the time doubted that
this was possible or considered it necessary.

Indeed, I think that for any grammar for which parsing does not pose a
halting problem this is true, because I can simply encode the grammar
rules as editing rules, and thus reduce the problem to parsing the
string.  And I think that there is no halting problem parsing SGML.

In a proof you start with a set of axioms and transform them step by step
with permitted rules of inference to produce theorems, which augment the
set of axioms. If by following this process recursively you derive the
thing-to-be-proved, then you've proved it to be true. If you derive the
negation of the thing-to-be-proved, then you've proved it to be false.
If you fail to do either, then... well, you've failed to do either.

In a ("fascist") structuring editor, you start with a valid structure
(or structured document, such as SGML), and step-by-step select & apply
individual permitted transformations, each one of which takes a valid
structure and produces another valid structure to replace it. If, though
this process, you manage to get the structure (or document) to the point
where you wanted to go (wherever that was), then you win. If you fail...
well, then you fail.

In the first case, Godel proved that (if the proof system is consistent)
there are some true statements that can be expressed within the system
that cannot be proved (from within the system) to be true (or false).

In the second case, I hypothesized that there are some legal SGML
documents that a human using a strict structuring editor cannot write
from scratch (from the grammar's start symbol), at least, not in any
practical sense.

I readily admit the analogy is a bit weak (but IMHO still more
appropriate than the Christopher Browne article I was replying to).

+---------------
|   Godel's Incompleteness Theorem isn't a trivial statement of a problem
|   with all sorts of complex systems.  is very carefully constrained to say
|   something about proofs _inside_ a complex system.
+---------------

Yes, I know that. [Although Gregory Chaitin's restatement of it in
terms of "complexity" makes it somewhat more approachable, e.g.,
  <URL:http://www.cs.auckland.ac.nz/CDMTCS/chaitin/georgia.html>
  <URL:http://www.cs.auckland.ac.nz/CDMTCS/chaitin/unm2.html>
  <URL:http://www.cs.auckland.ac.nz/CDMTCS/chaitin/rov.html>
for starters...]

+---------------
|   the above statement from Rob Warnock sounds like New Age flirting with
|   quantum physics to me.  it sounds profound because what it flirts with is
|   profound, while it's really just unfounded and confused opinion.
+---------------

Again, it was in reply to Christopher Browne's article <URL:news:slrn7pl9fo.
tro.cbbro...@knuth.brownes.org> which claimed that Godel's proof implied:

        "...that it may be *impossible* to create an editor that *guarantees*
        that (for instance) an SGML document is valid at every step."

I certainly don't believe *that*!  ...that is, if "SGML validity" has any
decidable meaning in the first place. (Which I surely *hope* it does, but
then, you're far more an expert on that than I.)

+---------------
|   in other words: I'd really like to see some evidence that there exists a
|   valid string in a regular syntax that cannot be produced by the grammar.
+---------------

Is SGML a "regular" syntax? And what exactly do you mean by "regular" here?
Certainly not "regular expression". "Context-free" perhaps? LL(k)? LALR(k)?
Or something more general still?  (Hopefully no full context-sensitive?)
Anyway, not to bicker.  That's not really the issue. What I was trying to
say to Browne was:

1. That *of course* it's possible to have an editor guarantee that an
   SGML document is valid at every step [assuming "SGML validity" has any
   meaning]. Simply run the document through your full "SGML validator"
   after every editing step, and if it fails, beep, print an error message,
   and forcefully undo the most recent editing step.

2. However, just because there may be an algorithmic way to validate (or not)
   a piece of text purporting to be SGML, there's no guarantee that there's
   any effective procedure for *getting* from "here" to "there" [where
   "here" is the (presumably-valid) SGML you started the editing session
   with and "there" is whatever goal you (a human) are trying to get to]
   using the "editing steps" available in the editor.

3. I would claim that generating one production of the SGML grammar per
   editing step is a totally unwieldy human interface, and anyway, how would
   you *select* which one to generate (expand) at each step? (E.g., if SGML
   has any ambiguity in the grammar at all, the combinatorics explode.)

   [I'm assuming of course that you don't *have* the desired end result
   already, otherwise you could just run it through an SGML parser and
   the walk the parse tree in the editor step-by-step to "create" it...]

4. Thus, depending on the primitive transformation steps the editor *does*
   permit you, there may well be valid SGML texts [that even pass the
   automated validator in the editor!] that no human could use that editor
   to write from scratch (from the SGML "start" symbol) in any practical sense.

The analogy to Godel's Proof seemed obvious to me (especially when
considering Chaitin's notion of "elegant programs" and their unprovability).

But maybe that still sounds like just more "New Age quantum-babble" to you.
If so, I apologize, and will shut up now.

-Rob

Unfortunately, `allowed transformations' *is* the issue, at least where
humans & editors are concerned. The point is *not* proving the validity
of an a priori given text, but starting with *nothing* (well, the SGML
grammar's "start" symbol) and writing something "useful" (whatever you
as a human consider a "useful" end-product to be) given only the `allowed
transformations' in a strict validating editor.

Think of it this way: Suppose you were asked to write a *huge* Lisp
program, but one of the rules was that you had to use an editor
that *forced* your program to be "legal Lisp" (including "validly"
compiling) after every single keystroke.  E.g., imagine using Emacs
and putting a hook in the keyboard input processing that ran the
Lisp compiler after every keystroke[*] and if the compiler barfed
it would *undo* the keystroke!  Do you actually think you could
do that?  [I don't think *I* could!]

-Rob

[*] O.k., to make it easier we'll even allow "fat" keys and macros to
count as "one" keystroke. And maybe even allow a whole Lisp symbol...

  sure, but where are the axioms of editing?  insert and delete?  and how
  are they related to the formal system under scrutiny?  as far as I know,
  SGML doesn't have such axioms to begin with, and production of a string
  from a grammer is not quite a transformation, it's a _production_.  so I
  think this is a stretch.

| Again, it was in reply to Christopher Browne's article <URL:news:slrn7pl9fo.
| tro.cbbro...@knuth.brownes.org> which claimed that Godel's proof implied:
|
|       "...that it may be *impossible* to create an editor that *guarantees*
|       that (for instance) an SGML document is valid at every step."
|
| I certainly don't believe *that*!  ...that is, if "SGML validity" has any
| decidable meaning in the first place. (Which I surely *hope* it does, but
| then, you're far more an expert on that than I.)

  *snicker*  yes, it has a decidable meaning.  SGML ain't _that_ bad.

  I found the statement you quote flimsy and impossible to argue against.

| Is SGML a "regular" syntax?  And what exactly do you mean by "regular" here?

  yes, SGML's DTDs defines a regular syntax, "regular" being defined as
  LL(0), or that any rule of grammar can only add tokens at the end of the
  string.

| Certainly not "regular expression".

  um, that's the idea.  why "certainly not"?

| 1. That *of course* it's possible to have an editor guarantee that an
| SGML document is valid at every step [assuming "SGML validity" has any
| meaning]. Simply run the document through your full "SGML validator"
| after every editing step, and if it fails, beep, print an error message,
| and forcefully undo the most recent editing step.

  <aside>and an SGML validator can return "this is not an SGML docuemnt" as
  its only error message, which is more useful than most of the other error
  messages you'll try to recover from.</aside>

| 3. I would claim that generating one production of the SGML grammar per
| editing step is a totally unwieldy human interface, and anyway, how would
| you *select* which one to generate (expand) at each step?

  the DTD grammar is fairly well constrained.  the approach isn't all that
  useful for writing DTDs, only the element structure of the document.

  consider a Lisp editor that does the same thing.  suppose you have an
  empty buffer, which is a fully valid Lisp source file.  if you insert to
  parens, (), you still have a valid Lisp source file, and I'll maintain
  that invariant.  inside the (), any function or special form in the
  prevailing package is allowed.  suppose you type a function name, the
  appropriate number of argument slots should be indicated and the document
  is at this point invalid until all slots have been filled in.  optional
  arguments could easily be indicated by a shaded slot or whatever.
  keyword arguments could be indicated by a key which expands to the list
  of available keywords when clicked on, like a menu of choices, etc.
  suppose you type LET instead of a function name.  a LET form is valid if
  it has an empty binding clause and an empty body, so the buffer would
  have to contain at least (LET ()).  the inner () is straight-forward to
  insert automatically, and any bindings inside it would know what they
  were, too, which could even be used to "verify" that any free variables
  were importable from the outer environment.  that's how a Lisp
  syntax-sensitive editor would work.  SGML makes this easier, since it
  allows far less choice.

| 4. Thus, depending on the primitive transformation steps the editor
| *does* permit you, there may well be valid SGML texts [that even pass the
| automated validator in the editor!] that no human could use that editor
| to write from scratch (from the SGML "start" symbol) in any practical
| sense.

  I still don't buy this.

| But maybe that still sounds like just more "New Age quantum-babble" to you.
| If so, I apologize, and will shut up now.

  ok.  ;)

However this is a classic chinese-room argument -- while I can argue
that it is theoretically possible to do this, the number of moves
might be kind of large.

(the kinds of moves in the editor I guess would be

        () -> (progn)
        (progn . x) -> (progn (defun y ()) . x)
        (defun () . x) -> (defun (y) . x)
        (defun (x . y) . z) -> (defun (p x . y) . z)

and so on.  Pretty painful!)