Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with code-generator

Email Gateway (Aug 19 2022 at 14:00):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

below you find an example where target-language
natural numbers are not properly supported in combination
with pattern matching.

Consider the following theory:

theory Test
imports
"~~/src/HOL/Library/Code_Binary_Nat"
begin

fun foo :: "nat * 'a list => bool" where
"foo (Suc 0, (x # xs)) = True"
| "foo (Suc 0, []) = False"
| "foo p = True"

export_code foo in Haskell

Using Code_Binary_Nat, the export_code raises an error
"Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
foo (Suc ?vc, ?x # ?xs) ≡ if equal_nat_inst.equal_nat ?vc zero_nat_inst.zero_nat then True else True

whereas it does not occur if Code_Binary_Nat is not imported.

Moreover, the error does not occur if I only do pattern matching on
natural numbers, but not on the lists.

The problem occurs in both Isabelle2013-2 and development version ede82d6e0abd.

Kind regards,
René

Email Gateway (Aug 19 2022 at 14:01):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,

Code_Binary_Nat contains an ML function that tries to replace Suc patterns on left-hand
sides while preprocessing the code equations. When natural numbers are implemented by
target-language numbers, Suc patterns must not appear on the left-hand sides of equations
any more. It is well-known that the conversion function is not complete, e.g. from this
thread from 2011:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-April/msg00012.html

You probably have to manually write a code equation for foo that pattern-matches on Suc
only on right-hand sides or not at all.

Best,
Andreas

Email Gateway (Aug 19 2022 at 14:01):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Hi Andreas,

Code_Binary_Nat contains an ML function that tries to replace Suc patterns on left-hand sides while preprocessing the code equations. When natural numbers are implemented by target-language numbers, Suc patterns must not appear on the left-hand sides of equations any more.

The latter is obvious.

It is well-known that the conversion function is not complete, e.g. from this thread from 2011:

I missed this knowledge and supposed that the conversion would/should be complete.

You probably have to manually write a code equation for foo that pattern-matches on Suc only on right-hand sides or not at all.

Obviously, hand written code-equations circumvent the problem (which is what I currently do). However, no one wants to
provide manual code-equations for each function that performs pattern matching on Suc.
This is why I hoped for completeness of the ML function to convert Suc patterns.

Cheers,
René

Email Gateway (Aug 19 2022 at 14:01):

From: Dmitriy Traytel <traytel@in.tum.de>
Am 17.03.2014 09:22, schrieb Andreas Lochbihler:

Hi René,

Code_Binary_Nat contains an ML function that tries to replace Suc
patterns on left-hand sides while preprocessing the code equations.
When natural numbers are implemented by target-language numbers, Suc
patterns must not appear on the left-hand sides of equations any more.
It is well-known that the conversion function is not complete, e.g.
from this thread from 2011:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-April/msg00012.html

You probably have to manually write a code equation for foo that
pattern-matches on Suc only on right-hand sides or not at all.
case_of_simps (cf. HOL/Library/Simps_Case_Conv.thy and
HOL/ex/Simps_Case_Conv_Examples.thy) might help automating this task.

Dmitriy

Best,
Andreas

On 14/03/14 20:06, René Thiemann wrote:

Dear all,

below you find an example where target-language
natural numbers are not properly supported in combination
with pattern matching.

Consider the following theory:

theory Test
imports
"~~/src/HOL/Library/Code_Binary_Nat"
begin

fun foo :: "nat * 'a list => bool" where
"foo (Suc 0, (x # xs)) = True"
| "foo (Suc 0, []) = False"
| "foo p = True"

export_code foo in Haskell

Using Code_Binary_Nat, the export_code raises an error
"Nat.Suc" is not a constructor, on left hand side of equation, in
theorem:
foo (Suc ?vc, ?x # ?xs) ≡ if equal_nat_inst.equal_nat ?vc
zero_nat_inst.zero_nat then True else True

whereas it does not occur if Code_Binary_Nat is not imported.

Moreover, the error does not occur if I only do pattern matching on
natural numbers, but not on the lists.

The problem occurs in both Isabelle2013-2 and development version
ede82d6e0abd.

Kind regards,
René

Last updated: Apr 19 2024 at 04:17 UTC