[isabelle-dev] auto raises a TYPE exception

[Lukas Bulwahn]

Hi everyone,

motivated by the current discussion, I used the Bavarian holiday today
to get the aforementioned Quickcheck tool into a stable state.
The latest stable version is at:

https://bitbucket.org/nicolai490/qcheck_tum

I will only have some spare time if at all to maintain it.
I hope someone at TUM is willing to take this over and
mentor a bachelor or master student, who could write
formal specifications for the unification and/or pattern
matching in Isabelle.

I bet quickchecking the specifications with appropriate
generators will uncover more surprises of the current
implementations.

@Makarius: Are you willing to include the current state in
Isabelle's repository, e.g. under src/Tools/?
The sources are in a stable state and maintenance in last
half year boiled down to only one minor change. Hence, I
believe that it is a low-maintenance part in Isabelle and can
be easily maintained the next few years with almost no
further effort.

Lukas

On 05/30/2013 12:23 AM, Tobias Nipkow wrote:
> this incident has again reminded me that in the absence of formal proofs about
> the code, assertions in the code would be a big step forward. they could have
> told us a long time ago that some precondition expected by the unification code
> is not guaranteed. lukas and a student had even put together a quickcheck
> infrastructure for Isabelle/ML. All of this could be confined to regression
> runs. i think we should make some effort in this direction to increase our
> confidence in the kernel.
>
> tobias
>
> Am 27/05/2013 19:54, schrieb Makarius:
>> On Mon, 27 May 2013, Makarius wrote:
>>
>>> The change ensures that variables with equal name are unified, in the same
>>> manner as the types of Free or Const are unified, before doing the real work
>>> of HO-unification.
>> Here is another example for Isabelle/Pure, without schematic variables with
>> different types.  It may be be tried before/after my change 3b9c31867707 from
>> today:
>>
>>
>> ML {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}
>> declare [[show_types]]
>>
>> typedecl nat
>> typedecl bool
>>
>> ML {*
>>    val read = Syntax.read_term (Proof_Context.set_mode
>> Proof_Context.mode_schematic @{context});
>>    val a = read "a :: nat =>  bool";
>>    val x = read "?x :: ?'b";
>> *}
>>
>> ML {* Seq.list_of (Unify.hounifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
>> ML {* Seq.list_of (Unify.unifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
>> ML {* Pattern.unify @{theory} (a, x) (Envir.empty 15); *}
>>
>> Before the change, Unify.hounifiers crashes; after the change it is able to work
>> out the type instantiation correctly.  Pattern.unify is still not quite there,
>> neither before nor after the change.
>>
>>
>> Note that the original implementation by Larry did try to unify the result types
>> in any case, using the body_type function.  But that was assuming that the arity
>> of the function type happens to coincide with the number of arguments in the
>> term application.
>>
>> This is why I introduced optional bounds to the function type traversal in
>> envir.ML 7f3549a316f4.  Note that in 3b9c31867707 the type unification of the
>> disagreement pair is done explicitly via unify_types_of, without taking the
>> functions apart, but also see the modification of assignment where these bounds
>> correspond to the number of actual arguments.
>>
>>
>> For the moment, I am not going to produce more changes.  Maybe Larry and Tobias
>> also want to comment, as the authors of these modules from some decades ago.
>> Stefan is of course the proven expert who re-investigated quite a lot of that
>> around 2000.
>>
>>
>>      Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev