*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 04 Nov 2013 20:17:52 -0600*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5277FEA1.2090506@informatik.tu-muenchen.de>*References*: <5276C6E4.9050903@gmx.com> <527778FA.4080209@inf.ethz.ch> <5277D374.7020708@gmx.com> <5277FEA1.2090506@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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,

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

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*)

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))"

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"

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 = (\<lambda>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 = (\<lambda>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 (\<lambda>(u ua). (u * ua)) 1 (nat_of 1)))" :: "rat" *) (* (int * int) *) theorem "oICq(oIf(a::int,b::int)) = rat_of(a ^ nat(b)) \<or> 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)) \<or> 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"*) (******************************************************************************) end (******************************************************************************)

**References**:**[isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Gottfried Barrow

**Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Andreas Lochbihler

**Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Gottfried Barrow

**Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Next by Date: Re: [isabelle] Problems with elder Isabelle Versions under MacOSX Maverick
- Previous by Thread: Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Next by Thread: [isabelle] Looking for rat & int powers to use with linordered_idom
- Cl-isabelle-users November 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