Email Gateway (Aug 19 2022 at 10:01): Email Gateway (Aug 19 2022 at 10:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I had a check. Seems to me the first former is the most relevant.
It appears code generation is really designed towards functional
languages, which is not easily suitable for procedural and automata
languages, even if those can of course be expressed in terms of lambda
calculus.
For other targets which are not functional languages, this may be better
to have a model of the target, as an Isabelle theory, then prove the
properties of a construct in that model (I don't know if “construct in
that model” is the proper wording, may be that should be “an instance of
that model”); then use a mapping from the modelled constructs to their
serialization in the target language. That would rather looks like writing
in the target language inside of Isabelle, and not be proper code
generation from any kind of proof, but that's more safe I believe.
Any comments welcome.
P.S. I believe
http://www4.informatik.tu-muenchen.de/~haftmann/pdf/code_generation_haftmann_nipkow.pdf
could be part of the standard documentations provided with the Isabelle
package. It's both useful and good enough for that.
Email Gateway (Aug 19 2022 at 10:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Yannick,
(I don't know Haskell, just SML)
here
http://www4.informatik.tu-muenchen.de/~haftmann/pdf/code_generation_haftmann_nipkow.pdf
a good entrance point indeed
and probably here
http://www4.informatik.tu-muenchen.de/~haftmann/pdf/codegen_hol_haftmann_phd.pdf
for some technical details, e.g. syntactic restrictions (there is a
small guide how to approach this thesis on
http://isabelle.in.tum.de/~haftmann/)
It appears code generation is really designed towards functional
languages
Yes.
For other targets which are not functional languages, this may be better
to have a model of the target, as an Isabelle theory, then prove the
properties of a construct in that model (I don't know if “construct in
that model” is the proper wording, may be that should be “an instance of
that model”); then use a mapping from the modelled constructs to their
serialization in the target language. That would rather looks like
writing in the target language inside of Isabelle, and not be proper
code generation from any kind of proof, but that's more safe I believe.
Code generation »as it is« is indeed based on shallow embedding. With
some ambition this can be carried to parallel programming
(src/HOL/Library/Parallel) and imperative data structures
(src/HOL/Imperative-HOL).
P.S. I believe
http://www4.informatik.tu-muenchen.de/~haftmann/pdf/code_generation_haftmann_nipkow.pdf
could be part of the standard documentations provided with the Isabelle
package. It's both useful and good enough for that.
There are many papers with explain conceptual background of Isabelle.
Once there has been a list of them maintained by Larry Paulson, but I do
not know if it is still publicly available. But they are accessible
through references from the official Isabelle manuals, sometimes by
direct delegation (cf. »If you consider imperative data structures as
inevitable for a specific application, you should consider […]
; the framework described there is available in session @{text
Imperative_HOL}, together with a short primer document.« in the code
generator tutorial).
Nevertheless such papers allows accumulate some dust over they years –
not wrt. to the concepts, but to the actual surface appearance in
implementation, naming, syntax etc.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 10:29):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi people,
The codegen.pdf document, says a single translations occurs before
serialization to a target language. This prior translation is said to have
a single target of its own: a kind of Mini-Haskell.
Is this Mini-Haskell described in some official or unofficial documents?
(I don't know Haskell, just SML)
By the way, why a Mini-Haskell instead of a Mini-SML? What do Haskell
offers here SML can't for this purpose? (not a criticism, that's just to
learn the rational behind it).
Have an happy day
Email Gateway (Aug 19 2022 at 10:30):From: Christian Sternagel <c.sternagel@gmail.com>
On 02/07/2013 09:54 PM, Yannick Duchêne (Hibou57) wrote:
Hi people,
The codegen.pdf document, says a single translations occurs before
serialization to a target language. This prior translation is said to
have a single target of its own: a kind of Mini-Haskell.Is this Mini-Haskell described in some official or unofficial documents?
(I don't know Haskell, just SML)
here
http://www4.informatik.tu-muenchen.de/~haftmann/pdf/code_generation_haftmann_nipkow.pdf
and probably here
http://www4.informatik.tu-muenchen.de/~haftmann/pdf/codegen_hol_haftmann_phd.pdf
(I did not check, though)
By the way, why a Mini-Haskell instead of a Mini-SML? What do Haskell
offers here SML can't for this purpose? (not a criticism, that's just to
learn the rational behind it).
I think that would be typeclasses (and the syntax is maybe a bit more
lightweight, but that's just an opinion).
cheers
chris
Last updated: Apr 23 2024 at 16:19 UTC