src/Tools/Code_Generator.thy
changeset 48891 c0eafbd55de3
parent 47657 1ba213363d0c
child 51275 3928173409e4
equal deleted inserted replaced
48890:d72ca5742f80 48891:c0eafbd55de3
    10   "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
    10   "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
    11   "code_class" "code_instance" "code_type"
    11   "code_class" "code_instance" "code_type"
    12     "code_const" "code_reserved" "code_include" "code_modulename"
    12     "code_const" "code_reserved" "code_include" "code_modulename"
    13     "code_abort" "code_monad" "code_reflect" :: thy_decl and
    13     "code_abort" "code_monad" "code_reflect" :: thy_decl and
    14   "datatypes" "functions" "module_name" "file" "checking"
    14   "datatypes" "functions" "module_name" "file" "checking"
    15 uses
       
    16   "~~/src/Tools/value.ML"
       
    17   "~~/src/Tools/cache_io.ML"
       
    18   "~~/src/Tools/Code/code_preproc.ML"
       
    19   "~~/src/Tools/Code/code_thingol.ML"
       
    20   "~~/src/Tools/Code/code_simp.ML"
       
    21   "~~/src/Tools/Code/code_printer.ML"
       
    22   "~~/src/Tools/Code/code_target.ML"
       
    23   "~~/src/Tools/Code/code_namespace.ML"
       
    24   "~~/src/Tools/Code/code_ml.ML"
       
    25   "~~/src/Tools/Code/code_haskell.ML"
       
    26   "~~/src/Tools/Code/code_scala.ML"
       
    27   ("~~/src/Tools/Code/code_runtime.ML")
       
    28   ("~~/src/Tools/nbe.ML")
       
    29 begin
    15 begin
       
    16 
       
    17 ML_file "~~/src/Tools/value.ML"
       
    18 ML_file "~~/src/Tools/cache_io.ML"
       
    19 ML_file "~~/src/Tools/Code/code_preproc.ML"
       
    20 ML_file "~~/src/Tools/Code/code_thingol.ML"
       
    21 ML_file "~~/src/Tools/Code/code_simp.ML"
       
    22 ML_file "~~/src/Tools/Code/code_printer.ML"
       
    23 ML_file "~~/src/Tools/Code/code_target.ML"
       
    24 ML_file "~~/src/Tools/Code/code_namespace.ML"
       
    25 ML_file "~~/src/Tools/Code/code_ml.ML"
       
    26 ML_file "~~/src/Tools/Code/code_haskell.ML"
       
    27 ML_file "~~/src/Tools/Code/code_scala.ML"
    30 
    28 
    31 setup {*
    29 setup {*
    32   Value.setup
    30   Value.setup
    33   #> Code_Preproc.setup
    31   #> Code_Preproc.setup
    34   #> Code_Simp.setup
    32   #> Code_Simp.setup
    63 next
    61 next
    64   show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    62   show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
    65     by rule (rule holds)+
    63     by rule (rule holds)+
    66 qed  
    64 qed  
    67 
    65 
    68 use "~~/src/Tools/Code/code_runtime.ML"
    66 ML_file "~~/src/Tools/Code/code_runtime.ML"
    69 use "~~/src/Tools/nbe.ML"
    67 ML_file "~~/src/Tools/nbe.ML"
    70 
       
    71 setup Nbe.setup
    68 setup Nbe.setup
    72 
    69 
    73 hide_const (open) holds
    70 hide_const (open) holds
    74 
    71 
    75 end
    72 end