src/HOL/TPTP/mash_export.ML
author blanchet
Tue, 10 Jul 2012 23:36:03 +0200
changeset 48239 0016290f904c
parent 48235 40655464a93b
child 48240 6a8d18798161
permissions -rw-r--r--
generate Meng--Paulson facts for evaluation purposes
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
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    10
  type stature = ATP_Problem_Generate.stature
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    11
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    12
  val non_tautological_facts_of :
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    13
    theory -> (((unit -> string) * stature) * thm) list
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    14
  val theory_ord : theory * theory -> order
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    15
  val thm_ord : thm * thm -> order
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    16
  val dependencies_of : string list -> thm -> string list
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    17
  val meng_paulson_facts :
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    18
    Proof.context -> string -> int -> real * real -> thm -> int
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    19
    -> (((unit -> string) * stature) * thm) list
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    20
    -> ((string * stature) * thm) list
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    21
  val generate_mash_accessibility : theory -> bool -> string -> unit
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    22
  val generate_mash_features : theory -> bool -> string -> unit
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    23
  val generate_mash_dependencies : theory -> bool -> string -> unit
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
    24
  val generate_mash_commands : theory -> string -> unit
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    25
  val generate_meng_paulson_suggestions :
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
    26
    Proof.context -> theory -> string -> unit
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    27
end;
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    28
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    29
structure MaSh_Export : MASH_EXPORT =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    30
struct
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    31
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    32
open ATP_Problem_Generate
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    33
open ATP_Util
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    34
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    35
fun stringN_of_int 0 _ = ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    36
  | stringN_of_int k n =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    37
    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    38
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    39
fun escape_meta_char c =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    40
  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    41
     c = #")" orelse c = #"," then
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    42
    String.str c
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    43
  else
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    44
    (* fixed width, in case more digits follow *)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    45
    "\\" ^ stringN_of_int 3 (Char.ord c)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    46
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    47
val escape_meta = String.translate escape_meta_char
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    48
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    49
val thy_prefix = "y_"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    50
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    51
val fact_name_of = escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    52
val thy_name_of = prefix thy_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    53
val const_name_of = prefix const_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    54
val type_name_of = prefix type_const_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    55
val class_name_of = prefix class_prefix o escape_meta
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    56
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    57
val thy_name_of_thm = theory_of_thm #> Context.theory_name
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    58
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    59
local
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    60
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    61
fun has_bool @{typ bool} = true
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    62
  | has_bool (Type (_, Ts)) = exists has_bool Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    63
  | has_bool _ = false
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    64
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    65
fun has_fun (Type (@{type_name fun}, _)) = true
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    66
  | has_fun (Type (_, Ts)) = exists has_fun Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    67
  | has_fun _ = false
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    68
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    69
val is_conn = member (op =)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    70
  [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    71
   @{const_name HOL.implies}, @{const_name Not},
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    72
   @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    73
   @{const_name HOL.eq}]
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    74
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    75
val has_bool_arg_const =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    76
  exists_Const (fn (c, T) =>
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    77
                   not (is_conn c) andalso exists has_bool (binder_types T))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    78
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    79
fun higher_inst_const thy (c, T) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    80
  case binder_types T of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    81
    [] => false
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    82
  | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    83
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    84
val binders = [@{const_name All}, @{const_name Ex}]
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    85
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    86
in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    87
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    88
fun is_fo_term thy t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    89
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    90
    val t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    91
      t |> Envir.beta_eta_contract
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    92
        |> transform_elim_prop
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    93
        |> Object_Logic.atomize_term thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    94
  in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    95
    Term.is_first_order binders t andalso
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    96
    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    97
                          | _ => false) t orelse
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    98
         has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
    99
  end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   100
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   101
end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   102
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   103
fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   104
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   105
    val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   106
    val bad_consts = atp_widely_irrelevant_consts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   107
    val add_classes =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   108
      subtract (op =) @{sort type} #> map class_name_of #> union (op =)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   109
    fun do_add_type (Type (s, Ts)) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   110
        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   111
        #> fold do_add_type Ts
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   112
      | do_add_type (TFree (_, S)) = add_classes S
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   113
      | do_add_type (TVar (_, S)) = add_classes S
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   114
    fun add_type T = type_max_depth >= 0 ? do_add_type T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   115
    fun mk_app s args =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   116
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   117
      else s
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   118
    fun patternify ~1 _ = ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   119
      | patternify depth t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   120
        case strip_comb t of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   121
          (Const (s, _), args) =>
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   122
          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   123
        | _ => ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   124
    fun add_term_patterns ~1 _ = I
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   125
      | add_term_patterns depth t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   126
        insert (op =) (patternify depth t)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   127
        #> add_term_patterns (depth - 1) t
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   128
    val add_term = add_term_patterns term_max_depth
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   129
    fun add_patterns t =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   130
      let val (head, args) = strip_comb t in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   131
        (case head of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   132
           Const (s, T) =>
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   133
           not (member (op =) bad_consts s) ? (add_term t #> add_type T)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   134
         | Free (_, T) => add_type T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   135
         | Var (_, T) => add_type T
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   136
         | Abs (_, T, body) => add_type T #> add_patterns body
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   137
         | _ => I)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   138
        #> fold add_patterns args
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   139
      end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   140
  in [] |> add_patterns t |> sort string_ord end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   141
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   142
fun is_likely_tautology th =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   143
  null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   144
  not (Thm.eq_thm_prop (@{thm ext}, th))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   145
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   146
fun is_too_meta thy th =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   147
  fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   148
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   149
fun non_tautological_facts_of thy =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   150
  all_facts_of_theory thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   151
  |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   152
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   153
fun theory_ord p =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   154
  if Theory.eq_thy p then EQUAL
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   155
  else if Theory.subthy p then LESS
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   156
  else if Theory.subthy (swap p) then GREATER
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   157
  else EQUAL
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   158
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   159
val thm_ord = theory_ord o pairself theory_of_thm
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   160
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   161
fun thms_by_thy ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   162
  ths |> map (snd #> `thy_name_of_thm)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   163
      |> AList.group (op =)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   164
      |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   165
                                   o hd o snd))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   166
      |> map (apsnd (sort thm_ord))
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   167
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   168
fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   169
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   170
fun parent_thms thy_ths thy =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   171
  Theory.parents_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   172
  |> map Context.theory_name
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   173
  |> map_filter (AList.lookup (op =) thy_ths)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   174
  |> map List.last
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   175
  |> map (fact_name_of o Thm.get_name_hint)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   176
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   177
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   178
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   179
val max_depth = 1
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   180
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   181
fun features_of thy (status, th) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   182
  let val t = Thm.prop_of th in
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   183
    thy_name_of (thy_name_of_thm th) ::
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   184
    interesting_terms_types_and_classes max_depth max_depth t
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   185
    |> not (has_no_lambdas t) ? cons "lambdas"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   186
    |> exists_Const is_exists t ? cons "skolems"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   187
    |> not (is_fo_term thy t) ? cons "ho"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   188
    |> (case status of
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   189
          General => I
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   190
        | Induction => cons "induction"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   191
        | Intro => cons "intro"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   192
        | Inductive => cons "inductive"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   193
        | Elim => cons "elim"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   194
        | Simp => cons "simp"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   195
        | Def => cons "def")
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   196
  end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   197
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   198
val dependencies_of =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   199
  map fact_name_of oo theorems_mentioned_in_proof_term o SOME
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   200
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   201
val freezeT = Type.legacy_freeze_type
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   202
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   203
fun freeze (t $ u) = freeze t $ freeze u
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   204
  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   205
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   206
  | freeze (Const (s, T)) = Const (s, freezeT T)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   207
  | freeze (Free (s, T)) = Free (s, freezeT T)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   208
  | freeze t = t
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   209
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   210
val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   211
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   212
fun meng_paulson_facts ctxt prover_name max_relevant relevance_thresholds
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   213
                       goal i =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   214
  let
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   215
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   216
    val is_built_in_const =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   217
      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   218
    val relevance_fudge =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   219
      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   220
    val relevance_override = {add = [], del = [], only = false}
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   221
  in
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   222
    Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   223
        max_relevant is_built_in_const relevance_fudge relevance_override []
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   224
        hyp_ts concl_t
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   225
  end
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   226
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   227
fun generate_mash_accessibility thy include_thy file_name =
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   228
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   229
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   230
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   231
    fun do_thm th prevs =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   232
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   233
        val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   234
        val _ = File.append path s
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   235
      in [th] end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   236
    val thy_ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   237
      non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   238
      |> not include_thy ? filter_out (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   239
      |> thms_by_thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   240
    fun do_thy ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   241
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   242
        val thy = theory_of_thm (hd ths)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   243
        val parents = parent_thms thy_ths thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   244
        val ths = ths |> map (fact_name_of o Thm.get_name_hint)
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   245
      in fold do_thm ths parents; () end
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   246
  in List.app (do_thy o snd) thy_ths end
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   247
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   248
fun generate_mash_features thy include_thy file_name =
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   249
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   250
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   251
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   252
    val facts =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   253
      non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   254
      |> not include_thy ? filter_out (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   255
    fun do_fact ((_, (_, status)), th) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   256
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   257
        val name = Thm.get_name_hint th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   258
        val feats = features_of thy (status, th)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   259
        val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   260
      in File.append path s end
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   261
  in List.app do_fact facts end
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   262
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   263
fun generate_mash_dependencies thy include_thy file_name =
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   264
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   265
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   266
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   267
    val ths =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   268
      non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   269
      |> not include_thy ? filter_out (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   270
      |> map snd
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   271
    val all_names = ths |> map Thm.get_name_hint
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   272
    fun do_thm th =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   273
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   274
        val name = Thm.get_name_hint th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   275
        val deps = dependencies_of all_names th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   276
        val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   277
      in File.append path s end
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   278
  in List.app do_thm ths end
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   279
48235
40655464a93b MaSh evaluation driver
blanchet
parents: 48234
diff changeset
   280
fun generate_mash_commands thy file_name =
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   281
  let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   282
    val path = file_name |> Path.explode
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   283
    val _ = File.write path ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   284
    val facts = non_tautological_facts_of thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   285
    val (new_facts, old_facts) =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   286
      facts |> List.partition (has_thy thy o snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   287
            |>> sort (thm_ord o pairself snd)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   288
    val ths = facts |> map snd
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   289
    val all_names = ths |> map Thm.get_name_hint
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   290
    fun do_fact ((_, (_, status)), th) prevs =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   291
      let
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   292
        val name = Thm.get_name_hint th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   293
        val feats = features_of thy (status, th)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   294
        val deps = dependencies_of all_names th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   295
        val kind = Thm.legacy_get_kind th
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   296
        val name = fact_name_of name
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   297
        val core =
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   298
          name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   299
        val query = if kind <> "" then "? " ^ core ^ "\n" else ""
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   300
        val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n"
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   301
        val _ = File.append path (query ^ update)
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   302
      in [name] end
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   303
    val thy_ths = old_facts |> thms_by_thy
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   304
    val parents = parent_thms thy_ths thy
48239
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   305
  in fold do_fact new_facts parents; () end
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   306
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   307
fun generate_meng_paulson_suggestions ctxt thy file_name =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   308
  let
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   309
    val {provers, max_relevant, relevance_thresholds, ...} =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   310
      Sledgehammer_Isar.default_params ctxt []
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   311
    val prover_name = hd provers
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   312
    val path = file_name |> Path.explode
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   313
    val _ = File.write path ""
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   314
    val facts = non_tautological_facts_of thy
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   315
    val (new_facts, old_facts) =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   316
      facts |> List.partition (has_thy thy o snd)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   317
            |>> sort (thm_ord o pairself snd)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   318
    val i = 1
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   319
    fun do_fact (fact as (_, th)) old_facts =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   320
      let
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   321
        val name = Thm.get_name_hint th
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   322
        val goal = goal_of_thm th
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   323
        val kind = Thm.legacy_get_kind th
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   324
        val _ =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   325
          if kind <> "" then
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   326
            let
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   327
              val suggs =
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   328
                old_facts
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   329
                |> meng_paulson_facts ctxt prover_name (the max_relevant)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   330
                                      relevance_thresholds goal i
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   331
                |> map (fact_name_of o Thm.get_name_hint o snd)
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   332
              val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   333
            in File.append path s end
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   334
          else
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   335
            ()
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   336
      in fact :: old_facts end
0016290f904c generate Meng--Paulson facts for evaluation purposes
blanchet
parents: 48235
diff changeset
   337
  in fold do_fact new_facts old_facts; () end
48234
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   338
06216c789ac9 moved MaSh into own files
blanchet
parents:
diff changeset
   339
end;