src/HOL/TPTP/MaSh_Export.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58206 3e22d3ed829f
child 63167 0909deb8059b
permissions -rw-r--r--
modernized header uniformly as section;
blanchet@48234
     1
(*  Title:      HOL/TPTP/MaSh_Export.thy
blanchet@48234
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48234
     3
*)
blanchet@48234
     4
wenzelm@58889
     5
section {* MaSh Exporter *}
blanchet@48234
     6
blanchet@48234
     7
theory MaSh_Export
blanchet@58206
     8
imports MaSh_Export_Base
blanchet@48234
     9
begin
blanchet@48234
    10
blanchet@50337
    11
ML {*
blanchet@50350
    12
if do_it then
blanchet@50350
    13
  Isabelle_System.mkdir (Path.explode prefix)
blanchet@50350
    14
else
blanchet@50350
    15
  ()
blanchet@48246
    16
*}
blanchet@48531
    17
blanchet@57120
    18
ML {*
blanchet@57120
    19
if do_it then
blanchet@57457
    20
  generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions
blanchet@57431
    21
    (prefix ^ "mash_nb_suggestions")
blanchet@57120
    22
else
blanchet@57120
    23
  ()
blanchet@57120
    24
*}
blanchet@57120
    25
blanchet@48246
    26
ML {*
blanchet@48245
    27
if do_it then
blanchet@57457
    28
  generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions
blanchet@57431
    29
    (prefix ^ "mash_knn_suggestions")
blanchet@57120
    30
else
blanchet@57120
    31
  ()
blanchet@57120
    32
*}
blanchet@57120
    33
blanchet@57457
    34
ML {*
blanchet@57457
    35
if do_it then
blanchet@57457
    36
  generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
blanchet@57457
    37
    (prefix ^ "mepo_suggestions")
blanchet@57457
    38
else
blanchet@57457
    39
  ()
blanchet@57457
    40
*}
blanchet@57457
    41
blanchet@57457
    42
ML {*
blanchet@57457
    43
if do_it then
blanchet@57457
    44
  generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions")
blanchet@57457
    45
    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions")
blanchet@57457
    46
else
blanchet@57457
    47
  ()
blanchet@57457
    48
*}
blanchet@57457
    49
blanchet@57457
    50
ML {*
blanchet@57457
    51
if do_it then
blanchet@57457
    52
  generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions")
blanchet@57457
    53
    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions")
blanchet@57457
    54
else
blanchet@57457
    55
  ()
blanchet@57457
    56
*}
blanchet@57120
    57
blanchet@57120
    58
ML {*
blanchet@57120
    59
if do_it then
blanchet@57457
    60
  generate_prover_dependencies @{context} params range thys
blanchet@57457
    61
    (prefix ^ "mash_nb_prover_dependencies")
blanchet@57457
    62
else
blanchet@57457
    63
  ()
blanchet@57457
    64
*}
blanchet@57457
    65
blanchet@57457
    66
ML {*
blanchet@57457
    67
if do_it then
blanchet@57457
    68
  generate_prover_dependencies @{context} params range thys
blanchet@57457
    69
    (prefix ^ "mash_knn_prover_dependencies")
blanchet@57457
    70
else
blanchet@57457
    71
  ()
blanchet@57457
    72
*}
blanchet@57457
    73
blanchet@57457
    74
ML {*
blanchet@57457
    75
if do_it then
blanchet@57457
    76
  generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions")
blanchet@57457
    77
    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions")
blanchet@57457
    78
else
blanchet@57457
    79
  ()
blanchet@57457
    80
*}
blanchet@57457
    81
blanchet@57457
    82
ML {*
blanchet@57457
    83
if do_it then
blanchet@57457
    84
  generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions")
blanchet@57457
    85
    (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions")
blanchet@57120
    86
else
blanchet@57120
    87
  ()
blanchet@57120
    88
*}
blanchet@57120
    89
blanchet@57120
    90
ML {*
blanchet@57120
    91
if do_it then
blanchet@57121
    92
  generate_accessibility @{context} thys (prefix ^ "mash_accessibility")
blanchet@48245
    93
else
blanchet@48245
    94
  ()
blanchet@48245
    95
*}
blanchet@48245
    96
blanchet@48245
    97
ML {*
blanchet@48245
    98
if do_it then
blanchet@55212
    99
  generate_features @{context} thys (prefix ^ "mash_features")
blanchet@48245
   100
else
blanchet@48245
   101
  ()
blanchet@48239
   102
*}
blanchet@48239
   103
blanchet@48239
   104
ML {*
blanchet@48245
   105
if do_it then
blanchet@57121
   106
  generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies")
blanchet@48333
   107
else
blanchet@48333
   108
  ()
blanchet@48333
   109
*}
blanchet@48333
   110
blanchet@48333
   111
ML {*
blanchet@48333
   112
if do_it then
blanchet@57121
   113
  generate_isar_commands @{context} prover (range, step) thys max_suggestions
blanchet@57120
   114
    (prefix ^ "mash_commands")
blanchet@48333
   115
else
blanchet@48333
   116
  ()
blanchet@48333
   117
*}
blanchet@48333
   118
blanchet@48333
   119
ML {*
blanchet@50816
   120
if do_it then
blanchet@57121
   121
  generate_prover_commands @{context} params (range, step) thys max_suggestions
blanchet@57120
   122
    (prefix ^ "mash_prover_commands")
blanchet@50411
   123
else
blanchet@50411
   124
  ()
blanchet@50411
   125
*}
blanchet@50411
   126
blanchet@48234
   127
end