Dear all,

this is not entirely OCaml related, but somewhat more general. However,
I hope that someone on that list can give me a pointer on how to proceed.

Assume a simple OCaml program with two primitives that can cause
side-effects:

let counter = ref 0
let incr x = counter := !counter + x ; !counter
let put n = counter := n; !counter
put (5 + let f x = incr x in f 3)

This example can be transformed into a pure program using a counter
monad (using ppx_monadic syntax):

do_;
  i <-- let f x = incr x in f 3 ;
  p <-- put (5 + i)
  return p

For a suitable definition of bind and return, both programs behave
equivalently. My question is: How can one automatically translate a
program of the former kind to the latter? I assume, one needs a normal
form that makes the order of evaluation explicit, but which normal form
would that be? Is there a textbook algorithm for that kind of analysis?

any pointers are appreciated,

Christoph