Re: [isabelle] linordered_idom: context affecting time & simp, printing numerals



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


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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.