Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Value restriction in generated SML code

Email Gateway (Aug 22 2022 at 17:59):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I ran into a value-restriction problem with generated SML code. 
I thought the code generator is supposed to do unit-insertion
automatically.

Consider the following example. Here, the generated code for "test"
will fail due to the value restriction. Manual unit-insertion "test2"
fixes the problem. Interestingly, the generated Scala code is fine.

Email Gateway (Aug 22 2022 at 18:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

no, it does not. It only eta-expands proper functions.

Unit insertion must be constructed explicitly, as in the following
canonical example by Lukas Bulwahn from around 2009 / 2010:

export_code "Predicate.bind" in SML

Hope this helps,
Florian
signature.asc

Last updated: Apr 26 2024 at 08:19 UTC