---

delay-df-program(dfp) ==
  let C,S,s,F = dfp
  in <C
     , S?  bag(C)
     , <inl s , {}>
     , s,a.
        evalall(let hs,buf = s 
                in case hs
                   of inl(s1) =>
                    let hs',out = F s1 a 
                    in let buf' = if 0 <z bag-size(out) then out else buf fi  in
                           <if (isl(hs'))  (bag-size(buf') = 0)
                            then inr  
                            else inl <hs', buf'> 
                            fi 
                           , buf
                           >
                    | inr(x) =>
                    <inl s , buf>)>  

---

Definitions occuring in Statement :  isl: isl(x),  eq_int: (i = j),  band: p  q,  bnot: b,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  let: let,  it: ,  spreadn: spread4,  unit: Unit,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x ,  union: left + right,  natural_number: $n,  bag-size: bag-size(bs),  empty-bag: {},  bag: bag(T),  evalall: evalall(t)
Definitions :  spreadn: spread4,  product: x:A  B[x],  union: left + right,  unit: Unit,  bag: bag(T),  empty-bag: {},  lambda: x.A[x],  evalall: evalall(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  apply: f a,  let: let,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  band: p  q,  bnot: b,  isl: isl(x),  eq_int: (i = j),  bag-size: bag-size(bs),  natural_number: $n,  inr: inr x ,  it: ,  pair: <a, b>,  inl: inl x 
FDL editor aliases :  delay-df-program

---

delay-df-program(dfp)  ==
    let  C,S,s,F  =  dfp
    in  <C
          ,  S?  \mtimes{}  bag(C)
          ,  <inl  s  ,  \{\}>
          ,  \mlambda{}s,a.
                evalall(let  hs,buf  =  s 
                                in  case  hs
                                      of  inl(s1)  =>
                                        let  hs',out  =  F  s1  a 
                                        in  let  buf'  =  if  0  <z  bag-size(out)  then  out  else  buf  fi    in
                                                      <if  (\mneg{}\msubb{}isl(hs'))  \mwedge{}\msubb{}  (bag-size(buf')  =\msubz{}  0)
                                                        then  inr  \mcdot{} 
                                                        else  inl  <hs',  buf'> 
                                                        fi 
                                                      ,  buf
                                                      >
                                        |  inr(x)  =>
                                        <inl  s  ,  buf>)>   


Date html generated: 2011_08_16-AM-09_47_38
Last ObjectModification: 2011_06_03-PM-12_19_11

Home Index