Re: [isabelle] Overlapping patterns in code export

Hi Sebastiaan,

The generated code indeed can contain overlapping rules and this is actually a feature of the code generator. For example, this makes it possible to implement generic algorithms in a modular way when data refinement in the code generator is used. In fact, the code generator cannot decide in general whether a given pattern has been covered by all previous equations, because it would have to know the semantics of the constructors, but the modular architecture prevents that.

The function package is also well-advised to generate overlapping simp rules. Perfect minimisation is NP complete (Alex Krauss has a paper on that), so function definitions would take much longer.


On 21/02/17 13:53, Sebastiaan Joosten wrote:
Hi Isabelle list,

I'm getting a ghc warning of overlapping patterns, and I'm wondering whether that's intended behavior. The example uses "fun" (or equivalently: function with sequential), shown below.
I consider these options:
1. Fun should not generate overlapping simp rules.
2. Fun may generate overlapping simp rules, but the code export should not generate code for the overlapped ones (or avoid the overlap in another way, like by changing the pattern order).
3. Code export may sometimes generate overlapping rules, this is intended behavior. In this case I need to disable some of Haskell's warnings on the generated files.

I'd love to hear which is the case.

Here is the example:

theory Test imports Main begin

fun foo where
  "foo (True, []) = True"
| "foo (False, [x]) = True"
| "foo _ = False"

export_code foo in Haskell


Here is the relevant Haskell code:

foo :: forall a. (Bool, [a]) -> Bool;
foo (True, []) = True;
foo (False, [x]) = True;
foo (False, []) = False;
foo (False, v : vc : vd) = False;
foo (True, vb : vc) = False;
foo (v, vb : va : vd) = False; -- overlapped by the two patterns above



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