Re: [isabelle] Adding a code equation for a class parameter



Hi Lars,

many packages implicitly declare some code equations for the constants you define. The code generator remembers that that these declarations have been implicity, so when you explicitly declare a new code equation, it silently drops the implicit ones. This behaviour is sensible in many cases because the user otherwise would have to manually delete the default equations first, which might not be that easy. Therefore, you have to declare all the code equations you want. For example,

declare plus_natt.simps [code]
lemma [code]: "x + Z = x" by (induct x) auto

should give you what you expect. Note that the code generator sorts the cases in the reverse order as you declare them.

Best,
Andreas

On 09/10/13 15:54, Lars Hupel wrote:
(Referring to both Isabelle2013 and Isabelle2013-1-RC2.)

Assume the following clone of the `nat` datatype and its obvious
instantiations for `zero` and `plus`, along with some auxiliary
definitions:

   datatype natt = Z | S natt

   instantiation natt :: "{zero,plus}" begin

   definition zero_natt_def:
   "0 = Z"

   primrec plus_natt where
   "Z + x = x" |
   "(S m) + n = S (m + n)"

   instance ..

   end

   fun f :: "'a::plus ⇒ 'a" where
   "f x = x + x"

   definition "i ≡ f (S Z)"

Now, exporting code for `i` works as expected, and

   value [code] i

correctly yields `S (S Z)`.

However, if I add this code equation:

   lemma [code]: "x + Z = x"
   by (induct x) auto

... the generated code looks fishy (there is no warning of "subsumed code
equations" or the like):

   export_code i in SML

   fun plus_natta x Z = x;

Invoking `value [code] i` again produces an error:

   Warning: Matches are not exhaustive.
   fun plus_natta x Z = x
   At (line 23 of "generated code")
   Exception- Match raised

(Side note: `value [simp] i` fails to produce a normal form too, it just
prints `S Z + S Z`.)

I have no idea why that happens. Is what I'm trying to do even supported?
I couldn't find a hint in the type class tutorial (nor in the code
generation tutorial).





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