*To*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Problems with Code-Generator*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 30 Sep 2016 15:25:40 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <75A0BCAF-7E82-4798-BDA3-B91BE1AAF63B@uibk.ac.at>*References*: <13F3E45C-B507-479E-B5DB-F470ECD384A6@uibk.ac.at> <e2f6507d-4168-b139-7570-f8bc8062d646@inf.ethz.ch> <75A0BCAF-7E82-4798-BDA3-B91BE1AAF63B@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Hi RenÃ,

lemma [code]: "foo (Suc n) = False" "foo m = Code.abort ''invalid argument'' (%_. foo m)" should raise the error "invalid argument" rather than ''pattern match failed''.

Andreas On 30/09/16 14:06, Thiemann, Rene wrote:

Hi Andreas, thanks for the hint. However, I do not see that the problem with incomplete patterns is so problematic. What about a translation according to the following idea? âfoo n = (if n = 1 then True else Code.abort ââpattern match failedâ' (% _. foo n))â Best regards, RenÃAm 30.09.2016 um 10:05 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>: Dear RenÃ, This problem only shows up if you import Code_Target_Nat from HOL/Library, which changes the code representation of naturals from 0/Suc to a copy of natural, which are in turn implemented by target-language integers. There is a preprocessor in Code_Abstract_Nat, which tries to eliminate pattern-matching on Suc, but it only works if there a corresponding code equation for 0, too. One could try to come up with a better implementation, but it's not that easy. Best, Andreas On 30/09/16 09:47, Thiemann, Rene wrote:Dear list, we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers. theory Test imports Main "~~/src/HOL/Library/Code_Target_Numeral" begin fun foo :: "nat â bool" where "foo (Suc 0) = True" export_code foo in Haskell (* "Nat.Suc" is not a constructor, on left hand side of equation, in theorem: foo (Suc zero_nat_inst.zero_nat) â True *) end Of course, it is easy to work around by providing suitable code-equations manually, but perhaps this can be fixed in the future. The problem occurs in both Isabelle 2016 and in the development version d4b89572ae71. Cheers, Akihisa and RenÃ

**References**:**[isabelle] Problems with Code-Generator***From:*Thiemann, Rene

**Re: [isabelle] Problems with Code-Generator***From:*Andreas Lochbihler

**Re: [isabelle] Problems with Code-Generator***From:*Thiemann, Rene

- Previous by Date: [isabelle] Model checking of Simulink components with Isabelle
- Next by Date: Re: [isabelle] pairs and friends
- Previous by Thread: Re: [isabelle] Problems with Code-Generator
- Next by Thread: [isabelle] pairs and friends
- Cl-isabelle-users September 2016 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