src/Tools/Code_Generator.thy
author traytel
Thu Sep 29 09:37:59 2011 +0200 (2011-09-29)
changeset 45102 7bb89635eb51
parent 44121 44adaa6db327
child 45190 58e33a125f32
permissions -rw-r--r--
correct coercion generation in case of unknown map functions
     1 (*  Title:   Tools/Code_Generator.thy
     2     Author:  Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Loading the code generator and related modules *}
     6 
     7 theory Code_Generator
     8 imports Pure
     9 uses
    10   "~~/src/Tools/misc_legacy.ML"
    11   "~~/src/Tools/codegen.ML"
    12   "~~/src/Tools/cache_io.ML"
    13   "~~/src/Tools/try.ML"
    14   "~~/src/Tools/solve_direct.ML"
    15   "~~/src/Tools/quickcheck.ML"
    16   "~~/src/Tools/value.ML"
    17   "~~/src/Tools/Code/code_preproc.ML" 
    18   "~~/src/Tools/Code/code_thingol.ML"
    19   "~~/src/Tools/Code/code_simp.ML"
    20   "~~/src/Tools/Code/code_printer.ML"
    21   "~~/src/Tools/Code/code_target.ML"
    22   "~~/src/Tools/Code/code_namespace.ML"
    23   "~~/src/Tools/Code/code_ml.ML"
    24   "~~/src/Tools/Code/code_haskell.ML"
    25   "~~/src/Tools/Code/code_scala.ML"
    26   ("~~/src/Tools/Code/code_runtime.ML")
    27   ("~~/src/Tools/nbe.ML")
    28 begin
    29 
    30 setup {*
    31   Solve_Direct.setup
    32   #> Code_Preproc.setup
    33   #> Code_Simp.setup
    34   #> Code_Target.setup
    35   #> Code_ML.setup
    36   #> Code_Haskell.setup
    37   #> Code_Scala.setup
    38   #> Quickcheck.setup
    39   #> Value.setup
    40 *}
    41 
    42 code_datatype "TYPE('a\<Colon>{})"
    43 
    44 definition holds :: "prop" where
    45   "holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
    46 
    47 lemma holds: "PROP holds"
    48   by (unfold holds_def) (rule reflexive)
    49 
    50 code_datatype holds
    51 
    52 lemma implies_code [code]:
    53   "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
    54   "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    55 proof -
    56   show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
    57   proof
    58     assume "PROP holds \<Longrightarrow> PROP P"
    59     then show "PROP P" using holds .
    60   next
    61     assume "PROP P"
    62     then show "PROP P" .
    63   qed
    64 next
    65   show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    66     by rule (rule holds)+
    67 qed  
    68 
    69 use "~~/src/Tools/Code/code_runtime.ML"
    70 use "~~/src/Tools/nbe.ML"
    71 
    72 setup Nbe.setup
    73 
    74 hide_const (open) holds
    75 
    76 end