Email Gateway (Aug 19 2022 at 14:39): Email Gateway (Aug 19 2022 at 14:39):From: René Neumann <rene.neumann@in.tum.de>
Dear all,
given I have some locale foo with a myriad of parameters. Now I want to
extend this into a locale bar, which should add some parameters. Also
(for convenience) the new parameters should go to the end and the old
order of parameters should not change. In general such a thing is
possible with:
locale bar = foo +
fixes param_b1 :: "'v => 's"
and param_b2 :: "'v => 's => 's"
But, if I want to unify the types of foo and bar, I get a problem:
locale bar = foo param_f1 param_f2
for param_f1 and param_f2 :: "'s => 'v" +
fixes param_b1 :: "'v => 's"
and param_b2 :: "'v => 's => 's"
This now has a different order of parameters:
params_f3 … param_fn param_f1 param_f2 param_b1 param_b2
The only way to keep the order is to list all n parameters in the
import-part -- which quickly gets nasty, especially if you have a larger
locale hierarchy.
Are there any means to specify type signatures without changing the
order of arguments? Something along the lines of:
locale bar = foo where param_f2 :: "'v => 's" +
fixes ...
(or, as 'where' is used for equations, other keywords like 'constraining')
or using the record-way (though then the question arises on how to
specify the order of the types in the annotation):
locale bar = ('v,'s) foo +
fixes ...
Any hints are very much appreciated.
Thanks,
René
P.S.: The same problem arises, when the only parameter using all
relevant type variables is the very last one of the imported locale.
smime.p7s
Email Gateway (Aug 19 2022 at 14:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
IMHO you should consider one of these:
a) What is the matter of your order? To have uniform appearance of
locale expressions? In that case, you might consider specification of
parameters by name. See the Isar reference manual for the syntactic
details.
b) If you really want to have structural control, consider grouping your
parameters to records. HOL-Algebra is a nice example how this is
accomplished in practice.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,
there is the context element "constrains" that can achieve this to some extend. This works
best if you constrain the types of all parameters of the imported locale that are
affected. Here's an example:
locale l1 =
fixes p1 :: 'b
and p2 :: 'b
and p3 :: 'a
assumes "p1 = p2"
locale l2 =
l1
+
constrains p1 :: "'c"
and p2 :: "'c"
fixes p4 :: "'c"
assumes "p4 = p2"
P.S.: The same problem arises, when the only parameter using all
relevant type variables is the very last one of the imported locale.
In that case, there is a simple trick using the wildcard _ in the import expression. These
wildcards are treated like parameters not mentioned and are therefore added implicitly to
the head of the for clause, as you desire.
locale l3 = fixes p1 :: 'a and p2 :: 'b and p3 :: "'a + 'b"
locale l4 = l3 _ _ p3
for p3 :: "'b + 'b"
+
fixes p4 :: 'b
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 14:49):From: René Neumann <rene.neumann@in.tum.de>
Am 30.06.2014 20:35, schrieb Florian Haftmann:
Hi René,
given I have some locale foo with a myriad of parameters. Now I
want to extend this into a locale bar, which should add some
parameters. Also (for convenience) the new parameters should go
to the end and the old order of parameters should not change.IMHO you should consider one of these: a) What is the matter of
your order? To have uniform appearance of locale expressions? In
that case, you might consider specification of parameters by
name. See the Isar reference manual for the syntactic details.
Ah, I wasn't aware that I can also use the where-clause in locale
specifications. This actually turns out to be (nearly) what I want: If
one specifies the _last_ parameter with a 'where'-clause, also the
order is kept the same (of course, this is only useful when all
necessary type variables are part of it):
locale bar = foo
where param_fn = param_fn
for param_fn :: "..." +
...
b) If you really want to have structural control, consider grouping
your parameters to records. HOL-Algebra is a nice example how this
is accomplished in practice.
Our "problem" arose from the fact that we had to abolish our setup
with records, as this gave rise to other problems with multiple
inheritance (if locale A specifies record rA
and locale B has record rB = rA + B_ext
and locale C has record rC = rA + C_ext
and I now want to have a locale BC which implements both B and C, I am
stuck, as I can't have a record rBC = rB + rC)
Hope this helps,
It did, thanks!
Email Gateway (Aug 19 2022 at 15:01):From: René Neumann <rene.neumann@in.tum.de>
Am 30.06.2014 21:27, schrieb Andreas Lochbihler:
Hi René,
there is the context element "constrains" that can achieve this to some
extend. This works best if you constrain the types of all parameters of
the imported locale that are affected.
Unfortunately, all parameters are affected, so there is no gain here.
But the 'constrains' provided the idea for the 'constraining'-thing in
my email.
(Also: 'constrains' is marked as deprecated, so I'd better avoid it in
new developments)
P.S.: The same problem arises, when the only parameter using all
relevant type variables is the very last one of the imported locale.
In that case, there is a simple trick using the wildcard _ in the import
expression. These wildcards are treated like parameters not mentioned
and are therefore added implicitly to the head of the for clause, as you
desire.locale l3 = fixes p1 :: 'a and p2 :: 'b and p3 :: "'a + 'b"
locale l4 = l3 _ _ p3
for p3 :: "'b + 'b"
+
fixes p4 :: 'b
Ah, forgot about those.
Thanks a lot,
René
smime.p7s
Last updated: Apr 26 2024 at 20:16 UTC