src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
author haftmann
Fri Nov 15 22:02:01 2013 +0100 (2013-11-15)
changeset 54437 0060957404c7
parent 54295 45a5523d4a63
child 58889 5b7a9633cfa8
permissions -rw-r--r--
proper code equations for Gcd and Lcm on nat and int
     1 
     2 (* Author: Ondrej Kuncar, TU Muenchen *)
     3 
     4 header {* 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 (* 
    15    The following code equations have to be deleted because they use 
    16    lists to implement sets in the code generetor. 
    17 *)
    18 
    19 lemma [code, code del]:
    20   "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    21 
    22 lemma [code, code del]:
    23   "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    24 
    25 lemma [code, code del]:
    26   "pred_of_set = pred_of_set" ..
    27 
    28 lemma [code, code del]:
    29   "Wellfounded.acc = Wellfounded.acc" ..
    30 
    31 lemma [code, code del]:
    32   "Cardinality.card' = Cardinality.card'" ..
    33 
    34 lemma [code, code del]:
    35   "Cardinality.finite' = Cardinality.finite'" ..
    36 
    37 lemma [code, code del]:
    38   "Cardinality.subset' = Cardinality.subset'" ..
    39 
    40 lemma [code, code del]:
    41   "Cardinality.eq_set = Cardinality.eq_set" ..
    42 
    43 lemma [code, code del]:
    44   "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
    45 
    46 lemma [code, code del]:
    47   "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
    48 
    49 lemma [code, code del]:
    50   "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
    51 
    52 lemma [code, code del]:
    53   "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
    54   
    55 (*
    56   If the code generation ends with an exception with the following message:
    57   '"List.set" is not a constructor, on left hand side of equation: ...',
    58   the code equation in question has to be either deleted (like many others in this file) 
    59   or implemented for RBT trees.
    60 *)
    61 
    62 export_code _ checking SML OCaml? Haskell?
    63 
    64 (* Extra setup to make Scala happy *)
    65 (* If the compilation fails with an error "ambiguous implicit values",
    66    read \<section>7.1 in the Code Generation Manual *)
    67 
    68 lemma [code]:
    69   "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    70 unfolding gfp_def by blast
    71 
    72 lemma [code]:
    73   "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    74 unfolding lfp_def by blast
    75 
    76 export_code _ checking Scala?
    77 
    78 end