Thanks again Dmitriy,
it seems that my "fix" was too quick. Since sending my email yesterday I
worried already whether doing unification inside adhoc_overloading.ML is
such a good idea (since the unifier might inject schematic type
variables stemming from the internal generic theory data of adhoc
overloading into the ongoing check-phase). Apparently it isn't.
Is there a way to turn arbitrary schematic type variables into ones that
will not cause problems during type-inference? If so, it might be better
to just check for unifiability and then inject a variant "v" with its
most general type but where "polymorphic" variables are made known to
the context.
I'm mostly guessing here. Maybe somebody with deeper knowledge of the
system could comment whether this would be feasible (and also the right
way to go).
cheers
chris
On 11/24/2014 09:03 AM, Dmitriy Traytel wrote:
Cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e
Dmitriy
On 23.11.2014 21:20, Christian Sternagel wrote:
*Moved from isabelle-users*
Thanks for the crucial hint Dmitriy!
Coming back to the original issue of Andreas, some explanation might
be in order.
What we did until now in adhoc_overloading.ML (more precisely, the
function "insert_variants") was to check for a given constant "c" of
type "T" whether there is a registered variant "v" whose type unifies
with "T". If so, "v" was inserted (but with all type-annotations
"flattened" to "dummyT"). After that we just hoped that type-inference
would do the trick. Apparently this worked quite well in many
situations (or maybe there are just not that many users of
"adhoc_overloading" ;)).
Be that as it may. In Andreas' example this "flattening" of types
leads to somewhat unexpected results. Funnily (or maybe it was to be
expected but I don't know the details) everything worked out in
top-level thoeries. Somehow types are more polymorphic there (even
though HOL is not polymorphic at all ;)). With notepad and a fixed
type "'b" the problem occurred (and I guess the same would happen with
locales).
(I'm not sure whether the TYPE_MATCH exception, which is not raised
inside adhoc_overloading.ML but caused by its result, is the best
problem-indicator for users here. Maybe there is also space for
improvement elsewhere. Comments?)
Anyway, attached is the following series of patches (to be applied in
this order):
delete - fixes a typo
drop_semicolons - drops semicolons
inst_unifier - uses the obtained unifier to instantiate the type of "v"
tune - misc tuning
With those applied (the important one is "inst_unifier")
"insert_variants" does the following. For a given constant "c" of type
"T", check whether there is a variant "v" of type T' such that T and
T' unify. If so, apply the obtained type-unifier to "v" and insert the
result instead of "c".
I hope this resolves your problem Andreas.
I tested the change on one of my local files that make heavy use of
adhoc overloading. Maybe someone could have a look, push the changes
to a test server, and push them to the main repo if everything is fine?
cheers
chris
On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:
Hi Christian,
just a few weeks ago, I learned that Envir.subst_term_types is indeed
the wrong function when substituting with a unifier (instead it is
intended for matchers).
The right functions for unifiers in envir.ML are the ones prefixed with
"norm".
Hope that helps,
Dmitriy
On 22.11.2014 21:02, Christian Sternagel wrote:
I'm currently a bit confused by the result of "Sign.typ_unify" (or
rather the result of applying the corresponding "unifier"). So maybe
the problem stems from my ignorance w.r.t. to its intended result.
After applying the attached "debug" patch for the following
consts pure :: "'a ⇒ 'b"
definition pure_stream :: "'a ⇒ 'a stream"
where "pure_stream = sconst"
adhoc_overloading pure pure_stream
consts ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream"
(infixl "◇" 70)
consts S_stream :: "(('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c) stream"
declare [[show_variants]]
term "pure id :: ('b ⇒ 'b) stream"
we obtain the output
oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
variant type: ?'a ⇒ ?'a stream
("unifier:",
{(("'a", 0), (["HOL.type"], "??'a ⇒ ??'a")),
(("?'a", 0),
(["HOL.type"],
"'b"))}) (line 165 of
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
("candidate term:",
Const ("Scratch.pure_stream",
"?'a
⇒ ?'a Stream.stream")) (line 167 of
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
("after unification:",
Const ("Scratch.pure_stream",
"(??'a ⇒ ??'a)
⇒ (??'a
⇒ ??'a) Stream.stream")) (line 168 of
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
"pure_stream id"
:: "('a ⇒ 'a) stream"
The result of unification is a bit surprising to me, since the
obtained "unifier" seems to claim that
('b => 'b) => ('b => 'b) stream
and
(??'a => ??'a) => (??'a => ??'a) stream
are equal. What am I missing here? Maybe Envir.subst_term_types is not
the way to apply the typenv obtained by typ_unify? (In this special
case, if I would call subst_term_types twice with the same typenv, the
result would be as I expected.)
cheers
chris
Btw: the "delete" patch (which is to be applied before "debug") fixes
a typo in the description of "no_adhoc_overloading". It is entirely
unrelated to the issue at hand, but maybe somebody could apply it
anyway.
On 11/21/2014 07:31 PM, Christian Sternagel wrote:
Dear Andreas,
Thanks for the report, I'll have a look. First an immediate
observation:
When adding the following to Scratch.thy
declare [[show_variants]]
notepad
begin
fix f :: "('b ⇒ 'b ⇒ 'a) stream"
and x :: "'b stream"
term "pure id :: ('b => 'b) stream"
the first "term" results in
"pure_stream id"
:: "('c ⇒ 'c) stream"
while the second results in
"pure_stream id"
:: "('b ⇒ 'b) stream"
So it is not surprising that the first causes problems while matching.
Why, however "'c" is produced instead of "'b" is not immediately clear
to me. I'll investigate.
cheers
chris
On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
Dear experts on adhoc overloading,
When I want to instantiate variables in a theorem using the attribute
"of", sometimes the exception TYPE_MATCH gets raised. This seems
strange
to me because I would expect that adhoc_overloading either complains
about not being able to uniquely resolve an overloaded constant or
exchanges the constant in the AST.
By adding more type annotations, I have so far been able to
circumvent
the exception, but there seems to be a check missing. Attached you
find
a small example.
Best,
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
