src/Tools/Code_Generator.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 52138 e21426f244aa
child 54890 cb892d835803
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
51275
3928173409e4 reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;
wenzelm
parents: 48891
diff changeset
    10
  "value" "print_codeproc" "code_thms" "code_deps" :: diag and
52138
e21426f244aa bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann
parents: 52137
diff changeset
    11
  "export_code" "code_identifier" "code_printing" "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"
52137
7f7337447b1b use generic data for code symbols for unified "code_printing" syntax for custom serialisations
haftmann
parents: 52136
diff changeset
    15
  "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
    16
begin
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff changeset
    17
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    18
ML_file "~~/src/Tools/value.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    19
ML_file "~~/src/Tools/cache_io.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    20
ML_file "~~/src/Tools/Code/code_preproc.ML"
52136
8c0818fe58c7 dedicated module for code symbol data
haftmann
parents: 51275
diff changeset
    21
ML_file "~~/src/Tools/Code/code_symbol.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    22
ML_file "~~/src/Tools/Code/code_thingol.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    23
ML_file "~~/src/Tools/Code/code_simp.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    24
ML_file "~~/src/Tools/Code/code_printer.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    25
ML_file "~~/src/Tools/Code/code_target.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    26
ML_file "~~/src/Tools/Code/code_namespace.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    27
ML_file "~~/src/Tools/Code/code_ml.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    28
ML_file "~~/src/Tools/Code/code_haskell.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    29
ML_file "~~/src/Tools/Code/code_scala.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    30
39423
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    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
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    33
  #> Code_Preproc.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    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
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    36
  #> Code_ML.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    37
  #> Code_Haskell.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    38
  #> Code_Scala.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    39
*}
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    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
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    68
ML_file "~~/src/Tools/Code/code_runtime.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47657
diff changeset
    69
ML_file "~~/src/Tools/nbe.ML"
39911
2b4430847310 moved ML_Context.value to Code_Runtime
haftmann
parents: 39474
diff changeset
    70
setup Nbe.setup
39474
1986f18c4940 adjusted setup
haftmann
parents: 39423
diff changeset
    71
39421
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    72
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
    73
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 31775
diff changeset
    74
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
    75