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