src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author wenzelm
Sat, 24 Jan 2015 21:36:21 +0100
changeset 59431 db440f97cf1a
parent 59058 a78612c67ec0
child 59433 9da5b2c61049
permissions -rw-r--r--
tuned message;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36062
194cb6e3c13f get rid of Polyhash, since it's no longer used
blanchet
parents: 35963
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_util.ML
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     3
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     4
General-purpose functions used by the Sledgehammer modules.
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     5
*)
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     6
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     7
signature SLEDGEHAMMER_UTIL =
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
     8
sig
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48383
diff changeset
     9
  val sledgehammerN : string
50608
5977de2993ac better weight functions for MePo/MaSh etc.
blanchet
parents: 50557
diff changeset
    10
  val log2 : real -> real
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51010
diff changeset
    11
  val app_hd : ('a -> 'a) -> 'a list -> 'a list
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36062
diff changeset
    12
  val plural_s : int -> string
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    13
  val serial_commas : string -> string list -> string list
38738
0ce517c1970f make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents: 38698
diff changeset
    14
  val simplify_spaces : string -> string
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48392
diff changeset
    15
  val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    16
  val time_mult : real -> Time.time -> Time.time
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    17
  val parse_bool_option : bool -> string -> string -> bool option
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    18
  val parse_time : string -> string -> Time.time
38044
463177795c49 minor refactoring
blanchet
parents: 38019
diff changeset
    19
  val subgoal_count : Proof.state -> int
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
    20
  val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
    21
    string list option
50267
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
    22
  val thms_of_name : Proof.context -> string -> thm list
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
    23
  val one_day : Time.time
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
    24
  val one_year : Time.time
50048
fb024bbf4b65 centralized term printing code
blanchet
parents: 48656
diff changeset
    25
  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
    26
  val hackish_string_of_term : Proof.context -> term -> string
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
    27
  val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    28
end;
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 38818
diff changeset
    29
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    30
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    31
struct
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    32
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43043
diff changeset
    33
open ATP_Util
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43043
diff changeset
    34
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48383
diff changeset
    35
val sledgehammerN = "sledgehammer"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48383
diff changeset
    36
50608
5977de2993ac better weight functions for MePo/MaSh etc.
blanchet
parents: 50557
diff changeset
    37
val log10_2 = Math.log10 2.0
5977de2993ac better weight functions for MePo/MaSh etc.
blanchet
parents: 50557
diff changeset
    38
fun log2 n = Math.log10 n / log10_2
5977de2993ac better weight functions for MePo/MaSh etc.
blanchet
parents: 50557
diff changeset
    39
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51010
diff changeset
    40
fun app_hd f (x :: xs) = f x :: xs
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51010
diff changeset
    41
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36062
diff changeset
    42
fun plural_s n = if n = 1 then "" else "s"
36062
194cb6e3c13f get rid of Polyhash, since it's no longer used
blanchet
parents: 35963
diff changeset
    43
43029
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43005
diff changeset
    44
val serial_commas = Try.serial_commas
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43043
diff changeset
    45
val simplify_spaces = strip_spaces false (K true)
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37575
diff changeset
    46
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48392
diff changeset
    47
fun with_cleanup clean_up f x =
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48392
diff changeset
    48
  Exn.capture f x
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48392
diff changeset
    49
  |> tap (fn _ => clean_up x)
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48392
diff changeset
    50
  |> Exn.release
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48392
diff changeset
    51
55212
blanchet
parents: 54821
diff changeset
    52
fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    53
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    54
fun parse_bool_option option name s =
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    55
  (case s of
51930
52fd62618631 prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents: 51181
diff changeset
    56
     "smart" => if option then NONE else raise Option.Option
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    57
   | "false" => SOME false
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    58
   | "true" => SOME true
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    59
   | "" => SOME true
51930
52fd62618631 prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents: 51181
diff changeset
    60
   | _ => raise Option.Option)
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    61
  handle Option.Option =>
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55223
diff changeset
    62
    let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55223
diff changeset
    63
      error ("Parameter " ^ quote name ^ " must be assigned " ^
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55223
diff changeset
    64
       space_implode " " (serial_commas "or" ss) ^ ".")
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55223
diff changeset
    65
    end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    66
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 39890
diff changeset
    67
val has_junk =
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 40341
diff changeset
    68
  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 39890
diff changeset
    69
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    70
fun parse_time name s =
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    71
  let val secs = if has_junk s then NONE else Real.fromString s in
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    72
    if is_none secs orelse Real.< (the secs, 0.0) then
59431
db440f97cf1a tuned message;
wenzelm
parents: 59058
diff changeset
    73
      error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55223
diff changeset
    74
        \(e.g., \"60\", \"0.5\") or \"none\".")
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    75
    else
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    76
      seconds (the secs)
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54695
diff changeset
    77
  end
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
    78
43029
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43005
diff changeset
    79
val subgoal_count = Try.subgoal_count
38044
463177795c49 minor refactoring
blanchet
parents: 38019
diff changeset
    80
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
    81
exception TOO_MANY of unit
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
    82
57108
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57055
diff changeset
    83
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57055
diff changeset
    84
   be missing over there; or maybe the two code portions are not doing the same? *)
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
    85
fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 46957
diff changeset
    86
  let
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
    87
    fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) =
54116
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    88
      let
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    89
        val (anonymous, enter_class) =
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    90
          (* The "name = outer_name" case caters for the uncommon case where the proved theorem
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    91
             occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    92
          if name = "" orelse name = outer_name then (true, false)
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    93
          else if map_inclass_name name = SOME outer_name then (true, true)
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    94
          else (false, false)
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    95
      in
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
    96
        if anonymous then
57756
92fe49c7ab3b peek instead of joining -- is perhaps less risky
blanchet
parents: 57727
diff changeset
    97
          (case Future.peek body of
92fe49c7ab3b peek instead of joining -- is perhaps less risky
blanchet
parents: 57727
diff changeset
    98
            SOME (Exn.Res the_body) =>
92fe49c7ab3b peek instead of joining -- is perhaps less risky
blanchet
parents: 57727
diff changeset
    99
            app_body (if enter_class then map_inclass_name else map_name) the_body accum
92fe49c7ab3b peek instead of joining -- is perhaps less risky
blanchet
parents: 57727
diff changeset
   100
          | NONE => accum)
54116
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
   101
        else
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   102
          (case map_name name of
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   103
            SOME name' =>
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   104
            if member (op =) names name' then accum
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   105
            else if num_thms = max_thms then raise TOO_MANY ()
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   106
            else (num_thms + 1, name' :: names)
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   107
          | NONE => accum)
54116
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
   108
      end
ba709c934470 made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
blanchet
parents: 54062
diff changeset
   109
    and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
57108
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57055
diff changeset
   110
  in
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   111
    snd (app_body map_plain_name body (0, []))
57108
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57055
diff changeset
   112
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 46957
diff changeset
   113
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57108
diff changeset
   114
fun thms_in_proof max_thms name_tabs th =
57838
c21f2c52f54b careful when calling 'Thm.proof_body_of' -- it can throw exceptions
blanchet
parents: 57306
diff changeset
   115
  (case try Thm.proof_body_of th of
c21f2c52f54b careful when calling 'Thm.proof_body_of' -- it can throw exceptions
blanchet
parents: 57306
diff changeset
   116
    NONE => NONE
c21f2c52f54b careful when calling 'Thm.proof_body_of' -- it can throw exceptions
blanchet
parents: 57306
diff changeset
   117
  | SOME body =>
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58928
diff changeset
   118
    let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
57838
c21f2c52f54b careful when calling 'Thm.proof_body_of' -- it can throw exceptions
blanchet
parents: 57306
diff changeset
   119
      SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
c21f2c52f54b careful when calling 'Thm.proof_body_of' -- it can throw exceptions
blanchet
parents: 57306
diff changeset
   120
      handle TOO_MANY () => NONE
c21f2c52f54b careful when calling 'Thm.proof_body_of' -- it can throw exceptions
blanchet
parents: 57306
diff changeset
   121
    end)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 46957
diff changeset
   122
50267
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   123
fun thms_of_name ctxt name =
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   124
  let
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   125
    val get = maps (Proof_Context.get_fact ctxt o fst)
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58919
diff changeset
   126
    val keywords = Thy_Header.get_keywords' ctxt
50267
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   127
  in
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   128
    Source.of_string name
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   129
    |> Symbol.source
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
   130
    |> Token.source keywords Position.start
50267
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   131
    |> Token.source_proper
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   132
    |> Source.source Token.stopper (Parse.xthms1 >> get)
50267
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   133
    |> Source.exhaust
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   134
  end
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 50049
diff changeset
   135
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   136
val one_day = seconds (24.0 * 60.0 * 60.0)
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   137
val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   138
50048
fb024bbf4b65 centralized term printing code
blanchet
parents: 48656
diff changeset
   139
fun with_vanilla_print_mode f x =
54821
blanchet
parents: 54816
diff changeset
   140
  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
50048
fb024bbf4b65 centralized term printing code
blanchet
parents: 48656
diff changeset
   141
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   142
fun hackish_string_of_term ctxt =
57727
02a53c1bbb6c generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
blanchet
parents: 57306
diff changeset
   143
  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> unyxml #> simplify_spaces
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   144
57727
02a53c1bbb6c generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
blanchet
parents: 57306
diff changeset
   145
val spying_version = "d"
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   146
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   147
fun spying false _ = ()
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   148
  | spying true f =
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   149
    let
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   150
      val (state, i, tool, message) = f ()
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   151
      val ctxt = Proof.context_of state
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   152
      val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   153
      val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   154
    in
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   155
      File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   156
        (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   157
    end
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53800
diff changeset
   158
35963
943e2582dc87 added options to Sledgehammer;
blanchet
parents:
diff changeset
   159
end;