|
1 (* Title: HOL/Codegenerator_Test/RBT_Set_Test.thy |
|
2 Author: Ondrej Kuncar |
|
3 *) |
|
4 |
|
5 header {* Test of the code generator using an implementation of sets by RBT trees *} |
|
6 |
|
7 theory RBT_Set_Test |
|
8 imports Library "~~/src/HOL/Library/RBT_Set" |
|
9 begin |
|
10 |
|
11 (* |
|
12 The following code equations have to be deleted because they use |
|
13 lists to implement sets in the code generetor. |
|
14 *) |
|
15 |
|
16 lemma [code, code del]: |
|
17 "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" .. |
|
18 |
|
19 lemma [code, code del]: |
|
20 "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. |
|
21 |
|
22 lemma [code, code del]: |
|
23 "pred_of_set = pred_of_set" .. |
|
24 |
|
25 |
|
26 lemma [code, code del]: |
|
27 "Cardinality.card' = Cardinality.card'" .. |
|
28 |
|
29 lemma [code, code del]: |
|
30 "Cardinality.finite' = Cardinality.finite'" .. |
|
31 |
|
32 lemma [code, code del]: |
|
33 "Cardinality.subset' = Cardinality.subset'" .. |
|
34 |
|
35 lemma [code, code del]: |
|
36 "Cardinality.eq_set = Cardinality.eq_set" .. |
|
37 |
|
38 |
|
39 lemma [code, code del]: |
|
40 "acc = acc" .. |
|
41 |
|
42 (* |
|
43 If the code generation ends with an exception with the following message: |
|
44 '"List.set" is not a constructor, on left hand side of equation: ...', |
|
45 the code equation in question has to be either deleted (like many others in this file) |
|
46 or implemented for RBT trees. |
|
47 *) |
|
48 |
|
49 export_code _ checking SML OCaml? Haskell? Scala? |
|
50 |
|
51 end |