Nuprl Definition : 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 ⋅ , 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 occuring in Statement :  create-component: create-component(t;P;x;Cs;L),  deliver-msg: deliver-msg(t;m;x;Cs;L),  comm-create: comm-create(c),  comm-msg: comm-msg(c),  com-kind: com-kind(c),  lg-is-source: lg-is-source(g;i),  lg-label: lg-label(g;x),  lg-remove: lg-remove(g;n),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  let: let,  it: ⋅,  spreadn: spread3,  apply: f a,  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  token: "$token"
FDL editor aliases :  do-chosen-command
Latex:
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: 2015_07_23-AM-11_09_11
Last ObjectModification: 2012_02_25-PM-03_39_44

Home Index