NetworkVerification/nv

Allow extended pattern-matching for function arguments and let bindings

DKLoehr opened this issue · 3 comments

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.

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

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.

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.