Re: [isabelle] Problems with Code-Generator
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:
we just stumbled upon the translation of pattern matching of natural numbers for code-generation in the presence of target-language integers.
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