src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54116 ba709c934470
child 54695 a9efdf970720
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
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@48383
    16
  val infinite_timeout : Time.time
blanchet@48318
    17
  val time_mult : real -> Time.time -> Time.time
blanchet@35963
    18
  val parse_bool_option : bool -> string -> string -> bool option
blanchet@35963
    19
  val parse_time_option : string -> string -> Time.time option
blanchet@38044
    20
  val subgoal_count : Proof.state -> int
blanchet@38696
    21
  val reserved_isar_keyword_table : unit -> unit Symtab.table
blanchet@50735
    22
  val thms_in_proof :
blanchet@50735
    23
    (string Symtab.table * string Symtab.table) option -> thm -> string list
smolkas@50267
    24
  val thms_of_name : Proof.context -> string -> thm list
blanchet@50557
    25
  val one_day : Time.time
blanchet@50557
    26
  val one_year : Time.time
blanchet@50557
    27
  val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
blanchet@50048
    28
  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
blanchet@53815
    29
  val hackish_string_of_term : Proof.context -> term -> string
blanchet@53815
    30
  val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
smolkas@52556
    31
smolkas@52556
    32
  (** extrema **)
smolkas@52556
    33
  val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
smolkas@52556
    34
  val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
smolkas@52556
    35
  val max_list : ('a * 'a -> order) -> 'a list -> 'a option
blanchet@35963
    36
end;
blanchet@39318
    37
blanchet@35963
    38
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
blanchet@35963
    39
struct
blanchet@35963
    40
blanchet@43085
    41
open ATP_Util
blanchet@43085
    42
blanchet@48392
    43
val sledgehammerN = "sledgehammer"
blanchet@48392
    44
blanchet@50608
    45
val log10_2 = Math.log10 2.0
blanchet@50608
    46
blanchet@50608
    47
fun log2 n = Math.log10 n / log10_2
blanchet@50608
    48
blanchet@51181
    49
fun app_hd f (x :: xs) = f x :: xs
blanchet@51181
    50
blanchet@36142
    51
fun plural_s n = if n = 1 then "" else "s"
blanchet@36062
    52
blanchet@43029
    53
val serial_commas = Try.serial_commas
blanchet@43085
    54
val simplify_spaces = strip_spaces false (K true)
blanchet@37962
    55
blanchet@48656
    56
fun with_cleanup clean_up f x =
blanchet@48656
    57
  Exn.capture f x
blanchet@48656
    58
  |> tap (fn _ => clean_up x)
blanchet@48656
    59
  |> Exn.release
blanchet@48656
    60
blanchet@48383
    61
val infinite_timeout = seconds 31536000.0 (* one year *)
blanchet@48383
    62
blanchet@48318
    63
fun time_mult k t =
blanchet@48318
    64
  Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
blanchet@48318
    65
blanchet@35963
    66
fun parse_bool_option option name s =
blanchet@35963
    67
  (case s of
wenzelm@51930
    68
     "smart" => if option then NONE else raise Option.Option
blanchet@35963
    69
   | "false" => SOME false
blanchet@35963
    70
   | "true" => SOME true
blanchet@35963
    71
   | "" => SOME true
wenzelm@51930
    72
   | _ => raise Option.Option)
blanchet@35963
    73
  handle Option.Option =>
blanchet@35963
    74
         let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
blanchet@35963
    75
           error ("Parameter " ^ quote name ^ " must be assigned " ^
blanchet@35963
    76
                  space_implode " " (serial_commas "or" ss) ^ ".")
blanchet@35963
    77
         end
blanchet@35963
    78
blanchet@40341
    79
val has_junk =
wenzelm@40627
    80
  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
blanchet@40341
    81
blanchet@35963
    82
fun parse_time_option _ "none" = NONE
blanchet@35963
    83
  | parse_time_option name s =
blanchet@40341
    84
    let val secs = if has_junk s then NONE else Real.fromString s in
blanchet@43034
    85
      if is_none secs orelse Real.< (the secs, 0.0) then
blanchet@43034
    86
        error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
blanchet@40341
    87
               \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
blanchet@35963
    88
      else
blanchet@40341
    89
        SOME (seconds (the secs))
blanchet@35963
    90
    end
blanchet@35963
    91
blanchet@43029
    92
val subgoal_count = Try.subgoal_count
blanchet@38044
    93
blanchet@38696
    94
fun reserved_isar_keyword_table () =
blanchet@48292
    95
  Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
blanchet@38696
    96
blanchet@48251
    97
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
blanchet@48251
    98
   fixes that seem to be missing over there; or maybe the two code portions are
blanchet@48251
    99
   not doing the same? *)
blanchet@54116
   100
fun fold_body_thm outer_name (map_plain_name, map_inclass_name) =
blanchet@48251
   101
  let
blanchet@54116
   102
    fun app_thm map_name (_, (name, _, body)) accum =
blanchet@54116
   103
      let
blanchet@54116
   104
        val (anonymous, enter_class) =
blanchet@54116
   105
          (* The "name = outer_name" case caters for the uncommon case where the proved theorem
blanchet@54116
   106
             occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)
blanchet@54116
   107
          if name = "" orelse name = outer_name then (true, false)
blanchet@54116
   108
          else if map_inclass_name name = SOME outer_name then (true, true)
blanchet@54116
   109
          else (false, false)
blanchet@54116
   110
      in
blanchet@54116
   111
        if anonymous then
blanchet@54116
   112
          accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body)
blanchet@54116
   113
        else
blanchet@54116
   114
          accum |> union (op =) (the_list (map_name name))
blanchet@54116
   115
      end
blanchet@54116
   116
    and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
blanchet@54116
   117
  in app_body map_plain_name end
blanchet@48251
   118
blanchet@50735
   119
fun thms_in_proof name_tabs th =
blanchet@54116
   120
  let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
blanchet@54116
   121
    fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) []
blanchet@54116
   122
  end
blanchet@48251
   123
smolkas@50267
   124
fun thms_of_name ctxt name =
smolkas@50267
   125
  let
smolkas@50267
   126
    val lex = Keyword.get_lexicons
smolkas@50267
   127
    val get = maps (Proof_Context.get_fact ctxt o fst)
smolkas@50267
   128
  in
smolkas@50267
   129
    Source.of_string name
smolkas@50267
   130
    |> Symbol.source
smolkas@50267
   131
    |> Token.source {do_recover = SOME false} lex Position.start
smolkas@50267
   132
    |> Token.source_proper
smolkas@50267
   133
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
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@50557
   140
fun time_limit NONE = I
blanchet@50557
   141
  | time_limit (SOME delay) = TimeLimit.timeLimit delay
blanchet@50557
   142
blanchet@50048
   143
fun with_vanilla_print_mode f x =
blanchet@50048
   144
  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
blanchet@50048
   145
                           (print_mode_value ())) f x
blanchet@50048
   146
blanchet@53815
   147
fun hackish_string_of_term ctxt =
blanchet@53815
   148
  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
blanchet@53815
   149
blanchet@54062
   150
val spying_version = "c"
blanchet@53815
   151
blanchet@53815
   152
fun spying false _ = ()
blanchet@53815
   153
  | spying true f =
blanchet@53815
   154
    let
blanchet@53815
   155
      val (state, i, tool, message) = f ()
blanchet@53815
   156
      val ctxt = Proof.context_of state
blanchet@53815
   157
      val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i
blanchet@53815
   158
      val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
blanchet@53815
   159
    in
blanchet@53815
   160
      File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
blanchet@53815
   161
        (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
blanchet@53815
   162
    end
blanchet@53815
   163
smolkas@52556
   164
(** extrema **)
smolkas@52556
   165
smolkas@52556
   166
fun max ord x y = case ord(x,y) of LESS => y | _ => x
smolkas@52556
   167
smolkas@52556
   168
fun max_option ord = max (option_ord ord)
smolkas@52556
   169
smolkas@52556
   170
fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
smolkas@52556
   171
blanchet@35963
   172
end;