Re: [isabelle] Questions concerning (Haskell) code generation

Hi René,

> 1.) It is in someway possible to make the generated code have an
> explicit export list? So something like
> export_code bla foo [export] in Haskell module_name Code file -
> that results in the following module definition
> module Code (bla, foo) where ...?
> The reason is, that w/o an explicit export list the compiler assumes
> that all functions are exported and therefore does not inline them or
> uses other code optimizations (see [1]).

this is an interesting observation.  Up until now, I did not pay much
attention to export lists, in order to keep things as simple as
possible.  So far I did not consider inlining issues.  There are
important enough to reconsider hiding and exporting anew.  Anyway,
analysis and implementation will take considerable time.

> 2.) I noted that when using "Efficient_Nat", I got two new types for
> natural numbers in code: Natural and Nat. The code of both looks nearly
> identical (see attached files) and also only one of them (Nat) is used
> throughout the rest of the code. Is there a deeper reason behind having
> them both?

Consider type classes: there is only one instantiation of a type per
class;  this prohibits to map two different types in the logic onto the
same type in Haskell.  This affects all languages with implicit
dictionaries, i.e. also Scala, but not SML/Ocaml.




PGP available:

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