| author | wenzelm | 
| Tue, 24 Nov 2009 17:19:33 +0100 | |
| changeset 33889 | 4328de748fb2 | 
| parent 33820 | 082d9bc6992d | 
| child 34028 | 1e6206763036 | 
| 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: 
33561diff
changeset | 8 | imports Pure | 
| 30929 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 9 | uses | 
| 33889 
4328de748fb2
some rearangement of load order to keep preferences adjacent -- slightly fragile;
 wenzelm parents: 
33820diff
changeset | 10 | "~~/src/Tools/auto_solve.ML" | 
| 33820 
082d9bc6992d
load ML directly into theory Code_Generator (quickcheck also requires this);
 wenzelm parents: 
33561diff
changeset | 11 | "~~/src/Tools/auto_counterexample.ML" | 
| 33889 
4328de748fb2
some rearangement of load order to keep preferences adjacent -- slightly fragile;
 wenzelm parents: 
33820diff
changeset | 12 | "~~/src/Tools/quickcheck.ML" | 
| 30929 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 13 | "~~/src/Tools/value.ML" | 
| 31775 | 14 | "~~/src/Tools/Code/code_preproc.ML" | 
| 15 | "~~/src/Tools/Code/code_thingol.ML" | |
| 16 | "~~/src/Tools/Code/code_printer.ML" | |
| 17 | "~~/src/Tools/Code/code_target.ML" | |
| 18 | "~~/src/Tools/Code/code_ml.ML" | |
| 19 | "~~/src/Tools/Code/code_haskell.ML" | |
| 30929 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 20 | "~~/src/Tools/nbe.ML" | 
| 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 21 | begin | 
| 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 22 | |
| 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 23 | setup {*
 | 
| 31125 
80218ee73167
transferred code generator preprocessor into separate module
 haftmann parents: 
31036diff
changeset | 24 | Code_Preproc.setup | 
| 
80218ee73167
transferred code generator preprocessor into separate module
 haftmann parents: 
31036diff
changeset | 25 | #> Code_ML.setup | 
| 30929 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 26 | #> Code_Haskell.setup | 
| 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 27 | #> Nbe.setup | 
| 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 28 | *} | 
| 
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
 haftmann parents: diff
changeset | 29 | |
| 33561 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
 blanchet parents: 
31775diff
changeset | 30 | end |