Nuprl Definition : bind-df-next1

bind-df-next1(F;dfpY;s;m) ==
  let s1,L = s
  in let s',b = if isl(s1) then F outl(s1) m else <s1, {}> fi
     in let L' = L + bag-map(

a.<a, inl df-program-state(dfpY a) >;b) in
let nxtouts = bind-nextouts1(L';dfpY;m) in
let spawned = bag-map(

p.(fst(p));nxtouts) in
let out =

p

nxtouts.snd(p) in
let nxtstate = if null(spawned)

(

isl(s')) then inr

else inl <s', spawned> fi in
<nxtstate, out>

Definitions occuring in Statement : bind-nextouts1: bind-nextouts1(L;dfpY;m), df-program-state: df-program-state(dfp), null: null(as), outl: outl(x), isl: isl(x), band: p

q, bnot:

b, ifthenelse: if b then t else f fi , let: let, it:

, pi1: fst(t), pi2: snd(t), apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, inr: inr x , inl: inl x , bag-combine:

x

bs.f[x], bag-append: as + bs, bag-map: bag-map(f;bs), empty-bag: {}
FDL editor aliases : bind-df-next1

bind-df-next1(F;dfpY;s;m) == let s1,L = s in let s',b = if isl(s1) then F outl(s1) m else <s1, \{\}> fi in let L' = L + bag-map(\mlambda{}a.<a, inl df-program-state(dfpY a) >b) in let nxtouts = bind-nextouts1(L';dfpY;m) in let spawned = bag-map(\mlambda{}p.(fst(p));nxtouts) in let out = \mcup{}p\mmember{}nxtouts.snd(p) in let nxtstate = if null(spawned) \mwedge{}\msubb{} (\mneg{}\msubb{}isl(s')) then inr \mcdot{} else inl <s', spawned> fi in <nxtstate, out> Date html generated: 2012_01_23-PM-12_01_27 Last ObjectModification: 2011_12_16-PM-06_23_29 Home Index