cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Add support for when-clauses in the front end.

Open charguer opened this issue 6 years ago • 0 comments

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.

charguer avatar Jul 02 '19 13:07 charguer