Email Gateway (Aug 19 2022 at 16:26): Email Gateway (Aug 19 2022 at 16:26):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Scratch.thy
Email Gateway (Aug 19 2022 at 16:27):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 16:28):From: Christian Sternagel <c.sternagel@gmail.com>
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.
delete
debug
Email Gateway (Aug 19 2022 at 16:28):From: Dmitriy Traytel <traytel@in.tum.de>
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
Last updated: Apr 24 2024 at 01:07 UTC