src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54116 ba709c934470
child 54695 a9efdf970720
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
     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 infinite_timeout : Time.time
    17   val time_mult : real -> Time.time -> Time.time
    18   val parse_bool_option : bool -> string -> string -> bool option
    19   val parse_time_option : string -> string -> Time.time option
    20   val subgoal_count : Proof.state -> int
    21   val reserved_isar_keyword_table : unit -> unit Symtab.table
    22   val thms_in_proof :
    23     (string Symtab.table * string Symtab.table) option -> thm -> string list
    24   val thms_of_name : Proof.context -> string -> thm list
    25   val one_day : Time.time
    26   val one_year : Time.time
    27   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
    28   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
    29   val hackish_string_of_term : Proof.context -> term -> string
    30   val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
    31 
    32   (** extrema **)
    33   val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
    34   val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
    35   val max_list : ('a * 'a -> order) -> 'a list -> 'a option
    36 end;
    37 
    38 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    39 struct
    40 
    41 open ATP_Util
    42 
    43 val sledgehammerN = "sledgehammer"
    44 
    45 val log10_2 = Math.log10 2.0
    46 
    47 fun log2 n = Math.log10 n / log10_2
    48 
    49 fun app_hd f (x :: xs) = f x :: xs
    50 
    51 fun plural_s n = if n = 1 then "" else "s"
    52 
    53 val serial_commas = Try.serial_commas
    54 val simplify_spaces = strip_spaces false (K true)
    55 
    56 fun with_cleanup clean_up f x =
    57   Exn.capture f x
    58   |> tap (fn _ => clean_up x)
    59   |> Exn.release
    60 
    61 val infinite_timeout = seconds 31536000.0 (* one year *)
    62 
    63 fun time_mult k t =
    64   Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
    65 
    66 fun parse_bool_option option name s =
    67   (case s of
    68      "smart" => if option then NONE else raise Option.Option
    69    | "false" => SOME false
    70    | "true" => SOME true
    71    | "" => SOME true
    72    | _ => raise Option.Option)
    73   handle Option.Option =>
    74          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
    75            error ("Parameter " ^ quote name ^ " must be assigned " ^
    76                   space_implode " " (serial_commas "or" ss) ^ ".")
    77          end
    78 
    79 val has_junk =
    80   exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
    81 
    82 fun parse_time_option _ "none" = NONE
    83   | parse_time_option name s =
    84     let val secs = if has_junk s then NONE else Real.fromString s in
    85       if is_none secs orelse Real.< (the secs, 0.0) then
    86         error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
    87                \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
    88       else
    89         SOME (seconds (the secs))
    90     end
    91 
    92 val subgoal_count = Try.subgoal_count
    93 
    94 fun reserved_isar_keyword_table () =
    95   Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
    96 
    97 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    98    fixes that seem to be missing over there; or maybe the two code portions are
    99    not doing the same? *)
   100 fun fold_body_thm outer_name (map_plain_name, map_inclass_name) =
   101   let
   102     fun app_thm map_name (_, (name, _, body)) accum =
   103       let
   104         val (anonymous, enter_class) =
   105           (* The "name = outer_name" case caters for the uncommon case where the proved theorem
   106              occurs in its own proof (e.g., "Transitive_Closure.trancl_into_trancl"). *)
   107           if name = "" orelse name = outer_name then (true, false)
   108           else if map_inclass_name name = SOME outer_name then (true, true)
   109           else (false, false)
   110       in
   111         if anonymous then
   112           accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body)
   113         else
   114           accum |> union (op =) (the_list (map_name name))
   115       end
   116     and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
   117   in app_body map_plain_name end
   118 
   119 fun thms_in_proof name_tabs th =
   120   let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
   121     fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) []
   122   end
   123 
   124 fun thms_of_name ctxt name =
   125   let
   126     val lex = Keyword.get_lexicons
   127     val get = maps (Proof_Context.get_fact ctxt o fst)
   128   in
   129     Source.of_string name
   130     |> Symbol.source
   131     |> Token.source {do_recover = SOME false} lex Position.start
   132     |> Token.source_proper
   133     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
   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 time_limit NONE = I
   141   | time_limit (SOME delay) = TimeLimit.timeLimit delay
   142 
   143 fun with_vanilla_print_mode f x =
   144   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   145                            (print_mode_value ())) f x
   146 
   147 fun hackish_string_of_term ctxt =
   148   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   149 
   150 val spying_version = "c"
   151 
   152 fun spying false _ = ()
   153   | spying true f =
   154     let
   155       val (state, i, tool, message) = f ()
   156       val ctxt = Proof.context_of state
   157       val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i
   158       val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12)
   159     in
   160       File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer")
   161         (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
   162     end
   163 
   164 (** extrema **)
   165 
   166 fun max ord x y = case ord(x,y) of LESS => y | _ => x
   167 
   168 fun max_option ord = max (option_ord ord)
   169 
   170 fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
   171 
   172 end;