Email Gateway (Aug 18 2022 at 19:39): Email Gateway (Aug 18 2022 at 19:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
For me (rev. ca5b629a5995), z does not work either.
The argument list given to export_code is parsed as a list of terms, so
abbreviations are expanded. The result is then checked to be a constant
of an appropriate type with implicit monomorphization of class
operations (cf. Code.read_const). In your example, x and y are such
instances of class operations; z and u are not but parametricly
polymorphic (although dependent on a class operation wrt. to the
underlying code equations) and thus need to be specified with their
general type.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 20:03):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,
I tried to test the code generator setup for sets in Isabelle2012-RC1. The
following test fails although I would have expected it to work. Moreover, I
neither understand the error message, nor do I have any idea how to fix the problem.
theory Scratch imports Main begin
export_code UNION in SML file -
*** Type
*** 'a::type set => ('a::type => 'b::type set) => 'b::type set
*** of constant "Complete_Lattices.complete_lattice_class.SUPR"
*** is too specific compared to declared type
*** ?'b::{} set => (?'b::{} => ?'a::{}) => ?'a::{}
*** At command "export_code"
Best regards,
Andreas
Email Gateway (Aug 18 2022 at 20:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
the issue is simple: UNION is just an abbrev for SUPR at a certain type,
and therefore has a »too specific« type. Want you want is:
export_code SUPR in SML
or
definition "foo = UNION"
export_code foo in SML
Hope this helps,
Florian
Email Gateway (Aug 18 2022 at 20:05):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Florian,
thanks for the explanation (and solution). So far, abbreviations in export_code
statements either worked for me or I got an error about "not a constant". Is
there a rule of thumb when the code generator accepts to generate code for
type-constrained constants?
For example, of the following abbreviations, x y and z work, although they
specialize types, but u does not. What is the fundamental difference?
abbreviation x :: nat where "x == 0" (* overloaded constant *)
abbreviation y :: "nat => nat => nat" where "y == op +" (* overloaded operator *)
abbreviation z :: "nat => nat => nat" where "z == power" (* definition in type
class *)
abbreviation u :: "(nat => bool) => nat" where "u == Least"
Andreas
Last updated: Apr 23 2024 at 12:29 UTC