|
1 |
|
2 (* Author: Ondrej Kuncar, TU Muenchen *) |
|
3 |
|
4 header {* Pervasive test of code generator *} |
|
5 |
|
6 theory Generate_Efficient_Datastructures |
|
7 imports |
|
8 Candidates |
|
9 "~~/src/HOL/Library/DAList" |
|
10 "~~/src/HOL/Library/RBT_Mapping" |
|
11 "~~/src/HOL/Library/RBT_Set" |
|
12 begin |
|
13 |
|
14 (* |
|
15 The following code equations have to be deleted because they use |
|
16 lists to implement sets in the code generetor. |
|
17 *) |
|
18 |
|
19 lemma [code, code del]: |
|
20 "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" .. |
|
21 |
|
22 lemma [code, code del]: |
|
23 "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. |
|
24 |
|
25 lemma [code, code del]: |
|
26 "pred_of_set = pred_of_set" .. |
|
27 |
|
28 lemma [code, code del]: |
|
29 "acc = acc" .. |
|
30 |
|
31 lemma [code, code del]: |
|
32 "Cardinality.card' = Cardinality.card'" .. |
|
33 |
|
34 lemma [code, code del]: |
|
35 "Cardinality.finite' = Cardinality.finite'" .. |
|
36 |
|
37 lemma [code, code del]: |
|
38 "Cardinality.subset' = Cardinality.subset'" .. |
|
39 |
|
40 lemma [code, code del]: |
|
41 "Cardinality.eq_set = Cardinality.eq_set" .. |
|
42 |
|
43 (* |
|
44 If the code generation ends with an exception with the following message: |
|
45 '"List.set" is not a constructor, on left hand side of equation: ...', |
|
46 the code equation in question has to be either deleted (like many others in this file) |
|
47 or implemented for RBT trees. |
|
48 *) |
|
49 |
|
50 export_code _ checking SML OCaml? Haskell? |
|
51 |
|
52 (* Extra setup to make Scala happy *) |
|
53 (* If the compilation fails with an error "ambiguous implicit values", |
|
54 read \<section>7.1 in the Code Generation Manual *) |
|
55 |
|
56 class ccpo_linorder = ccpo + linorder |
|
57 |
|
58 lemma [code]: |
|
59 "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = |
|
60 (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))" |
|
61 unfolding admissible_def by blast |
|
62 |
|
63 lemma [code]: |
|
64 "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}" |
|
65 unfolding gfp_def by blast |
|
66 |
|
67 lemma [code]: |
|
68 "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}" |
|
69 unfolding lfp_def by blast |
|
70 |
|
71 export_code _ checking Scala? |
|
72 |
|
73 end |