Email Gateway (Aug 18 2022 at 15:04): 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: Nov 21 2024 at 12:39 UTC