Re: [isabelle] value [code] raises Match in code_ml.ML

Hi Andreas,

> 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 "")
> code_const bar (SML "0")
> export_code foobar in SML file - (* works *)
> value [code] foobar (* fails with Match *)

the reason for the failure is that value [code] always involves a
suitable term_of expression.  You have to add a reasonable

  code_const "Code_Evaluation.term_of :: … foo …" (Eval …)

to regain it.

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

Abstract datatype constructors are explicitly checked for absence.
Maybe it is possible to tweak your application accordingly.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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