NetworkVerification / nv

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

Reconcile differences between parsing and printing #66

Closed alberdingk-thijm closed 3 years ago

alberdingk-thijm commented 3 years ago

Currently, there are a few situations in which NV expressions are parsed in one way but printed in another (see #64 for an example of this that was previously reconciled). These include:

Since NV typically doesn't need to print out any NV code to the user, this discrepancy is tolerable. However, these differences do mean that there are pain points for any tools that try to use a solution from NV (handled in #64) or that want to use NV's library to generate NV code (as in nvgen). Hence, it would be worthwhile to reconcile these differences by either adding new syntax, modifying printing to match syntax more closely, or both.

In cases where syntactic sugar is used, the discrepancies may be acceptable to leave as-is, as is the case for sets versus dicts. But other cases may be useful to have handled, particularly those for dicts.

DKLoehr commented 3 years ago

IMO:

alberdingk-thijm commented 3 years ago

@DKLoehr That's pretty much how I felt it should be settled. I think any case where we desugar, as with sets, is fine not to fix when printing since the AST is the same. For TGet and TSet, since for now at least I'm not doing any transformations on the network before printing it out, I don't see the need to change them to print as match statements for now, although it could be nice if we could allow lets with patterns like let (u,v) = e (similar to #44 in expanding the cases where pattern matching is allowed). Either way, a flag seems sensible for that to me.

For dictionaries, I've gone ahead and written some draft code to change Printing.op_to_string to also give some information on whether the operation is prefix, infix or "circumfix" (like the brackets in the mget/mset syntax which go around their arguments: there may be a clearer neologism than circumfix), which can then be used to do printing using the consistent dictionary syntax. The only thing that looks different now is that, in situations where the operator is printed by itself (generally just in error messages like in Interp.ml or Wellformed.ml), it prints using dummy variable names as "Error in operator: a[b]" and "Error in operator: a[b := c]" instead of "Error in operator: get" and "Error in operator: set".

Additionally, I think there may be some small things I need to understand better about how the Printing module computes precedence, just to make sure I don't mix anything up, but I think that part is mostly handled.