src/HOL/Codegenerator_Test/Candidates.thy
 author haftmann Wed Nov 07 11:08:12 2018 +0000 (8 months ago) changeset 69252 fc359b60121c parent 68484 59793df7f853 child 69597 ff784d5a5bfb permissions -rw-r--r--
dedicated examples for sorting
```     1
```
```     2 (* Author: Florian Haftmann, TU Muenchen *)
```
```     3
```
```     4 section \<open>A huge collection of equations to generate code from\<close>
```
```     5
```
```     6 theory Candidates
```
```     7 imports
```
```     8   Complex_Main
```
```     9   "HOL-Library.Library"
```
```    10   "HOL-Library.Sorting_Algorithms"
```
```    11   "HOL-Library.Subseq_Order"
```
```    12   "HOL-Library.RBT"
```
```    13   "HOL-Data_Structures.Tree_Map"
```
```    14   "HOL-Data_Structures.Tree_Set"
```
```    15   "HOL-Computational_Algebra.Computational_Algebra"
```
```    16   "HOL-Computational_Algebra.Polynomial_Factorial"
```
```    17   "HOL-Number_Theory.Eratosthenes"
```
```    18   "HOL-ex.Records"
```
```    19 begin
```
```    20
```
```    21 text \<open>Drop technical stuff from @{theory HOL.Quickcheck_Narrowing} which is tailored towards Haskell\<close>
```
```    22
```
```    23 setup \<open>
```
```    24 fn thy =>
```
```    25 let
```
```    26   val tycos = Sign.logical_types thy;
```
```    27   val consts = map_filter (try (curry (Axclass.param_of_inst thy)
```
```    28     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
```
```    29 in fold Code.declare_unimplemented_global consts thy end
```
```    30 \<close>
```
```    31
```
```    32 text \<open>Simple example for the predicate compiler.\<close>
```
```    33
```
```    34 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
```
```    35 where
```
```    36   empty: "sublist [] xs"
```
```    37 | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
```
```    38 | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
```
```    39
```
```    40 code_pred sublist .
```
```    41
```
```    42 text \<open>Avoid popular infix.\<close>
```
```    43
```
```    44 code_reserved SML upto
```
```    45
```
```    46 text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close>
```
```    47
```
```    48 definition funny_list :: "bool list"
```
```    49 where
```
```    50   "funny_list = [let b = True in b, False]"
```
```    51
```
```    52 definition funny_list' :: "bool list"
```
```    53 where
```
```    54   "funny_list' = funny_list"
```
```    55
```
```    56 lemma [code]:
```
```    57   "funny_list' = [True, False]"
```
```    58   by (simp add: funny_list_def funny_list'_def)
```
```    59
```
```    60 definition check_list :: unit
```
```    61 where
```
```    62   "check_list = (if funny_list = funny_list' then () else undefined)"
```
```    63
```
```    64 text \<open>Explicit check in \<open>Scala\<close> for correct bracketing of abstractions\<close>
```
```    65
```
```    66 definition funny_funs :: "(bool \<Rightarrow> bool) list \<Rightarrow> (bool \<Rightarrow> bool) list"
```
```    67 where
```
```    68   "funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs"
```
```    69
```
```    70 end
```