src/HOL/Codegenerator_Test/RBT_Set_Test.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Tue Jul 31 13:55:39 2012 +0200
@@ -0,0 +1,51 @@
+(*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
+    Author:     Ondrej Kuncar
+*)
+
+header {* Test of the code generator using an implementation of sets by RBT trees *}
+
+theory RBT_Set_Test
+imports Library "~~/src/HOL/Library/RBT_Set"
+begin
+
+(* 
+   The following code equations have to be deleted because they use 
+   lists to implement sets in the code generetor. 
+*)
+
+lemma [code, code del]:
+  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
+
+lemma [code, code del]:
+  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
+
+lemma [code, code del]:
+  "pred_of_set = pred_of_set" ..
+
+
+lemma [code, code del]:
+  "Cardinality.card' = Cardinality.card'" ..
+
+lemma [code, code del]:
+  "Cardinality.finite' = Cardinality.finite'" ..
+
+lemma [code, code del]:
+  "Cardinality.subset' = Cardinality.subset'" ..
+
+lemma [code, code del]:
+  "Cardinality.eq_set = Cardinality.eq_set" ..
+
+
+lemma [code, code del]:
+  "acc = acc" ..
+
+(*
+  If the code generation ends with an exception with the following message:
+  '"List.set" is not a constructor, on left hand side of equation: ...',
+  the code equation in question has to be either deleted (like many others in this file) 
+  or implemented for RBT trees.
+*)
+
+export_code _ checking SML OCaml? Haskell? Scala?
+
+end