[isabelle] Problems with Code-Generator

[Thiemann, Rene]

Dear list,

we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.

theory Test
imports
Main
"~~/src/HOL/Library/Code_Target_Numeral"
begin

fun foo :: "nat ⇒ bool" where
"foo (Suc 0) = True"

export_code foo in Haskell

(* "Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
foo (Suc zero_nat_inst.zero_nat) ≡ True *)

end

Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future.
The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71.

Cheers,
Akihisa and René

[Andreas Lochbihler]

Dear René,

This problem only shows up if you import Code_Target_Nat from HOL/Library, which changes
the code representation of naturals from 0/Suc to a copy of natural, which are in turn
implemented by target-language integers. There is a preprocessor in Code_Abstract_Nat,
which tries to eliminate pattern-matching on Suc, but it only works if there a
corresponding code equation for 0, too.

One could try to come up with a better implementation, but it's not that easy.

Best,
Andreas

Post by Thiemann, Rene
Dear list,
we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.
theory Test
imports
Main
"~~/src/HOL/Library/Code_Target_Numeral"
begin
fun foo :: "nat ⇒ bool" where
"foo (Suc 0) = True"
export_code foo in Haskell
foo (Suc zero_nat_inst.zero_nat) ≡ True *)
end
Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future.
The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71.
Cheers,
Akihisa and René

[Thiemann, Rene]

Hi Andreas,

thanks for the hint.

However, I do not see that the problem with incomplete patterns is so problematic. What about a translation according to the following idea?

“foo n = (if n = 1 then True else Code.abort ‘’pattern match failed’'
(% _. foo n))”


Best regards,
René

Post by Andreas Lochbihler
Dear René,
This problem only shows up if you import Code_Target_Nat from HOL/Library, which changes the code representation of naturals from 0/Suc to a copy of natural, which are in turn implemented by target-language integers. There is a preprocessor in Code_Abstract_Nat, which tries to eliminate pattern-matching on Suc, but it only works if there a corresponding code equation for 0, too.
One could try to come up with a better implementation, but it's not that easy.
Best,
Andreas

Post by Thiemann, Rene
Dear list,
we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.
theory Test
imports
Main
"~~/src/HOL/Library/Code_Target_Numeral"
begin
fun foo :: "nat ⇒ bool" where
"foo (Suc 0) = True"
export_code foo in Haskell
foo (Suc zero_nat_inst.zero_nat) ≡ True *)
end
Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future.
The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71.
Cheers,
Akihisa and René

[Andreas Lochbihler]

Hi René,

You are right, in the case of pattern matches on a single argument, the elimination of the
0/Suc patterns could be done like that. The only tricky bit is to handle sequential
pattern matches correctly, i.e.,

lemma [code]:
"foo (Suc n) = False"
"foo m = Code.abort ''invalid argument'' (%_. foo m)"

should raise the error "invalid argument" rather than ''pattern match failed''.

The situation gets complicated when there are pattern matches on several arguments and the
patterns overlap. Especially if you want to preserve the strictness of generated Haskell
functions, the task becomes non-trivial.

Feel free to improve the current preprocessor. Maybe being able to deal with a few special
cases would be enough in practice.

Andreas

Post by Thiemann, Rene
Hi Andreas,
thanks for the hint.
However, I do not see that the problem with incomplete patterns is so problematic. What about a translation according to the following idea?
“foo n = (if n = 1 then True else Code.abort ‘’pattern match failed’'
(% _. foo n))”
Best regards,
René

Post by Andreas Lochbihler
Dear René,
This problem only shows up if you import Code_Target_Nat from HOL/Library, which changes the code representation of naturals from 0/Suc to a copy of natural, which are in turn implemented by target-language integers. There is a preprocessor in Code_Abstract_Nat, which tries to eliminate pattern-matching on Suc, but it only works if there a corresponding code equation for 0, too.
One could try to come up with a better implementation, but it's not that easy.
Best,
Andreas

Post by Thiemann, Rene
Dear list,
we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.
theory Test
imports
Main
"~~/src/HOL/Library/Code_Target_Numeral"
begin
fun foo :: "nat ⇒ bool" where
"foo (Suc 0) = True"
export_code foo in Haskell
foo (Suc zero_nat_inst.zero_nat) ≡ True *)
end
Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future.
The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71.
Cheers,
Akihisa and René