*To*: Sebastiaan Joosten <sjcjoosten at gmail.com>*Subject*: Re: [isabelle] Overlapping patterns in code export*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 22 Feb 2017 16:12:51 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <F590F8C9-C7E7-424E-859F-36CF273D0202@gmail.com>*References*: <7764B389-3555-45C6-A16B-00BD8705DD3D@gmail.com> <983149ee-889a-74a9-22d8-2365e8960101@inf.ethz.ch> <F590F8C9-C7E7-424E-859F-36CF273D0202@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

Hi Sebastiaan,

Best, Andreas On 22/02/17 14:10, Sebastiaan Joosten wrote:

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

**References**:**[isabelle] Overlapping patterns in code export***From:*Sebastiaan Joosten

**Re: [isabelle] Overlapping patterns in code export***From:*Andreas Lochbihler

**Re: [isabelle] Overlapping patterns in code export***From:*Sebastiaan Joosten

- Previous by Date: [isabelle] Exception THM 0 raised (line 86 of tactic.ML)
- Next by Date: [isabelle] newbie: Binomial extensions
- Previous by Thread: Re: [isabelle] Overlapping patterns in code export
- Next by Thread: [isabelle] CFP: Special Issue of the AMAI on the Formalization of Geometry, Automated and Interactive Geometric Reasoning
- Cl-isabelle-users February 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list