From: Richard Underhill
Subject: Re: Why we must somtimes have lisp/scheme after all.
Date:
Message-ID: <dickkCuGJ4z.Fxq@netcom.com>
Handrik Boom writes
> I hear the usual complaints on this thread about Lisp's parentheses.
> There's been lots of syntaxes for different constructions that would
> otherwise be unreadable because of the parentheses. But there's a simple
> way to deal with most of the parentheses.
> Whenever a parenthesized phrase occurs at the end of another.
> use a slash instead of parenthesizing it, thus:
> (abf gut ( hnniuf slks))
> becomes
> (abf gut / hnniuf slks)
> this gets rid of most of the parenthesis clusters in Lisp.
> It makes it easy to use "if" instead of "cond",
> or a "let" without a list, because many such constructs naturally
> nest in their last argument.
That idea intrigues me but I am not convinced. Can someone
post a REAL program that uses the semicolon or the above slash
notation?
--
Richard Underhill ··@ccnext.ucsf.edu "If I cannot bring it up on my
monitor and it does not interfere with a major aspect of my physiology, like
eating, sleeping, or breathing, then it probably does not exist"
In article <···············@netcom.com>, Richard Underhill
<··@ccnext.ucsf.edu> wrote:
|Handrik Boom writes
|> I hear the usual complaints on this thread about Lisp's parentheses.
|> There's been lots of syntaxes for different constructions that would
|> otherwise be unreadable because of the parentheses. But there's a simple
|> way to deal with most of the parentheses.
|
|> Whenever a parenthesized phrase occurs at the end of another.
|> use a slash instead of parenthesizing it, thus:
|> (abf gut ( hnniuf slks))
|> becomes
|> (abf gut / hnniuf slks)
|> this gets rid of most of the parenthesis clusters in Lisp.
|> It makes it easy to use "if" instead of "cond",
|> or a "let" without a list, because many such constructs naturally
|> nest in their last argument.
|
|That idea intrigues me but I am not convinced. Can someone
|post a REAL program that uses the semicolon or the above slash
|notation?
FWIW, it looks to me like just an extension of the idea that one can write
(b . (a . NIL) as (b (a)) [Did I get that right? It's been years since
I've actually used dotted-pair notation.]
Of course we could take this to an extreme:
(c . (b . (a . nil))) -> (c (b (a)) --> (c (b / a)) --> (c / b / a)
The introduction of another symbol to grok and reform the list in my mind
doesn't seem like a savings to me for typing a few ()'s.
--
--
--
-- "TANSTAAFL" Rich ·····@ils.nwu.edu
Richard> FWIW, it looks to me like just an extension of the idea that
Richard> one can write
Richard> (b . (a . NIL) as (b (a)) [Did I get that right? It's been
Richard> years since I've actually used dotted-pair notation.]
No, actually it is
(b . (a . NIL)) == (b a)
or (b (a)) == (b . ((a . NIL) . NIL))
--
Simon.
In article <···············@netcom.com>, Richard Underhill <··@ccnext.ucsf.edu> writes:
|> Handrik Boom writes
...
|> That idea intrigues me but I am not convinced. Can someone
|> post a REAL program that uses the semicolon or the above slash
|> notation?
There is a lot of REDUCE code available somewhere using an Algol-style
syntax for Portable Standard Lisp (a precursor to Common Lisp).
Below is a small section of code written in Refine (a trademark of Reasoning
Systems), which is a wide-spectrum language built on top of Common Lisp.
There are a few non-lispish aspects used in this example, but I think any
Common Lisp programmer can read this and pretty much understand what is
happening. Some of it might look mysterious because Refine adds several
features to lisp such as an undefined value, pattern matching, it's own
object system, literal sequence formers, etc., but all of that is embedded
in an alternative syntax for lisp whose broad features are obvious here.
(This function is just one tiny piece of a system with several tens of
thousands of lines of code, so I'm not going to post the the whole program :)
Note that the third line of the file picks the grammar to use. In general,
functions can be defined with lisp or Refine (or other) syntax, whatever is
most convenient. Usually I find the Refine syntax convenient because I'm
using semantic features added by Refine, but occasionally lisp syntax is
convenient if I want to use macros or to control very precisely the lisp
code being generated.
Also note that once any of the top-level forms has been parsed by REFINE,
the resulting lisp code can be seen with a simple emacs command (e.g. meta-F).
I don't show the lisp code here simply because it's almost exactly what
you might expect.
I think the sequencing of LET's without indendation improves readability
as much as any other feature. This could be added directly to Common Lisp
with a MYLET macro that expands to LET forms:
(mylet (...)
...
mylet (...)
...)
Finally, the following example is not necessarily exemplary REFINE or LISP
code--it just illustrates the point about alternative syntax.
%%% -*- Mode: RE; Package: SLANG; Base: 10; Syntax: Refine -*-
!! in-package("SLANG")
!! in-grammar('re::regroup)
var *ASSUME-ALL-CONJECTURES-ARE-THEOREMS?* : boolean = false
var *QUERY-AFTER-PROVER-FAILURE?* : boolean = false
function VERIFY-CONJECTURE (conjecture : theorem,
s : spec)
: boolean =
let (s-nm = s-name(conjecture))
let (nm = if defined?(s-nm)
then format(false,"~A",s-nm)
else format(false,"~S",conjecture))
if *assume-all-conjectures-are-theorems?* then
comment("Assuming conjecture ~A is a theorem.",nm);
conjecture?(conjecture) <- false;
true
else
let (generic-task = make-verify-conjecture-task(conjecture,s))
let (kitp-task = convert-prover-task-to-kitp-proof-object(generic-task))
let (generic-constraint-assignments =
prover-constraint-assignments(prover-task-constraints(generic-task)),
generic-ui-assignments =
prover-ui-option-assignments(prover-task-ui-options(generic-task)))
let (kitp-assignments =
convert-generic-to-kitp-assignments(generic-constraint-assignments)
++
convert-generic-to-kitp-assignments(generic-ui-assignments))
let (vars = [v | (v) <v,@@> in kitp-assignments],
vals = [v | (v) <@@,v> in kitp-assignments])
let (result = progv(vars,vals,develop-proof(kitp-task)))
(if result = true then
comment(" Verified conjecture for ~A.",nm);
conjecture?(conjecture) <- false
else
warn("Prover (KITP) could not verify conjecture ~A : ~S", nm, conjecture);
if *query-after-prover-failure?* then
let (lisp::*package* = *spec-package*)
format(true,"~/pp/",conjecture);
if ri::menu-y-or-n?("Accept conjecture (shown in *REFINE* window) as verified anyway?")
then
conjecture?(conjecture) <- false;
result <- true);
result
--
James McDonald
Kestrel Institute ········@kestrel.edu
3260 Hillview Ave. (415) 493-6871 ext. 339
Palo Alto, CA 94304 fax: (415) 424-1807