[isabelle] Proof failed for BNF iterators at code_thms and export_code



Dear Isabelle developers,

I usually find the commands code_thms and export_code very useful while I work on setting up the code generator. In combination with the BNF codatatype command, however, they sometimes abort with "Proof failed." It reliably happens if the iterator or recursor for the codatatype is reachable in the code dependency graphs and I have forgotten to provide code equations for them. Here's a minimal example for Isabelle2013-1:

theory Scratch imports "~~/src/HOL/BNF/BNF" begin
codatatype foo = Foo | Bar foo
code_datatype Foo Bar
code_thms foo_unfold

At code_thms, I get "Proof failed." and a huge goal state talking about the internal BNF construction for the the foo instead of the usual list of theorems that I would like to inspect. The same happens at export_code and value [code].

I know that code generation for codatatypes is not yet set up in Isabelle2013-1, so it is kind of my own fault that I have forgotten to declare the relevent code equations. Nevertheless, why does the code generator even try to prove anything at all? And how can this fail?

Best,
Andreas




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