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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
