Nuprl Definition : pv8_p1_CommanderOutput

pv8_p1_CommanderOutput(Cid;Op;accpts;reps) ==
  zm.let bnum,zn = zm 
      in let s,p = zn 
         in let f = ldr,z.
                     let acloc,b = z 
                     in waitfor.if eqof(union-deq(  Id;Unit;product-deq(;Id;IntDeq;IdDeq);unit-deq())) bnum b
                                 then if bag-size(waitfor - acloc) <z pv8_p1_threshold(accpts)
                                      then pv8_p1_decision'broadcast(Cid;Op) reps <s, p>
                                      else {}
                                      fi 
                                 else {pv8_p1_preempted'send() ldr b}
                                 fi  in
                once-class(f@Loc|Loc,pv8_p1_p2b'base(), pv8_p1_CommanderState(accpts) bnum|)


Definitions occuring in Statement :  pv8_p1_CommanderState: pv8_p1_CommanderState(accpts),  pv8_p1_decision'broadcast: pv8_p1_decision'broadcast(Cid;Op),  pv8_p1_preempted'send: pv8_p1_preempted'send(),  pv8_p1_p2b'base: pv8_p1_p2b'base(),  pv8_p1_threshold: pv8_p1_threshold(accpts),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  once-class: once-class(X),  id-deq: IdDeq,  Id: Id,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  let: let,  unit: Unit,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  int: ,  bag-remove: bs - x,  union-deq: union-deq(A;B;a;b),  product-deq: product-deq(A;B;a;b),  unit-deq: unit-deq(),  int-deq: IntDeq,  eqof: eqof(d),  bag-size: bag-size(bs),  single-bag: {x},  empty-bag: {}
FDL editor aliases :  pv8_p1_CommanderOutput pv8_p1_CommanderOutput
pv8\_p1\_CommanderOutput(Cid;Op;accpts;reps)  ==
    \mlambda{}zm.let  bnum,zn  =  zm 
            in  let  s,p  =  zn 
                  in  let  f  =  \mlambda{}ldr,z.
                                          let  acloc,b  =  z 
                                          in  \mlambda{}waitfor.if  eqof(union-deq(\mBbbZ{}
                                                                        \mtimes{}  Id;Unit;product-deq(\mBbbZ{};Id;IntDeq;IdDeq);unit-deq())) 
                                                                        bnum 
                                                                        b
                                                                  then  if  bag-size(waitfor  -  acloc)  <z  pv8\_p1\_threshold(accpts)
                                                                            then  pv8\_p1\_decision'broadcast(Cid;Op)  reps  <s,  p>
                                                                            else  \{\}
                                                                            fi 
                                                                  else  \{pv8\_p1\_preempted'send()  ldr  b\}
                                                                  fi    in
                                once-class(f@Loc|Loc,pv8\_p1\_p2b'base(),  pv8\_p1\_CommanderState(accpts)  bnum|)


Date html generated: 2012_02_20-PM-07_27_30
Last ObjectModification: 2012_02_06-PM-01_45_40

Home Index