[isabelle-dev] Quickcheck Narrowing

[Lukas Bulwahn]

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