Re: [isabelle] Problems with Code-Generator

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,

> Am 30.09.2016 um 10:05 schrieb Andreas Lochbihler <andreas.lochbihler at>:
> 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Ã

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