[isabelle] Weird extra type token in locale interpretation
I stumbled across the following problem with locales, see below for a
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".
"%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:
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
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
where "sc_new_obj P h C = (h, None)"
interpretation test!: heap Map.empty "sc_new_obj P" id for P
Karlsruher Institut für Technologie
Adenauerring 20a, Gebäude 50.41, Raum 023
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