[isabelle] Weird extra type token in locale interpretation

Hi all,

I stumbled across the following problem with locales, see below for a small example.

Locale "heap" simply fixes the operations "empty_heap", "new_obj" and "typeof_addr" and defines in terms of them two other functions "addr_of_sys_xcpt" and "preallocated".

The first depends only on the parameters empty_heap and new_obj.
preallocated is defined in terms of addr_of_sys_xcpt and thus depends on all three parameters, although only on typeof_addr directly.

Next, I interpret this locale (with prefix test), where new_obj gets instantiated to some function sc_new_obj that is partially applied to some list P, which the for clause declares. In its definition, sc_new_obj is polymorphic in the list's element type.

Since interpretation parameters declared in for clauses become additional parameters of the abbreviations that the interpretation introduces, I would have expected that "test.preallocated" abbreviates

%P. heap.preallocated Map.empty (sc_new_obj P) id"

and has type "'a list => (nat ~=> ty) => bool".


term test.preallocated


"%TYPE P. heap.preallocated Map.empty (sc_new_obj P) id"
  :: "'a itself => 'a list => (nat ~=> ty) => bool"

test.preallocated expects an additional type token, which is unnecessary, because the same type variable also occurs in the second parameter! Why is that? And how can I get test.preallocated without the extra type token?

Here is the example for Isabelle2009-1:

typedecl ty

locale heap =
  fixes empty_heap :: "'heap"
  and new_obj :: "'heap => string => ('heap * nat option)"
  and typeof_addr :: "'heap => nat => ty option"

definition addr_of_sys_xcpt :: "string => nat"
  "addr_of_sys_xcpt C =
   (let (h0,  a0) = new_obj empty_heap ''foo''
    in if C = ''foo'' then the a0
       else undefined)"

definition preallocated :: "'heap => bool"
  "preallocated h = (typeof_addr h (addr_of_sys_xcpt ''foo'') ~= None)"


types sc_heap = "nat => ty option"

definition sc_new_obj :: "'a list => sc_heap => string => (sc_heap * nat option)"
where "sc_new_obj P h C = (h, None)"

interpretation test!: heap Map.empty "sc_new_obj P" id for P

term test.preallocated


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

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