src/Tools/Code_Generator.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58889 5b7a9633cfa8
child 59323 468bd3aedfa1
permissions -rw-r--r--
proper context for match_tac etc.;
haftmann@30929
     1
(*  Title:   Tools/Code_Generator.thy
haftmann@30929
     2
    Author:  Florian Haftmann, TU Muenchen
haftmann@30929
     3
*)
haftmann@30929
     4
wenzelm@58889
     5
section {* Loading the code generator and related modules *}
haftmann@30929
     6
haftmann@30929
     7
theory Code_Generator
wenzelm@33820
     8
imports Pure
wenzelm@46950
     9
keywords
haftmann@56925
    10
  "print_codeproc" "code_thms" "code_deps" :: diag and
haftmann@55372
    11
  "export_code" "code_identifier" "code_printing" "code_reserved"
haftmann@54890
    12
    "code_monad" "code_reflect" :: thy_decl and
wenzelm@46950
    13
  "datatypes" "functions" "module_name" "file" "checking"
haftmann@52137
    14
  "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
haftmann@30929
    15
begin
haftmann@30929
    16
wenzelm@48891
    17
ML_file "~~/src/Tools/cache_io.ML"
wenzelm@48891
    18
ML_file "~~/src/Tools/Code/code_preproc.ML"
haftmann@57430
    19
haftmann@57430
    20
attribute_setup code_preproc_trace = {*
haftmann@57430
    21
  (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
haftmann@57430
    22
  || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
haftmann@57430
    23
       >> Code_Preproc.trace_only_ext
haftmann@57430
    24
  || Scan.succeed Code_Preproc.trace_all)
haftmann@57430
    25
  >> (Thm.declaration_attribute o K)
haftmann@57430
    26
*} "tracing of the code generator preprocessor"
haftmann@57430
    27
haftmann@52136
    28
ML_file "~~/src/Tools/Code/code_symbol.ML"
wenzelm@48891
    29
ML_file "~~/src/Tools/Code/code_thingol.ML"
wenzelm@48891
    30
ML_file "~~/src/Tools/Code/code_simp.ML"
wenzelm@48891
    31
ML_file "~~/src/Tools/Code/code_printer.ML"
wenzelm@48891
    32
ML_file "~~/src/Tools/Code/code_target.ML"
wenzelm@48891
    33
ML_file "~~/src/Tools/Code/code_namespace.ML"
wenzelm@48891
    34
ML_file "~~/src/Tools/Code/code_ml.ML"
wenzelm@48891
    35
ML_file "~~/src/Tools/Code/code_haskell.ML"
wenzelm@48891
    36
ML_file "~~/src/Tools/Code/code_scala.ML"
wenzelm@48891
    37
haftmann@39423
    38
setup {*
haftmann@56970
    39
  Code_Simp.setup
wenzelm@43564
    40
  #> Code_Target.setup
haftmann@39423
    41
  #> Code_ML.setup
haftmann@39423
    42
  #> Code_Haskell.setup
haftmann@39423
    43
  #> Code_Scala.setup
haftmann@39423
    44
*}
haftmann@39423
    45
haftmann@39421
    46
code_datatype "TYPE('a\<Colon>{})"
haftmann@39421
    47
haftmann@39421
    48
definition holds :: "prop" where
haftmann@39421
    49
  "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
haftmann@39421
    50
haftmann@39421
    51
lemma holds: "PROP holds"
haftmann@39421
    52
  by (unfold holds_def) (rule reflexive)
haftmann@39421
    53
haftmann@39421
    54
code_datatype holds
haftmann@39421
    55
haftmann@39421
    56
lemma implies_code [code]:
haftmann@39421
    57
  "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
haftmann@39421
    58
  "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
haftmann@39421
    59
proof -
haftmann@39421
    60
  show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
haftmann@39421
    61
  proof
haftmann@39421
    62
    assume "PROP holds \<Longrightarrow> PROP P"
haftmann@39421
    63
    then show "PROP P" using holds .
haftmann@39421
    64
  next
haftmann@39421
    65
    assume "PROP P"
haftmann@39421
    66
    then show "PROP P" .
haftmann@39421
    67
  qed
haftmann@39421
    68
next
haftmann@39421
    69
  show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
haftmann@39421
    70
    by rule (rule holds)+
haftmann@39421
    71
qed  
haftmann@39421
    72
wenzelm@48891
    73
ML_file "~~/src/Tools/Code/code_runtime.ML"
wenzelm@48891
    74
ML_file "~~/src/Tools/nbe.ML"
haftmann@39474
    75
haftmann@39421
    76
hide_const (open) holds
haftmann@39421
    77
blanchet@33561
    78
end
haftmann@47657
    79