Email Gateway (Aug 22 2022 at 10:33): Email Gateway (Aug 22 2022 at 10:33):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear locale experts,
The commands for interpreting a locale (interpret/interpretation/sublocale) accept
parameters declared with a for clause. The generated abbreviations for the constants
defined in the locale then take the declared parameters as additional arguments. However,
the order of these additional arguments is IMHO all but intutive and a night-mare for
maintainability. The two examples below illustrate this.
Suppose we have a locale which fixes a parameter and defines a function f using the
parameter x. For the interpretation, let's define an abbreviation foo with two arguments
and interpret the locale for foo with both parameters declared in a for clause.
locale l = fixes x :: int begin
definition f where "f y = x + y"
end
abbreviation foo :: "nat ⇒ int ⇒ int" where "foo x y == y - 2 * int x"
interpretation sl!: l "foo x y" for x :: nat and y :: int .
term sl.f (* λy x. l.f (foo x y) *)
As can be seen by inspecting the generated abbreviation sl.f, the order of the parameters
in the for clause (first x, then y) has been ignored, as sl.f takes first the y and then
the x.
Now, if I later change foo from an abbreviation to a definition, the order of parameters
changes. Now, sl'.f takes the x first and then the y.
definition foo' :: "nat ⇒ int ⇒ int" where "foo' x y == y - 2 * int x"
interpretation sl'!: l "foo' x y" for x :: nat and y :: int .
term sl'.f (* λx y. l.f (foo' x y) *)
Apparently, not the order of the parameters in the for clause matters, but the order of
the parameters as they occur in the term which is used to instantiate the parameter. So,
when I going from an abbreviation to a definition, I have to reorder the first two
parameters of all occurrences of sl.f in my theories.
If we have a locale with several parameters (say 2), things get even worse. The order
of the parameter is not consistent over several constant declarations. In this example,
there are two parameters and two definitions each of which depends on only one of the
parameters.
locale l2 = fixes x :: int and z :: int begin
definition f where "f y = x + y"
definition g where "g y = z + y"
end
interpretation sl2!: l2 "y - 2 * int x" "int x - 2 * y" for x :: nat and y :: int .
term "sl2.f :: int ⇒ nat ⇒ int ⇒ int"
term "sl2.g :: nat ⇒ int ⇒ int ⇒ int"
Now we see that sl2.f first takes the y and then the x, whereas sl2.g first takes the x
and then the y.
I find this particularly annoying, because for every function defined in my locale I have
to remember separately the order of the parameters. I'd prefer much more if interpretation
and friends used the order of the parameters as given in the for clause consistently for
all constants. Can this behaviour be somehow changed?
I tried to use unnamed context blocks to fix the order of parameters, but interpretations
are gone at the end of the block and sublocale and permanent_interpretation do not work
inside such blocks.
Andreas
Email Gateway (Aug 22 2022 at 10:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
if I conclude correctly you suggest that exporting a term out of an
eigencontext (»for«) should honour the order in which variables have
been specified.
This sounds reasonable. What appears strange to me is that the
behaviour of eigencontexts differs from unnamed context blocks in that
respect, because as far as I know and can glimpse from the
implementation the internal treatment should be the same… can anybody
shed further light on this?
Cheers,
Florian
signature.asc
Last updated: Apr 20 2024 at 04:19 UTC