Email Gateway (Aug 19 2022 at 12:26): Email Gateway (Aug 19 2022 at 12:26):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Gottfried,
1) In the linordered_idom class context, the function foo_f takes 0.7 seconds to
process, where an identical function, foo_f2, in the global context takes
only about 0.1 second. Is there any advantage to defining foo_f in the
linordered_idom class context, other than it will localize its name?
As the definition of foo_f does not depend on any parameter of the linordered_idom type
class, I don't see a point in defining foo_f inside the type class context.
2) Inside the class context, the simp method will not use foo_f.simps, even
though the output message shows that foo_f.simps are available as rewrite
rules. Inside, linordered_idom_class.foo_f.simps must be added as a simp rule.
Is there something I can do to get it to use foo_f.simps, without having to
add the qualified name linordered_idom_class.foo_f.simps as a simp rule?
You are confused by Isabelle's type inference. Inside a type class context, the type
variable 'a is fixed, i.e., inside linorderd_idom, foo_f.simps only works for instances of
foo_f with type "'a foo_d". In your theorem, you try to instantiate 'a to int. This makes
Isabelle think that you want to refer to the exported version of foo_f, so you have to add
the exported foo_f.simps rules as well.
3) The value method prints linordered_idom numerals as sums of 1, even though
I import Code_Target_Numeral.thy. The simp method prints numerals in the nice
form. Is there something I can do to get the value method to print
linordered_idom numerals as single numbers rather than sums of 1?*)
value uses a different set of different equations for normalising terms, namely those
declared as [code], whereas the simp method uses [simp]. You can, of course, try to change
the setup of code generator, but that requires considerable effort.
Andreas
Email Gateway (Aug 19 2022 at 12:27):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 11/4/2013 4:37 AM, Andreas Lochbihler wrote:
You are confused by Isabelle's type inference. Inside a type class
context, the type variable 'a is fixed, i.e., inside linorderd_idom,
foo_f.simps only works for instances of foo_f with type "'a foo_d". In
your theorem, you try to instantiate 'a to int. This makes Isabelle
think that you want to refer to the exported version of foo_f, so you
have to add the exported foo_f.simps rules as well.
Andreas,
Thanks for the help. It helps to get help to understand the subtleties.
What I was doing in those other emails helped me here to experiment with
the type variables in the class context:
datatype 'a foo_d = Foo_d 'a
context linordered_idom
begin
fun foo_f :: "'b::linordered_idom foo_d => real" where
"foo_f (Foo_d x) = real x"
theorem "foo_f (Foo_d (1::int)) = (1::real)"
print_statement foo_f.simps
print_statement linordered_idom_class.foo_f.simps
by(simp)
end
As you talk about, the type variable 'a is special in the class context.
If I try fun foo_f :: "'a::linordered_idom foo_d => real", I get the
error Sort constraint linordered_idom inconsistent with default type
for type variable "'a". Using 'b works, and the two print statements
show I get what I want.
value uses a different set of different equations for normalising
terms, namely those declared as [code], whereas the simp method uses
[simp]. You can, of course, try to change the setup of code generator,
but that requires considerable effort.
The printing of numerals is bigger than me, but getting "value" to work
by using [code] is something I want to start doing.
Related to those other emails, I've created these commands:
consts nat_of :: "'a => nat"
abbreviation (input) nat_of_int :: "int => nat" where "nat_of_int == nat"
defs (overloaded) nat_of_int_def [simp,code_unfold]: "nat_of == nat_of_int"
These are based on the "real::'a => real" function in Real.thy.
The problem is that value "nat_of(1::int)" gets rewritten as "Suc 0",
but a slightly more complicated use of "nat_of" doesn't get simplified
with "value".
I don't know the relationship of "simp" to "code", but with
"declare[[simp_trace]]", when I use "value", the output panel shows the
rewriting that's being done.
Below, I give the simple example I just mentioned, along with the output
of the two "value"s, and some of the simp trace. I attach the THY, which
just duplicates the source I've put in this email.
Thanks for the help,
GB
consts nat_of :: "'a => nat"
abbreviation (input) nat_of_int :: "int => nat" where
"nat_of_int == nat"
defs (overloaded)
nat_of_int_def [simp,code_unfold]: "nat_of == nat_of_int"
datatype 'a foo_d2 = Foo_d2 'a
fun foo_g :: "'a foo_d2 => nat" where
"foo_g (Foo_d2 x) = nat_of(x)"
value "nat_of(1::int)"
(* Output: "(Suc (0::nat))" :: "nat" *)
(* With simp_trace, this is the first rewrite:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
(term_of_class.term_of (nat_of (1::int)))
[1]Applying instance of rewrite rule "??.unknown":
(nat_of == nat)
[1]Rewriting:
(nat_of == nat) *)
value "foo_g(Foo_d2(1::int))"
(* Output: "(nat_of (1::int))" :: "nat" *)
(* With simp_trace, this is the last rewrite:
[1]Rewriting:
(Numeral1 == (1::int))
"(nat_of (1::int))" :: "nat" *)
i131031a__q1b_context_slower__needs_qualified_simp__numeral_print.thy
Email Gateway (Aug 19 2022 at 12:29):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gottfried,
consts nat_of :: "'a => nat"
abbreviation (input) nat_of_int :: "int => nat" where
"nat_of_int == nat"defs (overloaded)
nat_of_int_def [simp,code_unfold]: "nat_of == nat_of_int"
without having had a closer look, I guess your problem is due to that
ad-hoc overloading; the code generator only supports Haskell-style
overloading with type classes.
value "foo_g(Foo_d2(1::int))"
If the output of »value t« surprises you, the first step is something like
definition
"blubb = t"
export_code blubb in SML file …
and inspecting the resulting code.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:30):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 11/4/2013 2:08 PM, Florian Haftmann wrote:
without having had a closer look, I guess your problem is due to that
ad-hoc overloading; the code generator only supports Haskell-style
overloading with type classes.
Florian,
The magic of the code generator kicks in with type classes in place. I
don't even have to declare anything for the code generator.
I don't know if I would want to be adding type classes like I'm doing
with the simple example I show here, but having learned how to do it has
been important.
(I said that before I used the "export_code" command. Up until then, I
was only associating "code generator" with the computation of values in
Isabelle. If there's nothing to export when type classes aren't being
used, then I definitely want to do whatever I need to do to be using
type classes, when computations are the potential end result.)
If the output of »value t« surprises you, the first step is something like
definition
"blubb = t"export_code blubb in SML file …
and inspecting the resulting code.
I had no interest in exporting code to bring a bunch of work onto myself
trying to track down a problem, and for the function "real" that I based
everything on, "export_code" tells me there's no code equations for
"real". Now that I have some type classes that get the code generator
working for me, I'm more interested in exporting.
I exported, but for Scala. Scala: it's a functional programming
language, an object oriented one, a scripting language, it's distributed
with Isabelle, and it's one of the four languages that the code
generator will export for. It's a good deal.
I couldn't have done it without your help.
The magic of the code generator is shown at the comment marked "(____)".
Regards,
GB
theory i131031a__q1c_using_type_classes_to_satisfy_the_code_generator
imports Complex_Main ("../../../iHelp/i")
begin
(*I based my original "nat_of" on the function "real::'a => real", where
I used
the "defs (overloaded)" command. It turns out, "real" can't be used
either by
the code generator.*)
definition foo_def :: "'a => real" where
"foo_def x = real(x)"
value "real(1::int)" (* OUTPUT: "1" :: "real"*)
value "foo_def(1::int)" (* OUTPUT: "(real 1)" :: "real" *)
(*export_code foo_def in Scala file "i131031a__q1c_foo_def.scala"
ERROR:
No code equations for real*)
(*Now I use the tip by Florian Haftmann that ad-hoc overloading is the
problem,
and that the code generator only supports Haskell-style overloading with
type
classes.*)
class lord_idom_nir = linordered_idom +
fixes nat_of :: "'a => nat"
fixes int_of :: "'a => int"
fixes rat_of :: "'a => rat"
instantiation int :: lord_idom_nir
begin
definition "nat_of = nat"
definition "int_of = (λx. x)"
definition "rat_of = rat_of_int"
instance proof qed
end
value "rat_of(int_of(int(nat_of(1::int))))" (* OUTPUT: 1::rat *)
class lord_ab_group_add_nir = linordered_ab_group_add +
fixes gnat_of :: "'a => nat"
fixes gint_of :: "'a => int"
fixes grat_of :: "'a => rat"
instantiation int :: lord_ab_group_add_nir
begin
definition "gnat_of = nat"
definition "gint_of = (λx. x)"
definition "grat_of = rat_of_int"
instance proof qed
end
datatype ('a,'b) oI =
oIf "'a * 'b"
|oIF "('a,'b) oI list"
fun oICq :: "('a::lord_idom_nir,'b::lord_ab_group_add_nir) oI => rat" where
"oICq (oIf p) = (if (snd p) < 0
then 1/rat_of(fst p ^ gnat_of(- snd p))
else rat_of(fst p ^ gnat_of(snd p)))"
|"oICq (oIF[]) = 1"
|"oICq (oIF (x#xs)) = oICq x * oICq (oIF xs)"
(export_code oICq in Scala file "i131031a__q1c_oICq.scala")
(____) It works by magic now. The output is (1::rat).*)
value "oICq(oIf(1::int,1::int))"
(*OUTPUT: (1::rat). Using the conversions that are based on ad-hoc
overloading,
the expression is never simplified. It is this:
"(rat_of (power.power 1 (λ(u ua). (u * ua)) 1 (nat_of 1)))" :: "rat" *)
(* (int * int) *)
theorem "oICq(oIf(a::int,b::int)) = rat_of(a ^ nat(b)) ∨
oICq(oIf(a::int,b::int)) = (1/rat_of(a ^ nat(-b)))"
by(simp add: gnat_of_int_def)
(* (nat * int) *)
theorem "oICq(oIf(a::nat,b::int)) = rat_of(a ^ nat(b)) ∨
oICq(oIf(a::nat,b::int)) = (1/rat_of(a ^ nat(-b)))"
by(simp add: zpower_int gnat_of_int_def)
(* (int * nat) *)
theorem "oICq(oIf(a::int,b::nat)) = rat_of(a ^ b)"
by(simp add: gnat_of_int_def)
(* (nat * nat) *)
theorem "oICq(oIf(a::nat,b::nat)) = rat_of(a ^ b)"
by(simp add: zpower_int gnat_of_int_def)
(* Export test of a simple definition using nat_of.*)
definition def_export_test :: "int => nat" where
"def_export_test x = nat_of x"
(*export_code def_export_test in Scala file
"i131031a__q1c_def_export_test.scala"*)
i131031a__q1c_using_type_classes_to_satisfy_the_code_generator.thy
Email Gateway (Aug 19 2022 at 12:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
This is the first of two emails with some questions about my use of the
linordered_idom class. In this email, I ask three fairly simple questions.
The questions are in the attached THY, at the top of the file, and I
include the contents of the THY below.
Thanks,
GB
(*I have three questions related to the 6 comments in the source below,
and which
are marked 1a, 1b, 2a, 2b, 3a, and 3b, though the comments aren't in
that order.
1) In the linordered_idom class context, the function foo_f takes 0.7
seconds to
process, where an identical function, foo_f2, in the global context takes
only about 0.1 second. Is there any advantage to defining foo_f in the
linordered_idom class context, other than it will localize its name?
2) Inside the class context, the simp method will not use foo_f.simps, even
though the output message shows that foo_f.simps are available as rewrite
rules. Inside, linordered_idom_class.foo_f.simps must be added as a simp
rule.
Is there something I can do to get it to use foo_f.simps, without having to
add the qualified name linordered_idom_class.foo_f.simps as a simp rule?
3) The value method prints linordered_idom numerals as sums of 1, even
though
I import Code_Target_Numeral.thy. The simp method prints numerals in the
nice
form. Is there something I can do to get the value method to print
linordered_idom numerals as single numbers rather than sums of 1?*)
datatype 'a foo_d = Foo_d 'a
context linordered_idom
begin
(___1a__ It takes about 0.7 second to process foo_f in this context.)
fun foo_f :: "'a foo_d => real" where
"foo_f (Foo_d x) = real x"
(*___2a__ Inside, foo_f.simps must be used with the fully qualified
name, even
though the output message shows it's present as a rewrite rule.*)
theorem "foo_f (Foo_d (1::int)) = (1::real)"
apply(simp add: foo_f.simps)
(*OUTPUT: Ignoring duplicate rewrite rule... Failed to apply proof
method...*)
apply(simp add: linordered_idom_class.foo_f.simps)
done
end
(___2b__ Outside, foo_f.simps works without the fully qualified name.)
theorem "foo_f (Foo_d (1::int)) = (1::real)"
by(simp)
(*___1b__ It takes about 0.1 second to process foo_f2 in the global
context.*)
fun foo_f2 :: "'a::linordered_idom foo_d => real" where
"foo_f2 (Foo_d x) = real x"
(*___3a__ Value prints numerals as sums of 1. Importing
Code_Target_Numeral.thy
doesn't help.*)
declare[[show_sorts=true]]
value "foo_f(Foo_d(2 * 2))"
(*OUTPUT:
"real (((1::'a::linordered_idom) + (1::'a::linordered_idom)) *
((1::'a::linordered_idom) + (1::'a::linordered_idom)))"
:: "real"*)
(___3b__ But simp prints numerals in the nice form.)
theorem "foo_f(Foo_d(2 * 2)) = (4::real)"
apply(simp)
(*OUTPUT:
goal (1 subgoal):
Last updated: Apr 19 2024 at 12:27 UTC