[racket] Where to put the ellipsis?

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. 


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