author | wenzelm |
Fri, 17 Aug 2012 11:23:57 +0200 | |
changeset 48835 | 574042d14fd9 |
parent 47657 | 1ba213363d0c |
child 48891 | c0eafbd55de3 |
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 |
|
39911 | 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 |
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
|
10 |
"value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and |
1ba213363d0c
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
haftmann
parents:
47610
diff
changeset
|
11 |
"code_class" "code_instance" "code_type" |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset
|
12 |
"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
|
13 |
"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
|
14 |
"datatypes" "functions" "module_name" "file" "checking" |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
15 |
uses |
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
|
16 |
"~~/src/Tools/value.ML" |
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37442
diff
changeset
|
17 |
"~~/src/Tools/cache_io.ML" |
47610 | 18 |
"~~/src/Tools/Code/code_preproc.ML" |
31775 | 19 |
"~~/src/Tools/Code/code_thingol.ML" |
37442 | 20 |
"~~/src/Tools/Code/code_simp.ML" |
31775 | 21 |
"~~/src/Tools/Code/code_printer.ML" |
22 |
"~~/src/Tools/Code/code_target.ML" |
|
38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
37818
diff
changeset
|
23 |
"~~/src/Tools/Code/code_namespace.ML" |
31775 | 24 |
"~~/src/Tools/Code/code_ml.ML" |
25 |
"~~/src/Tools/Code/code_haskell.ML" |
|
34294 | 26 |
"~~/src/Tools/Code/code_scala.ML" |
39474 | 27 |
("~~/src/Tools/Code/code_runtime.ML") |
39911 | 28 |
("~~/src/Tools/nbe.ML") |
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
29 |
begin |
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
30 |
|
39423 | 31 |
setup {* |
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
|
32 |
Value.setup |
39423 | 33 |
#> Code_Preproc.setup |
34 |
#> Code_Simp.setup |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43018
diff
changeset
|
35 |
#> Code_Target.setup |
39423 | 36 |
#> Code_ML.setup |
37 |
#> Code_Haskell.setup |
|
38 |
#> Code_Scala.setup |
|
39 |
*} |
|
40 |
||
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
41 |
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
|
42 |
|
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
43 |
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
|
44 |
"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
|
45 |
|
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
|
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
49 |
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
|
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 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
|
52 |
"(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
|
53 |
"(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
|
54 |
proof - |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
55 |
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
|
56 |
proof |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
next |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
qed |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
63 |
next |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
qed |
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
67 |
|
39474 | 68 |
use "~~/src/Tools/Code/code_runtime.ML" |
39911 | 69 |
use "~~/src/Tools/nbe.ML" |
70 |
||
71 |
setup Nbe.setup |
|
39474 | 72 |
|
39421
b6a77cffc231
introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents:
39401
diff
changeset
|
73 |
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
|
74 |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
31775
diff
changeset
|
75 |
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
|
76 |