*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] value [code] raises Match in code_ml.ML*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 26 Jun 2013 08:38:07 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51C9D6DB.2000801@informatik.tu-muenchen.de>*References*: <51BEBC87.3090306@inf.ethz.ch> <51C8837A.2010600@informatik.tu-muenchen.de> <51C95D5D.70802@inf.ethz.ch> <51C9D6DB.2000801@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130510 Thunderbird/17.0.6

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 setup?

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, ...) *) code_printing 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''" shows "term_of_class.term_of x =

(term_of_class.term_of (Rep_uint32' x))" by(simp add: term_of_anything)

fun rep_uint32 (... x) = x

lemma Rep_uint32_code [code]: "Rep_uint32 x = (BITS n. x !! n)" by transfer 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 get 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?

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? Andreas

**References**:**[isabelle] value [code] raises Match in code_ml.ML***From:*Andreas Lochbihler

**Re: [isabelle] value [code] raises Match in code_ml.ML***From:*Florian Haftmann

**Re: [isabelle] value [code] raises Match in code_ml.ML***From:*Andreas Lochbihler

**Re: [isabelle] value [code] raises Match in code_ml.ML***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] normalization method introduces schematic type variables in HOL/Word types
- Next by Date: Re: [isabelle] normalization method introduces schematic type variables in HOL/Word types
- Previous by Thread: Re: [isabelle] value [code] raises Match in code_ml.ML
- Next by Thread: [isabelle] MetiTarski 2.2 released!
- Cl-isabelle-users June 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list