restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
authorkuncar
Tue Jan 15 12:13:27 2013 +0100 (2013-01-15)
changeset 5099651ad7b4ac096
parent 50995 3371f5ee4ace
child 50997 31f9ba85dc2e
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
src/HOL/Codegenerator_Test/RBT_Set_Test.thy
src/HOL/Library/RBT_Set.thy
     1.1 --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Fri Jan 25 16:45:09 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Tue Jan 15 12:13:27 2013 +0100
     1.3 @@ -46,6 +46,27 @@
     1.4    or implemented for RBT trees.
     1.5  *)
     1.6  
     1.7 -export_code _ checking SML OCaml? Haskell? Scala?
     1.8 +export_code _ checking SML OCaml? Haskell?
     1.9 +
    1.10 +(* Extra setup to make Scala happy *)
    1.11 +(* If the compilation fails with an error "ambiguous implicit values",
    1.12 +   read \<section>7.1 in the Code Generation Manual *)
    1.13 +
    1.14 +class ccpo_linorder = ccpo + linorder
    1.15 +
    1.16 +lemma [code]:
    1.17 +  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
    1.18 +    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    1.19 +unfolding admissible_def by blast
    1.20 +
    1.21 +lemma [code]:
    1.22 +  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    1.23 +unfolding gfp_def by blast
    1.24 +
    1.25 +lemma [code]:
    1.26 +  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    1.27 +unfolding lfp_def by blast
    1.28 +
    1.29 +export_code _ checking Scala?
    1.30  
    1.31  end
     2.1 --- a/src/HOL/Library/RBT_Set.thy	Fri Jan 25 16:45:09 2013 +0100
     2.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Jan 15 12:13:27 2013 +0100
     2.3 @@ -63,8 +63,6 @@
     2.4  lemma [code, code del]:
     2.5    "Bex = Bex" ..
     2.6  
     2.7 -term can_select
     2.8 -
     2.9  lemma [code, code del]:
    2.10    "can_select = can_select" ..
    2.11  
    2.12 @@ -526,6 +524,8 @@
    2.13  
    2.14  code_datatype Set Coset
    2.15  
    2.16 +declare set.simps[code]
    2.17 +
    2.18  lemma empty_Set [code]:
    2.19    "Set.empty = Set RBT.empty"
    2.20  by (auto simp: Set_def)