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


typedecl foo
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?

Best,
Andreas




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