[isabelle] Non-exhaustive case certificates

Dear all,

suppose I have a type with a number of constructors, but only some of them are meant to be used for code generation. For example:

datatype foo = A | B | C | D
definition test
  where "test x = 4 + (case x of A => 0 | B => 1 | C => 2 | D => 3)"

In the exported code for test, the case expression is translated into a case expression of the target language. In particular, it does not use foo_case.
However, when I restrict foo to some subset of constructors, say

code_datatype A B C

then export_code on test generates the error message

*** "Test.foo.D" is not a constructor, on left hand side of equation:
*** case D of A => ?f1.0 | B => ?f2.0 | C => ?f3.0 | D => ?f4.0 == ?f4.0
*** At command "export_code"

This error message seems to stem from the case certificate that the datatype declaration registered in the code generator. I'd like to replace that after the code_datatype declaration with something like

lemma new_foo_case_cert:
  assumes "CASE == foo_case a b c d"
  shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c)"
using assms by auto
setup {*
  Code.add_case @{thm new_foo_case_cert}

This version raises the exception option, other variations yield "bad case certificate". How do I need to phrase the case certificate such that the code generator accepts it?

If this is impossible, I'd like to know why. If it is just a matter of adapting the code generator implementation, I'd be happy to assist in implementing this.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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