record patterns

[leque]

It would be useful if SATySFi supports record patterns.

In SML#, the first pattern in the example below matches a record having the specified set of labels, and the second pattern matches any record containing the set of specified labels. (8.3 Record patterns‣ Chapter 8 SML# feature: record polymorphism ‣ Part II Tutorials ‣ SML# Document Version 4.0.0 - SML# Project)

# fun f {X = x, Y = y} = (x, y);
val f = fn : [’a, ’b. {X: ’a, Y: ’b} -> ’a * ’b]
# fun f {X = x, Y = y, ...} = (x, y);
val f = fn : [’a#{X: ’b, Y: ’c}, ’b, ’c. ’a -> ’b * ’c]

I think SATySFi can follow the same strategy: e.g. (in 0.0.x syntax)

% val f: (| x : 'a; y : 'b |) -> 'a * 'b
let f (| x = x; y = y |) = (x, y)

% val g: 'r -> 'a * 'b constraint 'r :: (| x : 'a; y : 'b |)
let g (| x = x; y = y; _ |) = (x, y)