---

once-prog(dfp) ==
  let A,S,init,nxt = dfp
  in <A
     , S
     , init
     , s,m.
        evalall(let s',xout = nxt s m 
                in <case s'
                    of inl(s) =>
                     if bag-null(xout) then inl s  else inr   fi 
                     | inr(z) =>
                     inr  
                   , xout
                   >)>  

---

Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  it: ,  spreadn: spread4,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x ,  bag-null: bag-null(bs),  evalall: evalall(t)
Definitions :  spreadn: spread4,  lambda: x.A[x],  evalall: evalall(t),  spread: spread def,  apply: f a,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  bag-null: bag-null(bs),  inl: inl x ,  inr: inr x ,  it:
FDL editor aliases :  once-prog

---

once-prog(dfp)  ==
    let  A,S,init,nxt  =  dfp
    in  <A
          ,  S
          ,  init
          ,  \mlambda{}s,m.
                evalall(let  s',xout  =  nxt  s  m 
                                in  <case  s'
                                        of  inl(s)  =>
                                          if  bag-null(xout)  then  inl  s    else  inr  \mcdot{}    fi 
                                          |  inr(z)  =>
                                          inr  \mcdot{} 
                                      ,  xout
                                      >)>   


Date html generated: 2011_08_16-PM-06_17_08
Last ObjectModification: 2011_06_19-PM-07_31_33

Home Index