Nuprl Definition : bind-df-next3

bind-df-next3(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
<inl <s', spawned> , out>

Definitions occuring in Statement : bind-nextouts1: bind-nextouts1(L;dfpY;m), df-program-state: df-program-state(dfp), outl: outl(x), isl: isl(x), ifthenelse: if b then t else f fi , let: let, pi1: fst(t), pi2: snd(t), apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, 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-next3

bind-df-next3(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 <inl <s', spawned> , out> Date html generated: 2012_01_23-PM-12_01_58 Last ObjectModification: 2011_12_17-PM-12_12_46 Home Index