src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
author Manuel Eberl <eberlm@in.tum.de>
Fri Feb 26 22:15:09 2016 +0100 (2016-02-26)
changeset 62429 25271ff79171
parent 59842 9fda99b3d5ee
child 63132 8230358fab88
permissions -rw-r--r--
Tuned Euclidean Rings/GCD rings
haftmann@51161
     1
haftmann@51161
     2
(* Author: Ondrej Kuncar, TU Muenchen *)
haftmann@51161
     3
wenzelm@58889
     4
section {* 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
haftmann@59484
    14
setup \<open>
wenzelm@59842
    15
fn thy =>
haftmann@59484
    16
let
wenzelm@59842
    17
  val tycos = Sign.logical_types thy;
wenzelm@59842
    18
  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
haftmann@59484
    19
    @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
wenzelm@59842
    20
in fold Code.del_eqns consts thy end
haftmann@59484
    21
\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
haftmann@59484
    22
kuncar@48624
    23
(* 
kuncar@48624
    24
   The following code equations have to be deleted because they use 
kuncar@48624
    25
   lists to implement sets in the code generetor. 
kuncar@48624
    26
*)
kuncar@48624
    27
kuncar@48624
    28
lemma [code, code del]:
kuncar@48624
    29
  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
kuncar@48624
    30
kuncar@48624
    31
lemma [code, code del]:
kuncar@48624
    32
  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
kuncar@48624
    33
kuncar@48624
    34
lemma [code, code del]:
kuncar@48624
    35
  "pred_of_set = pred_of_set" ..
kuncar@48624
    36
kuncar@48624
    37
lemma [code, code del]:
haftmann@54295
    38
  "Wellfounded.acc = Wellfounded.acc" ..
kuncar@48624
    39
Andreas@51139
    40
lemma [code, code del]:
Andreas@51139
    41
  "Cardinality.card' = Cardinality.card'" ..
Andreas@51139
    42
Andreas@51139
    43
lemma [code, code del]:
Andreas@51139
    44
  "Cardinality.finite' = Cardinality.finite'" ..
Andreas@51139
    45
Andreas@51139
    46
lemma [code, code del]:
Andreas@51139
    47
  "Cardinality.subset' = Cardinality.subset'" ..
Andreas@51139
    48
Andreas@51139
    49
lemma [code, code del]:
Andreas@51139
    50
  "Cardinality.eq_set = Cardinality.eq_set" ..
Andreas@51116
    51
haftmann@54437
    52
lemma [code, code del]:
haftmann@54437
    53
  "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
haftmann@54437
    54
haftmann@54437
    55
lemma [code, code del]:
haftmann@54437
    56
  "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
haftmann@54437
    57
haftmann@54437
    58
lemma [code, code del]:
haftmann@54437
    59
  "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
haftmann@54437
    60
haftmann@54437
    61
lemma [code, code del]:
haftmann@54437
    62
  "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
eberlm@62429
    63
eberlm@62429
    64
lemma [code, code del]:
eberlm@62429
    65
  "(Gcd :: _ poly set \<Rightarrow> _) = Gcd" ..
eberlm@62429
    66
eberlm@62429
    67
lemma [code, code del]:
eberlm@62429
    68
  "(Lcm :: _ poly set \<Rightarrow> _) = Lcm" ..
eberlm@62429
    69
eberlm@62429
    70
lemma [code, code del]:
eberlm@62429
    71
  "Gcd_eucl = Gcd_eucl" ..
eberlm@62429
    72
eberlm@62429
    73
lemma [code, code del]:
eberlm@62429
    74
  "Lcm_eucl = Lcm_eucl" ..
eberlm@62429
    75
kuncar@48624
    76
(*
kuncar@48624
    77
  If the code generation ends with an exception with the following message:
kuncar@48624
    78
  '"List.set" is not a constructor, on left hand side of equation: ...',
kuncar@48624
    79
  the code equation in question has to be either deleted (like many others in this file) 
kuncar@48624
    80
  or implemented for RBT trees.
kuncar@48624
    81
*)
kuncar@48624
    82
kuncar@50996
    83
export_code _ checking SML OCaml? Haskell?
kuncar@50996
    84
kuncar@50996
    85
(* Extra setup to make Scala happy *)
kuncar@50996
    86
(* If the compilation fails with an error "ambiguous implicit values",
kuncar@50996
    87
   read \<section>7.1 in the Code Generation Manual *)
kuncar@50996
    88
kuncar@50996
    89
lemma [code]:
kuncar@50996
    90
  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
kuncar@50996
    91
unfolding gfp_def by blast
kuncar@50996
    92
kuncar@50996
    93
lemma [code]:
kuncar@50996
    94
  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
kuncar@50996
    95
unfolding lfp_def by blast
kuncar@50996
    96
kuncar@50996
    97
export_code _ checking Scala?
kuncar@48624
    98
kuncar@48624
    99
end