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



Hi Florian,


the reason for the failure is that value [code] always involves a
suitable term_of expression.
Thanks for the hint with term_of.

You have to add a reasonable

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

to regain it.
In my concrete case, it suffices to declare an appropriate code equation for term_of, because my type foo is just a typedef foo = "UNIV :: ...", so I have a representation function Rep_foo, i.e., my code equation looks as follows:

term_of_class.term_of x =
Code_Evaluation.App
   (Code_Evaluation.Const (STR ''Scratch.Abs_foo'')
      (typerep.Typerep (STR ''fun'') [..., typerep.Typerep (STR ''Scratch.foo'') []]))
   (term_of_class.term_of (Rep_foo x))

I am not happy about writing long Isabelle constant names and type names explicity. In ML, there are nice @{type_name} and @{const_name} to generate and check these representations. Is there some similar mechanism for these strings. I had a look at Code_Evaluation, but I haven't found anything.

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.
Abstract datatypes are a good idea, and it is possible in my case. I can also get rid of the code_const for the abstraction function (Abs_foo for the typedef, Foo in the original example). Unfortunately, I am then stuck with the representation function Rep_foo, for example

definition test where "test = Rep_foo bar"

If I declare a code equation for Rep_foo, code generation works for test, but code_simp loops. My current solution is to have another identical representation function Rep_foo' and a code equation for the Rep_foo' and the canonical "Rep_foo (Abs_foo x) = x" for code_simp. Functions then have to use Rep_foo' (except for equations declared as code abstract) - if they use Rep_foo directly, I am back at the exception Match when generating code. It would be great if there was a more informative error message.

Cheers,
Andreas




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