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

Hi Florian,

I am not sure whether I understand properly.  If Abs_foo is an abstract
constructor, the code equation

   Rep_foo (Abs_foo x) = x

is implicit.  I admit the system allows, pointlessly, to override this,
but this should be considered a feature aka bug.  So what is your exact
I have precisely tried to overwrite this code equation. Here's the simplified setup (for Isabelle 2cfe6656d6d6, backporting the example to Isabelle2013 does not seem to be worth the effort; I omitted a few tweaks that improve performance):

typedef uint32 = "{_ :: 32 word. True}" by simp
  (* I do not use UNIV to trick setup_lifting into setting
     up code generation for an abstract datatype instead of
     using Abs_foo as the free datatype constructor *)
setup_lifting type_definition_uint32

(* transfer all the type class instantiations for 32 word to uint32
   using lift_definition (neg_numeral, comm_ring, equal, bits, ...) *)

  type_constructor uint32 =>
  (SML) "Word32.word" and
| constant "0 :: uint32" =>
  (SML) "(Word32.fromInt 0)" and
| ...

lemma [code, code del]: "term_of_class.term_of = (term_of_class.term_of :: uint32 => _)"

definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32"

lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. x !! n)"
unfolding Rep_uint32'_def by transfer simp

(* Implement term reconstruction for uint32 in terms of 32 word. *)
lemma term_of_uint32_code [code]:
  defines "TR == typerep.Typerep" and "bit0 == STR ''Numeral_Type.bit0''"
  "term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
       (term_of_class.term_of (Rep_uint32' x))"
by(simp add: term_of_anything)

Note that in the last line of lemma term_of_uint32_code, I now use Rep_uint32' and not Rep_uint32. If I use Rep_uint32 instead, I get into trouble: every value [code] command then generates ML code that contains the definition

fun rep_uint32 (... x) = x

where ... is the serialisation of Abs_uint32. Without custom serialisation for Abs_uint32, I only got various exceptions in the code generator. But I cannot give any serialisation that would fit into that position, because there is no ML constructor to pattern match on. So I thought I should derive my own code equation for Rep_uint32:

lemma Rep_uint32_code [code]: "Rep_uint32 x = (BITS n. x !! n)" by transfer simp

Then, value [code] works perfectly fine and I don't even need to give a serialisation for Abs_uint32. :-) Unfortunately, value [simp] "Rep_uint32 5" loops, because value [simp] is not aware of all the code_printing (code_const/code_type/...) adaptations. I have not been able to trace the simplifier for value [simp] because [[simp_trace]] first outputs all the code_unfold preprocessing steps and that trace alone has more than 300000 lines which freezes jEdit and crashes PG). Do you know a way to trace value [simp]?

So I thought that the following might happen (without being able to verify this):

- 5 is represented as "numeral (num.Bit1 (num.Bit0 num.One))"
- I have a setup that implements uint32 numerals in terms of integer
  in the generated code via a coercion function Uint32 :: integer => uint32, i.e.,
  we are evaluating the following:
  Rep_uint32 (Uint32 (numeral (num.Bit1 (num.Bit0 num.One))))
- Uint32 has a code equation of the form
  Uint32_code: "Rep_uint32 (Uint32 n) = word_of_int (int_of_integer n)"
- So the simplfier now has two options, either rewrite with Rep_uint32_code
  or with Uint32_code. Unfortunately, it seems to pick the wrong Rep_uint32_code, so we
  BITS n. Uint32 ... !! n
- Now, the code equation for op !! kicks in: i !! n = Rep_uint32 i !! n
- And now, there is another Rep_uint32 waiting to be rewritten to with Rep_uint32_code.
  This closes the loop.

Is this understanding correct?

The code equation Rep_uint32 has not caused any problems in the generated code (both with export_code and value [code]), because the code generator eliminates all these Rep_uint32 occurrences (except for the one in term_of_uint32_code, but that's fine.

My solution at the moment is to define this second destructor Rep_uint32' and implement it with BITS and keep Rep_uint32 as it is for code_simp. There's only one downside with this so far. If I use Rep_uint32 in a position where the transformation for abstract datatypes does not eliminate it, e.g., in value [code] "Rep_uint32 5", I get a Match exception in code_ml.ML. If I add a serialisation for Abs_uint32, code generation succeeds, but the ML compiler rejects it because ... in the following cannot be a constructor:

fun Rep_uint32 (... n) = n

I would prefer if the code generator raises a more sensible error message than Match here.

What do you think of my setup? Is this going the right way?


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