Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generator produces non-linear patterns

Email Gateway (Aug 19 2022 at 17:11):

From: Lars Hupel <hupel@in.tum.de>
I've encountered some odd behaviour when generating code involving
non-trivial use of case combinators; I'm getting ML code which contains
non-linear pattern matches. Here's a small example to reproduce the problem:

datatype_new instr = A | B

type_synonym instr_table = "instr list × instr list list"

definition interp :: "instr_table ⇒ instr list" where
"interp tab =
(case tab of (A # is, _) ⇒ is |
(B # _, is # _) ⇒ is)"

export_code interp in SML module_name interp file "code/interp.ML"

The resulting ML code looks like this:

fun interp tab =
(case tab of (A :: is, x) => is | (B :: is, is :: _) => is);

... which fails to compile. This can be observed both in Isabelle2014
and in Isabelle/adaa430fc0f7. Same problem occurs when exporting to
Scala, but not when specifying 'interp' as 'fun' and using its built-in
pattern matching.

Workaround: In the second clause, rename 'is' to something else.

Cheers
Lars

Email Gateway (Aug 19 2022 at 17:13):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,

thanks for your report. I'll have a look at it.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC