src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
author haftmann
Thu Feb 05 19:44:14 2015 +0100 (2015-02-05)
changeset 59484 a130ae7a9398
parent 58889 5b7a9633cfa8
child 59842 9fda99b3d5ee
permissions -rw-r--r--
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
     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 let
    16   val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
    17   val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
    18     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    19 in fold Code.del_eqns consts end
    20 \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    21 
    22 (* 
    23    The following code equations have to be deleted because they use 
    24    lists to implement sets in the code generetor. 
    25 *)
    26 
    27 lemma [code, code del]:
    28   "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    29 
    30 lemma [code, code del]:
    31   "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    32 
    33 lemma [code, code del]:
    34   "pred_of_set = pred_of_set" ..
    35 
    36 lemma [code, code del]:
    37   "Wellfounded.acc = Wellfounded.acc" ..
    38 
    39 lemma [code, code del]:
    40   "Cardinality.card' = Cardinality.card'" ..
    41 
    42 lemma [code, code del]:
    43   "Cardinality.finite' = Cardinality.finite'" ..
    44 
    45 lemma [code, code del]:
    46   "Cardinality.subset' = Cardinality.subset'" ..
    47 
    48 lemma [code, code del]:
    49   "Cardinality.eq_set = Cardinality.eq_set" ..
    50 
    51 lemma [code, code del]:
    52   "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
    53 
    54 lemma [code, code del]:
    55   "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
    56 
    57 lemma [code, code del]:
    58   "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
    59 
    60 lemma [code, code del]:
    61   "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
    62   
    63 (*
    64   If the code generation ends with an exception with the following message:
    65   '"List.set" is not a constructor, on left hand side of equation: ...',
    66   the code equation in question has to be either deleted (like many others in this file) 
    67   or implemented for RBT trees.
    68 *)
    69 
    70 export_code _ checking SML OCaml? Haskell?
    71 
    72 (* Extra setup to make Scala happy *)
    73 (* If the compilation fails with an error "ambiguous implicit values",
    74    read \<section>7.1 in the Code Generation Manual *)
    75 
    76 lemma [code]:
    77   "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    78 unfolding gfp_def by blast
    79 
    80 lemma [code]:
    81   "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    82 unfolding lfp_def by blast
    83 
    84 export_code _ checking Scala?
    85 
    86 end