src/HOL/TPTP/mash_export.ML
author blanchet
Tue, 10 Jul 2012 23:36:03 +0200
changeset 48234 06216c789ac9
child 48235 40655464a93b
permissions -rw-r--r--
moved MaSh into own files
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/mash_export.ML
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     3
    Copyright   2012
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     4
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     5
Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer).
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     6
*)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     7
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     8
signature MASH_EXPORT =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
     9
sig
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    10
  val generate_mash_accessibility_file_for_theory :
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    11
    theory -> bool -> string -> unit
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    12
  val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    13
  val generate_mash_dependency_file_for_theory :
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    14
    theory -> bool -> string -> unit
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    15
  val generate_mash_problem_file_for_theory : theory -> string -> unit
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    16
end;
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    17
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    18
structure MaSh_Export : MASH_EXPORT =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    19
struct
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    20
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    21
open ATP_Problem_Generate
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    22
open ATP_Util
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    23
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    24
fun stringN_of_int 0 _ = ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    25
  | stringN_of_int k n =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    26
    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    27
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    28
fun escape_meta_char c =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    29
  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    30
     c = #")" orelse c = #"," then
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    31
    String.str c
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    32
  else if c = #"'" then
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    33
    "~"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    34
  else
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    35
    (* fixed width, in case more digits follow *)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    36
    "\\" ^ stringN_of_int 3 (Char.ord c)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    37
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    38
val escape_meta = String.translate escape_meta_char
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    39
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    40
val thy_prefix = "y_"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    41
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    42
val fact_name_of = escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    43
val thy_name_of = prefix thy_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    44
val const_name_of = prefix const_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    45
val type_name_of = prefix type_const_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    46
val class_name_of = prefix class_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    47
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    48
val thy_name_of_thm = theory_of_thm #> Context.theory_name
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    49
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    50
local
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    51
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    52
fun has_bool @{typ bool} = true
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    53
  | has_bool (Type (_, Ts)) = exists has_bool Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    54
  | has_bool _ = false
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    55
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    56
fun has_fun (Type (@{type_name fun}, _)) = true
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    57
  | has_fun (Type (_, Ts)) = exists has_fun Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    58
  | has_fun _ = false
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    59
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    60
val is_conn = member (op =)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    61
  [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    62
   @{const_name HOL.implies}, @{const_name Not},
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    63
   @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    64
   @{const_name HOL.eq}]
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    65
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    66
val has_bool_arg_const =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    67
  exists_Const (fn (c, T) =>
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    68
                   not (is_conn c) andalso exists has_bool (binder_types T))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    69
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    70
fun higher_inst_const thy (c, T) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    71
  case binder_types T of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    72
    [] => false
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    73
  | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    74
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    75
val binders = [@{const_name All}, @{const_name Ex}]
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    76
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    77
in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    78
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    79
fun is_fo_term thy t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    80
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    81
    val t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    82
      t |> Envir.beta_eta_contract
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    83
        |> transform_elim_prop
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    84
        |> Object_Logic.atomize_term thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    85
  in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    86
    Term.is_first_order binders t andalso
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    87
    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    88
                          | _ => false) t orelse
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    89
         has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    90
  end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    91
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    92
end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    93
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    94
fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    95
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    96
    val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    97
    val bad_consts = atp_widely_irrelevant_consts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    98
    val add_classes =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    99
      subtract (op =) @{sort type} #> map class_name_of #> union (op =)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   100
    fun do_add_type (Type (s, Ts)) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   101
        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   102
        #> fold do_add_type Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   103
      | do_add_type (TFree (_, S)) = add_classes S
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   104
      | do_add_type (TVar (_, S)) = add_classes S
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   105
    fun add_type T = type_max_depth >= 0 ? do_add_type T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   106
    fun mk_app s args =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   107
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   108
      else s
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   109
    fun patternify ~1 _ = ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   110
      | patternify depth t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   111
        case strip_comb t of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   112
          (Const (s, _), args) =>
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   113
          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   114
        | _ => ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   115
    fun add_term_patterns ~1 _ = I
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   116
      | add_term_patterns depth t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   117
        insert (op =) (patternify depth t)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   118
        #> add_term_patterns (depth - 1) t
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   119
    val add_term = add_term_patterns term_max_depth
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   120
    fun add_patterns t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   121
      let val (head, args) = strip_comb t in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   122
        (case head of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   123
           Const (s, T) =>
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   124
           not (member (op =) bad_consts s) ? (add_term t #> add_type T)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   125
         | Free (_, T) => add_type T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   126
         | Var (_, T) => add_type T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   127
         | Abs (_, T, body) => add_type T #> add_patterns body
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   128
         | _ => I)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   129
        #> fold add_patterns args
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   130
      end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   131
  in [] |> add_patterns t |> sort string_ord end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   132
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   133
fun is_likely_tautology th =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   134
  null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   135
  not (Thm.eq_thm_prop (@{thm ext}, th))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   136
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   137
fun is_too_meta thy th =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   138
  fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   139
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   140
fun non_tautological_facts_of thy =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   141
  all_facts_of_theory thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   142
  |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   143
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   144
fun theory_ord p =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   145
  if Theory.eq_thy p then EQUAL
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   146
  else if Theory.subthy p then LESS
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   147
  else if Theory.subthy (swap p) then GREATER
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   148
  else EQUAL
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   149
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   150
val thm_ord = theory_ord o pairself theory_of_thm
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   151
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   152
fun thms_by_thy ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   153
  ths |> map (snd #> `thy_name_of_thm)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   154
      |> AList.group (op =)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   155
      |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   156
                                   o hd o snd))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   157
      |> map (apsnd (sort thm_ord))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   158
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   159
fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   160
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   161
fun parent_thms thy_ths thy =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   162
  Theory.parents_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   163
  |> map Context.theory_name
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   164
  |> map_filter (AList.lookup (op =) thy_ths)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   165
  |> map List.last
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   166
  |> map (fact_name_of o Thm.get_name_hint)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   167
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   168
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   169
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   170
val max_depth = 1
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   171
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   172
fun features_of thy (status, th) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   173
  let val t = Thm.prop_of th in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   174
    thy_name_of (thy_name_of_thm th) ::
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   175
    interesting_terms_types_and_classes max_depth max_depth t
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   176
    |> not (has_no_lambdas t) ? cons "lambdas"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   177
    |> exists_Const is_exists t ? cons "skolems"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   178
    |> not (is_fo_term thy t) ? cons "ho"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   179
    |> (case status of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   180
          General => I
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   181
        | Induction => cons "induction"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   182
        | Intro => cons "intro"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   183
        | Inductive => cons "inductive"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   184
        | Elim => cons "elim"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   185
        | Simp => cons "simp"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   186
        | Def => cons "def")
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   187
  end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   188
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   189
val dependencies_of =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   190
  map fact_name_of oo theorems_mentioned_in_proof_term o SOME
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   191
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   192
fun generate_mash_accessibility_file_for_theory thy include_thy file_name =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   193
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   194
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   195
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   196
    fun do_thm th prevs =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   197
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   198
        val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   199
        val _ = File.append path s
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   200
      in [th] end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   201
    val thy_ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   202
      non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   203
      |> not include_thy ? filter_out (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   204
      |> thms_by_thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   205
    fun do_thy ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   206
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   207
        val thy = theory_of_thm (hd ths)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   208
        val parents = parent_thms thy_ths thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   209
        val ths = ths |> map (fact_name_of o Thm.get_name_hint)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   210
        val _ = fold do_thm ths parents
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   211
      in () end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   212
    val _ = List.app (do_thy o snd) thy_ths
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   213
  in () end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   214
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   215
fun generate_mash_feature_file_for_theory thy include_thy file_name =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   216
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   217
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   218
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   219
    val facts =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   220
      non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   221
      |> not include_thy ? filter_out (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   222
    fun do_fact ((_, (_, status)), th) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   223
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   224
        val name = Thm.get_name_hint th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   225
        val feats = features_of thy (status, th)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   226
        val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   227
      in File.append path s end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   228
    val _ = List.app do_fact facts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   229
  in () end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   230
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   231
fun generate_mash_dependency_file_for_theory thy include_thy file_name =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   232
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   233
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   234
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   235
    val ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   236
      non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   237
      |> not include_thy ? filter_out (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   238
      |> map snd
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   239
    val all_names = ths |> map Thm.get_name_hint
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   240
    fun do_thm th =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   241
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   242
        val name = Thm.get_name_hint th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   243
        val deps = dependencies_of all_names th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   244
        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   245
      in File.append path s end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   246
    val _ = List.app do_thm ths
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   247
  in () end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   248
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   249
fun generate_mash_problem_file_for_theory thy file_name =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   250
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   251
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   252
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   253
    val facts = non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   254
    val (new_facts, old_facts) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   255
      facts |> List.partition (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   256
            |>> sort (thm_ord o pairself snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   257
    val ths = facts |> map snd
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   258
    val all_names = ths |> map Thm.get_name_hint
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   259
    fun do_fact ((_, (_, status)), th) prevs =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   260
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   261
        val name = Thm.get_name_hint th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   262
        val feats = features_of thy (status, th)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   263
        val deps = dependencies_of all_names th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   264
        val kind = Thm.legacy_get_kind th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   265
        val name = fact_name_of name
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   266
        val core =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   267
          name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   268
        val query = if kind <> "" then "? " ^ core ^ "\n" else ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   269
        val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   270
        val _ = File.append path (query ^ update)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   271
      in [name] end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   272
    val thy_ths = old_facts |> thms_by_thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   273
    val parents = parent_thms thy_ths thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   274
    val _ = fold do_fact new_facts parents
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   275
  in () end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   276
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   277
end;