src/Tools/Code_Generator.thy
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 40116 9ed3711366c8
child 43018 121aa59b4d17
permissions -rw-r--r--
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
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
30929
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff changeset
     9
uses
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37442
diff changeset
    10
  "~~/src/Tools/cache_io.ML"
39323
ce5c6a8b0359 start renaming "Auto_Counterexample" to "Auto_Tools";
blanchet
parents: 38970
diff changeset
    11
  "~~/src/Tools/auto_tools.ML"
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39911
diff changeset
    12
  "~~/src/Tools/solve_direct.ML"
33889
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile;
wenzelm
parents: 33820
diff changeset
    13
  "~~/src/Tools/quickcheck.ML"
30929
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff changeset
    14
  "~~/src/Tools/value.ML"
31775
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31125
diff changeset
    15
  "~~/src/Tools/Code/code_preproc.ML" 
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31125
diff changeset
    16
  "~~/src/Tools/Code/code_thingol.ML"
37442
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 34968
diff changeset
    17
  "~~/src/Tools/Code/code_simp.ML"
31775
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31125
diff changeset
    18
  "~~/src/Tools/Code/code_printer.ML"
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31125
diff changeset
    19
  "~~/src/Tools/Code/code_target.ML"
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents: 37818
diff changeset
    20
  "~~/src/Tools/Code/code_namespace.ML"
31775
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31125
diff changeset
    21
  "~~/src/Tools/Code/code_ml.ML"
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 31125
diff changeset
    22
  "~~/src/Tools/Code/code_haskell.ML"
34294
19c1fd52d6c9 a primitive scala serializer
haftmann
parents: 34028
diff changeset
    23
  "~~/src/Tools/Code/code_scala.ML"
39474
1986f18c4940 adjusted setup
haftmann
parents: 39423
diff changeset
    24
  ("~~/src/Tools/Code/code_runtime.ML")
39911
2b4430847310 moved ML_Context.value to Code_Runtime
haftmann
parents: 39474
diff changeset
    25
  ("~~/src/Tools/nbe.ML")
30929
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff changeset
    26
begin
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff changeset
    27
39423
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    28
setup {*
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 39911
diff changeset
    29
  Solve_Direct.setup
39423
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    30
  #> Code_Preproc.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    31
  #> Code_Simp.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    32
  #> Code_ML.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    33
  #> Code_Haskell.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    34
  #> Code_Scala.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    35
  #> Quickcheck.setup
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    36
*}
9969401e1fb8 load code_runtime immediately again
haftmann
parents: 39421
diff changeset
    37
39421
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    38
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
    39
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    40
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
    41
  "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
    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
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
    44
  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
    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
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
    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
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
    49
  "(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
    50
  "(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
    51
proof -
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    52
  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
    53
  proof
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    54
    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
    55
    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
    56
  next
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 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" .
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    59
  qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    60
next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    61
  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
    62
    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
    63
qed  
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    64
39474
1986f18c4940 adjusted setup
haftmann
parents: 39423
diff changeset
    65
use "~~/src/Tools/Code/code_runtime.ML"
39911
2b4430847310 moved ML_Context.value to Code_Runtime
haftmann
parents: 39474
diff changeset
    66
use "~~/src/Tools/nbe.ML"
2b4430847310 moved ML_Context.value to Code_Runtime
haftmann
parents: 39474
diff changeset
    67
2b4430847310 moved ML_Context.value to Code_Runtime
haftmann
parents: 39474
diff changeset
    68
setup Nbe.setup
39474
1986f18c4940 adjusted setup
haftmann
parents: 39423
diff changeset
    69
39421
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
haftmann
parents: 39401
diff changeset
    70
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
    71
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 31775
diff changeset
    72
end