1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_util.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3
4General-purpose functions used by the Sledgehammer modules.
5*)
6
7signature SLEDGEHAMMER_UTIL =
8sig
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
27end;
28
29structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
30struct
31
32open ATP_Util
33
34val sledgehammerN = "sledgehammer"
35
36val log10_2 = Math.log10 2.0
37fun log2 n = Math.log10 n / log10_2
38
39fun app_hd f (x :: xs) = f x :: xs
40
41fun plural_s n = if n = 1 then "" else "s"
42
43val serial_commas = Try.serial_commas
44val simplify_spaces = strip_spaces false (K true)
45
46fun with_cleanup clean_up f x =
47  Exn.capture f x
48  |> tap (fn _ => clean_up x)
49  |> Exn.release
50
51fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
52
53fun 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
66val has_junk =
67  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
68
69fun 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
78val subgoal_count = Try.subgoal_count
79
80exception 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? *)
84fun 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
115fun 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 body))
121      handle TOO_MANY () => NONE
122    end)
123
124fun 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_Pos.explode (name, Position.start)
130    |> Token.tokenize keywords {strict = false}
131    |> filter Token.is_proper
132    |> Source.of_list
133    |> Source.source Token.stopper (Parse.thms1 >> get)
134    |> Source.exhaust
135  end
136
137val one_day = seconds (24.0 * 60.0 * 60.0)
138val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
139
140fun 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
146val spying_version = "d"
147
148fun 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
160end;
161