# 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 {*