Email Gateway (Aug 22 2022 at 15:29): Email Gateway (Aug 22 2022 at 15:29):From: Fabian Hellauer <hellauer@in.tum.de>
Hi,
in this example
theory Scratch
imports Main "~~/src/HOL/Library/Code_Target_Nat"
begin
fun foo :: "'a list ⇒ 'a list ⇒ nat ⇒ bool" where
"foo (t#ts) (s#ss) 0 ⟷ False" |
"foo (t#ts) ss (Suc i) ⟷ False" |
"foo ts [] 0 ⟷ False" |
"foo [] ss _ ⟷ False"
export_code foo in SML
end
the code export fails with the message:
"Nat.zero_nat_inst.zero_nat" is not a constructor, on left hand
side of equation, in theorem: foo ?ts [] zero_nat_inst.zero_nat ≡ False
If I remove any of the three arguments, it works fine.
Do you have an idea what is going on?
Cheers,
Fabian
Scratch.thy
Email Gateway (Aug 22 2022 at 15:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Fabian,
The problem is that your function has been defined with pattern-matching on natural
numbers and lists, but by importing Code_Target_Nat, you have instructed the code
generator to implement natural numbers as target-language integers, so pattern matching on
natural numbers cannot be done any more. This is what the error message tells you.
In most of the cases, you do not notice this problem because Code_Target_Nat installs a
preprocessor for code equations that eliminates pattern matches on natural numbers.
Unfortunately, this preprocessor does not work in all cases. Basically, whenever there is
an equation
foo pat1 pat2 0 = rhs1
then there must also be an equation
foo pat1 pat2 (Suc n) = rhs2 n
with the same patterns pat1 and pat2 such that they can be combined to
foo pat1 pat2 x = if x = 0 then rhs1 else rhs (x - 1)
For your function foo, this is not the case, as there is the pattern
foo ts [] 0 = False
but no corresponding
foo ts [] (Suc n) = ...
This problem is well-known [1]. A student of mine and I are currently working on a proper
solution for this. For the time being, you can manually complete the missing patterns in
the code equations as follows:
lemmas foo_code [code] =
foo.simps(1)
foo.simps(2)[of _ _ "[]"]
foo.simps(2)[of _ _ "_ # _"]
foo.simps(3)[of "_ # _"]
foo.simps(4)[of _ _ "0"]
foo.simps(5)
Hope this helps,
Andreas
[1] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September/msg00078.html
Last updated: Apr 26 2024 at 20:16 UTC