cakeml
cakeml copied to clipboard
Add support for when-clauses in the front end.
When clauses are very useful for writing concise ML code.
Yet, it is very hard to give them a semantics. On the one hand, it is useful to allow the when clause to perform side effects (e.g. a union-find query that may compress a path). On the other hand, mutating the data being matched is generally unsafe in the presence of pattern matching optimization (cause of a famous OCaml segfault).
A simple solution is to view when clauses as a mere syntactic sugar. Along the lines of:
match v with
| p1 when e1 -> body1
| _other_clauses_
would compile down to
let k() = match v with _other_clauses_ in
match v with
| p1 -> if e1 then body1 else k()
| _ -> k()
This prevents optimizations of the pattern matching branch selection, but at least would be clear in terms of semantics. Compilation using gotos would save the need to allocate the closure k.