[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
pattern matching.

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.