src/Tools/Code_Generator.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (8 weeks ago)
changeset 69981 3dced198b9ec
parent 69605 a96320074298
child 70009 435fb018e8ee
permissions -rw-r--r--
more strict AFP properties;
haftmann@30929
     1
(*  Title:   Tools/Code_Generator.thy
haftmann@30929
     2
    Author:  Florian Haftmann, TU Muenchen
haftmann@30929
     3
*)
haftmann@30929
     4
wenzelm@62020
     5
section \<open>Loading the code generator and related modules\<close>
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@63435
    13
  "checking" and
wenzelm@63435
    14
  "datatypes" "functions" "module_name" "file"
wenzelm@63435
    15
    "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
wenzelm@63435
    16
    :: quasi_command
haftmann@30929
    17
begin
haftmann@30929
    18
wenzelm@69605
    19
ML_file \<open>~~/src/Tools/cache_io.ML\<close>
wenzelm@69605
    20
ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
wenzelm@69605
    21
ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
wenzelm@69605
    22
ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
wenzelm@69605
    23
ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
wenzelm@69605
    24
ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
wenzelm@69605
    25
ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
wenzelm@69605
    26
ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
wenzelm@69605
    27
ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
wenzelm@69605
    28
ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
wenzelm@69605
    29
ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>
wenzelm@48891
    30
wenzelm@61076
    31
code_datatype "TYPE('a::{})"
haftmann@39421
    32
haftmann@39421
    33
definition holds :: "prop" where
haftmann@39421
    34
  "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
haftmann@39421
    35
haftmann@39421
    36
lemma holds: "PROP holds"
haftmann@39421
    37
  by (unfold holds_def) (rule reflexive)
haftmann@39421
    38
haftmann@39421
    39
code_datatype holds
haftmann@39421
    40
haftmann@39421
    41
lemma implies_code [code]:
haftmann@39421
    42
  "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
haftmann@39421
    43
  "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
haftmann@39421
    44
proof -
haftmann@39421
    45
  show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
haftmann@39421
    46
  proof
haftmann@39421
    47
    assume "PROP holds \<Longrightarrow> PROP P"
haftmann@39421
    48
    then show "PROP P" using holds .
haftmann@39421
    49
  next
haftmann@39421
    50
    assume "PROP P"
haftmann@39421
    51
    then show "PROP P" .
haftmann@39421
    52
  qed
haftmann@39421
    53
next
haftmann@39421
    54
  show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
haftmann@39421
    55
    by rule (rule holds)+
haftmann@39421
    56
qed  
haftmann@39421
    57
wenzelm@69605
    58
ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
wenzelm@69605
    59
ML_file \<open>~~/src/Tools/nbe.ML\<close>
haftmann@39474
    60
haftmann@39421
    61
hide_const (open) holds
haftmann@39421
    62
blanchet@33561
    63
end