author | haftmann |
Thu, 02 Sep 2010 13:58:16 +0200 | |
changeset 39056 | fa197571676b |
parent 38970 | 53d1ee3d98b8 |
child 39323 | ce5c6a8b0359 |
permissions | -rw-r--r-- |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
1 |
(* Title: Tools/Code_Generator.thy |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
3 |
*) |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
4 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
5 |
header {* Loading the code generator modules *} |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
6 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
7 |
theory Code_Generator |
33820
082d9bc6992d
load ML directly into theory Code_Generator (quickcheck also requires this);
wenzelm
parents:
33561
diff
changeset
|
8 |
imports Pure |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
9 |
uses |
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37442
diff
changeset
|
10 |
"~~/src/Tools/cache_io.ML" |
33889
4328de748fb2
some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents:
33820
diff
changeset
|
11 |
"~~/src/Tools/auto_solve.ML" |
33820
082d9bc6992d
load ML directly into theory Code_Generator (quickcheck also requires this);
wenzelm
parents:
33561
diff
changeset
|
12 |
"~~/src/Tools/auto_counterexample.ML" |
33889
4328de748fb2
some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents:
33820
diff
changeset
|
13 |
"~~/src/Tools/quickcheck.ML" |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
14 |
"~~/src/Tools/value.ML" |
31775 | 15 |
"~~/src/Tools/Code/code_preproc.ML" |
16 |
"~~/src/Tools/Code/code_thingol.ML" |
|
37442 | 17 |
"~~/src/Tools/Code/code_simp.ML" |
31775 | 18 |
"~~/src/Tools/Code/code_printer.ML" |
19 |
"~~/src/Tools/Code/code_target.ML" |
|
38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
37818
diff
changeset
|
20 |
"~~/src/Tools/Code/code_namespace.ML" |
31775 | 21 |
"~~/src/Tools/Code/code_ml.ML" |
22 |
"~~/src/Tools/Code/code_haskell.ML" |
|
34294 | 23 |
"~~/src/Tools/Code/code_scala.ML" |
38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
37818
diff
changeset
|
24 |
"~~/src/Tools/Code/code_eval.ML" |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
25 |
"~~/src/Tools/nbe.ML" |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
26 |
begin |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
27 |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
28 |
setup {* |
31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
31036
diff
changeset
|
29 |
Code_Preproc.setup |
37442 | 30 |
#> Code_Simp.setup |
31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
31036
diff
changeset
|
31 |
#> Code_ML.setup |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
32 |
#> Code_Haskell.setup |
34294 | 33 |
#> Code_Scala.setup |
38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
37818
diff
changeset
|
34 |
#> Code_Eval.setup |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
35 |
#> Nbe.setup |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
34294
diff
changeset
|
36 |
#> Quickcheck.setup |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
37 |
*} |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
38 |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
31775
diff
changeset
|
39 |
end |