src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author wenzelm
Tue Jun 06 13:13:25 2017 +0200 (2017-06-06)
changeset 66020 a31760eee09d
parent 64573 e6aee01da22d
child 67498 88a02f41246a
permissions -rw-r--r--
discontinued obsolete print mode;
blanchet@36062
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_util.ML
blanchet@35963
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35963
     3
blanchet@35963
     4
General-purpose functions used by the Sledgehammer modules.
blanchet@35963
     5
*)
blanchet@35963
     6
blanchet@35963
     7
signature SLEDGEHAMMER_UTIL =
blanchet@35963
     8
sig
blanchet@48392
     9
  val sledgehammerN : string
blanchet@50608
    10
  val log2 : real -> real
blanchet@51181
    11
  val app_hd : ('a -> 'a) -> 'a list -> 'a list
blanchet@36142
    12
  val plural_s : int -> string
blanchet@35963
    13
  val serial_commas : string -> string list -> string list
blanchet@38738
    14
  val simplify_spaces : string -> string
blanchet@48656
    15
  val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
blanchet@48318
    16
  val time_mult : real -> Time.time -> Time.time
blanchet@35963
    17
  val parse_bool_option : bool -> string -> string -> bool option
blanchet@54816
    18
  val parse_time : string -> string -> Time.time
blanchet@38044
    19
  val subgoal_count : Proof.state -> int
blanchet@57306
    20
  val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
blanchet@57306
    21
    string list option
smolkas@50267
    22
  val thms_of_name : Proof.context -> string -> thm list
blanchet@50557
    23
  val one_day : Time.time
blanchet@50557
    24
  val one_year : Time.time
blanchet@53815
    25
  val hackish_string_of_term : Proof.context -> term -> string
blanchet@53815
    26
  val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
blanchet@35963
    27
end;
blanchet@39318
    28
blanchet@35963
    29
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
blanchet@35963
    30
struct
blanchet@35963
    31
blanchet@43085
    32
open ATP_Util
blanchet@43085
    33
blanchet@48392
    34
val sledgehammerN = "sledgehammer"
blanchet@48392
    35
blanchet@50608
    36
val log10_2 = Math.log10 2.0
blanchet@50608
    37
fun log2 n = Math.log10 n / log10_2
blanchet@50608
    38
blanchet@51181
    39
fun app_hd f (x :: xs) = f x :: xs
blanchet@51181
    40
blanchet@36142
    41
fun plural_s n = if n = 1 then "" else "s"
blanchet@36062
    42
blanchet@43029
    43
val serial_commas = Try.serial_commas
blanchet@43085
    44
val simplify_spaces = strip_spaces false (K true)
blanchet@37962
    45
blanchet@48656
    46
fun with_cleanup clean_up f x =
blanchet@48656
    47
  Exn.capture f x
blanchet@48656
    48
  |> tap (fn _ => clean_up x)
blanchet@48656
    49
  |> Exn.release
blanchet@48656
    50
blanchet@55212
    51
fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
blanchet@48318
    52
blanchet@35963
    53
fun parse_bool_option option name s =
blanchet@35963
    54
  (case s of
wenzelm@51930
    55
     "smart" => if option then NONE else raise Option.Option
blanchet@35963
    56
   | "false" => SOME false
blanchet@35963
    57
   | "true" => SOME true
blanchet@35963
    58
   | "" => SOME true
wenzelm@51930
    59
   | _ => raise Option.Option)
blanchet@35963
    60
  handle Option.Option =>
blanchet@55285
    61
    let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
blanchet@55285
    62
      error ("Parameter " ^ quote name ^ " must be assigned " ^
blanchet@63692
    63
       space_implode " " (serial_commas "or" ss))
blanchet@55285
    64
    end
blanchet@35963
    65
blanchet@40341
    66
val has_junk =
wenzelm@40627
    67
  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
blanchet@40341
    68
blanchet@54816
    69
fun parse_time name s =
blanchet@54816
    70
  let val secs = if has_junk s then NONE else Real.fromString s in
wenzelm@62826
    71
    if is_none secs orelse the secs < 0.0 then
wenzelm@59431
    72
      error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
blanchet@63692
    73
        \(e.g., \"60\", \"0.5\") or \"none\"")
blanchet@54816
    74
    else
blanchet@54816
    75
      seconds (the secs)
blanchet@54816
    76
  end
blanchet@35963
    77
blanchet@43029
    78
val subgoal_count = Try.subgoal_count
blanchet@38044
    79
blanchet@57306
    80
exception TOO_MANY of unit
blanchet@57306
    81
blanchet@57108
    82
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
blanchet@57108
    83
   be missing over there; or maybe the two code portions are not doing the same? *)
blanchet@57306
    84
fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
blanchet@48251
    85
  let
wenzelm@64573
    86
    fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
blanchet@54116
    87
      let
wenzelm@64573
    88
        val name = Proofterm.thm_node_name thm_node
wenzelm@64573
    89
        val body = Proofterm.thm_node_body thm_node
blanchet@54116
    90
        val (anonymous, enter_class) =
blanchet@54116
    91
          (* The "name = outer_name" case caters for the uncommon case where the proved theorem
blanchet@54116
    92
             occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)
blanchet@54116
    93
          if name = "" orelse name = outer_name then (true, false)
blanchet@54116
    94
          else if map_inclass_name name = SOME outer_name then (true, true)
blanchet@54116
    95
          else (false, false)
blanchet@54116
    96
      in
blanchet@54116
    97
        if anonymous then
blanchet@57756
    98
          (case Future.peek body of
blanchet@57756
    99
            SOME (Exn.Res the_body) =>
blanchet@57756
   100
            app_body (if enter_class then map_inclass_name else map_name) the_body accum
blanchet@57756
   101
          | NONE => accum)
blanchet@54116
   102
        else
blanchet@57306
   103
          (case map_name name of
blanchet@57306
   104
            SOME name' =>
blanchet@57306
   105
            if member (op =) names name' then accum
blanchet@57306
   106
            else if num_thms = max_thms then raise TOO_MANY ()
blanchet@57306
   107
            else (num_thms + 1, name' :: names)
blanchet@57306
   108
          | NONE => accum)
blanchet@54116
   109
      end
blanchet@54116
   110
    and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
blanchet@57108
   111
  in
blanchet@57306
   112
    snd (app_body map_plain_name body (0, []))
blanchet@57108
   113
  end
blanchet@48251
   114
blanchet@57306
   115
fun thms_in_proof max_thms name_tabs th =
blanchet@57838
   116
  (case try Thm.proof_body_of th of
blanchet@57838
   117
    NONE => NONE
blanchet@57838
   118
  | SOME body =>
wenzelm@59058
   119
    let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
blanchet@57838
   120
      SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
blanchet@57838
   121
      handle TOO_MANY () => NONE
blanchet@57838
   122
    end)
blanchet@48251
   123
smolkas@50267
   124
fun thms_of_name ctxt name =
smolkas@50267
   125
  let
smolkas@50267
   126
    val get = maps (Proof_Context.get_fact ctxt o fst)
wenzelm@58928
   127
    val keywords = Thy_Header.get_keywords' ctxt
smolkas@50267
   128
  in
wenzelm@63936
   129
    Symbol.explode name
wenzelm@63936
   130
    |> Source.of_list
wenzelm@58904
   131
    |> Token.source keywords Position.start
smolkas@50267
   132
    |> Token.source_proper
wenzelm@62969
   133
    |> Source.source Token.stopper (Parse.thms1 >> get)
smolkas@50267
   134
    |> Source.exhaust
smolkas@50267
   135
  end
smolkas@50267
   136
blanchet@50557
   137
val one_day = seconds (24.0 * 60.0 * 60.0)
blanchet@50557
   138
val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
blanchet@50557
   139
blanchet@53815
   140
fun hackish_string_of_term ctxt =
blanchet@61432
   141
  (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
wenzelm@66020
   142
  #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
blanchet@61330
   143
  #> YXML.content_of
blanchet@61330
   144
  #> simplify_spaces
blanchet@53815
   145
blanchet@57727
   146
val spying_version = "d"
blanchet@53815
   147
blanchet@53815
   148
fun spying false _ = ()
blanchet@53815
   149
  | spying true f =
blanchet@53815
   150
    let
blanchet@53815
   151
      val (state, i, tool, message) = f ()
blanchet@53815
   152
      val ctxt = Proof.context_of state
wenzelm@59582
   153
      val goal = Logic.get_goal (Thm.prop_of (#goal (Proof.goal state))) i
blanchet@53815
   154
      val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
blanchet@53815
   155
    in
blanchet@53815
   156
      File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
blanchet@53815
   157
        (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
blanchet@53815
   158
    end
blanchet@53815
   159
blanchet@35963
   160
end;