isabelle: src/Tools/Code_Generator.thy@261f9de35b18 (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
39911 2b4430847310 moved ML_Context.value to Code_Runtime haftmann parents: 39474 diff changeset	5	header {* Loading the code generator and related modules *}
30929 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
46950 d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	9	keywords
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	10	"try" "solve_direct" "quickcheck" "value" "print_codeproc"
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	11	"code_thms" "code_deps" "export_code" :: diag and
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	12	"quickcheck_params" "code_class" "code_instance" "code_type"
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	13	"code_const" "code_reserved" "code_include" "code_modulename"
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	14	"code_abort" "code_monad" "code_reflect" :: thy_decl and
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	15	"datatypes" "functions" "module_name" "file" "checking"
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	16	uses
44121 44adaa6db327 old term operations are legacy; wenzelm parents: 44120 diff changeset	17	"~~/src/Tools/misc_legacy.ML"
37818 dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools haftmann parents: 37442 diff changeset	18	"~~/src/Tools/cache_io.ML"
43018 121aa59b4d17 renamed "Auto_Tools" "Try" blanchet parents: 40116 diff changeset	19	"~~/src/Tools/try.ML"
40116 9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct" blanchet parents: 39911 diff changeset	20	"~~/src/Tools/solve_direct.ML"
33889 4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile; wenzelm parents: 33820 diff changeset	21	"~~/src/Tools/quickcheck.ML"
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	22	"~~/src/Tools/value.ML"
47610 261f9de35b18 tuned whitespace haftmann parents: 46950 diff changeset	23	"~~/src/Tools/Code/code_preproc.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	24	"~~/src/Tools/Code/code_thingol.ML"
37442 037ee7b712b2 added code_simp infrastructure haftmann parents: 34968 diff changeset	25	"~~/src/Tools/Code/code_simp.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	26	"~~/src/Tools/Code/code_printer.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	27	"~~/src/Tools/Code/code_target.ML"
38970 53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML haftmann parents: 37818 diff changeset	28	"~~/src/Tools/Code/code_namespace.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	29	"~~/src/Tools/Code/code_ml.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	30	"~~/src/Tools/Code/code_haskell.ML"
34294 19c1fd52d6c9 a primitive scala serializer haftmann parents: 34028 diff changeset	31	"~~/src/Tools/Code/code_scala.ML"
39474 1986f18c4940 adjusted setup haftmann parents: 39423 diff changeset	32	("~~/src/Tools/Code/code_runtime.ML")
39911 2b4430847310 moved ML_Context.value to Code_Runtime haftmann parents: 39474 diff changeset	33	("~~/src/Tools/nbe.ML")
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	34	begin
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	35
39423 9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	36	setup {*
40116 9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct" blanchet parents: 39911 diff changeset	37	Solve_Direct.setup
39423 9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	38	#> Code_Preproc.setup
9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	39	#> Code_Simp.setup
43564 9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup; wenzelm parents: 43018 diff changeset	40	#> Code_Target.setup
39423 9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	41	#> Code_ML.setup
9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	42	#> Code_Haskell.setup
9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	43	#> Code_Scala.setup
9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	44	#> Quickcheck.setup
43612 c32144b8baba adding a value antiquotation bulwahn parents: 43564 diff changeset	45	#> Value.setup
39423 9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	46	*}
9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	47
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	48	code_datatype "TYPE('a\<Colon>{})"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	49
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	50	definition holds :: "prop" where
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	51	"holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	52
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	53	lemma holds: "PROP holds"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	54	by (unfold holds_def) (rule reflexive)
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	55
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	56	code_datatype holds
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	57
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	58	lemma implies_code [code]:
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	59	"(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	60	"(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	61	proof -
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	62	show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	63	proof
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	64	assume "PROP holds \<Longrightarrow> PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	65	then show "PROP P" using holds .
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	66	next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	67	assume "PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	68	then show "PROP P" .
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	69	qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	70	next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	71	show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	72	by rule (rule holds)+
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	73	qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	74
39474 1986f18c4940 adjusted setup haftmann parents: 39423 diff changeset	75	use "~~/src/Tools/Code/code_runtime.ML"
39911 2b4430847310 moved ML_Context.value to Code_Runtime haftmann parents: 39474 diff changeset	76	use "~~/src/Tools/nbe.ML"
2b4430847310 moved ML_Context.value to Code_Runtime haftmann parents: 39474 diff changeset	77
2b4430847310 moved ML_Context.value to Code_Runtime haftmann parents: 39474 diff changeset	78	setup Nbe.setup
39474 1986f18c4940 adjusted setup haftmann parents: 39423 diff changeset	79
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	80	hide_const (open) holds
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	81
33561 ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck; blanchet parents: 31775 diff changeset	82	end

author	haftmann
	Thu, 19 Apr 2012 19:18:47 +0200
changeset 47610	261f9de35b18
parent 46950	d0181abdbdac
child 47657	1ba213363d0c
permissions	-rw-r--r--