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
