[isabelle] value [code] raises Match in code_ml.ML
Dear experts on the code generator,
I want to map a HOL type to a built-in type of the target languages using code_type and
code_const. For evaluation with the simplifier, however, I want to implement the type by a
pseudo-constructor that has no analogue in the target language, i.e., there is no simple
code_const translation for the function declared with code_datatype. The following MWE
illustrates the setting:
consts Foo :: foo
code_datatype Foo (* constructor for value [simp] *)
definition "bar = Foo"
definition "foobar = bar"
value [code] foobar
code_type foo (SML "IntInf.int")
code_const bar (SML "0")
export_code foobar in SML file - (* works *)
value [code] foobar (* fails with Match *)
code_const Foo (SML "0")
value [code] foobar
Here, Foo is the constructor that value [simp] uses. After I have declared the adaptations
for the type foo and the constant bar, I can still export code for foobar, but "value
[code] foobar" now raises a Match exception in code_ml.ML (l. 240 in Isabelle2013). If I
add any translation for the code_datatype constructor Foo (it seems as if it does not
matter what), value [code] works again. The same exception occurs if I export code for
something that uses Foo directly:
definition "foo = Foo"
export_code foo in SML file - (* fails if placed between code_type and code_const Foo *)
For value [code] foobar, I would have expected no error at all.
For export_code foo, I would have expected some sensible error message saying that an
adaptation for Foo is missing.
My problem is now that I cannot provide a sensible code_const declaration for Foo (other
than raise an error at run-time, but I would prefer to get an error message at code
generation if my code uses Foo directly) and I am not allowed to prove a HOL code equation
for Foo either (because Foo is a code_datatype constructor), but I have to do something to
get value [code] working. What is the recommended solution here?
This archive was generated by a fusion of
Pipermail (Mailman edition) and