Email Gateway (Aug 19 2022 at 13:54): Email Gateway (Aug 19 2022 at 13:54):From: Jose Divasón <jose.divasonm@unirioja.es>
Hello,
Thank you so much for your help Fabian, now it works.
One remark for the rest of the users of the list. It's worth noting the
importance of the order when we are importing theories involving code
generation. In my case, I work using the Multivariate_Analysis session.
If one creates a new file importing both the Multivariate Analysis files
and the file "Code_Rational" that Fabian has sent previously, then an
exception is got when the code is exported. This is an example:
theory Code_Rational_Problem
imports
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
Code_Rational
begin
definition "test11 = [[273/2::rat,7],[28/2,7]]"
export_code test11
in Haskell
module_name "Gauss_Haskell"
file "haskell"
end
The exception is: exception BAD_THM "Not an abstract type: Rat.rat" raised
(line 436 of "Isar/code.ML")"
To solve it, in my case, I have had to import
"~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" at the beginning
of the theory Code_Rational attached by Fabian.
Thanks again.
Best,
Jose
Email Gateway (Aug 19 2022 at 14:02):From: Jose Divasón <jose.divasonm@unirioja.es>
Dear all,
attached you can find an attempt to serialise the rat type in Isabelle to
the Rational type in Haskell. It works, but I think that there are better
ways to do that.
For the moment, I have serialised the operations "Frct" and "quotient_of"
in the following way:
constant "Frct" ⇀ (Haskell) "(let (x,y) = _ in (Rational.fract
(integer'_of'_int x) (integer'_of'_int y)))"
| constant "quotient_of" ⇀ (Haskell) "(let x = _ in (Int'_of'_integer
(Rational.numerator x), Int'_of'_integer (Rational.denominator x)))"
I would like to avoid the use of integer_of_int and Int_of_integer in those
lines (because they are Isabelle functions and then, sometimes, if I don't
export them they are not automatically generated to Haskell).
I have tried to work out that problem by means of a function "Frct_integer"
and a code lemma, but it doesn't work:
lift_definition Frct_integer :: "integer × integer => rat"
is "Frct :: int × int => rat" .
lemma [code]:
"Frct a = Frct_integer ((of_int (fst a)), (of_int (snd a)))"
by (transfer, simp)
code_printing
constant "Frct_integer" ⇀ (Haskell) "Rational.fract (_)"
The problem arises in the code lemma, because the output says that there is
an "abstractor as head in equation". So I can prove it but not use it as a
code lemma.
I have a similar problem working with "quotient_of".
definition numerator :: "rat => int"
where "numerator x = fst (quotient_of x)"
definition denominator :: "rat => int"
where "denominator x = snd (quotient_of x)"
lemma quotient_of_num_den: "quotient_of x = ((numerator x), (denominator
x))"
unfolding numerator_def denominator_def
by simp
lift_definition numerator_integer :: "rat => integer"
is "numerator" .
lift_definition denominator_integer :: "rat => integer"
is "denominator" .
lemma [code]: "quotient_of x = (int_of_integer (numerator_integer x),
int_of_integer(denominator_integer x))"
by (transfer, simp add: quotient_of_num_den)
code_printing
constant "numerator_integer" ⇀ (Haskell) "Rational.numerator (_)"
| constant "denominator_integer" ⇀ (Haskell) "Rational.denominator (_)"
The code lemma can't be proven because there is a "Projection as head in
equation".
I think that all comes from this theorem, which is in the file HOL/Rat.thy:
lemma [code abstype]:
"Frct (quotient_of q) = q"
by (cases q) (auto intro: quotient_of_eq)
But I don't know if it is possible to remove that tag [code abstype], or
maybe there is another way to avoid the use of integer_of_int and
int_of_integer in the serialisation.
Thanks in advance for any advice.
Best,
Jose
Code_Rational.thy
Email Gateway (Aug 19 2022 at 14:03):From: Fabian Immler <immler@in.tum.de>
Hi Jose,
Apparently, you can delete Frct as abstractor by declaring any other constant as code_datatype (should not matter, because you map type rat to Haskell type Prelude.Rational):
consts Foo::rat
code_datatype Foo
With some minor tweaks and additional code equations, the setup you had commented out generates valid Haskell-code.
(See also the attached file).
Best regards,
Fabian
Code_Rational.thy
Last updated: Apr 24 2024 at 20:16 UTC