Ahhh!! Your suggestion really simplifies and cleans up my original model! Thanks :-)
On Mon, Jul 15, 2013 at 12:26 PM, Matthias Felleisen <matth...@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.tom...@gmail.com> > wrote: > > > > > > > > > On Mon, Jul 15, 2013 at 6:48 AM, Matthias Felleisen < > matth...@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
____________________ Racket Users list: http://lists.racket-lang.org/users
