---

do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm) ==
  let Cs,G = S in
    if lg-is-source(G;n)
   then let ev,x,c = lg-label(G;n) in 
        let G' = lg-remove(G;n) in
            if com-kind(c) =a "msg"
              then let ms = comm-msg(c) in
                       <inl <ev, x, ms> , deliver-msg(t;ms;x;Cs;G')>
            if com-kind(c) =a "create"
              then let P = comm-create(c) in
                       <inr  , create-component(t;P;x;Cs;G')>
            if com-kind(c) =a "choose"
              then let ms = nat2msg m in
                       <inl <ev, x, ms> , deliver-msg(t;ms;x;Cs;G')>
            if com-kind(c) =a "new"
              then let ms = loc2msg nm in
                       <inl <ev, x, ms> , deliver-msg(t;ms;x;Cs;G')>
            else <inr  , Cs, G'>
            fi 
   else <inr  , S>
   fi 

---

Definitions :  spread: spread def,  lg-is-source: lg-is-source(g;i),  spreadn: spread3,  lg-label: lg-label(g;x),  lg-remove: lg-remove(g;n),  comm-msg: comm-msg(c),  comm-create: comm-create(c),  create-component: create-component(t;P;x;Cs;L),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  com-kind: com-kind(c),  token: "$token",  let: let,  apply: f a,  inl: inl x ,  deliver-msg: deliver-msg(t;m;x;Cs;L),  pair: <a, b>,  inr: inr x ,  it:
FDL editor aliases :  do-chosen-command

---

do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm)  ==
    let  Cs,G  =  S  in
        if  lg-is-source(G;n)
      then  let  ev,x,c  =  lg-label(G;n)  in 
                let  G'  =  lg-remove(G;n)  in
                        if  com-kind(c)  =a  "msg"
                            then  let  ms  =  comm-msg(c)  in
                                              <inl  <ev,  x,  ms>  ,  deliver-msg(t;ms;x;Cs;G')>
                        if  com-kind(c)  =a  "create"
                            then  let  P  =  comm-create(c)  in
                                              <inr  \mcdot{}  ,  create-component(t;P;x;Cs;G')>
                        if  com-kind(c)  =a  "choose"
                            then  let  ms  =  nat2msg  m  in
                                              <inl  <ev,  x,  ms>  ,  deliver-msg(t;ms;x;Cs;G')>
                        if  com-kind(c)  =a  "new"
                            then  let  ms  =  loc2msg  nm  in
                                              <inl  <ev,  x,  ms>  ,  deliver-msg(t;ms;x;Cs;G')>
                        else  <inr  \mcdot{}  ,  Cs,  G'>
                        fi 
      else  <inr  \mcdot{}  ,  S>
      fi 


Date html generated: 2010_08_27-PM-03_52_38
Last ObjectModification: 2010_05_04-PM-06_35_54

Home Index