src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
author haftmann
Sun Nov 10 15:05:06 2013 +0100 (2013-11-10)
changeset 54295 45a5523d4a63
parent 53361 1cb7d3c0cf31
child 54437 0060957404c7
permissions -rw-r--r--
qualifed popular user space names
haftmann@51161
     1
haftmann@51161
     2
(* Author: Ondrej Kuncar, TU Muenchen *)
haftmann@51161
     3
haftmann@51161
     4
header {* Pervasive test of code generator *}
kuncar@48624
     5
haftmann@51161
     6
theory Generate_Efficient_Datastructures
haftmann@51161
     7
imports
haftmann@51161
     8
  Candidates
haftmann@51599
     9
  "~~/src/HOL/Library/DAList_Multiset"
haftmann@51161
    10
  "~~/src/HOL/Library/RBT_Mapping"
haftmann@51161
    11
  "~~/src/HOL/Library/RBT_Set"
kuncar@48624
    12
begin
kuncar@48624
    13
kuncar@48624
    14
(* 
kuncar@48624
    15
   The following code equations have to be deleted because they use 
kuncar@48624
    16
   lists to implement sets in the code generetor. 
kuncar@48624
    17
*)
kuncar@48624
    18
kuncar@48624
    19
lemma [code, code del]:
kuncar@48624
    20
  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
kuncar@48624
    21
kuncar@48624
    22
lemma [code, code del]:
kuncar@48624
    23
  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
kuncar@48624
    24
kuncar@48624
    25
lemma [code, code del]:
kuncar@48624
    26
  "pred_of_set = pred_of_set" ..
kuncar@48624
    27
kuncar@48624
    28
lemma [code, code del]:
haftmann@54295
    29
  "Wellfounded.acc = Wellfounded.acc" ..
kuncar@48624
    30
Andreas@51139
    31
lemma [code, code del]:
Andreas@51139
    32
  "Cardinality.card' = Cardinality.card'" ..
Andreas@51139
    33
Andreas@51139
    34
lemma [code, code del]:
Andreas@51139
    35
  "Cardinality.finite' = Cardinality.finite'" ..
Andreas@51139
    36
Andreas@51139
    37
lemma [code, code del]:
Andreas@51139
    38
  "Cardinality.subset' = Cardinality.subset'" ..
Andreas@51139
    39
Andreas@51139
    40
lemma [code, code del]:
Andreas@51139
    41
  "Cardinality.eq_set = Cardinality.eq_set" ..
Andreas@51116
    42
kuncar@48624
    43
(*
kuncar@48624
    44
  If the code generation ends with an exception with the following message:
kuncar@48624
    45
  '"List.set" is not a constructor, on left hand side of equation: ...',
kuncar@48624
    46
  the code equation in question has to be either deleted (like many others in this file) 
kuncar@48624
    47
  or implemented for RBT trees.
kuncar@48624
    48
*)
kuncar@48624
    49
kuncar@50996
    50
export_code _ checking SML OCaml? Haskell?
kuncar@50996
    51
kuncar@50996
    52
(* Extra setup to make Scala happy *)
kuncar@50996
    53
(* If the compilation fails with an error "ambiguous implicit values",
kuncar@50996
    54
   read \<section>7.1 in the Code Generation Manual *)
kuncar@50996
    55
kuncar@50996
    56
lemma [code]:
kuncar@50996
    57
  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
kuncar@50996
    58
unfolding gfp_def by blast
kuncar@50996
    59
kuncar@50996
    60
lemma [code]:
kuncar@50996
    61
  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
kuncar@50996
    62
unfolding lfp_def by blast
kuncar@50996
    63
kuncar@50996
    64
export_code _ checking Scala?
kuncar@48624
    65
kuncar@48624
    66
end