Per Bothner <xxxxxx@bothner.com> writes:

> Ok, let's finalize it then.  Thanks for your patience.

Ooops.  Mikael Djurfeldt <xxxxxx@mdj.nada.kth.se> just mailed me
a suggested formal syntax and semantics.  I'm just about to go
to bed, so I haven't had a chance to more than glance it, but it
seems to make sense to edit it in.  What do you people more
experienced in these things think?

I [i.e. Mikael] chose between an intuitive version which cuts pretty
deeply into the semantics of Scheme and a more conservative version
which was less intuitive.  I chose the former because of its clarity.

Though, it's worth noting that the change is less deep than it looks
like: We basically only add a new applicable type, and most
implementations in practise already have several applicable types
(several types of procedures, continuations etc).

----------------------------------------------------------------------
Extensions to formal syntax:

1. <generalized assignment> is substituted for <assignment> in the
   production for <expression>.

2. The following two productions are added:

   <generalized assignment> --> (set! <access spec> <expression>)

   <access spec> --> <variable>
		     | <procedure call>

----------------------------------------------------------------------
Extensions to formal semantics:

Abstract syntax:

1. A new alternative for `set!' is added to the production for Exp:

   Exp --> K | ... | (set! (E0 E*) E1)

Domain equations:

2. The following equation is added:

     Fs = L x (E* --> K --> C) x F

3. The equation for E is extended with Fs, i.e. it changes from

     E = Q + H + R + Ep + Ev + Es + M + F

   to

     E = Q + H + R + Ep + Ev + Es + M + F + Fs

Semantic functions:

4. The following definition is added:

     E[[ (set! (E0 E*) E1) ]] = E[[ ((setter E0) E* E1) ]]

Auxiliary functions:

5. `applicate' is changed from

     lambda e e* k . e belongs to F --> (e | F ref 2) e* k,
                       wrong "bad procedure"

   to

     lambda e e* k . e belongs to F --> (e | F ref 2) e* k,
                     e belongs to Fs --> (e | Fs ref 2) e* k,
                       wrong "bad procedure"

6. The following functions are added:

     setter: E* --> K --> C
     setter = onearg(lambda e k . e belongs to Fs --> send(e | Fs ref 3 in E),
				    wrong "bad procedure with setter")

     getter-with-setter: E* --> K --> C
     getter-with-setter =
       twoarg(lambda e1 e2 k sigma . e1 belongs to F -->
                (e2 belongs to F -->
		  (new sigma belongs to L -->
		    send(<new sigma, e1 | F ref 2, e2 | F> in E)
		    k
		    (update (new sigma | L) unspecified sigma),
		    wrong "out of memory" sigma),
		  wrong "bad procedure in second argument"),
		wrong "bad procedure in first argument")
--
	--Per Bothner
xxxxxx@bothner.com   http://www.bothner.com/~per/