[isabelle-dev] Quickcheck Narrowing
florian.haftmann at informatik.tu-muenchen.de
Sat Jul 28 17:32:30 CEST 2012
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
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
* 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
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev