Lean: add placeholder for state monad to stateful functions

[javra]

Adds a monad StateM which is added to all stateful functions. In the body of stateful function definitions, we put everything inside a return statement, but the idea is that in the future, doc_exp will return a pair of strings, one for the do block and one print of the pure part of the expression which goes into the return call

[github-actions]

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  748 tests ±0    748 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 491 runs  ±0  2 491 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit 0c87344. ± Comparison against base commit bf921f9.

♻️ This comment has been updated with latest results.

[ineol]

How do you plan to translate a function body like this?

let x = rX 0
if x then wX 0 3; return 11 
     else return 0

I don't get how the idea of returning a pair of string works.

[javra]

Something like

do
  let x ← rX 0
  if x then do
    wX 0 3
    return 11
  else do
    return 0

Only when doc_exp descends to 11 or 0 respectively does the result become non-monadic, so the caller of that instance of doc_exp would put it behind the return.

This PR does not make all expression constructor ready for this. I just thought we'd might get it merged since the work that remains will be a major overhaul of doc_exp.

[bacam]

Note that if you're using the usual rewrites, the Sail AST will already be in monadic form, with the monadic bind begin E_internal_plet nodes, and monadic return E_internal_return, so you can add the return in doc_exp rather than doc_funcl_body. I suppose that doesn't matter quite yet, though.

[ineol]

I think there is a typo in the commit/PR titles placehodler -> placeholder

[javra]

@bacam In the end I want to be able to translate return f(g(x)) to

... do
  return f (← g x)

if g is monadic, not quite sure yet, how to best implement that. Maybe we need to remove the rewrite that transforms it to the monadic form? The do blocks in Lean are quite a bit more expressive than just binds and returns, so maybe the current AST is not optimal because I guess it translates the applications to internal_plets?

[javra]

OTOH maybe that's a cosmetic thing that can be done afterwards

[bacam]

You could have a different version of that rewrite that leaves arguments like g x in place. Or maybe do something clever depending on what Lean's internal representation is.