<div dir="ltr">Ahhh!! Your suggestion really simplifies and cleans up my original model! <div> </div><div>Thanks :-)</div><div> <div class="gmail_extra"> <div class="gmail_quote">On Mon, Jul 15, 2013 at 12:26 PM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> 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. <div class="HOEnZb"><div class="h5"> On Jul 15, 2013, at 12:40 PM, Monica Tomson <<a href="mailto:monica.tomson@gmail.com">monica.tomson@gmail.com</a>> wrote: > > > > On Mon, Jul 15, 2013 at 6:48 AM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>> 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: > > <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> > > </div></div></blockquote></div> <div> </div>-- <div dir="ltr">Monica</div> </div></div></div>