| author | Manuel Eberl <manuel@pruvisto.org> |
| Tue, 22 Apr 2025 19:02:33 +0200 | |
| changeset 82537 | 3dfd62b4e2c8 |
| parent 75804 | dd04e81172a8 |
| 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 |
|
| 63167 | 4 |
section \<open>Pervasive test of code generator\<close> |
| 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 |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66404
diff
changeset
|
9 |
"HOL-Library.DAList_Multiset" |
|
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66404
diff
changeset
|
10 |
"HOL-Library.RBT_Mapping" |
|
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66404
diff
changeset
|
11 |
"HOL-Library.RBT_Set" |
| 48624 | 12 |
begin |
13 |
||
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
14 |
text \<open> |
|
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
15 |
The following code equations have to be deleted because they use |
|
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
16 |
lists to implement sets in the code generetor. |
|
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
17 |
\<close> |
|
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
|
18 |
|
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
19 |
declare [[code drop: |
| 66016 | 20 |
"Inf :: _ Predicate.pred set \<Rightarrow> _" |
21 |
"Sup :: _ Predicate.pred set \<Rightarrow> _" |
|
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
22 |
pred_of_set |
|
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
23 |
Wellfounded.acc |
|
73886
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
73477
diff
changeset
|
24 |
Code_Cardinality.card' |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
73477
diff
changeset
|
25 |
Code_Cardinality.finite' |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
73477
diff
changeset
|
26 |
Code_Cardinality.subset' |
|
93ba8e3fdcdf
move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents:
73477
diff
changeset
|
27 |
Code_Cardinality.eq_set |
| 66016 | 28 |
Euclidean_Algorithm.Gcd |
29 |
Euclidean_Algorithm.Lcm |
|
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
30 |
"Gcd :: _ poly set \<Rightarrow> _" |
|
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
31 |
"Lcm :: _ poly set \<Rightarrow> _" |
|
75804
dd04e81172a8
nlists is picked up automatically but conflicts with the RBT setup
nipkow
parents:
73886
diff
changeset
|
32 |
nlists |
|
82537
3dfd62b4e2c8
dropped problematic code equation for multisets for RBT code testing
Manuel Eberl <manuel@pruvisto.org>
parents:
75804
diff
changeset
|
33 |
Multiset.multisets_of_size |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
63965
diff
changeset
|
34 |
]] |
|
63965
d510b816ea41
Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
35 |
|
| 66016 | 36 |
text \<open> |
37 |
If code generation fails with a message like |
|
| 67226 | 38 |
\<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>, |
| 73477 | 39 |
feel free to add an RBT implementation for the corresponding operation |
40 |
or delete that code equation (see above). |
|
| 66016 | 41 |
\<close> |
| 73477 | 42 |
|
| 65919 | 43 |
export_code _ checking SML OCaml? Haskell? Scala |
| 48624 | 44 |
|
45 |
end |