# [isabelle] interpretation and sublocale ignore order of parameters

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.
`

`1. 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.
`

`2. 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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*