[isabelle] Code generator produces non-linear patterns
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
Workaround: In the second clause, rename 'is' to something else.
This archive was generated by a fusion of
Pipermail (Mailman edition) and