Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Overlapping patterns in code export

Email Gateway (Aug 22 2022 at 15:07):

From: Sebastiaan Joosten <sjcjoosten@gmail.com>
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

end

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

Best,

Sebastiaan

Email Gateway (Aug 22 2022 at 15:07):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.

Best,
Andreas

Email Gateway (Aug 22 2022 at 15:07):

From: Sebastiaan Joosten <sjcjoosten@gmail.com>
Hi Andreas,

thank you for your response!

it surprised me that Haskell's overlapping patterns warning had not hit me earlier. If the function package can be simplified such that it creates more overlapping rules, I may not have been as surprised, and I would be all for it.

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.

I don't agree with this reasoning: eagerly removing an overlapped simp rule is something else than perfect minimisation. The function package might annotate which simp rules are overlapped by all the earlier ones, such that the code generator only produces code for those that are non-overlapped. Alternatively, the function package might generate a code lemma that uses in-order if-then-else, also to avoid unnecessary blowup in code size, as illustrated by the following:

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

In any case, I suppose I should just suppress code-overlap warnings in Haskell for now.

Best,

Sebastiaan

Email Gateway (Aug 22 2022 at 15:07):

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

Indeed, it would be great if the sequential option in the function package produces less
redundant rules than it is doing now. In particular, as all those redundant cases show up
in the induction rule for the function, so if one uses this induction rule, one has to
prove a lot of redundant subgoals, too :-).

If you have some time, feel free to look into the code. The pattern splitting is done in
src/HOL/Tools/Function/pattern_split.ML.

Best,
Andreas

Last updated: Apr 25 2024 at 04:18 UTC