Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Types for Function.get_info

Email Gateway (Aug 18 2022 at 18:02):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hi all,

While using "Function.get_info" in Isabelle/HOL(ML), I got an "Empty"
exception coming from the "the_single" function.

I discovered that when defining a function in Isabelle/HOL, as soon as the
type variables of the type annotation differs from the ones of the infered
type (without type annotation), the function is added twice (with these two
typing informations) to the FunctionData. Then the "the_single" call of
"Function.get_info" fails (with an Empty exception while the list contains 2
elements, which can be a little confusing :-)).

Here is a simple example:

fun foo :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b)" where
"foo a b = (a, b)"

ML {*
Item_Net.retrieve (Function_Common.get_function @{context}) @{term "foo"}
|> map #1
} ( 1 element in the list *)

fun foo' :: "'a \<Rightarrow> 'c \<Rightarrow> ('a * 'c)" where
"foo' a b = (a, b)"

ML {*
Item_Net.retrieve (Function_Common.get_function @{context}) @{term "foo'"}
|> map #1
} ( 2 elements with similar types in the list *)

ML {* Function.get_info @{context} @{term "foo"} } ( OK *)
ML {* Function.get_info @{context} @{term "foo'"} } ( exception Empty *)

Bug or feature ?

Thanks,

Mathieu

Email Gateway (Aug 18 2022 at 18:03):

From: Alexander Krauss <krauss@in.tum.de>
Hi Mathieu,

I discovered that when defining a function in Isabelle/HOL, as soon as the
type variables of the type annotation differs from the ones of the infered
type (without type annotation), the function is added twice (with these two
typing informations) to the FunctionData.

[...]

Bug or feature ?

I confirm that this is a bug in function's way of declaring its data.
After the termination proof, the data is updated by just re-issuing the
declaration, but the termination part has a different typing than the
function part, even if they come from the same thing originally.

It is not really easy to do this right in the presence of arbitrary
local theory magic... I'll have a look at some point (I hope it is not a
show-stopper for you).

Thanks,
Alex

Last updated: Apr 26 2024 at 16:20 UTC