Nuprl Definition : Comm-next-continue

Comm-next-continue(l_comm;l_choose;piD;cSt) ==
  let st = Comm-st(cSt) in
   let q = Comm-q(cSt) in
   let waiting = Comm-waiting(cSt) in
   let count = Comm-count(cSt) in
   if waiting
   then <cSt, make-lg([])>
   else let p = Comm-process-q(q;l_comm;st) in
         let q' = fst(p) in
         let st' = fst(snd(p)) in
         let loc = fst(snd(snd(p))) in
         let mList = snd(snd(snd(p))) in
         if null(q')
         then <<st', [], l_comm, ff, count>, make-lg([])>
         else let msgs2choose = map(λx.<l_choose, mk-tagged("msg";pDVrequest(x;count))>;mList) in
                  <<st', q', loc, tt, count + 1>, make-lg([<l_comm, mk-tagged("msg";pDVcontinue())>] @ msgs2choose)>
         fi 
   fi 


Definitions occuring in Statement :  Comm-process-q: Comm-process-q(q;id;st),  Comm-count: Comm-count(cSt),  Comm-waiting: Comm-waiting(cSt),  Comm-q: Comm-q(cSt),  Comm-st: Comm-st(cSt),  pDVrequest: pDVrequest(rndv2;counter),  pDVcontinue: pDVcontinue(),  make-lg: make-lg(L),  map: map(f;as),  append: as @ bs,  null: null(as),  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  let: let,  pi1: fst(t),  pi2: snd(t),  lambda: λx.A[x],  pair: <a, b>,  add: n + m,  natural_number: $n,  token: "$token",  mk-tagged: mk-tagged(tg;x)
FDL editor aliases :  Comm-next-continue
Latex:
Comm-next-continue(l$_{comm}$;l$_{choose}$;piD;cSt)  ==
    let  st  =  Comm-st(cSt)  in
      let  q  =  Comm-q(cSt)  in
      let  waiting  =  Comm-waiting(cSt)  in
      let  count  =  Comm-count(cSt)  in
      if  waiting
      then  <cSt,  make-lg([])>
      else  let  p  =  Comm-process-q(q;l$_{comm}$;st)  in
                  let  q'  =  fst(p)  in
                  let  st'  =  fst(snd(p))  in
                  let  loc  =  fst(snd(snd(p)))  in
                  let  mList  =  snd(snd(snd(p)))  in
                  if  null(q')
                  then  <<st',  [],  l$_{comm}$,  ff,  count>,  make-lg([])>
                  else  let  msgs2choose  =  map(\mlambda{}x.<l$_{choose}$,  mk-tagged("msg";pDVrequest\000C(x;count))>mList)  in
                                    <<st',  q',  loc,  tt,  count  +  1>
                                    ,  make-lg([<l$_{comm}$,  mk-tagged("msg";pDVcontinue())>]  @  msg\000Cs2choose)
                                    >
                  fi 
      fi 


Date html generated: 2015_07_23-AM-11_58_52
Last ObjectModification: 2012_08_30-PM-01_49_35

Home Index