[isabelle] imp_program replace more bindings by let



Dear code-generator experts,

does anyone understand the code and the assumptions of the function imp_program (used for example by the code target SML_imp)? Currently, it is able to replace some of the (fn f_ => fn () => f_ args) by lets, but not in every case.


For example, consider the following variant of the identity function:

definition f1 where
  ‹f1 n = (if False then do {a ← return n; return a} else return n)›


The code can be exported by
export_code f1 in SML_imp

Readable code is produced:

fun f1 (A1_, A2_) n =
  (if false
    then (fn () =>
           let
             val x = n;
           in
             x
           end)
    else (fn () => n));


However, if I change the definition by adding a return at the end of the function:


definition f2 where
  ‹f2 n = (if False then  do {a ← return n; return a} else return n) ⤜ return›

Then the exported code is less readable:

fun f2 (A1_, A2_) n =
  (fn () =>
    let
      val x =
        (if false
          then  (fn f_ => fn () => f_ ((fn () => n) ()) ())
                 (fn a => (fn () => a))
          else (fn () => n))
          ();
    in
      x
    end);

This kind of code appears frequently in the code I generate with the Refinement Framework, because of while-loops. An extreme version of this behaviour can be found in the code generated from my verified SAT solver https://bitbucket.org/isafol/isafol/src/020eeeda9228b809b1977bc54b5fa853c5a8ef14/Weidenbach_Book/code/IsaSAT_solver.sml?at=master&fileviewer=file-view-default#IsaSAT_solver.sml-1720 <https://bitbucket.org/isafol/isafol/src/020eeeda9228b809b1977bc54b5fa853c5a8ef14/Weidenbach_Book/code/IsaSAT_solver.sml?at=master&fileviewer=file-view-default#IsaSAT_solver.sml-1720>. Changing this behaviour would improve readability, make it easier for me to try how changes perform before verifying them in Isabelle, and make it easier to see if there are performance bugs in my code, like copying of arrays.

I know of a workaround: giving a name to ‹do {a ← return n; return a}› works.


By looking at the code of imp_monad_bind/imp_monad_bind' in SML_imp and comparing the calls for ICase (imp_monad_bind') and functions (imp_monad_bind'), I believe that

imp_monad_bind'' [(t1, ty1), (t2, ty2)]

is missing recursive calls and could be:

imp_monad_bind'' [(imp_monad_bind t1, ty1), (imp_monad_bind t2, ty2)]


However,
  1. this change might make the code generator unsound. I don't know what assumptions are made here.
  2. this change prevents the grouping of lets to happen:

definition f3 where
  ‹f3 n = (if False then  do {a ← return n; a ← return n; return a} else return n)›

now gets:

fun f3 (A1_, A2_) n =
  (if false
    then (fn () =>
           let
             val _ =  n;
           in
             (fn () =>
               let
                 val x = n;
               in
                 x
               end)
               ()
           end)
    else (fn () => n));

instead of

fun f3 (A1_, A2_) n =
  (if false
    then (fn () =>
           let
             val _ = n;
             val x = n;
           in
             x
           end)
    else (fn () => n));




Best,
Mathias




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.