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