1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 27 13:52:47 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 27 13:52:47 2011 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  val proverK = "prover"
     1.5  val prover_timeoutK = "prover_timeout"
     1.6  val keepK = "keep"
     1.7 -val full_typesK = "full_types"
     1.8  val type_sysK = "type_sys"
     1.9  val slicingK = "slicing"
    1.10  val e_weight_methodK = "e_weight_method"
    1.11 @@ -630,8 +629,6 @@
    1.12    end
    1.13  
    1.14  fun invoke args =
    1.15 -  let
    1.16 -    val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
    1.17 -  in Mirabelle.register (init, sledgehammer_action args, done) end
    1.18 +  Mirabelle.register (init, sledgehammer_action args, done)
    1.19  
    1.20  end

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 13:52:47 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 13:52:47 2011 +0200
     2.3 @@ -23,7 +23,7 @@
     2.4       prem_kind : formula_kind,
     2.5       formats : format list,
     2.6       best_slices :
     2.7 -       Proof.context -> (real * (bool * (int * string list * string))) list}
     2.8 +       Proof.context -> (real * (bool * (int * string * string))) list}
     2.9  
    2.10    val e_smartN : string
    2.11    val e_autoN : string
    2.12 @@ -52,7 +52,7 @@
    2.13    val remote_atp :
    2.14      string -> string -> string list -> (string * string) list
    2.15      -> (failure * string) list -> formula_kind -> formula_kind -> format list
    2.16 -    -> (Proof.context -> int * string list) -> string * atp_config
    2.17 +    -> (Proof.context -> int * string) -> string * atp_config
    2.18    val add_atp : string * atp_config -> theory -> theory
    2.19    val get_atp : theory -> string -> atp_config
    2.20    val supported_atps : theory -> string list
    2.21 @@ -81,19 +81,19 @@
    2.22     prem_kind : formula_kind,
    2.23     formats : format list,
    2.24     best_slices :
    2.25 -     Proof.context -> (real * (bool * (int * string list * string))) list}
    2.26 +     Proof.context -> (real * (bool * (int * string * string))) list}
    2.27  
    2.28  (* "best_slices" must be found empirically, taking a wholistic approach since
    2.29     the ATPs are run in parallel. The "real" components give the faction of the
    2.30 -   time available given to the slice; these should add up to 1.0. The "bool"
    2.31 +   time available given to the slice and should add up to 1.0. The "bool"
    2.32     component indicates whether the slice's strategy is complete; the "int", the
    2.33 -   preferred number of facts to pass; the "string list", the preferred type
    2.34 -   systems, which should be of the form [sound] or [unsound, sound], where
    2.35 -   "sound" is a sound type system and "unsound" is an unsound one.
    2.36 +   preferred number of facts to pass; the first "string", the preferred type
    2.37 +   system; the second "string", extra information to the prover (e.g., SOS or no
    2.38 +   SOS).
    2.39  
    2.40     The last slice should be the most "normal" one, because it will get all the
    2.41 -   time available if the other slices fail early and also because it is used for
    2.42 -   remote provers and if slicing is disabled. *)
    2.43 +   time available if the other slices fail early and also because it is used if
    2.44 +   slicing is disabled (e.g., by the minimizer). *)
    2.45  
    2.46  val known_perl_failures =
    2.47    [(CantConnect, "HTTP error"),
    2.48 @@ -217,11 +217,11 @@
    2.49       let val method = effective_e_weight_method ctxt in
    2.50         (* FUDGE *)
    2.51         if method = e_smartN then
    2.52 -         [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))),
    2.53 -          (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))),
    2.54 -          (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))]
    2.55 +         [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
    2.56 +          (0.334, (true, (50, "mangled_preds?", e_fun_weightN))),
    2.57 +          (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
    2.58         else
    2.59 -         [(1.0, (true, (500, ["mangled_tags?"], method)))]
    2.60 +         [(1.0, (true, (500, "mangled_tags?", method)))]
    2.61       end}
    2.62  
    2.63  val e = (eN, e_config)
    2.64 @@ -237,7 +237,7 @@
    2.65  val spass_config : atp_config =
    2.66    {exec = ("ISABELLE_ATP", "scripts/spass"),
    2.67     required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
    2.68 -   arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
    2.69 +   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
    2.70       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    2.71        \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
    2.72       |> sos = sosN ? prefix "-SOS=1 ",
    2.73 @@ -256,9 +256,9 @@
    2.74     formats = [FOF],
    2.75     best_slices = fn ctxt =>
    2.76       (* FUDGE *)
    2.77 -     [(0.333, (false, (150, ["mangled_tags"], sosN))),
    2.78 -      (0.333, (false, (300, ["poly_tags?"], sosN))),
    2.79 -      (0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
    2.80 +     [(0.333, (false, (150, "mangled_tags", sosN))),
    2.81 +      (0.333, (false, (300, "poly_tags?", sosN))),
    2.82 +      (0.334, (true, (50, "mangled_tags?", no_sosN)))]
    2.83       |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
    2.84           else I)}
    2.85  
    2.86 @@ -273,7 +273,7 @@
    2.87  val vampire_config : atp_config =
    2.88    {exec = ("VAMPIRE_HOME", "vampire"),
    2.89     required_execs = [],
    2.90 -   arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
    2.91 +   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
    2.92       "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
    2.93       " --thanks \"Andrei and Krystof\" --input_file"
    2.94       |> sos = sosN ? prefix "--sos on ",
    2.95 @@ -297,9 +297,9 @@
    2.96     formats = [FOF],
    2.97     best_slices = fn ctxt =>
    2.98       (* FUDGE *)
    2.99 -     [(0.333, (false, (150, ["poly_preds"], sosN))),
   2.100 -      (0.334, (true, (50, ["mangled_preds?"], no_sosN))),
   2.101 -      (0.333, (false, (500, ["mangled_tags?"], sosN)))]
   2.102 +     [(0.333, (false, (150, "poly_preds", sosN))),
   2.103 +      (0.334, (true, (50, "mangled_preds?", no_sosN))),
   2.104 +      (0.333, (false, (500, "mangled_tags?", sosN)))]
   2.105       |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
   2.106           else I)}
   2.107  
   2.108 @@ -325,7 +325,7 @@
   2.109     formats = [FOF],
   2.110     best_slices =
   2.111       (* FUDGE (FIXME) *)
   2.112 -     K [(1.0, (false, (250, [], "")))]}
   2.113 +     K [(1.0, (false, (250, "mangled_preds?", "")))]}
   2.114  
   2.115  val z3_atp = (z3_atpN, z3_atp_config)
   2.116  
   2.117 @@ -385,8 +385,8 @@
   2.118     prem_kind = prem_kind,
   2.119     formats = formats,
   2.120     best_slices = fn ctxt =>
   2.121 -     let val (max_relevant, type_syss) = best_slice ctxt in
   2.122 -       [(1.0, (false, (max_relevant, type_syss, "")))]
   2.123 +     let val (max_relevant, type_sys) = best_slice ctxt in
   2.124 +       [(1.0, (false, (max_relevant, type_sys, "")))]
   2.125       end}
   2.126  
   2.127  fun remotify_config system_name system_versions best_slice
   2.128 @@ -406,36 +406,35 @@
   2.129  
   2.130  val remote_e =
   2.131    remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   2.132 -               (K (750, ["mangled_tags?"]) (* FUDGE *))
   2.133 +               (K (750, "mangled_tags?") (* FUDGE *))
   2.134  val remote_vampire =
   2.135    remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   2.136 -               (K (200, ["mangled_preds?"]) (* FUDGE *))
   2.137 +               (K (200, "mangled_preds?") (* FUDGE *))
   2.138  val remote_z3_atp =
   2.139 -  remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *))
   2.140 +  remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
   2.141  val remote_leo2 =
   2.142    remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
   2.143 -             (K (100, ["simple"]) (* FUDGE *))
   2.144 +             (K (100, "simple") (* FUDGE *))
   2.145  val remote_satallax =
   2.146    remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   2.147 -             (K (64, ["simple"]) (* FUDGE *))
   2.148 +             (K (64, "simple") (* FUDGE *))
   2.149  val remote_sine_e =
   2.150 -  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
   2.151 -             Axiom Conjecture [FOF]
   2.152 -             (K (500, ["mangled_preds?"]) (* FUDGE *))
   2.153 +  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   2.154 +             Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
   2.155  val remote_snark =
   2.156    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   2.157               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   2.158 -             [TFF, FOF] (K (100, ["simple"]) (* FUDGE *))
   2.159 +             [TFF, FOF] (K (100, "simple") (* FUDGE *))
   2.160  val remote_tofof_e =
   2.161    remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
   2.162 -             Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
   2.163 +             Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
   2.164  val remote_waldmeister =
   2.165    remote_atp waldmeisterN "Waldmeister" ["710"]
   2.166               [("#START OF PROOF", "Proved Goals:")]
   2.167               [(OutOfResources, "Too many function symbols"),
   2.168                (Crashed, "Unrecoverable Segmentation Fault")]
   2.169               Hypothesis Hypothesis [CNF_UEQ]
   2.170 -             (K (50, ["mangled_tags?"]) (* FUDGE *))
   2.171 +             (K (50, "mangled_tags?") (* FUDGE *))
   2.172  
   2.173  (* Setup *)
   2.174  

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 27 13:52:47 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jun 27 13:52:47 2011 +0200
     3.3 @@ -12,7 +12,6 @@
     3.4    val auto : bool Unsynchronized.ref
     3.5    val provers : string Unsynchronized.ref
     3.6    val timeout : int Unsynchronized.ref
     3.7 -  val full_types : bool Unsynchronized.ref
     3.8    val default_params : Proof.context -> (string * string) list -> params
     3.9    val setup : theory -> theory
    3.10  end;
    3.11 @@ -65,7 +64,6 @@
    3.12  
    3.13  val provers = Unsynchronized.ref ""
    3.14  val timeout = Unsynchronized.ref 30
    3.15 -val full_types = Unsynchronized.ref false
    3.16  
    3.17  val _ =
    3.18    ProofGeneralPgip.add_preference Preferences.category_proof
    3.19 @@ -79,11 +77,6 @@
    3.20            "Sledgehammer: Time Limit"
    3.21            "ATPs will be interrupted after this time (in seconds)")
    3.22  
    3.23 -val _ =
    3.24 -  ProofGeneralPgip.add_preference Preferences.category_proof
    3.25 -      (Preferences.bool_pref full_types
    3.26 -          "Sledgehammer: Full Types" "ATPs will use full type information")
    3.27 -
    3.28  type raw_param = string * string list
    3.29  
    3.30  val default_default_params =
    3.31 @@ -108,16 +101,15 @@
    3.32     ("quiet", "verbose"),
    3.33     ("no_overlord", "overlord"),
    3.34     ("non_blocking", "blocking"),
    3.35 -   ("partial_types", "full_types"),
    3.36     ("no_isar_proof", "isar_proof"),
    3.37     ("no_slicing", "slicing")]
    3.38  
    3.39  val params_for_minimize =
    3.40 -  ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    3.41 +  ["debug", "verbose", "overlord", "type_sys", "max_mono_iters",
    3.42     "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    3.43     "preplay_timeout"]
    3.44  
    3.45 -val property_dependent_params = ["provers", "full_types", "timeout"]
    3.46 +val property_dependent_params = ["provers", "timeout"]
    3.47  
    3.48  fun is_known_raw_param s =
    3.49    AList.defined (op =) default_default_params s orelse
    3.50 @@ -218,7 +210,6 @@
    3.51              [("provers", [case !provers of
    3.52                              "" => default_provers_param_value ctxt
    3.53                            | s => s]),
    3.54 -             ("full_types", [if !full_types then "true" else "false"]),
    3.55               ("timeout", let val timeout = !timeout in
    3.56                             [if timeout <= 0 then "none"
    3.57                              else string_of_int timeout]
    3.58 @@ -272,10 +263,10 @@
    3.59                    |> mode = Auto_Try ? single o hd
    3.60      val type_sys =
    3.61        if mode = Auto_Try then
    3.62 -        Smart_Type_Sys true
    3.63 +        NONE
    3.64        else case lookup_string "type_sys" of
    3.65 -        "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
    3.66 -      | s => Dumb_Type_Sys (type_sys_from_string s)
    3.67 +        "smart" => NONE
    3.68 +      | s => SOME (type_sys_from_string s)
    3.69      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    3.70      val max_relevant = lookup_option lookup_int "max_relevant"
    3.71      val max_mono_iters = lookup_int "max_mono_iters"

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 13:52:47 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 13:52:47 2011 +0200
     4.3 @@ -18,17 +18,13 @@
     4.4  
     4.5    datatype mode = Auto_Try | Try | Normal | Minimize
     4.6  
     4.7 -  datatype rich_type_sys =
     4.8 -    Dumb_Type_Sys of type_sys |
     4.9 -    Smart_Type_Sys of bool
    4.10 -
    4.11    type params =
    4.12      {debug: bool,
    4.13       verbose: bool,
    4.14       overlord: bool,
    4.15       blocking: bool,
    4.16       provers: string list,
    4.17 -     type_sys: rich_type_sys,
    4.18 +     type_sys: type_sys option,
    4.19       relevance_thresholds: real * real,
    4.20       max_relevant: int option,
    4.21       max_mono_iters: int,
    4.22 @@ -286,17 +282,13 @@
    4.23  
    4.24  (** problems, results, ATPs, etc. **)
    4.25  
    4.26 -datatype rich_type_sys =
    4.27 -  Dumb_Type_Sys of type_sys |
    4.28 -  Smart_Type_Sys of bool
    4.29 -
    4.30  type params =
    4.31    {debug: bool,
    4.32     verbose: bool,
    4.33     overlord: bool,
    4.34     blocking: bool,
    4.35     provers: string list,
    4.36 -   type_sys: rich_type_sys,
    4.37 +   type_sys: type_sys option,
    4.38     relevance_thresholds: real * real,
    4.39     max_relevant: int option,
    4.40     max_mono_iters: int,
    4.41 @@ -510,16 +502,11 @@
    4.42     them each time. *)
    4.43  val atp_important_message_keep_quotient = 10
    4.44  
    4.45 -val fallback_best_type_syss =
    4.46 -  [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)]
    4.47 -
    4.48 -fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
    4.49 -    choose_format formats type_sys
    4.50 -  | choose_format_and_type_sys best_type_syss formats
    4.51 -                               (Smart_Type_Sys full_types) =
    4.52 -    map type_sys_from_string best_type_syss @ fallback_best_type_syss
    4.53 -    |> find_first (if full_types then is_type_sys_virtually_sound else K true)
    4.54 -    |> the |> choose_format formats
    4.55 +fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
    4.56 +  (case type_sys_opt of
    4.57 +     SOME ts => ts
    4.58 +   | NONE => type_sys_from_string best_type_sys)
    4.59 +  |> choose_format formats
    4.60  
    4.61  val metis_minimize_max_time = seconds 2.0
    4.62  
    4.63 @@ -609,14 +596,14 @@
    4.64                  |> maps (fn (name, rths) => map (pair name o snd) rths)
    4.65                end
    4.66              fun run_slice (slice, (time_frac, (complete,
    4.67 -                                   (best_max_relevant, best_type_syss, extra))))
    4.68 +                                    (best_max_relevant, best_type_sys, extra))))
    4.69                            time_left =
    4.70                let
    4.71                  val num_facts =
    4.72                    length facts |> is_none max_relevant
    4.73                                    ? Integer.min best_max_relevant
    4.74                  val (format, type_sys) =
    4.75 -                  choose_format_and_type_sys best_type_syss formats type_sys
    4.76 +                  choose_format_and_type_sys best_type_sys formats type_sys
    4.77                  val fairly_sound = is_type_sys_fairly_sound type_sys
    4.78                  val facts =
    4.79                    facts |> map untranslated_fact

     5.1 --- a/src/HOL/ex/atp_export.ML	Mon Jun 27 13:52:47 2011 +0200
     5.2 +++ b/src/HOL/ex/atp_export.ML	Mon Jun 27 13:52:47 2011 +0200
     5.3 @@ -120,7 +120,7 @@
     5.4        " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
     5.5        File.shell_path prob_file
     5.6    in
     5.7 -    TimeLimit.timeLimit (seconds 0.15) bash_output command
     5.8 +    TimeLimit.timeLimit (seconds 0.3) bash_output command
     5.9      |> fst
    5.10      |> extract_tstplike_proof_and_outcome false true proof_delims
    5.11                                            known_failures
    5.12 @@ -129,7 +129,7 @@
    5.13    handle TimeLimit.TimeOut => SOME TimedOut
    5.14  
    5.15  val likely_tautology_prefixes =
    5.16 -  [@{theory HOL}, @{theory Meson}, @{theory Metis}]
    5.17 +  [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
    5.18    |> map (fact_name_of o Context.theory_name)
    5.19  
    5.20  fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =