Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-RC2: Name-sensitivity of adhoc_ov...

Email Gateway (Feb 19 2025 at 12:01):

From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,

First, thanks for all your work on Isabelle2025, esp. the localization of syntax translations and making adhoc_overloading part of Main – this is great to see!

Below is a (to me) unexpected behaviour of adhoc_overloading. I don’t know if it is intended or not, and if not, whether it could still be changed for Isabelle2025. But since you worked on inner syntax a lot in 2025, you may know the answer off-hand:

Behaviour: When using adhoc_overloading in a locale A, other locales inheriting from A inherit the adhoc_overloading _only_ if they use exactly the same parameter name(s) as in A’s original declaration. This name-sensitivity is unexpected to me.

Minimal example follows.

=============

theory Scratch
imports Main
begin

consts uninterpreted_const :: ‹'a ⇒ 'a ⇒ 'a› ("_ ⋆⋆ _")

locale test0 =
fixes some_operator :: ‹'foo ⇒ 'foo ⇒ 'foo›
begin
adhoc_overloading uninterpreted_const ⇌ some_operator
term ‹a ⋆⋆ b› (* "a ⋆⋆ b" :: "'foo" ) ( ALL GOOD *)
end

(* Derived locale, using the same parameter name, but different type parameter name *)
locale test1 = test0 some_operator for some_operator :: ‹'bar ⇒ 'bar ⇒ 'bar›
begin
term ‹a ⋆⋆ b› (* "a ⋆⋆ b" :: "'bar" ) ( ALL GOOD *)
end

(* Derived locale, using a different parameter name *)
locale test2 = test0 some_operator' for some_operator' :: ‹'bar ⇒ 'bar ⇒ 'bar›
begin
term ‹a ⋆⋆ b› (* Unresolved adhoc overloading of constant uninterpreted_const :: "??'a ⇒ ??'a ⇒ ??'a" in term "a ⋆⋆ b"
no instances *)
end

end

============

Thanks for your help,
Hanno

Email Gateway (Feb 19 2025 at 21:53):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Hanno,

Syntax declarations generally don't survive renaming or instantiation of
term parameters, and the implementors of ad hoc overloading apparently
respected this policy. You may consider the following example:

locale test3 =
a: test0 some_operator + b: test0 some_operator' for some_operator ...
and some_operator' ...

Clemens

On 2025-02-19 12:59, "Becker, Hanno" wrote:

locale test0 =
fixes some_operator :: ‹'foo ⇒ 'foo ⇒ 'foo›
begin
adhoc_overloading uninterpreted_const ⇌ some_operator
term ‹a ⋆⋆ b› (* "a ⋆⋆ b" :: "'foo" ) ( ALL GOOD *)
end

(* Derived locale, using the same parameter name, but different type
parameter name *)
locale test1 = test0 some_operator for some_operator :: ‹'bar ⇒ 'bar ⇒
'bar›
begin
term ‹a ⋆⋆ b› (* "a ⋆⋆ b" :: "'bar" ) ( ALL GOOD *)
end

(* Derived locale, using a different parameter name *)
locale test2 = test0 some_operator' for some_operator' :: ‹'bar ⇒ 'bar
⇒ 'bar›
begin
term ‹a ⋆⋆ b› (* Unresolved adhoc overloading of constant
uninterpreted_const :: "??'a ⇒ ??'a ⇒ ??'a" in term "a ⋆⋆ b"
no instances *)
end

end

============

Thanks for your help,
Hanno

Email Gateway (Feb 20 2025 at 05:46):

From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Clemens,

Thank you for the reply!

Is this the right approach for _overloaded_ syntax provided, though?

And what is the reason to make an exception and inherit syntax declarations if names are unchanged? The naming of parameters having an effect of what gets inherited feels fragile.

Best,
Hanno

On 19/02/2025, 21:44, "Clemens Ballarin" <ballarin@in.tum.de <mailto:ballarin@in.tum.de>> wrote:

CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe.

Hi Hanno,

Syntax declarations generally don't survive renaming or instantiation of
term parameters, and the implementors of ad hoc overloading apparently
respected this policy. You may consider the following example:

locale test3 =
a: test0 some_operator + b: test0 some_operator' for some_operator ...
and some_operator' ...

Clemens

On 2025-02-19 12:59, "Becker, Hanno" wrote:

locale test0 =
fixes some_operator :: ‹'foo ⇒ 'foo ⇒ 'foo›
begin
adhoc_overloading uninterpreted_const ⇌ some_operator
term ‹a ⋆⋆ b› (* "a ⋆⋆ b" :: "'foo" ) ( ALL GOOD *)
end

(* Derived locale, using the same parameter name, but different type
parameter name *)
locale test1 = test0 some_operator for some_operator :: ‹'bar ⇒ 'bar ⇒
'bar›
begin
term ‹a ⋆⋆ b› (* "a ⋆⋆ b" :: "'bar" ) ( ALL GOOD *)
end

(* Derived locale, using a different parameter name *)
locale test2 = test0 some_operator' for some_operator' :: ‹'bar ⇒ 'bar
⇒ 'bar›
begin
term ‹a ⋆⋆ b› (* Unresolved adhoc overloading of constant
uninterpreted_const :: "??'a ⇒ ??'a ⇒ ??'a" in term "a ⋆⋆ b"
no instances *)
end

end

============

Thanks for your help,
Hanno

Last updated: Mar 09 2025 at 12:28 UTC