Re: [isabelle] Where to learn about the Mini-Haskell of the code generator?



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





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