Email Gateway (Feb 06 2024 at 19:52): Email Gateway (Feb 06 2024 at 19:52):From: hannobecker@posteo.de
Hi all,
This is about enabling/disabling adhoc overloading.
Expectation: A pair of adhoc_overloading const term and
no_adhoc_overloading const term in the same context should work and
lead to the overloading of const by term be disabled subsequently.
Observed behavior: In the context of locales and polymorphic term,
unrelated definitions in between adhoc_overloading and
no_adhoc_overloading can lead to no_adhoc_overloading failing.
Example:
theory Scratch
imports Main "HOL-Library.Adhoc_Overloading"
begin
consts abstract :: ‹'x›
locale foo =
fixes param :: ‹'s›
begin
definition concrete :: ‹'v ⇒ 'v›
where ‹concrete ≡ id›
adhoc_overloading abstract concrete
no_adhoc_overloading abstract concrete (* OK *)
adhoc_overloading abstract concrete
(* debug only *)
ML‹"concrete" |> Syntax.parse_term @{context}
|> singleton (Variable.polymorphic @{context})
|> Term.fastype_of
|> Syntax.pretty_typ @{context}
|> Pretty.writeln› (* ?<position> *)
(* Seemingly unrelated ... *)
definition test :: ‹'s ⇒ 'v ⇒ 'v› where
‹test _ x ≡ x›
(* debug only *)
ML‹"concrete" |> Syntax.parse_term @{context}
|> singleton (Variable.polymorphic @{context})
|> Term.fastype_of
|> Syntax.pretty_typ @{context}
|> Pretty.writeln› (* ?<position>1 *)
(* Mismatch due to strict type equality check
cf. L60 in Adhoc_Overloading.thy
fun variants_eq ((v1, T1), (v2, T2)) =
Term.aconv_untyped (v1, v2) andalso T1 = T2;
*)
no_adhoc_overloading abstract concrete
(* FAIL: Not a variant of "Scratch.abstract" *)
end
end
As indicated in the comment, the issue here is that
`no_adhoc_overloading const term` expects the type of `term` to be
_equal_ to the type of `term` at the time of `adhoc_overloading const
term`. However, if `term` is polymorphic, the polymorphic parsing of
`term` (using Syntax.parse_term + Variable.polymorphic, cf. source of
adhoc_overloading) introduces schematic type variables whose names are
not stable. This can be witnessed by the ML snippets inserted above.
It seems that the type-comparison needs weakening, but I am not sure
what the right comparator would be.
If this could be addressed for Isabelle2024, I'd be grateful. In the
meantime, if anyone has a workaround at hand, that would be much
appreciated as well, as we have encountered the above issue multiple
times.
Thank you,
Hanno
From: hannobecker@posteo.de
Hi,
Quick correction: It's read_term, not parse_term, that is used by
the adhoc overloading code. The problem is still the same, though.
Updated example below.
Best,
Hanno
theory Scratch
imports Main "HOL-Library.Adhoc_Overloading"
begin
declare [[show_variants]]
consts abstract :: ‹'x›
locale foo =
fixes param :: ‹'s›
begin
definition concrete :: ‹'v ⇒ 'v›
where ‹concrete ≡ id›
adhoc_overloading abstract concrete
no_adhoc_overloading abstract concrete (* OK *)
adhoc_overloading abstract concrete
(* debug only *)
ML‹"concrete" |> Syntax.read_term @{context}
|> singleton (Variable.polymorphic @{context})
|> Term.fastype_of
|> Syntax.pretty_typ @{context}
|> Pretty.writeln› (* ?'a ⇒ ?'a *)
(* Seemingly unrelated ... *)
definition test :: ‹'s ⇒ 'v ⇒ 'v› where
‹test _ x ≡ x›
(* debug only *)
ML‹"concrete" |> Syntax.read_term @{context}
|> singleton (Variable.polymorphic @{context})
|> Term.fastype_of
|> Syntax.pretty_typ @{context}
|> Pretty.writeln› (* ?'a1 ⇒ ?'a1 *)
(* Mismatch due to strict type equality check
cf. L60 in Adhoc_Overloading.thy
fun variants_eq ((v1, T1), (v2, T2)) =
Term.aconv_untyped (v1, v2) andalso T1 = T2;
*)
no_adhoc_overloading abstract concrete
(* FAIL: Not a variant of "Scratch.abstract" *)
end
end
From: hannobecker <hannobecker@posteo.de>
Hi all,The issue seems to have been addressed in Isabelle2025-RC2 -- thanks!Best,Hanno
-------- Original message --------From: hannobecker@posteo.de Date: 07/02/2024 08:51 (GMT+00:00) To: Cl isabelle users <cl-isabelle-users@lists.cam.ac.uk> Cc: cl-isabelle-users-request@lists.cam.ac.uk Subject: Re: [isabelle] Adhoc Overloading corrupted by unrelated definition Hi,Quick correction: It's read_term, not parse_term, that is used by the adhoc overloading code. The problem is still the same, though.Updated example below.Best,Hannotheory Scratch imports Main "HOL-Library.Adhoc_Overloading"begindeclare [[show_variants]]consts abstract :: ‹'x›locale foo = fixes param :: ‹'s›begindefinition concrete :: ‹'v ⇒ 'v› where ‹concrete ≡ id›adhoc_overloading abstract concreteno_adhoc_overloading abstract concrete (* OK *)adhoc_overloading abstract concrete(* debug only *)ML‹"concrete" |> Syntax.read_term @{context} |> singleton (Variable.polymorphic @{context}) |> Term.fastype_of |> Syntax.pretty_typ @{context} |> Pretty.writeln› (* ?'a ⇒ ?'a *)(* Seemingly unrelated ... *)definition test :: ‹'s ⇒ 'v ⇒ 'v› where ‹test _ x ≡ x›(* debug only *)ML‹"concrete" |> Syntax.read_term @{context} |> singleton (Variable.polymorphic @{context}) |> Term.fastype_of |> Syntax.pretty_typ @{context} |> Pretty.writeln› (* ?'a1 ⇒ ?'a1 *)(* Mismatch due to strict type equality check cf. L60 in Adhoc_Overloading.thy fun variants_eq ((v1, T1), (v2, T2)) = Term.aconv_untyped (v1, v2) andalso T1 = T2;*)no_adhoc_overloading abstract concrete(* FAIL: Not a variant of "Scratch.abstract" *)endendAm 06.02.2024 19:52 schrieb hannobecker@posteo.de:> Hi all,> > This is about enabling/disabling adhoc overloading.> > Expectation: A pair of adhoc_overloading const term and> no_adhoc_overloading const term in the same context should work and> lead to the overloading of const by term be disabled subsequently.> > Observed behavior: In the context of locales and polymorphic term,> unrelated definitions in between adhoc_overloading and> no_adhoc_overloading can lead to no_adhoc_overloading failing.> > Example:> > ``> theory Scratch> imports Main "HOL-Library.Adhoc_Overloading"> begin> > consts abstract :: ‹'x›> > locale foo => fixes param :: ‹'s›> begin> > definition concrete :: ‹'v ⇒ 'v›> where ‹concrete ≡ id›> > adhoc_overloading abstract concrete> no_adhoc_overloading abstract concrete (* OK *)> > adhoc_overloading abstract concrete> > (* debug only *)> ML‹"concrete" |> Syntax.parse_term @{context}> |> singleton (Variable.polymorphic @{context})> |> Term.fastype_of> |> Syntax.pretty_typ @{context}> |> Pretty.writeln› (* ?<position> *)> > (* Seemingly unrelated ... *)> definition test :: ‹'s ⇒ 'v ⇒ 'v› where> ‹test _ x ≡ x›> > (* debug only *)> ML‹"concrete" |> Syntax.parse_term @{context}> |> singleton (Variable.polymorphic @{context})> |> Term.fastype_of> |> Syntax.pretty_typ @{context}> |> Pretty.writeln› (* ?<position>1 *)> > (* Mismatch due to strict type equality check> cf. L60 in Adhoc_Overloading.thy> > fun variants_eq ((v1, T1), (v2, T2)) => Term.aconv_untyped (v1, v2) andalso T1 = T2;> *)> no_adhoc_overloading abstract concrete> (* FAIL: Not a variant of "Scratch.abstract" *)> > end> > end> > As indicated in the comment, the issue here is that> no_adhoc_overloading const term expects the type of term to be> _equal_ to the type of term at the time of adhoc_overloading const> term. However, if term is polymorphic, the polymorphic parsing of> term` (using Syntax.parse_term + Variable.polymorphic, cf. source of> adhoc_overloading) introduces schematic type variables whose names are> not stable. This can be witnessed by the ML snippets inserted above.> > It seems that the type-comparison needs weakening, but I am not sure> what the right comparator would be.> > If this could be addressed for Isabelle2024, I'd be grateful. In the> meantime, if anyone has a workaround at hand, that would be much> appreciated as well, as we have encountered the above issue multiple> times.> > Thank you,> Hanno
Last updated: Mar 09 2025 at 12:28 UTC