isabelle: src/Tools/Code_Generator.thy@f8da913b6c3a (annotated)

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
33889 4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile; wenzelm parents: 33820 diff changeset	10	"~~/src/Tools/auto_solve.ML"
33820 082d9bc6992d load ML directly into theory Code_Generator (quickcheck also requires this); wenzelm parents: 33561 diff changeset	11	"~~/src/Tools/auto_counterexample.ML"
33889 4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile; wenzelm parents: 33820 diff 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 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	14	"~~/src/Tools/Code/code_preproc.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	15	"~~/src/Tools/Code/code_thingol.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	16	"~~/src/Tools/Code/code_printer.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	17	"~~/src/Tools/Code/code_target.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	18	"~~/src/Tools/Code/code_ml.ML"
34028 1e6206763036 split off evaluation mechanisms in separte module Code_Eval haftmann parents: 33889 diff changeset	19	"~~/src/Tools/Code/code_eval.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	20	"~~/src/Tools/Code/code_haskell.ML"
34294 19c1fd52d6c9 a primitive scala serializer haftmann parents: 34028 diff changeset	21	"~~/src/Tools/Code/code_scala.ML"
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	22	"~~/src/Tools/nbe.ML"
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	23	begin
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	24
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	25	setup {*
31125 80218ee73167 transferred code generator preprocessor into separate module haftmann parents: 31036 diff changeset	26	Code_Preproc.setup
80218ee73167 transferred code generator preprocessor into separate module haftmann parents: 31036 diff changeset	27	#> Code_ML.setup
34028 1e6206763036 split off evaluation mechanisms in separte module Code_Eval haftmann parents: 33889 diff changeset	28	#> Code_Eval.setup
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	29	#> Code_Haskell.setup
34294 19c1fd52d6c9 a primitive scala serializer haftmann parents: 34028 diff changeset	30	#> Code_Scala.setup
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	31	#> Nbe.setup
34968 ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy haftmann parents: 34294 diff changeset	32	#> Quickcheck.setup
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	33	*}
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	34
33561 ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck; blanchet parents: 31775 diff changeset	35	end

author	blanchet
	Wed, 28 Apr 2010 18:11:11 +0200
changeset 36550	f8da913b6c3a
parent 34968	ceeffca32eb0
child 37442	037ee7b712b2
permissions	-rw-r--r--