[racket] Where to put the ellipsis?

On Mon, Jul 15, 2013 at 1:31 PM, Matthias Felleisen <matthias at ccs.neu.edu>wrote:

>
> For thread swapping, consider
>
> (--> [n C E S K {th_1 ... (n_i C_i E_i K_i) th_j ...}]
>      [n_i C_i E_i S K_i {th_1 ... (n C E K) th_j ...}])
>
> as a rule. This illustrates ellipses. The rule non-deterministically picks
> one of the threads to swap in and Redex can show you all branches.
>
> Alternative, rotate threads in and out.
>
> The above rule uses different kinds of parens to delimit pieces; this
> works in Redex.
>
> BTW, names are optional.
>
>
>
Really useful! Good learning experience so far!
 Appreciated!

Doing wait/notifyall now, in addition to the join/spawn. :)

Hopefully I can test out some simple cases when it is done..

Thanks again,
--Monica


> On Jul 15, 2013, at 2:57 PM, Monica Tomson <monica.tomson at gmail.com>
> wrote:
>
> > Ahhh!! Your suggestion really simplifies and cleans up my original model!
> >
> > Thanks :-)
> >
> >
> >
> > On Mon, Jul 15, 2013 at 12:26 PM, Matthias Felleisen <
> matthias at ccs.neu.edu> wrote:
> >
> > I don't think you need 'dots' for what you want.
> >
> > Here is how you can organize your states:
> >  n -- name of current thread
> >  C -- control of current thread
> >  E -- env of current thread
> >  S -- global store
> >  K -- continuation of current thread
> >  T -- thread pool : Name |-->f <C E K> (a finite map from names to
> states)
> >
> > Then your beta-value reduction works as normal on the registers C
> through K and you can keep n and T opaque.
> >
> > Thread switches swap in/out the relevant C E Ks.
> >
> > No ellipses needed to single out the current thread.
> >
> >
> >
> > On Jul 15, 2013, at 12:40 PM, Monica Tomson <monica.tomson at gmail.com>
> wrote:
> >
> > >
> > >
> > >
> > > On Mon, Jul 15, 2013 at 6:48 AM, Matthias Felleisen <
> matthias at ccs.neu.edu> wrote:
> > >
> > > Is this supposed to be a CESK machine state where you apply \x.M to V
> (actually V and the empty env, which is a highly unusual left-hand side)?
> > >
> > > Yeah. the machine is a CESK machine, and the reduction rule is
> function application essentially.
> > >
> > > The change is that I want to model thread spawn and join,
> > > which I think I can remodel the whole machine  in the way  that I can
> still "plug" the previous rules, except join and spawn, which i need to
> write new). and So, the model with thread is:
> > >
> > >  (context (M ε κ))
> > >  (thread (tid context) )
> > >  (threads  (thread ...))
> > >
> > > at the same time using a global store (Store) for simplicity, but
> really a state is a threads * store
> > >
> > > and for the reduction with syntax error reported in the previous rule,
> > >  (Some mistakes in  the original post, so I copy-past it again below),
> > > I try to use pattern matching the treads list, which tries to get the
> first thread entry from the list of threads,
> > >
> > > (-->
> > >     (((tid   (V ε (fn ((λ X M) ε_f) κ))) ...) S) ; tid, context
> > >      (((tid  (M  (update ε_f X σ_n) κ)) ...) S)
> > >      tcesk3
> > >      (where σ_n ,(fresh-σ))
> > >      (side-condition
> > >       (not (redex-match thread-cesk-iswim-plus X (term V ))) )
>  ;syntax: missing ellipsis with pattern variable in template in: V
> > >     (side-condition
> > >       (begin (store-update! (term σ_n) (term (V ε)) Store) #t)))
> > >
> > > I am not sure the design or the whole things making sense or not, but
> just trying to do some exercise of using PLT-Redex...
> > >
> > > Thanks,
> > > --Monica
> > >
> > >
> > >
> > > On Jul 15, 2013, at 4:28 AM, Monica Tomson wrote:
> > >
> > > > Hi,
> > > >
> > > > I have the following reduction rule, it keeps on throwing the
> compiling error:missing ellipsis with pattern variable in template in: V
> > > >
> > > > I am confused where to put the ellipsis?
> > > >
> > > >
> > > > (--> ;((V ε) S (fn ((λ X M) ε_f) κ))
> > > >         ;((M (update ε_f X σ_n)) S κ)
> > > >      ((tid  (V ε (fn ((λ X M) ε_f) κ))) ...) ; tid, context
> > > >      ((tid  (M  (update ε_f X σ_n) κ)) ...)
> > > >      tcesk3
> > > >      (where σ_n ,(fresh-σ))
> > > >      (side-condition
> > > >       (not (redex-match thread-cesk-iswim-plus X (term V ))) )  ;
> ERROR: syntax: missing ellipsis with pattern variable in template in: V
> > > >     (side-condition
> > > >       (begin (store-update! (term σ_n) (term (V ε)) Store) #t)))
> > > >
> > > > Thanks,
> > > >
> > > > --Shuying
> > > > ____________________
> > > >  Racket Users list:
> > > >  http://lists.racket-lang.org/users
> > >
> > >
> >
> >
> >
> >
> > --
> > Monica
>
>


-- 
Monica
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130715/258ea2a3/attachment-0001.html>