Hi Lukas, I have corrected cs 6efff142bb54 by cs 7c497a239007, and have relaxed the issue with Efficient_Nat a little (cs 084cd758a8ab, see below for a short discussion). This has raised a couple of questions:
1. Why did the testboard not check this? Bad environment settings? I guess you are aware of the following issues to some extent, but also that your priorities are elsewhere at the moment. Nevertheless I would appreciate it if at one point in time you can return to them, maybe as joint work: 2. The poking in generated code which happens in narrowing_generators.ML is highly discouraged and was the primary source for the breakdown in 6efff142bb54. It should be possible to get around without that using the code_include mechanism. 3. The evaluation machinery for Haskell should be separate thing (maybe code_eval_haskell.ML), and also the communication could be less technically involved, e.g. a yxml output rather than invoking the SML compiler right after the Haskell compiler just to parse something. 4. After 084cd758a8ab, Efficient_Nat works in principle, but there are other problems: * the type ambiguity inference seems not to work as expected * there is no term_of equation for nat * … I did not dive into detail here, because all these must be treated at a glance. I guess the term_of issue can be dealt with as soon as Efficient_Nat uses a different architecture. Another issue is that we really need to understand what a generic Haskell evaluation machinery consists of. 5. There are still all those funny sequence theories in HOL (New_Foo_Sequence) which are awaiting cleanup. 6. What I so far have not been aware of is that in Haskell there are always multiple modules (one module =^= one file), contrary to ML and Scala. I think at some stage I have to make this more explicit in the overall architecture. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev