1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Tue Jul 31 13:55:39 2012 +0200
     1.3 @@ -0,0 +1,51 @@
     1.4 +(*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
     1.5 +    Author:     Ondrej Kuncar
     1.6 +*)
     1.7 +
     1.8 +header {* Test of the code generator using an implementation of sets by RBT trees *}
     1.9 +
    1.10 +theory RBT_Set_Test
    1.11 +imports Library "~~/src/HOL/Library/RBT_Set"
    1.12 +begin
    1.13 +
    1.14 +(* 
    1.15 +   The following code equations have to be deleted because they use 
    1.16 +   lists to implement sets in the code generetor. 
    1.17 +*)
    1.18 +
    1.19 +lemma [code, code del]:
    1.20 +  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    1.21 +
    1.22 +lemma [code, code del]:
    1.23 +  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    1.24 +
    1.25 +lemma [code, code del]:
    1.26 +  "pred_of_set = pred_of_set" ..
    1.27 +
    1.28 +
    1.29 +lemma [code, code del]:
    1.30 +  "Cardinality.card' = Cardinality.card'" ..
    1.31 +
    1.32 +lemma [code, code del]:
    1.33 +  "Cardinality.finite' = Cardinality.finite'" ..
    1.34 +
    1.35 +lemma [code, code del]:
    1.36 +  "Cardinality.subset' = Cardinality.subset'" ..
    1.37 +
    1.38 +lemma [code, code del]:
    1.39 +  "Cardinality.eq_set = Cardinality.eq_set" ..
    1.40 +
    1.41 +
    1.42 +lemma [code, code del]:
    1.43 +  "acc = acc" ..
    1.44 +
    1.45 +(*
    1.46 +  If the code generation ends with an exception with the following message:
    1.47 +  '"List.set" is not a constructor, on left hand side of equation: ...',
    1.48 +  the code equation in question has to be either deleted (like many others in this file) 
    1.49 +  or implemented for RBT trees.
    1.50 +*)
    1.51 +
    1.52 +export_code _ checking SML OCaml? Haskell? Scala?
    1.53 +
    1.54 +end

     2.1 --- a/src/HOL/Codegenerator_Test/ROOT.ML	Tue Jul 31 13:55:39 2012 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/ROOT.ML	Tue Jul 31 13:55:39 2012 +0200
     2.3 @@ -1,1 +1,1 @@
     2.4 -use_thys ["Generate", "Generate_Pretty"];
     2.5 +use_thys ["Generate", "Generate_Pretty", "RBT_Set_Test"];

     3.1 --- a/src/HOL/ROOT	Tue Jul 31 13:55:39 2012 +0200
     3.2 +++ b/src/HOL/ROOT	Tue Jul 31 13:55:39 2012 +0200
     3.3 @@ -153,7 +153,7 @@
     3.4  
     3.5  session Codegenerator_Test = "HOL-Library" +
     3.6    options [document = false, document_graph = false, browser_info = false]
     3.7 -  theories Generate Generate_Pretty
     3.8 +  theories Generate Generate_Pretty RBT_Set_Test
     3.9  
    3.10  session Metis_Examples = HOL +
    3.11    description {*