NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Allow multiple patterns per match branch #69

Closed alberdingk-thijm closed 3 years ago

alberdingk-thijm commented 3 years ago

Another small but nice language improvement that would be easy to add: changing our match statements to allow users to specify multiple patterns for one branch.

One way to do this is basically just sugar, where we add syntax such that:

match x with p | q -> e

desugars to:

match x with 
  | p -> e | q -> e

Or in other words, the parser produces a list of patterns for each branch, and then when constructing the branches type we desugar into one pattern per branch. This has the downside of not being preserved when printing out the program, unless we are willing to pay the cost of a Union-Find style algorithm examining branches to check if they can be joined. On the other hand, it's dead simple to add to the language.

Alternatively (I'm just spitballing ideas), if we wanted this to be more heavily engineered, we could:

  1. change the type of branches to map lists of patterns to expressions; or
  2. add a new kind of disjunctive pattern, which returns a match if either disjunct is true
DKLoehr commented 3 years ago

Generally speaking, I take the opinion that it's not worth the effort to try to preserve the source program exactly during printing, especially because the parser is so bloated already. The important thing is that the printed program be equivalent to the original, but not necessarily identical. So I'd favor the former approach of just splitting into multiple identical branches during parsing.