| author | wenzelm |
| Mon, 01 Jun 2015 13:35:16 +0200 | |
| changeset 60328 | 9c94e6a30d29 |
| parent 59842 | 9fda99b3d5ee |
| child 61129 | 774752af4a1f |
| permissions | -rw-r--r-- |
| 31378 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
| 21917 | 3 |
|
| 58889 | 4 |
section {* A huge collection of equations to generate code from *}
|
| 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" |
| 51173 | 11 |
"~~/src/HOL/Number_Theory/Eratosthenes" |
| 35303 | 12 |
"~~/src/HOL/ex/Records" |
| 21917 | 13 |
begin |
14 |
||
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
15 |
setup \<open> |
| 59842 | 16 |
fn thy => |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
17 |
let |
| 59842 | 18 |
val tycos = Sign.logical_types thy; |
19 |
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
|
20 |
@{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
|
| 59842 | 21 |
in fold Code.del_eqns consts thy end |
|
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
22 |
\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
|
|
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
23 |
|
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
24 |
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
|
25 |
where |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
26 |
empty: "sublist [] xs" |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
27 |
| 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
|
28 |
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" |
| 33500 | 29 |
|
30 |
code_pred sublist . |
|
31 |
||
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
32 |
code_reserved SML upto -- {* avoid popular infix *}
|
| 31378 | 33 |
|
| 21917 | 34 |
end |