src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author blanchet
Wed Dec 12 21:48:29 2012 +0100 (2012-12-12 ago)
changeset 50510 7e4f2f8d9b50
parent 50485 3c6ac2da2f45
child 50557 31313171deb5
permissions -rw-r--r--
export a pair of ML functions
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@36142
    10
  val plural_s : int -> string
blanchet@35963
    11
  val serial_commas : string -> string list -> string list
blanchet@38738
    12
  val simplify_spaces : string -> string
blanchet@48656
    13
  val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
blanchet@48383
    14
  val infinite_timeout : Time.time
blanchet@48318
    15
  val time_mult : real -> Time.time -> Time.time
blanchet@35963
    16
  val parse_bool_option : bool -> string -> string -> bool option
blanchet@35963
    17
  val parse_time_option : string -> string -> Time.time option
blanchet@38044
    18
  val subgoal_count : Proof.state -> int
blanchet@38696
    19
  val reserved_isar_keyword_table : unit -> unit Symtab.table
blanchet@50485
    20
  val thms_in_proof : string Symtab.table option -> thm -> string list
smolkas@50267
    21
  val thms_of_name : Proof.context -> string -> thm list
blanchet@50048
    22
  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
blanchet@35963
    23
end;
blanchet@39318
    24
blanchet@35963
    25
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
blanchet@35963
    26
struct
blanchet@35963
    27
blanchet@43085
    28
open ATP_Util
blanchet@43085
    29
blanchet@48392
    30
val sledgehammerN = "sledgehammer"
blanchet@48392
    31
blanchet@36142
    32
fun plural_s n = if n = 1 then "" else "s"
blanchet@36062
    33
blanchet@43029
    34
val serial_commas = Try.serial_commas
blanchet@43085
    35
val simplify_spaces = strip_spaces false (K true)
blanchet@37962
    36
blanchet@48656
    37
fun with_cleanup clean_up f x =
blanchet@48656
    38
  Exn.capture f x
blanchet@48656
    39
  |> tap (fn _ => clean_up x)
blanchet@48656
    40
  |> Exn.release
blanchet@48656
    41
blanchet@48383
    42
val infinite_timeout = seconds 31536000.0 (* one year *)
blanchet@48383
    43
blanchet@48318
    44
fun time_mult k t =
blanchet@48318
    45
  Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
blanchet@48318
    46
blanchet@35963
    47
fun parse_bool_option option name s =
blanchet@35963
    48
  (case s of
blanchet@35963
    49
     "smart" => if option then NONE else raise Option
blanchet@35963
    50
   | "false" => SOME false
blanchet@35963
    51
   | "true" => SOME true
blanchet@35963
    52
   | "" => SOME true
blanchet@35963
    53
   | _ => raise Option)
blanchet@35963
    54
  handle Option.Option =>
blanchet@35963
    55
         let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
blanchet@35963
    56
           error ("Parameter " ^ quote name ^ " must be assigned " ^
blanchet@35963
    57
                  space_implode " " (serial_commas "or" ss) ^ ".")
blanchet@35963
    58
         end
blanchet@35963
    59
blanchet@40341
    60
val has_junk =
wenzelm@40627
    61
  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
blanchet@40341
    62
blanchet@35963
    63
fun parse_time_option _ "none" = NONE
blanchet@35963
    64
  | parse_time_option name s =
blanchet@40341
    65
    let val secs = if has_junk s then NONE else Real.fromString s in
blanchet@43034
    66
      if is_none secs orelse Real.< (the secs, 0.0) then
blanchet@43034
    67
        error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
blanchet@40341
    68
               \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
blanchet@35963
    69
      else
blanchet@40341
    70
        SOME (seconds (the secs))
blanchet@35963
    71
    end
blanchet@35963
    72
blanchet@43029
    73
val subgoal_count = Try.subgoal_count
blanchet@38044
    74
blanchet@38696
    75
fun reserved_isar_keyword_table () =
blanchet@48292
    76
  Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
blanchet@38696
    77
blanchet@48251
    78
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
blanchet@48251
    79
   fixes that seem to be missing over there; or maybe the two code portions are
blanchet@48251
    80
   not doing the same? *)
blanchet@48251
    81
fun fold_body_thms thm_name f =
blanchet@48251
    82
  let
blanchet@48251
    83
    fun app n (PBody {thms, ...}) =
blanchet@48316
    84
      thms |> fold (fn (_, (name, _, body)) => fn accum =>
blanchet@48316
    85
          let
blanchet@48316
    86
            (* The second disjunct caters for the uncommon case where the proved
blanchet@48316
    87
               theorem occurs in its own proof (e.g.,
blanchet@48316
    88
               "Transitive_Closure.trancl_into_trancl"). *)
blanchet@48316
    89
            val no_name = (name = "" orelse (n = 1 andalso name = thm_name))
blanchet@48316
    90
            val accum =
blanchet@48316
    91
              accum |> (if n = 1 andalso not no_name then f name else I)
blanchet@48316
    92
            val n = n + (if no_name then 0 else 1)
blanchet@48316
    93
          in accum |> (if n <= 1 then app n (Future.join body) else I) end)
blanchet@48251
    94
  in fold (app 0) end
blanchet@48251
    95
blanchet@48251
    96
fun thms_in_proof all_names th =
blanchet@48251
    97
  let
blanchet@48316
    98
    val collect =
blanchet@48251
    99
      case all_names of
blanchet@50485
   100
        SOME names =>
blanchet@50485
   101
        (fn s => case Symtab.lookup names s of
blanchet@50485
   102
                   SOME s' => insert (op =) s'
blanchet@50485
   103
                 | NONE => I)
blanchet@48316
   104
      | NONE => insert (op =)
blanchet@48251
   105
    val names =
blanchet@48251
   106
      [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
blanchet@48251
   107
  in names end
blanchet@48251
   108
smolkas@50267
   109
fun thms_of_name ctxt name =
smolkas@50267
   110
  let
smolkas@50267
   111
    val lex = Keyword.get_lexicons
smolkas@50267
   112
    val get = maps (Proof_Context.get_fact ctxt o fst)
smolkas@50267
   113
  in
smolkas@50267
   114
    Source.of_string name
smolkas@50267
   115
    |> Symbol.source
smolkas@50267
   116
    |> Token.source {do_recover = SOME false} lex Position.start
smolkas@50267
   117
    |> Token.source_proper
smolkas@50267
   118
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
smolkas@50267
   119
    |> Source.exhaust
smolkas@50267
   120
  end
smolkas@50267
   121
blanchet@50048
   122
fun with_vanilla_print_mode f x =
blanchet@50048
   123
  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
blanchet@50048
   124
                           (print_mode_value ())) f x
blanchet@50048
   125
blanchet@35963
   126
end;