src/HOL/Codegenerator_Test/RBT_Set_Test.thy
author Andreas Lochbihler
Fri Feb 15 09:41:25 2013 +0100 (2013-02-15)
changeset 51139 c8e3cf3520b3
parent 51116 0dac0158b8d4
permissions -rw-r--r--
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
provide better error messages instead for card and subseteq
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
haftmann@49948
     8
imports "~~/src/HOL/Library/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
lemma [code, code del]:
kuncar@48624
    26
  "acc = acc" ..
kuncar@48624
    27
Andreas@51139
    28
lemma [code, code del]:
Andreas@51139
    29
  "Cardinality.card' = Cardinality.card'" ..
Andreas@51139
    30
Andreas@51139
    31
lemma [code, code del]:
Andreas@51139
    32
  "Cardinality.finite' = Cardinality.finite'" ..
Andreas@51139
    33
Andreas@51139
    34
lemma [code, code del]:
Andreas@51139
    35
  "Cardinality.subset' = Cardinality.subset'" ..
Andreas@51139
    36
Andreas@51139
    37
lemma [code, code del]:
Andreas@51139
    38
  "Cardinality.eq_set = Cardinality.eq_set" ..
Andreas@51116
    39
kuncar@48624
    40
(*
kuncar@48624
    41
  If the code generation ends with an exception with the following message:
kuncar@48624
    42
  '"List.set" is not a constructor, on left hand side of equation: ...',
kuncar@48624
    43
  the code equation in question has to be either deleted (like many others in this file) 
kuncar@48624
    44
  or implemented for RBT trees.
kuncar@48624
    45
*)
kuncar@48624
    46
kuncar@50996
    47
export_code _ checking SML OCaml? Haskell?
kuncar@50996
    48
kuncar@50996
    49
(* Extra setup to make Scala happy *)
kuncar@50996
    50
(* If the compilation fails with an error "ambiguous implicit values",
kuncar@50996
    51
   read \<section>7.1 in the Code Generation Manual *)
kuncar@50996
    52
kuncar@50996
    53
class ccpo_linorder = ccpo + linorder
kuncar@50996
    54
kuncar@50996
    55
lemma [code]:
kuncar@50996
    56
  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
kuncar@50996
    57
    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
kuncar@50996
    58
unfolding admissible_def by blast
kuncar@50996
    59
kuncar@50996
    60
lemma [code]:
kuncar@50996
    61
  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
kuncar@50996
    62
unfolding gfp_def by blast
kuncar@50996
    63
kuncar@50996
    64
lemma [code]:
kuncar@50996
    65
  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
kuncar@50996
    66
unfolding lfp_def by blast
kuncar@50996
    67
kuncar@50996
    68
export_code _ checking Scala?
kuncar@48624
    69
kuncar@48624
    70
end