Splitting/Grouping channels using patterns

[np]

The process language and type system was designed to keep the burden of where/when splitting tensors & pars really low.

Channel splitting

This means that channel splittings can be done early and freely ordered.
However we could directly name the sessions deeply and automate these splittings.

Example:

pattern_example = proc[ a : !Int, [: b : !Int, c : !Int :], { d : [!Int, !Int], e : {?Int, ?Int} } ]
   (send a 1 | send b 2. send c 3 | fwd [!Int,!Int] (d,e))

Which should desugar to:

pattern_example_expanded =
  proc(abcde : [!Int, [: !Int, !Int :], { [!Int, !Int], {?Int, ?Int} } ])
    abcde[a, bc, de]
    bc[: b, c :]
    de{d, e}
    (send a 1 | send b 2. send c 3 | fwd [!Int,!Int] (d,e))

Splitting patterns are not only for processes-as-terms but should be allowed for normal splitting as well:

pattern_example_2 = proc(abcde)
   abcde[ a : !Int, [: b, c :], { d, e } ]
   (send a 1 | send b 2. send c 3 | fwd [!Int,!Int] (d,e))

This example also recalls that session annotations are optional.

Patterns for grouping

[Grouping has been implemented in commit 72a3388]

When injecting a term as a process one must pass in some channels.
For instance consider we want to inject the term above in another process where the protocol is equivalent up-to some permutations.

-- notice how various parts gets commuted
test_pat =
  proc[ [: b : !Int, c : !Int :], a : !Int, { e : {?Int, ?Int}, d : [!Int, !Int] } ]
  @pattern_example[a, [: b, c :], {d, e}]

Alternatively with pattern splitting expanded:

test_pat_expanded_splitting =
  proc(bcaed : [[: !Int, !Int :], !Int, { {?Int, ?Int}, [!Int, !Int] } ])
    bcaed[bc, a, ed]
    bc[: b, c :]
    ed{e, d}
  @pattern_example_expanded[a, [: b, c :], {d, e}]

These grouping patterns can be expanded away as well. While we need to have this expansion in place eventually it is better to check the process un-expanded.

The expansion of grouping patterns for our example is:

test_pat_expanded_grouping =
  proc[ [: b : !Int, c : !Int :], a : !Int, { e : {?Int, ?Int}, d : [!Int, !Int] } ]
  new(f, g)
  ( @pattern_example(f)
  | g[a, [: b, c :], {d, e}])

So expansion of grouping patterns rely on the expansion of splitting patterns.

Syntax of Patterns

[also in commit 72a3388]

After the keyword proc we change `"(" ChanDecs ")", into TopPatt.

TPOld. TopPatt ::= "(" [Patt] ")" ;
TPPar. TopPatt ::= "{" [Patt] "}" ;
TPTen. TopPatt ::= "[" [Patt] "]" ;
TPOrd. TopPatt ::= "[:" [Patt] ":]" ;

PaVar. Patt ::= Name ":" Session ;
PaPar. Patt ::= "{" [Patt] "}" ;
PaTen. Patt ::= "[" [Patt] "]" ;
PaOrd. Patt ::= "[:" [Patt] ":]" ;

Implementation sketch