Email Gateway (Aug 18 2022 at 11:50): Email Gateway (Aug 18 2022 at 11:50):From: John Matthews <matthews@galois.com>
Hi,
I am trying to generate executable code for some overloaded definitions:
consts cplus :: "'a => 'b => 'b"
defs (overloaded)
cplus_nat_int_def[code func]:
"cplus (a::nat) (b::int) == int a + b"
cplus_int_nat_def[code func]:
"cplus (a::int) (b::nat) == nat a + b"
However, the code generator gives the following error:
*** Type
*** nat => int => int
*** of defining equation
*** "cplus ?a ?b == int ?a + ?b"
*** is incompatible with declared function type
*** ?'a::type => ?'b::type => ?'b::type
*** At command "defs".
What is the correct way to register code equations for overloaded
functions?
Thanks,
-john
Email Gateway (Aug 18 2022 at 11:50):From: Tobias Nipkow <nipkow@in.tum.de>
I suspect that the presence of two type variables in the generic type of
cplus is to blame. The code generator can only deal with overloading
that's resolved by a single type argument.
Tobias
John Matthews schrieb:
Email Gateway (Aug 18 2022 at 11:52):From: John Matthews <matthews@galois.com>
Thanks, Florian. But will this work for autoquickcheck? I thought
that used a separate code generator.
-john
Email Gateway (Aug 18 2022 at 11:53):From: florian.haftmann@in.tum.de
Hi John,
indeed you can use the preprocessor to deal with overloading:
consts
foo :: "'a => 'b => int"
defs (overloaded)
foo1_def: "foo (n::nat) (k::int) == int n - k"
foo2_def: "foo (k::int) (n::nat) == k + int n"
definition foo1 :: "nat => int => int" where
foo1_aux_def: "foo1 = foo"
definition foo2 :: "int => nat => int" where
foo2_aux_def: "foo2 = foo"
lemma [code func]:
"foo1 n k = int n - k"
"foo2 k n = k + int n"
unfolding foo1_aux_def foo2_aux_def foo1_def foo2_def by rule+
lemma [code inline]:
"foo = foo1"
"foo = foo2"
unfolding foo1_aux_def foo2_aux_def by rule+
This will eliminate ad-hoc overloading before the code generator
actually "sees" it. Note that this does not introduce any
polymorphism due to overloading (for which you have to use type
classes).
Hope this helps
Florian
Last updated: May 03 2024 at 04:19 UTC