*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] imp_program replace more bindings by let*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Wed, 14 Feb 2018 08:01:41 +0100

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

**Follow-Ups**:**Re: [isabelle] imp_program replace more bindings by let***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Sledgehammer option to stop if first prover finds a proof
- Next by Date: Re: [isabelle] Sledgehammer option to stop if first prover finds a proof
- Previous by Thread: Re: [isabelle] Sledgehammer option to stop if first prover finds a proof
- Next by Thread: Re: [isabelle] imp_program replace more bindings by let
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list