2 (* Author: Ondrej Kuncar, TU Muenchen *)
4 section {* Pervasive test of code generator *}
6 theory Generate_Efficient_Datastructures
9 "~~/src/HOL/Library/DAList_Multiset"
10 "~~/src/HOL/Library/RBT_Mapping"
11 "~~/src/HOL/Library/RBT_Set"
15 The following code equations have to be deleted because they use
16 lists to implement sets in the code generetor.
19 lemma [code, code del]:
20 "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
22 lemma [code, code del]:
23 "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
25 lemma [code, code del]:
26 "pred_of_set = pred_of_set" ..
28 lemma [code, code del]:
29 "Wellfounded.acc = Wellfounded.acc" ..
31 lemma [code, code del]:
32 "Cardinality.card' = Cardinality.card'" ..
34 lemma [code, code del]:
35 "Cardinality.finite' = Cardinality.finite'" ..
37 lemma [code, code del]:
38 "Cardinality.subset' = Cardinality.subset'" ..
40 lemma [code, code del]:
41 "Cardinality.eq_set = Cardinality.eq_set" ..
43 lemma [code, code del]:
44 "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
46 lemma [code, code del]:
47 "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
49 lemma [code, code del]:
50 "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
52 lemma [code, code del]:
53 "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
56 If the code generation ends with an exception with the following message:
57 '"List.set" is not a constructor, on left hand side of equation: ...',
58 the code equation in question has to be either deleted (like many others in this file)
59 or implemented for RBT trees.
62 export_code _ checking SML OCaml? Haskell?
64 (* Extra setup to make Scala happy *)
65 (* If the compilation fails with an error "ambiguous implicit values",
66 read \<section>7.1 in the Code Generation Manual *)
69 "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
70 unfolding gfp_def by blast
73 "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
74 unfolding lfp_def by blast
76 export_code _ checking Scala?