[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

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