Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Weird extra type token in locale interpretation


view this post on Zulip Email Gateway (Aug 18 2022 at 15:04):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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".

However

term test.preallocated

produces

"%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"
begin

definition addr_of_sys_xcpt :: "string => nat"
where
"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"
where
"preallocated h = (typeof_addr h (addr_of_sys_xcpt ''foo'') ~= None)"

end

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

Regards,
Andreas


Last updated: Mar 29 2024 at 04:18 UTC