author | blanchet |
Mon, 26 Nov 2012 13:35:05 +0100 | |
changeset 50222 | 40e3c3be6bca |
parent 49948 | 744934b818c7 |
child 50996 | 51ad7b4ac096 |
permissions | -rw-r--r-- |
48624 | 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 |
|
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
48624
diff
changeset
|
8 |
imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set" |
48624 | 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 |