more refactoring
authorblanchet
Tue Jul 27 18:33:10 2010 +0200 (2010-07-27)
changeset 38023962b0a7f544b
parent 38022 d9c4d87838f3
child 38024 e4a95eb5530e
more refactoring
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:58:30 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 18:33:10 2010 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4    ("Tools/ATP_Manager/atp_problem.ML")
     1.5    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
     1.6    ("Tools/ATP_Manager/async_manager.ML")
     1.7 -  ("Tools/ATP_Manager/atp_manager.ML")
     1.8    ("Tools/ATP_Manager/atp_systems.ML")
     1.9 +  ("Tools/Sledgehammer/sledgehammer.ML")
    1.10    ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    1.11    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.12  begin
    1.13 @@ -97,9 +97,10 @@
    1.14  use "Tools/ATP_Manager/atp_problem.ML"
    1.15  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.16  use "Tools/ATP_Manager/async_manager.ML"
    1.17 -use "Tools/Sledgehammer/sledgehammer.ML"
    1.18  use "Tools/ATP_Manager/atp_systems.ML"
    1.19  setup ATP_Systems.setup
    1.20 +use "Tools/Sledgehammer/sledgehammer.ML"
    1.21 +setup Sledgehammer.setup
    1.22  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    1.23  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.24  setup Metis_Tactics.setup
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:58:30 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 18:33:10 2010 +0200
     2.3 @@ -7,9 +7,23 @@
     2.4  
     2.5  signature ATP_SYSTEMS =
     2.6  sig
     2.7 -  val dest_dir : string Config.T
     2.8 -  val problem_prefix : string Config.T
     2.9 -  val measure_runtime : bool Config.T
    2.10 +  datatype failure =
    2.11 +    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
    2.12 +    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
    2.13 +
    2.14 +  type prover_config =
    2.15 +    {home_var: string,
    2.16 +     executable: string,
    2.17 +     arguments: bool -> Time.time -> string,
    2.18 +     proof_delims: (string * string) list,
    2.19 +     known_failures: (failure * string) list,
    2.20 +     max_new_relevant_facts_per_iter: int,
    2.21 +     prefers_theory_relevant: bool,
    2.22 +     explicit_forall: bool}
    2.23 +
    2.24 +  val add_prover: string * prover_config -> theory -> theory
    2.25 +  val get_prover: theory -> string -> prover_config
    2.26 +  val available_atps: theory -> unit
    2.27    val refresh_systems_on_tptp : unit -> unit
    2.28    val default_atps_param_value : unit -> string
    2.29    val setup : theory -> theory
    2.30 @@ -18,28 +32,11 @@
    2.31  structure ATP_Systems : ATP_SYSTEMS =
    2.32  struct
    2.33  
    2.34 -open Metis_Clauses
    2.35 -open Sledgehammer_Util
    2.36 -open Sledgehammer_Fact_Filter
    2.37 -open ATP_Problem
    2.38 -open Sledgehammer_Proof_Reconstruct
    2.39 -open Sledgehammer
    2.40 -
    2.41 -(** generic ATP **)
    2.42 -
    2.43 -(* external problem files *)
    2.44 +(* prover configuration *)
    2.45  
    2.46 -val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    2.47 -  (*Empty string means create files in Isabelle's temporary files directory.*)
    2.48 -
    2.49 -val (problem_prefix, problem_prefix_setup) =
    2.50 -  Attrib.config_string "atp_problem_prefix" (K "prob");
    2.51 -
    2.52 -val (measure_runtime, measure_runtime_setup) =
    2.53 -  Attrib.config_bool "atp_measure_runtime" (K false);
    2.54 -
    2.55 -
    2.56 -(* prover configuration *)
    2.57 +datatype failure =
    2.58 +  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
    2.59 +  OldSpass | MalformedInput | MalformedOutput | UnknownError
    2.60  
    2.61  type prover_config =
    2.62    {home_var: string,
    2.63 @@ -52,728 +49,32 @@
    2.64     explicit_forall: bool}
    2.65  
    2.66  
    2.67 -(* basic template *)
    2.68 -
    2.69 -val remotify = prefix "remote_"
    2.70 -
    2.71 -fun with_path cleanup after f path =
    2.72 -  Exn.capture f path
    2.73 -  |> tap (fn _ => cleanup path)
    2.74 -  |> Exn.release
    2.75 -  |> tap (after path)
    2.76 -
    2.77 -(* Splits by the first possible of a list of delimiters. *)
    2.78 -fun extract_proof delims output =
    2.79 -  case pairself (find_first (fn s => String.isSubstring s output))
    2.80 -                (ListPair.unzip delims) of
    2.81 -    (SOME begin_delim, SOME end_delim) =>
    2.82 -    (output |> first_field begin_delim |> the |> snd
    2.83 -            |> first_field end_delim |> the |> fst
    2.84 -            |> first_field "\n" |> the |> snd
    2.85 -     handle Option.Option => "")
    2.86 -  | _ => ""
    2.87 -
    2.88 -fun extract_proof_and_outcome complete res_code proof_delims known_failures
    2.89 -                              output =
    2.90 -  case map_filter (fn (failure, pattern) =>
    2.91 -                      if String.isSubstring pattern output then SOME failure
    2.92 -                      else NONE) known_failures of
    2.93 -    [] => (case extract_proof proof_delims output of
    2.94 -             "" => ("", SOME UnknownError)
    2.95 -           | proof => if res_code = 0 then (proof, NONE)
    2.96 -                      else ("", SOME UnknownError))
    2.97 -  | (failure :: _) =>
    2.98 -    ("", SOME (if failure = IncompleteUnprovable andalso complete then
    2.99 -                 Unprovable
   2.100 -               else
   2.101 -                 failure))
   2.102 -
   2.103 -fun string_for_failure Unprovable = "The ATP problem is unprovable."
   2.104 -  | string_for_failure IncompleteUnprovable =
   2.105 -    "The ATP cannot prove the problem."
   2.106 -  | string_for_failure CantConnect = "Can't connect to remote ATP."
   2.107 -  | string_for_failure TimedOut = "Timed out."
   2.108 -  | string_for_failure OutOfResources = "The ATP ran out of resources."
   2.109 -  | string_for_failure OldSpass =
   2.110 -    (* FIXME: Change the error message below to point to the Isabelle download
   2.111 -       page once the package is there. *)
   2.112 -    "Warning: Sledgehammer requires a more recent version of SPASS with \
   2.113 -    \support for the TPTP syntax. To install it, download and untar the \
   2.114 -    \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
   2.115 -    \\"spass-3.7\" directory's full path to \"" ^
   2.116 -    Path.implode (Path.expand (Path.appends
   2.117 -        (Path.variable "ISABELLE_HOME_USER" ::
   2.118 -         map Path.basic ["etc", "components"]))) ^
   2.119 -    "\" on a line of its own."
   2.120 -  | string_for_failure MalformedInput =
   2.121 -    "Internal Sledgehammer error: The ATP problem is malformed. Please report \
   2.122 -    \this to the Isabelle developers."
   2.123 -  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   2.124 -  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
   2.125 -
   2.126 -
   2.127 -(* Clause preparation *)
   2.128 -
   2.129 -datatype fol_formula =
   2.130 -  FOLFormula of {formula_name: string,
   2.131 -                 kind: kind,
   2.132 -                 combformula: (name, combterm) formula,
   2.133 -                 ctypes_sorts: typ list}
   2.134 -
   2.135 -fun mk_anot phi = AConn (ANot, [phi])
   2.136 -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   2.137 -fun mk_ahorn [] phi = phi
   2.138 -  | mk_ahorn (phi :: phis) psi =
   2.139 -    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   2.140 -
   2.141 -(* ### FIXME: reintroduce
   2.142 -fun make_clause_table xs =
   2.143 -  fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
   2.144 -(* Remove existing axiom clauses from the conjecture clauses, as this can
   2.145 -   dramatically boost an ATP's performance (for some reason). *)
   2.146 -fun subtract_cls ax_clauses =
   2.147 -  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   2.148 -*)
   2.149 -
   2.150 -fun combformula_for_prop thy =
   2.151 -  let
   2.152 -    val do_term = combterm_from_term thy
   2.153 -    fun do_quant bs q s T t' =
   2.154 -      do_formula ((s, T) :: bs) t'
   2.155 -      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   2.156 -    and do_conn bs c t1 t2 =
   2.157 -      do_formula bs t1 ##>> do_formula bs t2
   2.158 -      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   2.159 -    and do_formula bs t =
   2.160 -      case t of
   2.161 -        @{const Not} $ t1 =>
   2.162 -        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   2.163 -      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   2.164 -        do_quant bs AForall s T t'
   2.165 -      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   2.166 -        do_quant bs AExists s T t'
   2.167 -      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
   2.168 -      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
   2.169 -      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
   2.170 -      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   2.171 -        do_conn bs AIff t1 t2
   2.172 -      | _ => (fn ts => do_term bs (Envir.eta_contract t)
   2.173 -                       |>> APred ||> union (op =) ts)
   2.174 -  in do_formula [] end
   2.175 -
   2.176 -(* Converts an elim-rule into an equivalent theorem that does not have the
   2.177 -   predicate variable. Leaves other theorems unchanged. We simply instantiate
   2.178 -   the conclusion variable to False. (Cf. "transform_elim_term" in
   2.179 -   "ATP_Systems".) *)
   2.180 -(* FIXME: test! *)
   2.181 -fun transform_elim_term t =
   2.182 -  case Logic.strip_imp_concl t of
   2.183 -    @{const Trueprop} $ Var (z, @{typ bool}) =>
   2.184 -    subst_Vars [(z, @{const True})] t
   2.185 -  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
   2.186 -  | _ => t
   2.187 -
   2.188 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
   2.189 -   (Cf. "extensionalize_theorem" in "Clausifier".) *)
   2.190 -fun extensionalize_term t =
   2.191 -  let
   2.192 -    fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
   2.193 -               $ t2 $ Abs (s, var_T, t')) =
   2.194 -        let val var_t = Var (("x", j), var_T) in
   2.195 -          Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
   2.196 -            $ betapply (t2, var_t) $ subst_bound (var_t, t')
   2.197 -          |> aux (j + 1)
   2.198 -        end
   2.199 -      | aux _ t = t
   2.200 -  in aux (maxidx_of_term t + 1) t end
   2.201 -
   2.202 -(* FIXME: Guarantee freshness *)
   2.203 -fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
   2.204 -fun conceal_bounds Ts t =
   2.205 -  subst_bounds (map (Free o apfst concealed_bound_name)
   2.206 -                    (length Ts - 1 downto 0 ~~ rev Ts), t)
   2.207 -fun reveal_bounds Ts =
   2.208 -  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   2.209 -                    (0 upto length Ts - 1 ~~ Ts))
   2.210 +(* named provers *)
   2.211  
   2.212 -fun introduce_combinators_in_term ctxt kind t =
   2.213 -  let
   2.214 -    val thy = ProofContext.theory_of ctxt
   2.215 -    fun aux Ts t =
   2.216 -      case t of
   2.217 -        @{const Not} $ t1 => @{const Not} $ aux Ts t1
   2.218 -      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   2.219 -        t0 $ Abs (s, T, aux (T :: Ts) t')
   2.220 -      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   2.221 -        t0 $ Abs (s, T, aux (T :: Ts) t')
   2.222 -      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   2.223 -      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   2.224 -      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   2.225 -      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   2.226 -          $ t1 $ t2 =>
   2.227 -        t0 $ aux Ts t1 $ aux Ts t2
   2.228 -      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   2.229 -               t
   2.230 -             else
   2.231 -               let
   2.232 -                 val t = t |> conceal_bounds Ts
   2.233 -                           |> Envir.eta_contract
   2.234 -                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
   2.235 -               in
   2.236 -                 t |> cterm_of thy
   2.237 -                   |> Clausifier.introduce_combinators_in_cterm
   2.238 -                   |> singleton (Variable.export ctxt' ctxt)
   2.239 -                   |> prop_of |> Logic.dest_equals |> snd
   2.240 -                   |> reveal_bounds Ts
   2.241 -               end
   2.242 -  in t |> not (Meson.is_fol_term thy t) ? aux [] end
   2.243 -  handle THM _ =>
   2.244 -         (* A type variable of sort "{}" will make abstraction fail. *)
   2.245 -         case kind of
   2.246 -           Axiom => HOLogic.true_const
   2.247 -         | Conjecture => HOLogic.false_const
   2.248 -
   2.249 -(* making axiom and conjecture clauses *)
   2.250 -fun make_clause ctxt (formula_name, kind, t) =
   2.251 -  let
   2.252 -    val thy = ProofContext.theory_of ctxt
   2.253 -    (* ### FIXME: perform other transformations previously done by
   2.254 -       "Clausifier.to_nnf", e.g. "HOL.If" *)
   2.255 -    val t = t |> transform_elim_term
   2.256 -              |> Object_Logic.atomize_term thy
   2.257 -              |> extensionalize_term
   2.258 -              |> introduce_combinators_in_term ctxt kind
   2.259 -    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   2.260 -  in
   2.261 -    FOLFormula {formula_name = formula_name, combformula = combformula,
   2.262 -                kind = kind, ctypes_sorts = ctypes_sorts}
   2.263 -  end
   2.264 -
   2.265 -fun make_axiom_clause ctxt (name, th) =
   2.266 -  (name, make_clause ctxt (name, Axiom, prop_of th))
   2.267 -fun make_conjecture_clauses ctxt ts =
   2.268 -  map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
   2.269 -       (0 upto length ts - 1) ts
   2.270 -
   2.271 -(** Helper clauses **)
   2.272 -
   2.273 -fun count_combterm (CombConst ((s, _), _, _)) =
   2.274 -    Symtab.map_entry s (Integer.add 1)
   2.275 -  | count_combterm (CombVar _) = I
   2.276 -  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   2.277 -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   2.278 -  | count_combformula (AConn (_, phis)) = fold count_combformula phis
   2.279 -  | count_combformula (APred tm) = count_combterm tm
   2.280 -fun count_fol_formula (FOLFormula {combformula, ...}) =
   2.281 -  count_combformula combformula
   2.282 -
   2.283 -val optional_helpers =
   2.284 -  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
   2.285 -   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
   2.286 -   (["c_COMBS"], @{thms COMBS_def})]
   2.287 -val optional_typed_helpers =
   2.288 -  [(["c_True", "c_False"], @{thms True_or_False}),
   2.289 -   (["c_If"], @{thms if_True if_False True_or_False})]
   2.290 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   2.291 -
   2.292 -val init_counters =
   2.293 -  Symtab.make (maps (maps (map (rpair 0) o fst))
   2.294 -                    [optional_helpers, optional_typed_helpers])
   2.295 -
   2.296 -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
   2.297 -  let
   2.298 -    val ct = fold (fold count_fol_formula) [conjectures, axclauses]
   2.299 -                  init_counters
   2.300 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   2.301 -    val cnfs =
   2.302 -      (optional_helpers
   2.303 -       |> full_types ? append optional_typed_helpers
   2.304 -       |> maps (fn (ss, ths) =>
   2.305 -                   if exists is_needed ss then map (`Thm.get_name_hint) ths
   2.306 -                   else [])) @
   2.307 -      (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   2.308 -  in map (snd o make_axiom_clause ctxt) cnfs end
   2.309 -
   2.310 -fun s_not (@{const Not} $ t) = t
   2.311 -  | s_not t = @{const Not} $ t
   2.312 -
   2.313 -(* prepare for passing to writer,
   2.314 -   create additional clauses based on the information from extra_cls *)
   2.315 -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
   2.316 -  let
   2.317 -    val thy = ProofContext.theory_of ctxt
   2.318 -    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   2.319 -    val is_FO = Meson.is_fol_term thy goal_t
   2.320 -    val axtms = map (prop_of o snd) extra_cls
   2.321 -    val subs = tfree_classes_of_terms [goal_t]
   2.322 -    val supers = tvar_classes_of_terms axtms
   2.323 -    val tycons = type_consts_of_terms thy (goal_t :: axtms)
   2.324 -    (* TFrees in conjecture clauses; TVars in axiom clauses *)
   2.325 -    val conjectures =
   2.326 -      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
   2.327 -        [HOLogic.dest_Trueprop concl_t]
   2.328 -      |> make_conjecture_clauses ctxt
   2.329 -    val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
   2.330 -    val (clnames, axiom_clauses) =
   2.331 -      ListPair.unzip (map (make_axiom_clause ctxt) axcls)
   2.332 -    (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
   2.333 -       "get_helper_clauses" call? *)
   2.334 -    val helper_clauses =
   2.335 -      get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
   2.336 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   2.337 -    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   2.338 -  in
   2.339 -    (Vector.fromList clnames,
   2.340 -      (conjectures, axiom_clauses, extra_clauses, helper_clauses,
   2.341 -       class_rel_clauses, arity_clauses))
   2.342 -  end
   2.343 -
   2.344 -val axiom_prefix = "ax_"
   2.345 -val conjecture_prefix = "conj_"
   2.346 -val arity_clause_prefix = "clsarity_"
   2.347 -val tfrees_name = "tfrees"
   2.348 -
   2.349 -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   2.350 -
   2.351 -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   2.352 -  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   2.353 -  | fo_term_for_combtyp (CombType (name, tys)) =
   2.354 -    ATerm (name, map fo_term_for_combtyp tys)
   2.355 -
   2.356 -fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   2.357 -    (true, ATerm (class, [ATerm (name, [])]))
   2.358 -  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   2.359 -    (true, ATerm (class, [ATerm (name, [])]))
   2.360 -
   2.361 -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
   2.362 -
   2.363 -fun fo_term_for_combterm full_types =
   2.364 -  let
   2.365 -    fun aux top_level u =
   2.366 -      let
   2.367 -        val (head, args) = strip_combterm_comb u
   2.368 -        val (x, ty_args) =
   2.369 -          case head of
   2.370 -            CombConst (name, _, ty_args) =>
   2.371 -            if fst name = "equal" then
   2.372 -              (if top_level andalso length args = 2 then name
   2.373 -               else ("c_fequal", @{const_name fequal}), [])
   2.374 -            else
   2.375 -              (name, if full_types then [] else ty_args)
   2.376 -          | CombVar (name, _) => (name, [])
   2.377 -          | CombApp _ => raise Fail "impossible \"CombApp\""
   2.378 -        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   2.379 -                          map (aux false) args)
   2.380 -    in
   2.381 -      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   2.382 -    end
   2.383 -  in aux true end
   2.384 -
   2.385 -fun formula_for_combformula full_types =
   2.386 -  let
   2.387 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   2.388 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   2.389 -      | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
   2.390 -  in aux end
   2.391 -
   2.392 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
   2.393 -  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   2.394 -                (type_literals_for_types ctypes_sorts))
   2.395 -           (formula_for_combformula full_types combformula)
   2.396 -
   2.397 -fun problem_line_for_axiom full_types
   2.398 -        (formula as FOLFormula {formula_name, kind, ...}) =
   2.399 -  Fof (axiom_prefix ^ ascii_of formula_name, kind,
   2.400 -       formula_for_axiom full_types formula)
   2.401 -
   2.402 -fun problem_line_for_class_rel_clause
   2.403 -        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
   2.404 -  let val ty_arg = ATerm (("T", "T"), []) in
   2.405 -    Fof (ascii_of axiom_name, Axiom,
   2.406 -         AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
   2.407 -                           APred (ATerm (superclass, [ty_arg]))]))
   2.408 -  end
   2.409 -
   2.410 -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   2.411 -    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   2.412 -  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   2.413 -    (false, ATerm (c, [ATerm (sort, [])]))
   2.414 -
   2.415 -fun problem_line_for_arity_clause
   2.416 -        (ArityClause {axiom_name, conclLit, premLits, ...}) =
   2.417 -  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
   2.418 -       mk_ahorn (map (formula_for_fo_literal o apfst not
   2.419 -                      o fo_literal_for_arity_literal) premLits)
   2.420 -                (formula_for_fo_literal
   2.421 -                     (fo_literal_for_arity_literal conclLit)))
   2.422 -
   2.423 -fun problem_line_for_conjecture full_types
   2.424 -        (FOLFormula {formula_name, kind, combformula, ...}) =
   2.425 -  Fof (conjecture_prefix ^ formula_name, kind,
   2.426 -       formula_for_combformula full_types combformula)
   2.427 +structure Data = Theory_Data
   2.428 +(
   2.429 +  type T = (prover_config * stamp) Symtab.table
   2.430 +  val empty = Symtab.empty
   2.431 +  val extend = I
   2.432 +  fun merge data : T = Symtab.merge (eq_snd op =) data
   2.433 +    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   2.434 +)
   2.435  
   2.436 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   2.437 -  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   2.438 -
   2.439 -fun problem_line_for_free_type lit =
   2.440 -  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
   2.441 -fun problem_lines_for_free_types conjectures =
   2.442 -  let
   2.443 -    val litss = map free_type_literals_for_conjecture conjectures
   2.444 -    val lits = fold (union (op =)) litss []
   2.445 -  in map problem_line_for_free_type lits end
   2.446 -
   2.447 -(** "hBOOL" and "hAPP" **)
   2.448 -
   2.449 -type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   2.450 -
   2.451 -fun consider_term top_level (ATerm ((s, _), ts)) =
   2.452 -  (if is_tptp_variable s then
   2.453 -     I
   2.454 -   else
   2.455 -     let val n = length ts in
   2.456 -       Symtab.map_default
   2.457 -           (s, {min_arity = n, max_arity = 0, sub_level = false})
   2.458 -           (fn {min_arity, max_arity, sub_level} =>
   2.459 -               {min_arity = Int.min (n, min_arity),
   2.460 -                max_arity = Int.max (n, max_arity),
   2.461 -                sub_level = sub_level orelse not top_level})
   2.462 -     end)
   2.463 -  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   2.464 -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   2.465 -  | consider_formula (AConn (_, phis)) = fold consider_formula phis
   2.466 -  | consider_formula (APred tm) = consider_term true tm
   2.467 -
   2.468 -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   2.469 -fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   2.470 -
   2.471 -fun const_table_for_problem explicit_apply problem =
   2.472 -  if explicit_apply then NONE
   2.473 -  else SOME (Symtab.empty |> consider_problem problem)
   2.474 -
   2.475 -val tc_fun = make_fixed_type_const @{type_name fun}
   2.476 -
   2.477 -fun min_arity_of thy full_types NONE s =
   2.478 -    (if s = "equal" orelse s = type_wrapper_name orelse
   2.479 -        String.isPrefix type_const_prefix s orelse
   2.480 -        String.isPrefix class_prefix s then
   2.481 -       16383 (* large number *)
   2.482 -     else if full_types then
   2.483 -       0
   2.484 -     else case strip_prefix_and_undo_ascii const_prefix s of
   2.485 -       SOME s' => num_type_args thy (invert_const s')
   2.486 -     | NONE => 0)
   2.487 -  | min_arity_of _ _ (SOME the_const_tab) s =
   2.488 -    case Symtab.lookup the_const_tab s of
   2.489 -      SOME ({min_arity, ...} : const_info) => min_arity
   2.490 -    | NONE => 0
   2.491 -
   2.492 -fun full_type_of (ATerm ((s, _), [ty, _])) =
   2.493 -    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   2.494 -  | full_type_of _ = raise Fail "expected type wrapper"
   2.495 -
   2.496 -fun list_hAPP_rev _ t1 [] = t1
   2.497 -  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   2.498 -    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   2.499 -  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   2.500 -    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   2.501 -                         [full_type_of t2, ty]) in
   2.502 -      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   2.503 -    end
   2.504 -
   2.505 -fun repair_applications_in_term thy full_types const_tab =
   2.506 -  let
   2.507 -    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   2.508 -      if s = type_wrapper_name then
   2.509 -        case ts of
   2.510 -          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   2.511 -        | _ => raise Fail "malformed type wrapper"
   2.512 -      else
   2.513 -        let
   2.514 -          val ts = map (aux NONE) ts
   2.515 -          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   2.516 -        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   2.517 -  in aux NONE end
   2.518 -
   2.519 -fun boolify t = ATerm (`I "hBOOL", [t])
   2.520 +fun add_prover (name, config) thy =
   2.521 +  Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   2.522 +  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   2.523  
   2.524 -(* True if the constant ever appears outside of the top-level position in
   2.525 -   literals, or if it appears with different arities (e.g., because of different
   2.526 -   type instantiations). If false, the constant always receives all of its
   2.527 -   arguments and is used as a predicate. *)
   2.528 -fun is_predicate NONE s =
   2.529 -    s = "equal" orelse String.isPrefix type_const_prefix s orelse
   2.530 -    String.isPrefix class_prefix s
   2.531 -  | is_predicate (SOME the_const_tab) s =
   2.532 -    case Symtab.lookup the_const_tab s of
   2.533 -      SOME {min_arity, max_arity, sub_level} =>
   2.534 -      not sub_level andalso min_arity = max_arity
   2.535 -    | NONE => false
   2.536 -
   2.537 -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   2.538 -  if s = type_wrapper_name then
   2.539 -    case ts of
   2.540 -      [_, t' as ATerm ((s', _), _)] =>
   2.541 -      if is_predicate const_tab s' then t' else boolify t
   2.542 -    | _ => raise Fail "malformed type wrapper"
   2.543 -  else
   2.544 -    t |> not (is_predicate const_tab s) ? boolify
   2.545 -
   2.546 -fun close_universally phi =
   2.547 -  let
   2.548 -    fun term_vars bounds (ATerm (name as (s, _), tms)) =
   2.549 -        (is_tptp_variable s andalso not (member (op =) bounds name))
   2.550 -          ? insert (op =) name
   2.551 -        #> fold (term_vars bounds) tms
   2.552 -    fun formula_vars bounds (AQuant (q, xs, phi)) =
   2.553 -        formula_vars (xs @ bounds) phi
   2.554 -      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   2.555 -      | formula_vars bounds (APred tm) = term_vars bounds tm
   2.556 -  in
   2.557 -    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   2.558 -  end
   2.559 -
   2.560 -fun repair_formula thy explicit_forall full_types const_tab =
   2.561 -  let
   2.562 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   2.563 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   2.564 -      | aux (APred tm) =
   2.565 -        APred (tm |> repair_applications_in_term thy full_types const_tab
   2.566 -                  |> repair_predicates_in_term const_tab)
   2.567 -  in aux #> explicit_forall ? close_universally end
   2.568 -
   2.569 -fun repair_problem_line thy explicit_forall full_types const_tab
   2.570 -                        (Fof (ident, kind, phi)) =
   2.571 -  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   2.572 -fun repair_problem_with_const_table thy =
   2.573 -  map o apsnd o map ooo repair_problem_line thy
   2.574 -
   2.575 -fun repair_problem thy explicit_forall full_types explicit_apply problem =
   2.576 -  repair_problem_with_const_table thy explicit_forall full_types
   2.577 -      (const_table_for_problem explicit_apply problem) problem
   2.578 -
   2.579 -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
   2.580 -                    file (conjectures, axiom_clauses, extra_clauses,
   2.581 -                          helper_clauses, class_rel_clauses, arity_clauses) =
   2.582 -  let
   2.583 -    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
   2.584 -    val class_rel_lines =
   2.585 -      map problem_line_for_class_rel_clause class_rel_clauses
   2.586 -    val arity_lines = map problem_line_for_arity_clause arity_clauses
   2.587 -    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
   2.588 -    val conjecture_lines =
   2.589 -      map (problem_line_for_conjecture full_types) conjectures
   2.590 -    val tfree_lines = problem_lines_for_free_types conjectures
   2.591 -    (* Reordering these might or might not confuse the proof reconstruction
   2.592 -       code or the SPASS Flotter hack. *)
   2.593 -    val problem =
   2.594 -      [("Relevant facts", axiom_lines),
   2.595 -       ("Class relationships", class_rel_lines),
   2.596 -       ("Arity declarations", arity_lines),
   2.597 -       ("Helper facts", helper_lines),
   2.598 -       ("Conjectures", conjecture_lines),
   2.599 -       ("Type variables", tfree_lines)]
   2.600 -      |> repair_problem thy explicit_forall full_types explicit_apply
   2.601 -    val (problem, pool) = nice_tptp_problem readable_names problem
   2.602 -    val conjecture_offset =
   2.603 -      length axiom_lines + length class_rel_lines + length arity_lines
   2.604 -      + length helper_lines
   2.605 -    val _ = File.write_list file (strings_for_tptp_problem problem)
   2.606 -  in
   2.607 -    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   2.608 -     conjecture_offset)
   2.609 -  end
   2.610 -
   2.611 -fun extract_clause_sequence output =
   2.612 -  let
   2.613 -    val tokens_of = String.tokens (not o Char.isAlphaNum)
   2.614 -    fun extract_num ("clause" :: (ss as _ :: _)) =
   2.615 -    Int.fromString (List.last ss)
   2.616 -      | extract_num _ = NONE
   2.617 -  in output |> split_lines |> map_filter (extract_num o tokens_of) end
   2.618 +fun get_prover thy name =
   2.619 +  the (Symtab.lookup (Data.get thy) name) |> fst
   2.620 +  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   2.621  
   2.622 -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
   2.623 -
   2.624 -val parse_clause_formula_pair =
   2.625 -  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
   2.626 -  --| Scan.option ($$ ",")
   2.627 -val parse_clause_formula_relation =
   2.628 -  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   2.629 -  |-- Scan.repeat parse_clause_formula_pair
   2.630 -val extract_clause_formula_relation =
   2.631 -  Substring.full
   2.632 -  #> Substring.position set_ClauseFormulaRelationN
   2.633 -  #> snd #> Substring.string #> strip_spaces #> explode
   2.634 -  #> parse_clause_formula_relation #> fst
   2.635 -
   2.636 -fun repair_conjecture_shape_and_theorem_names output conjecture_shape
   2.637 -                                              thm_names =
   2.638 -  if String.isSubstring set_ClauseFormulaRelationN output then
   2.639 -    (* This is a hack required for keeping track of axioms after they have been
   2.640 -       clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
   2.641 -       of this hack. *)
   2.642 -    let
   2.643 -      val j0 = hd conjecture_shape
   2.644 -      val seq = extract_clause_sequence output
   2.645 -      val name_map = extract_clause_formula_relation output
   2.646 -      fun renumber_conjecture j =
   2.647 -        AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
   2.648 -        |> the_single
   2.649 -        |> (fn s => find_index (curry (op =) s) seq + 1)
   2.650 -    in
   2.651 -      (conjecture_shape |> map renumber_conjecture,
   2.652 -       seq |> map (the o AList.lookup (op =) name_map)
   2.653 -           |> map (fn s => case try (unprefix axiom_prefix) s of
   2.654 -                             SOME s' => undo_ascii_of s'
   2.655 -                           | NONE => "")
   2.656 -           |> Vector.fromList)
   2.657 -    end
   2.658 -  else
   2.659 -    (conjecture_shape, thm_names)
   2.660 -
   2.661 -
   2.662 -(* generic TPTP-based provers *)
   2.663 -
   2.664 -fun generic_tptp_prover
   2.665 -        (name, {home_var, executable, arguments, proof_delims, known_failures,
   2.666 -                max_new_relevant_facts_per_iter, prefers_theory_relevant,
   2.667 -                explicit_forall})
   2.668 -        ({debug, overlord, full_types, explicit_apply, relevance_threshold,
   2.669 -          relevance_convergence, theory_relevant, defs_relevant, isar_proof,
   2.670 -          isar_shrink_factor, ...} : params)
   2.671 -        minimize_command timeout
   2.672 -        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
   2.673 -         : problem) =
   2.674 -  let
   2.675 -    (* get clauses and prepare them for writing *)
   2.676 -    val (ctxt, (_, th)) = goal;
   2.677 -    val thy = ProofContext.theory_of ctxt
   2.678 -    (* ### FIXME: (1) preprocessing for "if" etc. *)
   2.679 -    val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
   2.680 -    val the_filtered_clauses =
   2.681 -      case filtered_clauses of
   2.682 -        SOME fcls => fcls
   2.683 -      | NONE => relevant_facts full_types relevance_threshold
   2.684 -                    relevance_convergence defs_relevant
   2.685 -                    max_new_relevant_facts_per_iter
   2.686 -                    (the_default prefers_theory_relevant theory_relevant)
   2.687 -                    relevance_override goal hyp_ts concl_t
   2.688 -    val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
   2.689 -    val (internal_thm_names, clauses) =
   2.690 -      prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
   2.691 -                      the_filtered_clauses
   2.692 -
   2.693 -    (* path to unique problem file *)
   2.694 -    val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   2.695 -                       else Config.get ctxt dest_dir;
   2.696 -    val the_problem_prefix = Config.get ctxt problem_prefix;
   2.697 -    fun prob_pathname nr =
   2.698 -      let
   2.699 -        val probfile =
   2.700 -          Path.basic ((if overlord then "prob_" ^ name
   2.701 -                       else the_problem_prefix ^ serial_string ())
   2.702 -                      ^ "_" ^ string_of_int nr)
   2.703 -      in
   2.704 -        if the_dest_dir = "" then File.tmp_path probfile
   2.705 -        else if File.exists (Path.explode the_dest_dir)
   2.706 -        then Path.append (Path.explode the_dest_dir) probfile
   2.707 -        else error ("No such directory: " ^ the_dest_dir ^ ".")
   2.708 -      end;
   2.709 +fun available_atps thy =
   2.710 +  priority ("Available ATPs: " ^
   2.711 +            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
   2.712  
   2.713 -    val home = getenv home_var
   2.714 -    val command = Path.explode (home ^ "/" ^ executable)
   2.715 -    (* write out problem file and call prover *)
   2.716 -    fun command_line complete probfile =
   2.717 -      let
   2.718 -        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   2.719 -                   " " ^ File.shell_path probfile
   2.720 -      in
   2.721 -        (if Config.get ctxt measure_runtime then
   2.722 -           "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
   2.723 -         else
   2.724 -           "exec " ^ core) ^ " 2>&1"
   2.725 -      end
   2.726 -    fun split_time s =
   2.727 -      let
   2.728 -        val split = String.tokens (fn c => str c = "\n");
   2.729 -        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   2.730 -        fun as_num f = f >> (fst o read_int);
   2.731 -        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   2.732 -        val digit = Scan.one Symbol.is_ascii_digit;
   2.733 -        val num3 = as_num (digit ::: digit ::: (digit >> single));
   2.734 -        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   2.735 -        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   2.736 -      in (output, as_time t) end;
   2.737 -    fun run_on probfile =
   2.738 -      if home = "" then
   2.739 -        error ("The environment variable " ^ quote home_var ^ " is not set.")
   2.740 -      else if File.exists command then
   2.741 -        let
   2.742 -          fun do_run complete =
   2.743 -            let
   2.744 -              val command = command_line complete probfile
   2.745 -              val ((output, msecs), res_code) =
   2.746 -                bash_output command
   2.747 -                |>> (if overlord then
   2.748 -                       prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   2.749 -                     else
   2.750 -                       I)
   2.751 -                |>> (if Config.get ctxt measure_runtime then split_time
   2.752 -                     else rpair 0)
   2.753 -              val (proof, outcome) =
   2.754 -                extract_proof_and_outcome complete res_code proof_delims
   2.755 -                                          known_failures output
   2.756 -            in (output, msecs, proof, outcome) end
   2.757 -          val readable_names = debug andalso overlord
   2.758 -          val (pool, conjecture_offset) =
   2.759 -            write_tptp_file thy readable_names explicit_forall full_types
   2.760 -                            explicit_apply probfile clauses
   2.761 -          val conjecture_shape =
   2.762 -            conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   2.763 -          val result =
   2.764 -            do_run false
   2.765 -            |> (fn (_, msecs0, _, SOME _) =>
   2.766 -                   do_run true
   2.767 -                   |> (fn (output, msecs, proof, outcome) =>
   2.768 -                          (output, msecs0 + msecs, proof, outcome))
   2.769 -                 | result => result)
   2.770 -        in ((pool, conjecture_shape), result) end
   2.771 -      else
   2.772 -        error ("Bad executable: " ^ Path.implode command ^ ".");
   2.773 -
   2.774 -    (* If the problem file has not been exported, remove it; otherwise, export
   2.775 -       the proof file too. *)
   2.776 -    fun cleanup probfile =
   2.777 -      if the_dest_dir = "" then try File.rm probfile else NONE
   2.778 -    fun export probfile (_, (output, _, _, _)) =
   2.779 -      if the_dest_dir = "" then
   2.780 -        ()
   2.781 -      else
   2.782 -        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   2.783 -
   2.784 -    val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
   2.785 -      with_path cleanup export run_on (prob_pathname subgoal)
   2.786 -    val (conjecture_shape, internal_thm_names) =
   2.787 -      repair_conjecture_shape_and_theorem_names output conjecture_shape
   2.788 -                                                internal_thm_names
   2.789 -
   2.790 -    val (message, used_thm_names) =
   2.791 -      case outcome of
   2.792 -        NONE =>
   2.793 -        proof_text isar_proof
   2.794 -            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   2.795 -            (full_types, minimize_command, proof, internal_thm_names, th,
   2.796 -             subgoal)
   2.797 -      | SOME failure => (string_for_failure failure ^ "\n", [])
   2.798 -  in
   2.799 -    {outcome = outcome, message = message, pool = pool,
   2.800 -     used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   2.801 -     output = output, proof = proof, internal_thm_names = internal_thm_names,
   2.802 -     conjecture_shape = conjecture_shape,
   2.803 -     filtered_clauses = the_filtered_clauses}
   2.804 -  end
   2.805 -
   2.806 -fun tptp_prover name p = (name, generic_tptp_prover (name, p));
   2.807 +fun available_atps thy =
   2.808 +  priority ("Available ATPs: " ^
   2.809 +            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
   2.810  
   2.811  fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
   2.812  
   2.813 @@ -801,7 +102,7 @@
   2.814     max_new_relevant_facts_per_iter = 80 (* FIXME *),
   2.815     prefers_theory_relevant = false,
   2.816     explicit_forall = false}
   2.817 -val e = tptp_prover "e" e_config
   2.818 +val e = ("e", e_config)
   2.819  
   2.820  
   2.821  (* The "-VarWeight=3" option helps the higher-order problems, probably by
   2.822 @@ -826,7 +127,7 @@
   2.823     max_new_relevant_facts_per_iter = 26 (* FIXME *),
   2.824     prefers_theory_relevant = true,
   2.825     explicit_forall = true}
   2.826 -val spass = tptp_prover "spass" spass_config
   2.827 +val spass = ("spass", spass_config)
   2.828  
   2.829  (* Vampire *)
   2.830  
   2.831 @@ -848,11 +149,11 @@
   2.832     max_new_relevant_facts_per_iter = 40 (* FIXME *),
   2.833     prefers_theory_relevant = false,
   2.834     explicit_forall = false}
   2.835 -val vampire = tptp_prover "vampire" vampire_config
   2.836 +val vampire = ("vampire", vampire_config)
   2.837  
   2.838  (* Remote prover invocation via SystemOnTPTP *)
   2.839  
   2.840 -val systems = Synchronized.var "atp_systems" ([]: string list);
   2.841 +val systems = Synchronized.var "atp_systems" ([]: string list)
   2.842  
   2.843  fun get_systems () =
   2.844    case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
   2.845 @@ -893,27 +194,23 @@
   2.846     prefers_theory_relevant = prefers_theory_relevant,
   2.847     explicit_forall = explicit_forall}
   2.848  
   2.849 -fun remote_tptp_prover prover atp_prefix args config =
   2.850 -  tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
   2.851 +val remote_name = prefix "remote_"
   2.852  
   2.853 -val remote_e = remote_tptp_prover e "EP---" "" e_config
   2.854 -val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config
   2.855 -val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config
   2.856 +fun remote_prover prover atp_prefix args config =
   2.857 +  (remote_name (fst prover), remote_config atp_prefix args config)
   2.858 +
   2.859 +val remote_e = remote_prover e "EP---" "" e_config
   2.860 +val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
   2.861 +val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
   2.862  
   2.863  fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
   2.864 -  name |> getenv home_var = "" ? remotify
   2.865 +  name |> getenv home_var = "" ? remote_name
   2.866  
   2.867  fun default_atps_param_value () =
   2.868    space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   2.869 -                     remotify (fst vampire)]
   2.870 +                     remote_name (fst vampire)]
   2.871  
   2.872  val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
   2.873 -val prover_setup = fold add_prover provers
   2.874 -
   2.875 -val setup =
   2.876 -  dest_dir_setup
   2.877 -  #> problem_prefix_setup
   2.878 -  #> measure_runtime_setup
   2.879 -  #> prover_setup
   2.880 +val setup = fold add_prover provers
   2.881  
   2.882  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 17:58:30 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 18:33:10 2010 +0200
     3.3 @@ -8,6 +8,7 @@
     3.4  
     3.5  signature SLEDGEHAMMER =
     3.6  sig
     3.7 +  type failure = ATP_Systems.failure
     3.8    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     3.9    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    3.10    type params =
    3.11 @@ -31,9 +32,6 @@
    3.12       relevance_override: relevance_override,
    3.13       axiom_clauses: (string * thm) list option,
    3.14       filtered_clauses: (string * thm) list option}
    3.15 -  datatype failure =
    3.16 -    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
    3.17 -    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
    3.18    type prover_result =
    3.19      {outcome: failure option,
    3.20       message: string,
    3.21 @@ -48,24 +46,30 @@
    3.22    type prover =
    3.23      params -> minimize_command -> Time.time -> problem -> prover_result
    3.24  
    3.25 +  val dest_dir : string Config.T
    3.26 +  val problem_prefix : string Config.T
    3.27 +  val measure_runtime : bool Config.T
    3.28    val kill_atps: unit -> unit
    3.29    val running_atps: unit -> unit
    3.30    val messages: int option -> unit
    3.31 -  val add_prover: string * prover -> theory -> theory
    3.32 -  val get_prover: theory -> string -> prover
    3.33 -  val available_atps: theory -> unit
    3.34 +  val get_prover_fun : theory -> string -> prover
    3.35    val start_prover_thread :
    3.36      params -> int -> int -> relevance_override -> (string -> minimize_command)
    3.37      -> Proof.state -> string -> unit
    3.38 +  val setup : theory -> theory
    3.39  end;
    3.40  
    3.41  structure Sledgehammer : SLEDGEHAMMER =
    3.42  struct
    3.43  
    3.44  open Metis_Clauses
    3.45 +open Sledgehammer_Util
    3.46  open Sledgehammer_Fact_Filter
    3.47 +open ATP_Problem
    3.48 +open ATP_Systems
    3.49  open Sledgehammer_Proof_Reconstruct
    3.50  
    3.51 +
    3.52  (** The Sledgehammer **)
    3.53  
    3.54  val das_Tool = "Sledgehammer"
    3.55 @@ -99,10 +103,6 @@
    3.56     axiom_clauses: (string * thm) list option,
    3.57     filtered_clauses: (string * thm) list option}
    3.58  
    3.59 -datatype failure =
    3.60 -  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
    3.61 -  OldSpass | MalformedInput | MalformedOutput | UnknownError
    3.62 -
    3.63  type prover_result =
    3.64    {outcome: failure option,
    3.65     message: string,
    3.66 @@ -118,38 +118,744 @@
    3.67  type prover =
    3.68    params -> minimize_command -> Time.time -> problem -> prover_result
    3.69  
    3.70 -(* named provers *)
    3.71 +(* configuration attributes *)
    3.72 +
    3.73 +val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    3.74 +  (*Empty string means create files in Isabelle's temporary files directory.*)
    3.75 +
    3.76 +val (problem_prefix, problem_prefix_setup) =
    3.77 +  Attrib.config_string "atp_problem_prefix" (K "prob");
    3.78 +
    3.79 +val (measure_runtime, measure_runtime_setup) =
    3.80 +  Attrib.config_bool "atp_measure_runtime" (K false);
    3.81  
    3.82 -structure Data = Theory_Data
    3.83 -(
    3.84 -  type T = (prover * stamp) Symtab.table;
    3.85 -  val empty = Symtab.empty;
    3.86 -  val extend = I;
    3.87 -  fun merge data : T = Symtab.merge (eq_snd op =) data
    3.88 -    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
    3.89 -);
    3.90 +fun with_path cleanup after f path =
    3.91 +  Exn.capture f path
    3.92 +  |> tap (fn _ => cleanup path)
    3.93 +  |> Exn.release
    3.94 +  |> tap (after path)
    3.95 +
    3.96 +(* Splits by the first possible of a list of delimiters. *)
    3.97 +fun extract_proof delims output =
    3.98 +  case pairself (find_first (fn s => String.isSubstring s output))
    3.99 +                (ListPair.unzip delims) of
   3.100 +    (SOME begin_delim, SOME end_delim) =>
   3.101 +    (output |> first_field begin_delim |> the |> snd
   3.102 +            |> first_field end_delim |> the |> fst
   3.103 +            |> first_field "\n" |> the |> snd
   3.104 +     handle Option.Option => "")
   3.105 +  | _ => ""
   3.106  
   3.107 -fun add_prover (name, prover) thy =
   3.108 -  Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
   3.109 -  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   3.110 +fun extract_proof_and_outcome complete res_code proof_delims known_failures
   3.111 +                              output =
   3.112 +  case map_filter (fn (failure, pattern) =>
   3.113 +                      if String.isSubstring pattern output then SOME failure
   3.114 +                      else NONE) known_failures of
   3.115 +    [] => (case extract_proof proof_delims output of
   3.116 +             "" => ("", SOME UnknownError)
   3.117 +           | proof => if res_code = 0 then (proof, NONE)
   3.118 +                      else ("", SOME UnknownError))
   3.119 +  | (failure :: _) =>
   3.120 +    ("", SOME (if failure = IncompleteUnprovable andalso complete then
   3.121 +                 Unprovable
   3.122 +               else
   3.123 +                 failure))
   3.124  
   3.125 -fun get_prover thy name =
   3.126 -  the (Symtab.lookup (Data.get thy) name) |> fst
   3.127 -  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   3.128 -
   3.129 -fun available_atps thy =
   3.130 -  priority ("Available ATPs: " ^
   3.131 -            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
   3.132 +fun string_for_failure Unprovable = "The ATP problem is unprovable."
   3.133 +  | string_for_failure IncompleteUnprovable =
   3.134 +    "The ATP cannot prove the problem."
   3.135 +  | string_for_failure CantConnect = "Can't connect to remote ATP."
   3.136 +  | string_for_failure TimedOut = "Timed out."
   3.137 +  | string_for_failure OutOfResources = "The ATP ran out of resources."
   3.138 +  | string_for_failure OldSpass =
   3.139 +    (* FIXME: Change the error message below to point to the Isabelle download
   3.140 +       page once the package is there. *)
   3.141 +    "Warning: Sledgehammer requires a more recent version of SPASS with \
   3.142 +    \support for the TPTP syntax. To install it, download and untar the \
   3.143 +    \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
   3.144 +    \\"spass-3.7\" directory's full path to \"" ^
   3.145 +    Path.implode (Path.expand (Path.appends
   3.146 +        (Path.variable "ISABELLE_HOME_USER" ::
   3.147 +         map Path.basic ["etc", "components"]))) ^
   3.148 +    "\" on a line of its own."
   3.149 +  | string_for_failure MalformedInput =
   3.150 +    "Internal Sledgehammer error: The ATP problem is malformed. Please report \
   3.151 +    \this to the Isabelle developers."
   3.152 +  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   3.153 +  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
   3.154  
   3.155  
   3.156 +(* Clause preparation *)
   3.157 +
   3.158 +datatype fol_formula =
   3.159 +  FOLFormula of {formula_name: string,
   3.160 +                 kind: kind,
   3.161 +                 combformula: (name, combterm) formula,
   3.162 +                 ctypes_sorts: typ list}
   3.163 +
   3.164 +fun mk_anot phi = AConn (ANot, [phi])
   3.165 +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   3.166 +fun mk_ahorn [] phi = phi
   3.167 +  | mk_ahorn (phi :: phis) psi =
   3.168 +    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   3.169 +
   3.170 +(* ### FIXME: reintroduce
   3.171 +fun make_clause_table xs =
   3.172 +  fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
   3.173 +(* Remove existing axiom clauses from the conjecture clauses, as this can
   3.174 +   dramatically boost an ATP's performance (for some reason). *)
   3.175 +fun subtract_cls ax_clauses =
   3.176 +  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   3.177 +*)
   3.178 +
   3.179 +fun combformula_for_prop thy =
   3.180 +  let
   3.181 +    val do_term = combterm_from_term thy
   3.182 +    fun do_quant bs q s T t' =
   3.183 +      do_formula ((s, T) :: bs) t'
   3.184 +      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   3.185 +    and do_conn bs c t1 t2 =
   3.186 +      do_formula bs t1 ##>> do_formula bs t2
   3.187 +      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   3.188 +    and do_formula bs t =
   3.189 +      case t of
   3.190 +        @{const Not} $ t1 =>
   3.191 +        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   3.192 +      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   3.193 +        do_quant bs AForall s T t'
   3.194 +      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   3.195 +        do_quant bs AExists s T t'
   3.196 +      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
   3.197 +      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
   3.198 +      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
   3.199 +      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   3.200 +        do_conn bs AIff t1 t2
   3.201 +      | _ => (fn ts => do_term bs (Envir.eta_contract t)
   3.202 +                       |>> APred ||> union (op =) ts)
   3.203 +  in do_formula [] end
   3.204 +
   3.205 +(* Converts an elim-rule into an equivalent theorem that does not have the
   3.206 +   predicate variable. Leaves other theorems unchanged. We simply instantiate
   3.207 +   the conclusion variable to False. (Cf. "transform_elim_term" in
   3.208 +   "ATP_Systems".) *)
   3.209 +(* FIXME: test! *)
   3.210 +fun transform_elim_term t =
   3.211 +  case Logic.strip_imp_concl t of
   3.212 +    @{const Trueprop} $ Var (z, @{typ bool}) =>
   3.213 +    subst_Vars [(z, @{const True})] t
   3.214 +  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
   3.215 +  | _ => t
   3.216 +
   3.217 +(* Removes the lambdas from an equation of the form "t = (%x. u)".
   3.218 +   (Cf. "extensionalize_theorem" in "Clausifier".) *)
   3.219 +fun extensionalize_term t =
   3.220 +  let
   3.221 +    fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
   3.222 +               $ t2 $ Abs (s, var_T, t')) =
   3.223 +        let val var_t = Var (("x", j), var_T) in
   3.224 +          Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
   3.225 +            $ betapply (t2, var_t) $ subst_bound (var_t, t')
   3.226 +          |> aux (j + 1)
   3.227 +        end
   3.228 +      | aux _ t = t
   3.229 +  in aux (maxidx_of_term t + 1) t end
   3.230 +
   3.231 +(* FIXME: Guarantee freshness *)
   3.232 +fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
   3.233 +fun conceal_bounds Ts t =
   3.234 +  subst_bounds (map (Free o apfst concealed_bound_name)
   3.235 +                    (length Ts - 1 downto 0 ~~ rev Ts), t)
   3.236 +fun reveal_bounds Ts =
   3.237 +  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   3.238 +                    (0 upto length Ts - 1 ~~ Ts))
   3.239 +
   3.240 +fun introduce_combinators_in_term ctxt kind t =
   3.241 +  let
   3.242 +    val thy = ProofContext.theory_of ctxt
   3.243 +    fun aux Ts t =
   3.244 +      case t of
   3.245 +        @{const Not} $ t1 => @{const Not} $ aux Ts t1
   3.246 +      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   3.247 +        t0 $ Abs (s, T, aux (T :: Ts) t')
   3.248 +      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   3.249 +        t0 $ Abs (s, T, aux (T :: Ts) t')
   3.250 +      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   3.251 +      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   3.252 +      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   3.253 +      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   3.254 +          $ t1 $ t2 =>
   3.255 +        t0 $ aux Ts t1 $ aux Ts t2
   3.256 +      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   3.257 +               t
   3.258 +             else
   3.259 +               let
   3.260 +                 val t = t |> conceal_bounds Ts
   3.261 +                           |> Envir.eta_contract
   3.262 +                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
   3.263 +               in
   3.264 +                 t |> cterm_of thy
   3.265 +                   |> Clausifier.introduce_combinators_in_cterm
   3.266 +                   |> singleton (Variable.export ctxt' ctxt)
   3.267 +                   |> prop_of |> Logic.dest_equals |> snd
   3.268 +                   |> reveal_bounds Ts
   3.269 +               end
   3.270 +  in t |> not (Meson.is_fol_term thy t) ? aux [] end
   3.271 +  handle THM _ =>
   3.272 +         (* A type variable of sort "{}" will make abstraction fail. *)
   3.273 +         case kind of
   3.274 +           Axiom => HOLogic.true_const
   3.275 +         | Conjecture => HOLogic.false_const
   3.276 +
   3.277 +(* making axiom and conjecture clauses *)
   3.278 +fun make_clause ctxt (formula_name, kind, t) =
   3.279 +  let
   3.280 +    val thy = ProofContext.theory_of ctxt
   3.281 +    (* ### FIXME: perform other transformations previously done by
   3.282 +       "Clausifier.to_nnf", e.g. "HOL.If" *)
   3.283 +    val t = t |> transform_elim_term
   3.284 +              |> Object_Logic.atomize_term thy
   3.285 +              |> extensionalize_term
   3.286 +              |> introduce_combinators_in_term ctxt kind
   3.287 +    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   3.288 +  in
   3.289 +    FOLFormula {formula_name = formula_name, combformula = combformula,
   3.290 +                kind = kind, ctypes_sorts = ctypes_sorts}
   3.291 +  end
   3.292 +
   3.293 +fun make_axiom_clause ctxt (name, th) =
   3.294 +  (name, make_clause ctxt (name, Axiom, prop_of th))
   3.295 +fun make_conjecture_clauses ctxt ts =
   3.296 +  map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
   3.297 +       (0 upto length ts - 1) ts
   3.298 +
   3.299 +(** Helper clauses **)
   3.300 +
   3.301 +fun count_combterm (CombConst ((s, _), _, _)) =
   3.302 +    Symtab.map_entry s (Integer.add 1)
   3.303 +  | count_combterm (CombVar _) = I
   3.304 +  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   3.305 +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   3.306 +  | count_combformula (AConn (_, phis)) = fold count_combformula phis
   3.307 +  | count_combformula (APred tm) = count_combterm tm
   3.308 +fun count_fol_formula (FOLFormula {combformula, ...}) =
   3.309 +  count_combformula combformula
   3.310 +
   3.311 +val optional_helpers =
   3.312 +  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
   3.313 +   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
   3.314 +   (["c_COMBS"], @{thms COMBS_def})]
   3.315 +val optional_typed_helpers =
   3.316 +  [(["c_True", "c_False"], @{thms True_or_False}),
   3.317 +   (["c_If"], @{thms if_True if_False True_or_False})]
   3.318 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   3.319 +
   3.320 +val init_counters =
   3.321 +  Symtab.make (maps (maps (map (rpair 0) o fst))
   3.322 +                    [optional_helpers, optional_typed_helpers])
   3.323 +
   3.324 +fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
   3.325 +  let
   3.326 +    val ct = fold (fold count_fol_formula) [conjectures, axclauses]
   3.327 +                  init_counters
   3.328 +    fun is_needed c = the (Symtab.lookup ct c) > 0
   3.329 +    val cnfs =
   3.330 +      (optional_helpers
   3.331 +       |> full_types ? append optional_typed_helpers
   3.332 +       |> maps (fn (ss, ths) =>
   3.333 +                   if exists is_needed ss then map (`Thm.get_name_hint) ths
   3.334 +                   else [])) @
   3.335 +      (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   3.336 +  in map (snd o make_axiom_clause ctxt) cnfs end
   3.337 +
   3.338 +fun s_not (@{const Not} $ t) = t
   3.339 +  | s_not t = @{const Not} $ t
   3.340 +
   3.341 +(* prepare for passing to writer,
   3.342 +   create additional clauses based on the information from extra_cls *)
   3.343 +fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
   3.344 +  let
   3.345 +    val thy = ProofContext.theory_of ctxt
   3.346 +    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   3.347 +    val is_FO = Meson.is_fol_term thy goal_t
   3.348 +    val axtms = map (prop_of o snd) extra_cls
   3.349 +    val subs = tfree_classes_of_terms [goal_t]
   3.350 +    val supers = tvar_classes_of_terms axtms
   3.351 +    val tycons = type_consts_of_terms thy (goal_t :: axtms)
   3.352 +    (* TFrees in conjecture clauses; TVars in axiom clauses *)
   3.353 +    val conjectures =
   3.354 +      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
   3.355 +        [HOLogic.dest_Trueprop concl_t]
   3.356 +      |> make_conjecture_clauses ctxt
   3.357 +    val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
   3.358 +    val (clnames, axiom_clauses) =
   3.359 +      ListPair.unzip (map (make_axiom_clause ctxt) axcls)
   3.360 +    (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
   3.361 +       "get_helper_clauses" call? *)
   3.362 +    val helper_clauses =
   3.363 +      get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
   3.364 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   3.365 +    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   3.366 +  in
   3.367 +    (Vector.fromList clnames,
   3.368 +      (conjectures, axiom_clauses, extra_clauses, helper_clauses,
   3.369 +       class_rel_clauses, arity_clauses))
   3.370 +  end
   3.371 +
   3.372 +val axiom_prefix = "ax_"
   3.373 +val conjecture_prefix = "conj_"
   3.374 +val arity_clause_prefix = "clsarity_"
   3.375 +val tfrees_name = "tfrees"
   3.376 +
   3.377 +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   3.378 +
   3.379 +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   3.380 +  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   3.381 +  | fo_term_for_combtyp (CombType (name, tys)) =
   3.382 +    ATerm (name, map fo_term_for_combtyp tys)
   3.383 +
   3.384 +fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   3.385 +    (true, ATerm (class, [ATerm (name, [])]))
   3.386 +  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   3.387 +    (true, ATerm (class, [ATerm (name, [])]))
   3.388 +
   3.389 +fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
   3.390 +
   3.391 +fun fo_term_for_combterm full_types =
   3.392 +  let
   3.393 +    fun aux top_level u =
   3.394 +      let
   3.395 +        val (head, args) = strip_combterm_comb u
   3.396 +        val (x, ty_args) =
   3.397 +          case head of
   3.398 +            CombConst (name, _, ty_args) =>
   3.399 +            if fst name = "equal" then
   3.400 +              (if top_level andalso length args = 2 then name
   3.401 +               else ("c_fequal", @{const_name fequal}), [])
   3.402 +            else
   3.403 +              (name, if full_types then [] else ty_args)
   3.404 +          | CombVar (name, _) => (name, [])
   3.405 +          | CombApp _ => raise Fail "impossible \"CombApp\""
   3.406 +        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   3.407 +                          map (aux false) args)
   3.408 +    in
   3.409 +      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   3.410 +    end
   3.411 +  in aux true end
   3.412 +
   3.413 +fun formula_for_combformula full_types =
   3.414 +  let
   3.415 +    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   3.416 +      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   3.417 +      | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
   3.418 +  in aux end
   3.419 +
   3.420 +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
   3.421 +  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   3.422 +                (type_literals_for_types ctypes_sorts))
   3.423 +           (formula_for_combformula full_types combformula)
   3.424 +
   3.425 +fun problem_line_for_axiom full_types
   3.426 +        (formula as FOLFormula {formula_name, kind, ...}) =
   3.427 +  Fof (axiom_prefix ^ ascii_of formula_name, kind,
   3.428 +       formula_for_axiom full_types formula)
   3.429 +
   3.430 +fun problem_line_for_class_rel_clause
   3.431 +        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
   3.432 +  let val ty_arg = ATerm (("T", "T"), []) in
   3.433 +    Fof (ascii_of axiom_name, Axiom,
   3.434 +         AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
   3.435 +                           APred (ATerm (superclass, [ty_arg]))]))
   3.436 +  end
   3.437 +
   3.438 +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   3.439 +    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   3.440 +  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   3.441 +    (false, ATerm (c, [ATerm (sort, [])]))
   3.442 +
   3.443 +fun problem_line_for_arity_clause
   3.444 +        (ArityClause {axiom_name, conclLit, premLits, ...}) =
   3.445 +  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
   3.446 +       mk_ahorn (map (formula_for_fo_literal o apfst not
   3.447 +                      o fo_literal_for_arity_literal) premLits)
   3.448 +                (formula_for_fo_literal
   3.449 +                     (fo_literal_for_arity_literal conclLit)))
   3.450 +
   3.451 +fun problem_line_for_conjecture full_types
   3.452 +        (FOLFormula {formula_name, kind, combformula, ...}) =
   3.453 +  Fof (conjecture_prefix ^ formula_name, kind,
   3.454 +       formula_for_combformula full_types combformula)
   3.455 +
   3.456 +fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   3.457 +  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   3.458 +
   3.459 +fun problem_line_for_free_type lit =
   3.460 +  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
   3.461 +fun problem_lines_for_free_types conjectures =
   3.462 +  let
   3.463 +    val litss = map free_type_literals_for_conjecture conjectures
   3.464 +    val lits = fold (union (op =)) litss []
   3.465 +  in map problem_line_for_free_type lits end
   3.466 +
   3.467 +(** "hBOOL" and "hAPP" **)
   3.468 +
   3.469 +type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   3.470 +
   3.471 +fun consider_term top_level (ATerm ((s, _), ts)) =
   3.472 +  (if is_tptp_variable s then
   3.473 +     I
   3.474 +   else
   3.475 +     let val n = length ts in
   3.476 +       Symtab.map_default
   3.477 +           (s, {min_arity = n, max_arity = 0, sub_level = false})
   3.478 +           (fn {min_arity, max_arity, sub_level} =>
   3.479 +               {min_arity = Int.min (n, min_arity),
   3.480 +                max_arity = Int.max (n, max_arity),
   3.481 +                sub_level = sub_level orelse not top_level})
   3.482 +     end)
   3.483 +  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   3.484 +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   3.485 +  | consider_formula (AConn (_, phis)) = fold consider_formula phis
   3.486 +  | consider_formula (APred tm) = consider_term true tm
   3.487 +
   3.488 +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   3.489 +fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   3.490 +
   3.491 +fun const_table_for_problem explicit_apply problem =
   3.492 +  if explicit_apply then NONE
   3.493 +  else SOME (Symtab.empty |> consider_problem problem)
   3.494 +
   3.495 +val tc_fun = make_fixed_type_const @{type_name fun}
   3.496 +
   3.497 +fun min_arity_of thy full_types NONE s =
   3.498 +    (if s = "equal" orelse s = type_wrapper_name orelse
   3.499 +        String.isPrefix type_const_prefix s orelse
   3.500 +        String.isPrefix class_prefix s then
   3.501 +       16383 (* large number *)
   3.502 +     else if full_types then
   3.503 +       0
   3.504 +     else case strip_prefix_and_undo_ascii const_prefix s of
   3.505 +       SOME s' => num_type_args thy (invert_const s')
   3.506 +     | NONE => 0)
   3.507 +  | min_arity_of _ _ (SOME the_const_tab) s =
   3.508 +    case Symtab.lookup the_const_tab s of
   3.509 +      SOME ({min_arity, ...} : const_info) => min_arity
   3.510 +    | NONE => 0
   3.511 +
   3.512 +fun full_type_of (ATerm ((s, _), [ty, _])) =
   3.513 +    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   3.514 +  | full_type_of _ = raise Fail "expected type wrapper"
   3.515 +
   3.516 +fun list_hAPP_rev _ t1 [] = t1
   3.517 +  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   3.518 +    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   3.519 +  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   3.520 +    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   3.521 +                         [full_type_of t2, ty]) in
   3.522 +      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   3.523 +    end
   3.524 +
   3.525 +fun repair_applications_in_term thy full_types const_tab =
   3.526 +  let
   3.527 +    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   3.528 +      if s = type_wrapper_name then
   3.529 +        case ts of
   3.530 +          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   3.531 +        | _ => raise Fail "malformed type wrapper"
   3.532 +      else
   3.533 +        let
   3.534 +          val ts = map (aux NONE) ts
   3.535 +          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   3.536 +        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   3.537 +  in aux NONE end
   3.538 +
   3.539 +fun boolify t = ATerm (`I "hBOOL", [t])
   3.540 +
   3.541 +(* True if the constant ever appears outside of the top-level position in
   3.542 +   literals, or if it appears with different arities (e.g., because of different
   3.543 +   type instantiations). If false, the constant always receives all of its
   3.544 +   arguments and is used as a predicate. *)
   3.545 +fun is_predicate NONE s =
   3.546 +    s = "equal" orelse String.isPrefix type_const_prefix s orelse
   3.547 +    String.isPrefix class_prefix s
   3.548 +  | is_predicate (SOME the_const_tab) s =
   3.549 +    case Symtab.lookup the_const_tab s of
   3.550 +      SOME {min_arity, max_arity, sub_level} =>
   3.551 +      not sub_level andalso min_arity = max_arity
   3.552 +    | NONE => false
   3.553 +
   3.554 +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   3.555 +  if s = type_wrapper_name then
   3.556 +    case ts of
   3.557 +      [_, t' as ATerm ((s', _), _)] =>
   3.558 +      if is_predicate const_tab s' then t' else boolify t
   3.559 +    | _ => raise Fail "malformed type wrapper"
   3.560 +  else
   3.561 +    t |> not (is_predicate const_tab s) ? boolify
   3.562 +
   3.563 +fun close_universally phi =
   3.564 +  let
   3.565 +    fun term_vars bounds (ATerm (name as (s, _), tms)) =
   3.566 +        (is_tptp_variable s andalso not (member (op =) bounds name))
   3.567 +          ? insert (op =) name
   3.568 +        #> fold (term_vars bounds) tms
   3.569 +    fun formula_vars bounds (AQuant (q, xs, phi)) =
   3.570 +        formula_vars (xs @ bounds) phi
   3.571 +      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   3.572 +      | formula_vars bounds (APred tm) = term_vars bounds tm
   3.573 +  in
   3.574 +    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   3.575 +  end
   3.576 +
   3.577 +fun repair_formula thy explicit_forall full_types const_tab =
   3.578 +  let
   3.579 +    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   3.580 +      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   3.581 +      | aux (APred tm) =
   3.582 +        APred (tm |> repair_applications_in_term thy full_types const_tab
   3.583 +                  |> repair_predicates_in_term const_tab)
   3.584 +  in aux #> explicit_forall ? close_universally end
   3.585 +
   3.586 +fun repair_problem_line thy explicit_forall full_types const_tab
   3.587 +                        (Fof (ident, kind, phi)) =
   3.588 +  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   3.589 +fun repair_problem_with_const_table thy =
   3.590 +  map o apsnd o map ooo repair_problem_line thy
   3.591 +
   3.592 +fun repair_problem thy explicit_forall full_types explicit_apply problem =
   3.593 +  repair_problem_with_const_table thy explicit_forall full_types
   3.594 +      (const_table_for_problem explicit_apply problem) problem
   3.595 +
   3.596 +fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
   3.597 +                    file (conjectures, axiom_clauses, extra_clauses,
   3.598 +                          helper_clauses, class_rel_clauses, arity_clauses) =
   3.599 +  let
   3.600 +    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
   3.601 +    val class_rel_lines =
   3.602 +      map problem_line_for_class_rel_clause class_rel_clauses
   3.603 +    val arity_lines = map problem_line_for_arity_clause arity_clauses
   3.604 +    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
   3.605 +    val conjecture_lines =
   3.606 +      map (problem_line_for_conjecture full_types) conjectures
   3.607 +    val tfree_lines = problem_lines_for_free_types conjectures
   3.608 +    (* Reordering these might or might not confuse the proof reconstruction
   3.609 +       code or the SPASS Flotter hack. *)
   3.610 +    val problem =
   3.611 +      [("Relevant facts", axiom_lines),
   3.612 +       ("Class relationships", class_rel_lines),
   3.613 +       ("Arity declarations", arity_lines),
   3.614 +       ("Helper facts", helper_lines),
   3.615 +       ("Conjectures", conjecture_lines),
   3.616 +       ("Type variables", tfree_lines)]
   3.617 +      |> repair_problem thy explicit_forall full_types explicit_apply
   3.618 +    val (problem, pool) = nice_tptp_problem readable_names problem
   3.619 +    val conjecture_offset =
   3.620 +      length axiom_lines + length class_rel_lines + length arity_lines
   3.621 +      + length helper_lines
   3.622 +    val _ = File.write_list file (strings_for_tptp_problem problem)
   3.623 +  in
   3.624 +    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   3.625 +     conjecture_offset)
   3.626 +  end
   3.627 +
   3.628 +fun extract_clause_sequence output =
   3.629 +  let
   3.630 +    val tokens_of = String.tokens (not o Char.isAlphaNum)
   3.631 +    fun extract_num ("clause" :: (ss as _ :: _)) =
   3.632 +    Int.fromString (List.last ss)
   3.633 +      | extract_num _ = NONE
   3.634 +  in output |> split_lines |> map_filter (extract_num o tokens_of) end
   3.635 +
   3.636 +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
   3.637 +
   3.638 +val parse_clause_formula_pair =
   3.639 +  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
   3.640 +  --| Scan.option ($$ ",")
   3.641 +val parse_clause_formula_relation =
   3.642 +  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   3.643 +  |-- Scan.repeat parse_clause_formula_pair
   3.644 +val extract_clause_formula_relation =
   3.645 +  Substring.full
   3.646 +  #> Substring.position set_ClauseFormulaRelationN
   3.647 +  #> snd #> Substring.string #> strip_spaces #> explode
   3.648 +  #> parse_clause_formula_relation #> fst
   3.649 +
   3.650 +fun repair_conjecture_shape_and_theorem_names output conjecture_shape
   3.651 +                                              thm_names =
   3.652 +  if String.isSubstring set_ClauseFormulaRelationN output then
   3.653 +    (* This is a hack required for keeping track of axioms after they have been
   3.654 +       clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
   3.655 +       of this hack. *)
   3.656 +    let
   3.657 +      val j0 = hd conjecture_shape
   3.658 +      val seq = extract_clause_sequence output
   3.659 +      val name_map = extract_clause_formula_relation output
   3.660 +      fun renumber_conjecture j =
   3.661 +        AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
   3.662 +        |> the_single
   3.663 +        |> (fn s => find_index (curry (op =) s) seq + 1)
   3.664 +    in
   3.665 +      (conjecture_shape |> map renumber_conjecture,
   3.666 +       seq |> map (the o AList.lookup (op =) name_map)
   3.667 +           |> map (fn s => case try (unprefix axiom_prefix) s of
   3.668 +                             SOME s' => undo_ascii_of s'
   3.669 +                           | NONE => "")
   3.670 +           |> Vector.fromList)
   3.671 +    end
   3.672 +  else
   3.673 +    (conjecture_shape, thm_names)
   3.674 +
   3.675 +
   3.676 +(* generic TPTP-based provers *)
   3.677 +
   3.678 +fun prover_fun name
   3.679 +        {home_var, executable, arguments, proof_delims, known_failures,
   3.680 +         max_new_relevant_facts_per_iter, prefers_theory_relevant,
   3.681 +         explicit_forall}
   3.682 +        ({debug, overlord, full_types, explicit_apply, relevance_threshold,
   3.683 +          relevance_convergence, theory_relevant, defs_relevant, isar_proof,
   3.684 +          isar_shrink_factor, ...} : params)
   3.685 +        minimize_command timeout
   3.686 +        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
   3.687 +         : problem) =
   3.688 +  let
   3.689 +    (* get clauses and prepare them for writing *)
   3.690 +    val (ctxt, (_, th)) = goal;
   3.691 +    val thy = ProofContext.theory_of ctxt
   3.692 +    (* ### FIXME: (1) preprocessing for "if" etc. *)
   3.693 +    val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
   3.694 +    val the_filtered_clauses =
   3.695 +      case filtered_clauses of
   3.696 +        SOME fcls => fcls
   3.697 +      | NONE => relevant_facts full_types relevance_threshold
   3.698 +                    relevance_convergence defs_relevant
   3.699 +                    max_new_relevant_facts_per_iter
   3.700 +                    (the_default prefers_theory_relevant theory_relevant)
   3.701 +                    relevance_override goal hyp_ts concl_t
   3.702 +    val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
   3.703 +    val (internal_thm_names, clauses) =
   3.704 +      prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
   3.705 +                      the_filtered_clauses
   3.706 +
   3.707 +    (* path to unique problem file *)
   3.708 +    val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   3.709 +                       else Config.get ctxt dest_dir;
   3.710 +    val the_problem_prefix = Config.get ctxt problem_prefix;
   3.711 +    fun prob_pathname nr =
   3.712 +      let
   3.713 +        val probfile =
   3.714 +          Path.basic ((if overlord then "prob_" ^ name
   3.715 +                       else the_problem_prefix ^ serial_string ())
   3.716 +                      ^ "_" ^ string_of_int nr)
   3.717 +      in
   3.718 +        if the_dest_dir = "" then File.tmp_path probfile
   3.719 +        else if File.exists (Path.explode the_dest_dir)
   3.720 +        then Path.append (Path.explode the_dest_dir) probfile
   3.721 +        else error ("No such directory: " ^ the_dest_dir ^ ".")
   3.722 +      end;
   3.723 +
   3.724 +    val home = getenv home_var
   3.725 +    val command = Path.explode (home ^ "/" ^ executable)
   3.726 +    (* write out problem file and call prover *)
   3.727 +    fun command_line complete probfile =
   3.728 +      let
   3.729 +        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   3.730 +                   " " ^ File.shell_path probfile
   3.731 +      in
   3.732 +        (if Config.get ctxt measure_runtime then
   3.733 +           "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
   3.734 +         else
   3.735 +           "exec " ^ core) ^ " 2>&1"
   3.736 +      end
   3.737 +    fun split_time s =
   3.738 +      let
   3.739 +        val split = String.tokens (fn c => str c = "\n");
   3.740 +        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   3.741 +        fun as_num f = f >> (fst o read_int);
   3.742 +        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   3.743 +        val digit = Scan.one Symbol.is_ascii_digit;
   3.744 +        val num3 = as_num (digit ::: digit ::: (digit >> single));
   3.745 +        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   3.746 +        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   3.747 +      in (output, as_time t) end;
   3.748 +    fun run_on probfile =
   3.749 +      if home = "" then
   3.750 +        error ("The environment variable " ^ quote home_var ^ " is not set.")
   3.751 +      else if File.exists command then
   3.752 +        let
   3.753 +          fun do_run complete =
   3.754 +            let
   3.755 +              val command = command_line complete probfile
   3.756 +              val ((output, msecs), res_code) =
   3.757 +                bash_output command
   3.758 +                |>> (if overlord then
   3.759 +                       prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   3.760 +                     else
   3.761 +                       I)
   3.762 +                |>> (if Config.get ctxt measure_runtime then split_time
   3.763 +                     else rpair 0)
   3.764 +              val (proof, outcome) =
   3.765 +                extract_proof_and_outcome complete res_code proof_delims
   3.766 +                                          known_failures output
   3.767 +            in (output, msecs, proof, outcome) end
   3.768 +          val readable_names = debug andalso overlord
   3.769 +          val (pool, conjecture_offset) =
   3.770 +            write_tptp_file thy readable_names explicit_forall full_types
   3.771 +                            explicit_apply probfile clauses
   3.772 +          val conjecture_shape =
   3.773 +            conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   3.774 +          val result =
   3.775 +            do_run false
   3.776 +            |> (fn (_, msecs0, _, SOME _) =>
   3.777 +                   do_run true
   3.778 +                   |> (fn (output, msecs, proof, outcome) =>
   3.779 +                          (output, msecs0 + msecs, proof, outcome))
   3.780 +                 | result => result)
   3.781 +        in ((pool, conjecture_shape), result) end
   3.782 +      else
   3.783 +        error ("Bad executable: " ^ Path.implode command ^ ".");
   3.784 +
   3.785 +    (* If the problem file has not been exported, remove it; otherwise, export
   3.786 +       the proof file too. *)
   3.787 +    fun cleanup probfile =
   3.788 +      if the_dest_dir = "" then try File.rm probfile else NONE
   3.789 +    fun export probfile (_, (output, _, _, _)) =
   3.790 +      if the_dest_dir = "" then
   3.791 +        ()
   3.792 +      else
   3.793 +        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   3.794 +
   3.795 +    val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
   3.796 +      with_path cleanup export run_on (prob_pathname subgoal)
   3.797 +    val (conjecture_shape, internal_thm_names) =
   3.798 +      repair_conjecture_shape_and_theorem_names output conjecture_shape
   3.799 +                                                internal_thm_names
   3.800 +
   3.801 +    val (message, used_thm_names) =
   3.802 +      case outcome of
   3.803 +        NONE =>
   3.804 +        proof_text isar_proof
   3.805 +            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   3.806 +            (full_types, minimize_command, proof, internal_thm_names, th,
   3.807 +             subgoal)
   3.808 +      | SOME failure => (string_for_failure failure ^ "\n", [])
   3.809 +  in
   3.810 +    {outcome = outcome, message = message, pool = pool,
   3.811 +     used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   3.812 +     output = output, proof = proof, internal_thm_names = internal_thm_names,
   3.813 +     conjecture_shape = conjecture_shape,
   3.814 +     filtered_clauses = the_filtered_clauses}
   3.815 +  end
   3.816 +
   3.817 +fun get_prover_fun thy name = prover_fun name (get_prover thy name)
   3.818 +
   3.819  (* start prover thread *)
   3.820 -
   3.821  fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
   3.822                          relevance_override minimize_command proof_state name =
   3.823    let
   3.824 +    val thy = Proof.theory_of proof_state
   3.825      val birth_time = Time.now ()
   3.826      val death_time = Time.+ (birth_time, timeout)
   3.827 -    val prover = get_prover (Proof.theory_of proof_state) name
   3.828 +    val prover = get_prover_fun thy name
   3.829      val {context = ctxt, facts, goal} = Proof.goal proof_state;
   3.830      val desc =
   3.831        "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
   3.832 @@ -168,4 +874,9 @@
   3.833              end)
   3.834    end
   3.835  
   3.836 +val setup =
   3.837 +  dest_dir_setup
   3.838 +  #> problem_prefix_setup
   3.839 +  #> measure_runtime_setup
   3.840 +
   3.841  end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 17:58:30 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 18:33:10 2010 +0200
     4.3 @@ -81,7 +81,7 @@
     4.4    let
     4.5      val thy = Proof.theory_of state
     4.6      val prover = case atps of
     4.7 -                   [atp_name] => get_prover thy atp_name
     4.8 +                   [atp_name] => get_prover_fun thy atp_name
     4.9                   | _ => error "Expected a single ATP."
    4.10      val msecs = Time.toMilliseconds minimize_timeout
    4.11      val _ =