Nuprl Definition : bind-df-next2

bind-df-next2(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, df-program-state(dfpY a)>;b) in
         let nxtouts = bind-nextouts2(L';dfpY;m) in
         let spawned = bag-mapfilter(p.let a,s = fst(p) 
                                        in <a, outl(s)>;p.isl(snd(fst(p)));nxtouts) in
         let out = pnxtouts.snd(p) in
         <inl <s', spawned> , out>


Definitions occuring in Statement :  bind-nextouts2: bind-nextouts2(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: xbs.f[x],  bag-mapfilter: bag-mapfilter(f;P;bs),  bag-append: as + bs,  bag-map: bag-map(f;bs),  empty-bag: {}
FDL editor aliases :  bind-df-next2
bind-df-next2(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,  df-program-state(dfpY  a)>b)  in
                  let  nxtouts  =  bind-nextouts2(L';dfpY;m)  in
                  let  spawned  =  bag-mapfilter(\mlambda{}p.let  a,s  =  fst(p) 
                                                                                in  <a,  outl(s)>\mlambda{}p.isl(snd(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_49
Last ObjectModification: 2011_12_17-PM-12_06_23

Home Index