author | eberlm <eberlm@in.tum.de> |
Tue, 16 Aug 2016 12:02:09 +0200 | |
changeset 63704 | 6209c06d776f |
parent 63503 | 6c644d547db7 |
child 65417 | fc41a5650fb1 |
permissions | -rw-r--r-- |
31378 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
21917 | 3 |
|
63167 | 4 |
section \<open>A huge collection of equations to generate code from\<close> |
21917 | 5 |
|
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37407
diff
changeset
|
6 |
theory Candidates |
21917 | 7 |
imports |
27421 | 8 |
Complex_Main |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
49077
diff
changeset
|
9 |
"~~/src/HOL/Library/Library" |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
10 |
"~~/src/HOL/Library/Sublist_Order" |
62425 | 11 |
"~~/src/HOL/Number_Theory/Euclidean_Algorithm" |
63704 | 12 |
"~~/src/HOL/Library/Polynomial_Factorial" |
61227
19ee25fe9737
include some data structures into code generation
haftmann
parents:
61130
diff
changeset
|
13 |
"~~/src/HOL/Data_Structures/Tree_Map" |
19ee25fe9737
include some data structures into code generation
haftmann
parents:
61130
diff
changeset
|
14 |
"~~/src/HOL/Data_Structures/Tree_Set" |
51173 | 15 |
"~~/src/HOL/Number_Theory/Eratosthenes" |
35303 | 16 |
"~~/src/HOL/ex/Records" |
21917 | 17 |
begin |
18 |
||
61129
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
19 |
text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close> |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
20 |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
21 |
setup \<open> |
59842 | 22 |
fn thy => |
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
23 |
let |
59842 | 24 |
val tycos = Sign.logical_types thy; |
25 |
val consts = map_filter (try (curry (Axclass.param_of_inst thy) |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
26 |
@{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos; |
59842 | 27 |
in fold Code.del_eqns consts thy end |
61129
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
28 |
\<close> |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
29 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
30 |
text \<open>Simple example for the predicate compiler.\<close> |
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
31 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
32 |
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
33 |
where |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
34 |
empty: "sublist [] xs" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
35 |
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
36 |
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" |
33500 | 37 |
|
38 |
code_pred sublist . |
|
39 |
||
61129
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
40 |
text \<open>Avoid popular infix.\<close> |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
41 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
42 |
code_reserved SML upto |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
43 |
|
63167 | 44 |
text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close> |
61129
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
45 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
46 |
definition funny_list :: "bool list" |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
47 |
where |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
48 |
"funny_list = [let b = True in b, False]" |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
49 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
50 |
definition funny_list' :: "bool list" |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
51 |
where |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
52 |
"funny_list' = funny_list" |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
53 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
54 |
lemma [code]: |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
55 |
"funny_list' = [True, False]" |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
56 |
by (simp add: funny_list_def funny_list'_def) |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
57 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
58 |
definition check_list :: unit |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
59 |
where |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
60 |
"check_list = (if funny_list = funny_list' then () else undefined)" |
31378 | 61 |
|
63167 | 62 |
text \<open>Explicit check in \<open>Scala\<close> for correct bracketing of abstractions\<close> |
61130
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
63 |
|
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
64 |
definition funny_funs :: "(bool \<Rightarrow> bool) list \<Rightarrow> (bool \<Rightarrow> bool) list" |
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
65 |
where |
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
66 |
"funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs" |
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
67 |
|
21917 | 68 |
end |