Re: [isabelle] [code func] attribute on overloaded definitions

Thanks, Florian. But will this work for autoquickcheck? I thought that used a separate code generator.


On May 13, 2008, at 2:38 AM, haftmann at mailbroy.informatik.tu- wrote:

Hi John,

indeed you can use the preprocessor to deal with overloading:

 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.