author | paulson <lp15@cam.ac.uk> |
Mon, 22 Apr 2024 22:08:28 +0100 | |
changeset 80142 | 34e0ddfc6dcc |
parent 75955 | 5305c65dcbb2 |
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 |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
9 |
"HOL-Library.Library" |
69252 | 10 |
"HOL-Library.Sorting_Algorithms" |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
11 |
"HOL-Library.Subseq_Order" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
12 |
"HOL-Library.RBT" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
13 |
"HOL-Data_Structures.Tree_Map" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
14 |
"HOL-Data_Structures.Tree_Set" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
15 |
"HOL-Computational_Algebra.Computational_Algebra" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
16 |
"HOL-Computational_Algebra.Polynomial_Factorial" |
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66251
diff
changeset
|
17 |
"HOL-Number_Theory.Eratosthenes" |
72029 | 18 |
"HOL-Examples.Records" |
75955 | 19 |
"HOL-Examples.Gauss_Numbers" |
21917 | 20 |
begin |
21 |
||
69597 | 22 |
text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close> |
61129
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
23 |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
24 |
setup \<open> |
59842 | 25 |
fn thy => |
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
26 |
let |
59842 | 27 |
val tycos = Sign.logical_types thy; |
28 |
val consts = map_filter (try (curry (Axclass.param_of_inst thy) |
|
69597 | 29 |
\<^const_name>\<open>Quickcheck_Narrowing.partial_term_of\<close>)) tycos; |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
66014
diff
changeset
|
30 |
in fold Code.declare_unimplemented_global 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
|
31 |
\<close> |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
32 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
33 |
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
|
34 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
35 |
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
|
36 |
where |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
37 |
empty: "sublist [] xs" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
38 |
| 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
|
39 |
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" |
33500 | 40 |
|
41 |
code_pred sublist . |
|
42 |
||
61129
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
43 |
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
|
44 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
45 |
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
|
46 |
|
63167 | 47 |
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
|
48 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
49 |
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
|
50 |
where |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
51 |
"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
|
52 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
53 |
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
|
54 |
where |
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' = funny_list" |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
56 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
57 |
lemma [code]: |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
58 |
"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
|
59 |
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
|
60 |
|
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
61 |
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
|
62 |
where |
774752af4a1f
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
haftmann
parents:
59842
diff
changeset
|
63 |
"check_list = (if funny_list = funny_list' then () else undefined)" |
31378 | 64 |
|
63167 | 65 |
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
|
66 |
|
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
67 |
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
|
68 |
where |
8e736ce4c6f4
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
haftmann
parents:
61129
diff
changeset
|
69 |
"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
|
70 |
|
75647
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
71 |
text \<open>Explicit checks for strings etc.\<close> |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
72 |
|
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
73 |
definition \<open>hello = ''Hello, world!''\<close> |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
74 |
|
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
75 |
definition \<open>hello2 = String.explode (String.implode hello)\<close> |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
76 |
|
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
77 |
definition \<open>which_hello \<longleftrightarrow> hello \<le> hello2\<close> |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
72515
diff
changeset
|
78 |
|
21917 | 79 |
end |