On 07/28/2012 05:32 PM, Florian Haftmann wrote:
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:
Hi Florian,
My priorities are indeed somewhere else. To give a few short answer to
all your questions:
1. The testboard does not check it because ISABELLE_GHC probably is not
set there. Maybe we could easily fix that.
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.
2. I tried out the code_include mechanism a while ago, but I could not
succeed within half a day. There were other problems that were even
worse than poking around.
So I gave up and stayed with the current solution. We could give it
another try if it's worth the effort.
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.
3. I thought of this as well, but did not find another prime application
besides Quickcheck.
That's why the mechanism is still in the module Quickcheck-Narrowing.
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.
4. I cannot comment on that.
5. There are still all those funny sequence theories in HOL
(New_Foo_Sequence) which are awaiting cleanup.
5. That's true. I will get rid of them soon.
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.
6. I see. Okay, that's the reason, why some modes of the code generator
produce non-compilable files after some reasonable code setup.
Lukas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
