Email Gateway (Aug 18 2022 at 13:57): Email Gateway (Aug 18 2022 at 13:57):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
I do not understand the following behavior of abbreviations inside locales:
locale dummy = fixes F::'a
context dummy begin
abbreviation G :: 'a where "G == id F"
term "id F" term G (* OK *)
(* *)
definition F1::nat where "F1 == 7"
abbreviation G1 :: nat where "G1 == F1"
term F1 term G1 (* OK *)
(* *)
definition F2::nat where "F2 == 7"
abbreviation G2 :: nat where "G2 == id F2"
term "id F2" term G2 (* ? *)
end
Why doesn't "G2" abbreviate "id F2" inside "dummy"? It appears that, to the
contrary, "id F2" abbreviates "G2". (This is not the case of "G" and "G1",
however, which do behave as I would expect. )
Thank you in advance,
Andrei
Email Gateway (Aug 18 2022 at 13:57):From: popescu2@illinois.edu
My previous message sent from yahoo got polluted with extra question
marks. Here is a hopefully clean version:
I do not understand the following behavior of abbreviations inside locales:
locale dummy = fixes F::'a
context dummy begin
abbreviation G :: 'a where "G == id F"
term "id F" term G (* OK *)
(* *)
definition F1::nat where "F1 == 7"
abbreviation G1 :: nat where "G1 == F1"
term F1 term G1 (* OK *)
(* *)
definition F2::nat where "F2 == 7"
abbreviation G2 :: nat where "G2 == id F2"
term "id F2" term G2 (* ? *)
end
Why doesn't "G2" abbreviate "id F2" inside "dummy"? It appears that, to the
contrary, "id F2" abbreviates "G2". (This is not the case of "G" and "G1",
however, which do behave as I would expect. )
Thank you in advance,
Andrei
Email Gateway (Aug 18 2022 at 13:58):From: Makarius <makarius@sketis.net>
The abbreviation "G2 == id F2" expands correctly, but printing produces an
unexpected result. The reason for this is an extra indirection in F2,
which is also associated with an internal abbreviation, because it is a
constant inside a locale target (even though it does not depend on any
locale parameters).
You can inspect the internals like this:
ML {* set long_names *}
print_abbrevs
The print mechanism folds "local.F2 == Scratch.dummy.F2" first, so
"Scratch.dummy.G2 == Fun.id Scratch.dummy.F2" cannot be folded anymore.
Folding abbreviations that depend on each other is a bit unpredictable in
general. The abbreviation mechanism could be a bit smarter in its
strategy, but some uncertainty would always remain.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC