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
>
>
____________________
Racket Users list:
http://lists.racket-lang.org/users
