Re: [isabelle] Problems with Code-Generator
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))â
> 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.
> 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
>> 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 *)
>> 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.
>> Akihisa and RenÃ
This archive was generated by a fusion of
Pipermail (Mailman edition) and