Re: [isabelle] imp_program replace more bindings by let

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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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