Email Gateway (Aug 19 2022 at 15:29): Email Gateway (Aug 19 2022 at 15:29):From: Holden Lee <hl422@cam.ac.uk>
Hi,
I'm wondering whether it is possible to declare a sublocale when the one of
the records is an extension of the other. Suppose I first define
locale ab_locale
which is based off the record (a_object::'a, b_object::'b), and later
decide it would be useful to have a more general
locale a_locale
which is based off the record (a_object::'a). Could I make ab_object a
sublocale of a_object (here I would just want to set the a_object's equal)?
-Holden
Email Gateway (Aug 19 2022 at 15:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Holden,
Locales and records are independent, so your setting is not well-specified. However, I
suspect that your situation resembles the following.
record 'a a = a_object :: 'a
record ('a, 'b) ab = "'a a" + b_object :: 'b
locale a = fixes r_a :: "'a a"
locale ab = fixes r_b :: "('a, 'b) ab" begin
sublocale a r_b .
Here, the sublocale command fails because r_b has type "(_, _) ab" which is incompatible
with type "_ a" as required by locale a. The reason is that the locales use the closed
record types "_ a" and "(_, _) ab" instead of the extensible record schemes that the
record package uses internally. If you generalise your locales to schemes, it works in
this setting:
locale a = fixes r_a :: "('a, 'more) a_scheme"
locale ab = fixes r_b :: "('a, 'b, 'more) ab_scheme" begin
sublocale a r_b .
What happens here is the following: The type parameter 'more from locale a gets
instantiated with the extension type ('b, 'more) ab_ext which implements the extension of
record type ab over record type a.
Hope this helps,
Andreas
Last updated: Apr 20 2024 at 04:19 UTC