Re: [isabelle] 'where'-clause for defining locales



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

On 30/06/14 16:46, René Neumann wrote:
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.





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