<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Cf.
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e">http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e</a><br>
<br>
Dmitriy<br>
<br>
On 23.11.2014 21:20, Christian Sternagel wrote:<br>
</div>
<blockquote cite="mid:54724182.8070202@gmail.com" type="cite">*Moved
from isabelle-users*
<br>
<br>
Thanks for the crucial hint Dmitriy!
<br>
<br>
Coming back to the original issue of Andreas, some explanation
might be in order.
<br>
<br>
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" ;)).
<br>
<br>
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).
<br>
<br>
(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?)
<br>
<br>
Anyway, attached is the following series of patches (to be applied
in this order):
<br>
<br>
delete - fixes a typo
<br>
drop_semicolons - drops semicolons
<br>
inst_unifier - uses the obtained unifier to instantiate the type
of "v"
<br>
tune - misc tuning
<br>
<br>
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".
<br>
<br>
I hope this resolves your problem Andreas.
<br>
<br>
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?
<br>
<br>
cheers
<br>
<br>
chris
<br>
<br>
On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:
<br>
<blockquote type="cite">Hi Christian,
<br>
<br>
just a few weeks ago, I learned that Envir.subst_term_types is
indeed
<br>
the wrong function when substituting with a unifier (instead it
is
<br>
intended for matchers).
<br>
<br>
The right functions for unifiers in envir.ML are the ones
prefixed with
<br>
"norm".
<br>
<br>
Hope that helps,
<br>
Dmitriy
<br>
<br>
On 22.11.2014 21:02, Christian Sternagel wrote:
<br>
<blockquote type="cite">I'm currently a bit confused by the
result of "Sign.typ_unify" (or
<br>
rather the result of applying the corresponding "unifier"). So
maybe
<br>
the problem stems from my ignorance w.r.t. to its intended
result.
<br>
<br>
After applying the attached "debug" patch for the following
<br>
<br>
consts pure :: "'a ⇒ 'b"
<br>
<br>
definition pure_stream :: "'a ⇒ 'a stream"
<br>
where "pure_stream = sconst"
<br>
<br>
adhoc_overloading pure pure_stream
<br>
<br>
consts ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b
stream"
<br>
(infixl "◇" 70)
<br>
consts S_stream :: "(('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c)
stream"
<br>
<br>
declare [[show_variants]]
<br>
<br>
term "pure id :: ('b ⇒ 'b) stream"
<br>
<br>
we obtain the output
<br>
<br>
oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
<br>
variant type: ?'a ⇒ ?'a stream
<br>
("unifier:",
<br>
{(("'a", 0), (["HOL.type"], "??'a ⇒ ??'a")),
<br>
(("?'a", 0),
<br>
(["HOL.type"],
<br>
"'b"))}) (line 165 of
<br>
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
<br>
("candidate term:",
<br>
Const ("Scratch.pure_stream",
<br>
"?'a
<br>
⇒ ?'a Stream.stream")) (line 167 of
<br>
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
<br>
("after unification:",
<br>
Const ("Scratch.pure_stream",
<br>
"(??'a ⇒ ??'a)
<br>
⇒ (??'a
<br>
⇒ ??'a) Stream.stream")) (line 168 of
<br>
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
<br>
"pure_stream id"
<br>
:: "('a ⇒ 'a) stream"
<br>
<br>
The result of unification is a bit surprising to me, since the
<br>
obtained "unifier" seems to claim that
<br>
<br>
('b => 'b) => ('b => 'b) stream
<br>
<br>
and
<br>
<br>
(??'a => ??'a) => (??'a => ??'a) stream
<br>
<br>
are equal. What am I missing here? Maybe
Envir.subst_term_types is not
<br>
the way to apply the typenv obtained by typ_unify? (In this
special
<br>
case, if I would call subst_term_types twice with the same
typenv, the
<br>
result would be as I expected.)
<br>
<br>
cheers
<br>
<br>
chris
<br>
<br>
Btw: the "delete" patch (which is to be applied before
"debug") fixes
<br>
a typo in the description of "no_adhoc_overloading". It is
entirely
<br>
unrelated to the issue at hand, but maybe somebody could apply
it anyway.
<br>
<br>
On 11/21/2014 07:31 PM, Christian Sternagel wrote:
<br>
<blockquote type="cite">Dear Andreas,
<br>
<br>
Thanks for the report, I'll have a look. First an immediate
observation:
<br>
<br>
When adding the following to Scratch.thy
<br>
<br>
declare [[show_variants]]
<br>
<br>
notepad
<br>
begin
<br>
fix f :: "('b ⇒ 'b ⇒ 'a) stream"
<br>
and x :: "'b stream"
<br>
term "pure id :: ('b => 'b) stream"
<br>
<br>
the first "term" results in
<br>
<br>
"pure_stream id"
<br>
:: "('c ⇒ 'c) stream"
<br>
<br>
while the second results in
<br>
<br>
"pure_stream id"
<br>
:: "('b ⇒ 'b) stream"
<br>
<br>
So it is not surprising that the first causes problems while
matching.
<br>
Why, however "'c" is produced instead of "'b" is not
immediately clear
<br>
to me. I'll investigate.
<br>
<br>
cheers
<br>
<br>
chris
<br>
<br>
On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
<br>
<blockquote type="cite">Dear experts on adhoc overloading,
<br>
<br>
When I want to instantiate variables in a theorem using
the attribute
<br>
"of", sometimes the exception TYPE_MATCH gets raised. This
seems
<br>
strange
<br>
to me because I would expect that adhoc_overloading either
complains
<br>
about not being able to uniquely resolve an overloaded
constant or
<br>
exchanges the constant in the AST.
<br>
<br>
By adding more type annotations, I have so far been able
to circumvent
<br>
the exception, but there seems to be a check missing.
Attached you find
<br>
a small example.
<br>
<br>
Best,
<br>
Andreas
<br>
</blockquote>
</blockquote>
</blockquote>
<br>
</blockquote>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>