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,
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Ã
>> 



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