author | haftmann |
Thu, 05 Feb 2015 19:44:14 +0100 | |
changeset 59484 | a130ae7a9398 |
parent 58889 | 5b7a9633cfa8 |
child 59842 | 9fda99b3d5ee |
permissions | -rw-r--r-- |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
1 |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
2 |
(* Author: Ondrej Kuncar, TU Muenchen *) |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
3 |
|
58889 | 4 |
section {* Pervasive test of code generator *} |
48624 | 5 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
6 |
theory Generate_Efficient_Datastructures |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
7 |
imports |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
8 |
Candidates |
51599
1559e9266280
optionalized very specific code setup for multisets
haftmann
parents:
51161
diff
changeset
|
9 |
"~~/src/HOL/Library/DAList_Multiset" |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
10 |
"~~/src/HOL/Library/RBT_Mapping" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51139
diff
changeset
|
11 |
"~~/src/HOL/Library/RBT_Set" |
48624 | 12 |
begin |
13 |
||
59484
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
14 |
setup \<open> |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
15 |
let |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
16 |
val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory}; |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
17 |
val consts = map_filter (try (curry (Axclass.param_of_inst @{theory}) |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
18 |
@{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos; |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
19 |
in fold Code.del_eqns consts end |
a130ae7a9398
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents:
58889
diff
changeset
|
20 |
\<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
|
21 |
|
48624 | 22 |
(* |
23 |
The following code equations have to be deleted because they use |
|
24 |
lists to implement sets in the code generetor. |
|
25 |
*) |
|
26 |
||
27 |
lemma [code, code del]: |
|
28 |
"Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" .. |
|
29 |
||
30 |
lemma [code, code del]: |
|
31 |
"Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. |
|
32 |
||
33 |
lemma [code, code del]: |
|
34 |
"pred_of_set = pred_of_set" .. |
|
35 |
||
36 |
lemma [code, code del]: |
|
54295 | 37 |
"Wellfounded.acc = Wellfounded.acc" .. |
48624 | 38 |
|
51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
39 |
lemma [code, code del]: |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
40 |
"Cardinality.card' = Cardinality.card'" .. |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
41 |
|
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
42 |
lemma [code, code del]: |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
43 |
"Cardinality.finite' = Cardinality.finite'" .. |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
44 |
|
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
45 |
lemma [code, code del]: |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
46 |
"Cardinality.subset' = Cardinality.subset'" .. |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
47 |
|
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
48 |
lemma [code, code del]: |
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset
|
49 |
"Cardinality.eq_set = Cardinality.eq_set" .. |
51116
0dac0158b8d4
implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug
Andreas Lochbihler
parents:
50996
diff
changeset
|
50 |
|
54437
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
51 |
lemma [code, code del]: |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
52 |
"(Gcd :: nat set \<Rightarrow> nat) = Gcd" .. |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
53 |
|
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
54 |
lemma [code, code del]: |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
55 |
"(Lcm :: nat set \<Rightarrow> nat) = Lcm" .. |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
56 |
|
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
57 |
lemma [code, code del]: |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
58 |
"(Gcd :: int set \<Rightarrow> int) = Gcd" .. |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
59 |
|
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
60 |
lemma [code, code del]: |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
61 |
"(Lcm :: int set \<Rightarrow> int) = Lcm" .. |
0060957404c7
proper code equations for Gcd and Lcm on nat and int
haftmann
parents:
54295
diff
changeset
|
62 |
|
48624 | 63 |
(* |
64 |
If the code generation ends with an exception with the following message: |
|
65 |
'"List.set" is not a constructor, on left hand side of equation: ...', |
|
66 |
the code equation in question has to be either deleted (like many others in this file) |
|
67 |
or implemented for RBT trees. |
|
68 |
*) |
|
69 |
||
50996
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
70 |
export_code _ checking SML OCaml? Haskell? |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
71 |
|
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
72 |
(* Extra setup to make Scala happy *) |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
73 |
(* If the compilation fails with an error "ambiguous implicit values", |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
74 |
read \<section>7.1 in the Code Generation Manual *) |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
75 |
|
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
76 |
lemma [code]: |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
77 |
"(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}" |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
78 |
unfolding gfp_def by blast |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
79 |
|
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
80 |
lemma [code]: |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
81 |
"(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}" |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
82 |
unfolding lfp_def by blast |
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
83 |
|
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset
|
84 |
export_code _ checking Scala? |
48624 | 85 |
|
86 |
end |