Email Gateway (Aug 19 2022 at 11:17): Email Gateway (Aug 19 2022 at 11:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 11:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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 "IntInf.int")
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.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 11:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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?
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
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, ...) *)
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 =
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):
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
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?
Andreas
Last updated: Apr 20 2024 at 12:26 UTC