isabelle: src/Tools/Code_Generator.thy@7e55bd4f9b0e (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
56925 601edd9a6859 degeneralized value command into HOL haftmann parents: 55372 diff changeset	10	"print_codeproc" "code_thms" "code_deps" :: diag and
55372 3662c44d018c dropped legacy finally haftmann parents: 54890 diff changeset	11	"export_code" "code_identifier" "code_printing" "code_reserved"
54890 cb892d835803 fundamental treatment of undefined vs. universally partial replaces code_abort haftmann parents: 52138 diff changeset	12	"code_monad" "code_reflect" :: thy_decl and
46950 d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 46947 diff changeset	13	"datatypes" "functions" "module_name" "file" "checking"
52137 7f7337447b1b use generic data for code symbols for unified "code_printing" syntax for custom serialisations haftmann parents: 52136 diff changeset	14	"constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	15	begin
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	16
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	17	ML_file "~~/src/Tools/cache_io.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	18	ML_file "~~/src/Tools/Code/code_preproc.ML"
57430 020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	19
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	20	attribute_setup code_preproc_trace = {*
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	21	(Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	22	\|\| (Scan.lift (Args.$$$ "only" \|-- Args.colon \|-- Scan.repeat1 Parse.term))
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	23	>> Code_Preproc.trace_only_ext
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	24	\|\| Scan.succeed Code_Preproc.trace_all)
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	25	>> (Thm.declaration_attribute o K)
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	26	*} "tracing of the code generator preprocessor"
020cea57eaa4 tracing facilities for the code generator preprocessor haftmann parents: 56970 diff changeset	27
52136 8c0818fe58c7 dedicated module for code symbol data haftmann parents: 51275 diff changeset	28	ML_file "~~/src/Tools/Code/code_symbol.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	29	ML_file "~~/src/Tools/Code/code_thingol.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	30	ML_file "~~/src/Tools/Code/code_simp.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	31	ML_file "~~/src/Tools/Code/code_printer.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	32	ML_file "~~/src/Tools/Code/code_target.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	33	ML_file "~~/src/Tools/Code/code_namespace.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	34	ML_file "~~/src/Tools/Code/code_ml.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	35	ML_file "~~/src/Tools/Code/code_haskell.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	36	ML_file "~~/src/Tools/Code/code_scala.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	37
39423 9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	38	setup {*
56970 a3f911785efa modernized setup haftmann parents: 56925 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	*}
9969401e1fb8 load code_runtime immediately again haftmann parents: 39421 diff changeset	45
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	46	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	47
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	48	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	49	"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	50
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	51	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	52	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	53
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	54	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	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	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	57	"(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	58	"(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	59	proof -
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	60	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	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	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	63	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	64	next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	65	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	66	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	67	qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	68	next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	69	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	70	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	71	qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	72
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	73	ML_file "~~/src/Tools/Code/code_runtime.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47657 diff changeset	74	ML_file "~~/src/Tools/nbe.ML"
39474 1986f18c4940 adjusted setup haftmann parents: 39423 diff changeset	75
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	76	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	77
33561 ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck; blanchet parents: 31775 diff changeset	78	end
47657 1ba213363d0c moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator haftmann parents: 47610 diff changeset	79

author	blanchet
	Sun, 29 Jun 2014 18:28:27 +0200
changeset 57433	7e55bd4f9b0e
parent 57430	020cea57eaa4
child 58889	5b7a9633cfa8
permissions	-rw-r--r--