src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
author wenzelm
Sun Mar 29 19:32:27 2015 +0200 (2015-03-29)
changeset 59842 9fda99b3d5ee
parent 59484 a130ae7a9398
child 62429 25271ff79171
permissions -rw-r--r--
tuned;
     1 
     2 (* Author: Ondrej Kuncar, TU Muenchen *)
     3 
     4 section {* Pervasive test of code generator *}
     5 
     6 theory Generate_Efficient_Datastructures
     7 imports
     8   Candidates
     9   "~~/src/HOL/Library/DAList_Multiset"
    10   "~~/src/HOL/Library/RBT_Mapping"
    11   "~~/src/HOL/Library/RBT_Set"
    12 begin
    13 
    14 setup \<open>
    15 fn thy =>
    16 let
    17   val tycos = Sign.logical_types thy;
    18   val consts = map_filter (try (curry (Axclass.param_of_inst thy)
    19     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    20 in fold Code.del_eqns consts thy end
    21 \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    22 
    23 (* 
    24    The following code equations have to be deleted because they use 
    25    lists to implement sets in the code generetor. 
    26 *)
    27 
    28 lemma [code, code del]:
    29   "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    30 
    31 lemma [code, code del]:
    32   "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    33 
    34 lemma [code, code del]:
    35   "pred_of_set = pred_of_set" ..
    36 
    37 lemma [code, code del]:
    38   "Wellfounded.acc = Wellfounded.acc" ..
    39 
    40 lemma [code, code del]:
    41   "Cardinality.card' = Cardinality.card'" ..
    42 
    43 lemma [code, code del]:
    44   "Cardinality.finite' = Cardinality.finite'" ..
    45 
    46 lemma [code, code del]:
    47   "Cardinality.subset' = Cardinality.subset'" ..
    48 
    49 lemma [code, code del]:
    50   "Cardinality.eq_set = Cardinality.eq_set" ..
    51 
    52 lemma [code, code del]:
    53   "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
    54 
    55 lemma [code, code del]:
    56   "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
    57 
    58 lemma [code, code del]:
    59   "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
    60 
    61 lemma [code, code del]:
    62   "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
    63   
    64 (*
    65   If the code generation ends with an exception with the following message:
    66   '"List.set" is not a constructor, on left hand side of equation: ...',
    67   the code equation in question has to be either deleted (like many others in this file) 
    68   or implemented for RBT trees.
    69 *)
    70 
    71 export_code _ checking SML OCaml? Haskell?
    72 
    73 (* Extra setup to make Scala happy *)
    74 (* If the compilation fails with an error "ambiguous implicit values",
    75    read \<section>7.1 in the Code Generation Manual *)
    76 
    77 lemma [code]:
    78   "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    79 unfolding gfp_def by blast
    80 
    81 lemma [code]:
    82   "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    83 unfolding lfp_def by blast
    84 
    85 export_code _ checking Scala?
    86 
    87 end