Email Gateway (Aug 19 2022 at 12:03): Email Gateway (Aug 19 2022 at 12:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Since this would issue warnings in the common case that default code
equations stemming from definitions are replaced by elaborated code
equations.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:22):From: Lars Hupel <hupel@in.tum.de>
(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).
Email Gateway (Aug 19 2022 at 12:22):From: Lars Hupel <hupel@in.tum.de>
My mail client mangled the Unicode symbols. I attached the theory file for
reproducing the problem.
Scratch.thy
Email Gateway (Aug 19 2022 at 12:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 12:23):From: Lars Hupel <hupel@in.tum.de>
Hello Andreas,
thanks, that explanation makes perfect sense. I do wonder why there's
no warning in this case, though, just like the warning you get when
adding a code equation which subsumes others.
Cheers
Lars
Last updated: Apr 18 2024 at 08:19 UTC