[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.

Andreas

--
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
http://pp.info.uni-karlsruhe.de
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.