Email Gateway (Aug 22 2022 at 16:45): Email Gateway (Aug 22 2022 at 16:45):From: Mathias Fleury <mathias.fleury12@gmail.com>
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
Email Gateway (Aug 22 2022 at 16:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Mathias,
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.
well, imp_monad_bind is a transformation on expressions of the code
generation intermediate language and imp_program lifts that to transform
whole programs of the code generation intermediate language.
As is always the case with such extra-logical transformations, they are
error-prone; most of this code goes back to the first
(over-)enthusiastic Imperative-HOL experiments in 2008 (rev.
54bf1fea9252) and has only been changed in cases of urgent need.
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)]
1. this change might make the code generator unsound. I don't know what assumptions are made here.
Since imp_monad_bind is supposed to be semantic-preserving, it could be
assumed that the recursive calls are safe.
2. this change prevents the grouping of lets to happen:
It is indeed hard to tell on the spot how this could be resolved.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 16:20 UTC