src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
author blanchet
Wed Dec 12 21:48:29 2012 +0100 (2012-12-12 ago)
changeset 50510 7e4f2f8d9b50
parent 50485 3c6ac2da2f45
child 50557 31313171deb5
permissions -rw-r--r--
export a pair of ML functions
     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 plural_s : int -> string
    11   val serial_commas : string -> string list -> string list
    12   val simplify_spaces : string -> string
    13   val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
    14   val infinite_timeout : Time.time
    15   val time_mult : real -> Time.time -> Time.time
    16   val parse_bool_option : bool -> string -> string -> bool option
    17   val parse_time_option : string -> string -> Time.time option
    18   val subgoal_count : Proof.state -> int
    19   val reserved_isar_keyword_table : unit -> unit Symtab.table
    20   val thms_in_proof : string Symtab.table option -> thm -> string list
    21   val thms_of_name : Proof.context -> string -> thm list
    22   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
    23 end;
    24 
    25 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    26 struct
    27 
    28 open ATP_Util
    29 
    30 val sledgehammerN = "sledgehammer"
    31 
    32 fun plural_s n = if n = 1 then "" else "s"
    33 
    34 val serial_commas = Try.serial_commas
    35 val simplify_spaces = strip_spaces false (K true)
    36 
    37 fun with_cleanup clean_up f x =
    38   Exn.capture f x
    39   |> tap (fn _ => clean_up x)
    40   |> Exn.release
    41 
    42 val infinite_timeout = seconds 31536000.0 (* one year *)
    43 
    44 fun time_mult k t =
    45   Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
    46 
    47 fun parse_bool_option option name s =
    48   (case s of
    49      "smart" => if option then NONE else raise Option
    50    | "false" => SOME false
    51    | "true" => SOME true
    52    | "" => SOME true
    53    | _ => raise Option)
    54   handle Option.Option =>
    55          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
    56            error ("Parameter " ^ quote name ^ " must be assigned " ^
    57                   space_implode " " (serial_commas "or" ss) ^ ".")
    58          end
    59 
    60 val has_junk =
    61   exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
    62 
    63 fun parse_time_option _ "none" = NONE
    64   | parse_time_option name s =
    65     let val secs = if has_junk s then NONE else Real.fromString s in
    66       if is_none secs orelse Real.< (the secs, 0.0) then
    67         error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
    68                \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
    69       else
    70         SOME (seconds (the secs))
    71     end
    72 
    73 val subgoal_count = Try.subgoal_count
    74 
    75 fun reserved_isar_keyword_table () =
    76   Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
    77 
    78 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    79    fixes that seem to be missing over there; or maybe the two code portions are
    80    not doing the same? *)
    81 fun fold_body_thms thm_name f =
    82   let
    83     fun app n (PBody {thms, ...}) =
    84       thms |> fold (fn (_, (name, _, body)) => fn accum =>
    85           let
    86             (* The second disjunct caters for the uncommon case where the proved
    87                theorem occurs in its own proof (e.g.,
    88                "Transitive_Closure.trancl_into_trancl"). *)
    89             val no_name = (name = "" orelse (n = 1 andalso name = thm_name))
    90             val accum =
    91               accum |> (if n = 1 andalso not no_name then f name else I)
    92             val n = n + (if no_name then 0 else 1)
    93           in accum |> (if n <= 1 then app n (Future.join body) else I) end)
    94   in fold (app 0) end
    95 
    96 fun thms_in_proof all_names th =
    97   let
    98     val collect =
    99       case all_names of
   100         SOME names =>
   101         (fn s => case Symtab.lookup names s of
   102                    SOME s' => insert (op =) s'
   103                  | NONE => I)
   104       | NONE => insert (op =)
   105     val names =
   106       [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
   107   in names end
   108 
   109 fun thms_of_name ctxt name =
   110   let
   111     val lex = Keyword.get_lexicons
   112     val get = maps (Proof_Context.get_fact ctxt o fst)
   113   in
   114     Source.of_string name
   115     |> Symbol.source
   116     |> Token.source {do_recover = SOME false} lex Position.start
   117     |> Token.source_proper
   118     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
   119     |> Source.exhaust
   120   end
   121 
   122 fun with_vanilla_print_mode f x =
   123   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   124                            (print_mode_value ())) f x
   125 
   126 end;