1 |
13. x:Id. vartype(i;x) r ds(x)?Top
14. e:E. loc(e) = i Id  (valtype(e) r ma-valtype(da; kind(e)))
15. e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e)))
16. {m:Msg| source(mlnk(m)) = i } r Msg(( l,tg. da(rcv(l; tg))?Top))
17. t: .
17. isnull(a(i;t))
17. 
17. (islocal(kind(a(i;t)))
17. (
17. (deq-member(IdDeq;act(kind(a(i;t)));1of())
17. (
17. (2of()(act(kind(a(i;t))), x.s(i;t).x,val(a(i;t))))
17. & ( x:Id.
17. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
17. & (
17. & (s(i;t+1).x
17. & (=
17. & (2of()(<kind(a(i;t)),x>, x.s(i;t).x,val(a(i;t)))
17. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
17. & ( l@0:IdLnk.
17. & ((eqof(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq))(<k,l>,<kind(a(i;t)),l@0>)
17. & (( false )
17. & (
17. & (withlnk(l@0;m(i;t))
17. & (=
17. & (if source(l@0) = i
17. & (if concat(map( tgf.map( x.<1of(tgf),x>;2of(tgf)
17. & (if concat(map( tgf.map( x.<1of(tgf),x>;(( x.s(i;t).x)
17. & (if concat(map( tgf.map( x.<1of(tgf),x>;,val(a(i;t))));f))
17. & (else nil fi
17. & ( (tg:Id if source(l@0) = i da(rcv(l@0; tg))?Top else Top fi) List)
17. & ( x:Id.
17. & ( (deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
17. & (
17. & (s(i;t).x
17. & (=
17. & (s(i;t+1).x
17. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
17. & ( l@0:IdLnk, tg:Id.
17. & ( (deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0,tg>;1of())
17. & ( (
17. & ( (deq-member(KindDeq;kind(a(i;t));2of()(<l@0,tg>)))
17. & (
17. & (w-tagged(tg; onlnk(l@0;m(i;t))) = nil Msg List)
18. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
19. x:Id.
19. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
20. IdDeq EqDecider(Id)
21. ( z.(z initially i)) State(ds)
22. x:Id. vartype(i;x) r ds(x)?Top
23. e:E. loc(e) = i Id  (valtype(e) r ma-valtype(da; kind(e)))
24. e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e)))
25. {m:Msg| source(mlnk(m)) = i } r Msg(( l,tg. da(rcv(l; tg))?Top))
E Type{i}
 | Auto |