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