NetworkVerification / nv

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

Allow extended pattern-matching for function arguments and let bindings #44

Open DKLoehr opened 4 years ago

DKLoehr commented 4 years ago

Would be nice to write e.g. let trans _ x = x + 1 instead of having to declare an unused variable for the edge. It would also be easier to e.g. unpack tuples automatically.

alberdingk-thijm commented 3 years ago

This seems like a worthwhile change outside of functions too: if we could make the left-hand side of a let binding be a pattern, instead of an identifier, we could then destruct data into multiple identifiers with one let, e.g.:

let trans e (x1, _) =
  let u~v = e in
  let { a; b; c } = x1 in
  if u = 0n then a + b else a + c
DKLoehr commented 3 years ago

Yeah, this is a nice QoL feature to have. I think we already allow this in let-statements, it just gets turned into a match statement during parsing. We could possibly implement it for function arguments by creating fresh variable for each argument pattern during parsing, then starting the body with a match to destruct it according to the user's pattern.

alberdingk-thijm commented 3 years ago

From what I can see, this is only done for tuples in let statements right now. Parsing throws an error for both patterns above. That being said, I would think they would both be implementable using that desugaring approach you describe.