# HG changeset patch
# User kuncar
# Date 1343735739 -7200
# Node ID 9b71daba4ec7fc4d9c6fdd870bcc8923f1c40114
# Parent  bea613f2543d5a2cf4fc9639269064543c4db77e
add testing file for RBT_Set

diff -r bea613f2543d -r 9b71daba4ec7 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
diff -r bea613f2543d -r 9b71daba4ec7 src/HOL/Codegenerator_Test/ROOT.ML
--- a/src/HOL/Codegenerator_Test/ROOT.ML	Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/Codegenerator_Test/ROOT.ML	Tue Jul 31 13:55:39 2012 +0200
@@ -1,1 +1,1 @@
-use_thys ["Generate", "Generate_Pretty"];
+use_thys ["Generate", "Generate_Pretty", "RBT_Set_Test"];
diff -r bea613f2543d -r 9b71daba4ec7 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jul 31 13:55:39 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 31 13:55:39 2012 +0200
@@ -153,7 +153,7 @@
 
 session Codegenerator_Test = "HOL-Library" +
   options [document = false, document_graph = false, browser_info = false]
-  theories Generate Generate_Pretty
+  theories Generate Generate_Pretty RBT_Set_Test
 
 session Metis_Examples = HOL +
   description {*