src/HOL/Codegenerator_Test/RBT_Set_Test.thy
author kuncar
Tue Jul 31 13:55:39 2012 +0200 (2012-07-31)
changeset 48624 9b71daba4ec7
child 49948 744934b818c7
permissions -rw-r--r--
add testing file for RBT_Set
kuncar@48624
     1
(*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
kuncar@48624
     2
    Author:     Ondrej Kuncar
kuncar@48624
     3
*)
kuncar@48624
     4
kuncar@48624
     5
header {* Test of the code generator using an implementation of sets by RBT trees *}
kuncar@48624
     6
kuncar@48624
     7
theory RBT_Set_Test
kuncar@48624
     8
imports Library "~~/src/HOL/Library/RBT_Set"
kuncar@48624
     9
begin
kuncar@48624
    10
kuncar@48624
    11
(* 
kuncar@48624
    12
   The following code equations have to be deleted because they use 
kuncar@48624
    13
   lists to implement sets in the code generetor. 
kuncar@48624
    14
*)
kuncar@48624
    15
kuncar@48624
    16
lemma [code, code del]:
kuncar@48624
    17
  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
kuncar@48624
    18
kuncar@48624
    19
lemma [code, code del]:
kuncar@48624
    20
  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
kuncar@48624
    21
kuncar@48624
    22
lemma [code, code del]:
kuncar@48624
    23
  "pred_of_set = pred_of_set" ..
kuncar@48624
    24
kuncar@48624
    25
kuncar@48624
    26
lemma [code, code del]:
kuncar@48624
    27
  "Cardinality.card' = Cardinality.card'" ..
kuncar@48624
    28
kuncar@48624
    29
lemma [code, code del]:
kuncar@48624
    30
  "Cardinality.finite' = Cardinality.finite'" ..
kuncar@48624
    31
kuncar@48624
    32
lemma [code, code del]:
kuncar@48624
    33
  "Cardinality.subset' = Cardinality.subset'" ..
kuncar@48624
    34
kuncar@48624
    35
lemma [code, code del]:
kuncar@48624
    36
  "Cardinality.eq_set = Cardinality.eq_set" ..
kuncar@48624
    37
kuncar@48624
    38
kuncar@48624
    39
lemma [code, code del]:
kuncar@48624
    40
  "acc = acc" ..
kuncar@48624
    41
kuncar@48624
    42
(*
kuncar@48624
    43
  If the code generation ends with an exception with the following message:
kuncar@48624
    44
  '"List.set" is not a constructor, on left hand side of equation: ...',
kuncar@48624
    45
  the code equation in question has to be either deleted (like many others in this file) 
kuncar@48624
    46
  or implemented for RBT trees.
kuncar@48624
    47
*)
kuncar@48624
    48
kuncar@48624
    49
export_code _ checking SML OCaml? Haskell? Scala?
kuncar@48624
    50
kuncar@48624
    51
end