[isabelle-dev] Quickcheck Narrowing

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120728/d80161bc/attachment.asc>