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
Last updated: Apr 28 2024 at 20:16 UTC