Arbitrary sequencing of processes

[np]

Notice that this is implemented now. This remains a place holder for discussions around this topic.

Typically right-nested sequencing is preferable since we can clearly scope the newly introduced channels and variables.

However in several we break this rule, for instance fwd and @ can be sequenced and they might expand into a process which cannot be right-nested. Another cause is slice which has a sub-process and should have a sequential continuation. As in this example:

rotate_seq =
  \(A : Type)
   (n : Int)->
   proc(i : [: ?A ^(1 + n) :], o : [: !A ^(n + 1) :])
   i[:iL, iH^n:]
   o[:oL^n, oH:]
   recv iL (xL : A).
   (slice (iH, oL) n as _
      fwd(?A)(iH, oL)).
   send oH xL

[np]

The reason I want to keep this in the tracker for a while is that the scopes are not completely satisfactory.

Notice first that (recv c (x : Int)). send d x is accepted.

These are not:

• @(proc(c) recv c (x : Int))(c). send d x
• (slice (c) 1 as _ (recv c (x : Int))). send d x

While they both reduce to the example above.

This raises the question of a potential output telescope for processes.