1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100
1.3 @@ -474,21 +474,20 @@
1.4 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
1.5 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
1.6 hyp_ts concl_t
1.7 - val fact_triple =
1.8 + val factss =
1.9 facts
1.10 |> filter (is_appropriate_prop o prop_of o snd)
1.11 |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
1.12 (the_default default_max_facts max_facts)
1.13 Sledgehammer_Fact.no_fact_override hyp_ts concl_t
1.14 - |> tap (fn fact_triple =>
1.15 + |> tap (fn factss =>
1.16 "Line " ^ str0 (Position.line_of pos) ^ ": " ^
1.17 - Sledgehammer_Run.string_of_fact_triple fact_triple
1.18 + Sledgehammer_Run.string_of_factss factss
1.19 |> Output.urgent_message)
1.20 val prover = get_prover ctxt prover_name params goal facts
1.21 val problem =
1.22 {state = st', goal = goal, subgoal = i,
1.23 - subgoal_count = Sledgehammer_Util.subgoal_count st,
1.24 - fact_triple = fact_triple}
1.25 + subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
1.26 in prover params (K (K (K ""))) problem end)) ()
1.27 handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
1.28 | Fail "inappropriate" => failed ATP_Proof.Inappropriate
2.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100
2.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100
2.3 @@ -42,15 +42,15 @@
2.4 |> relevant_facts ctxt params name
2.5 (the_default default_max_facts max_facts) fact_override hyp_ts
2.6 concl_t
2.7 - |> #1
2.8 + |> hd |> snd
2.9 val problem =
2.10 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
2.11 - fact_triple = (facts, facts, facts)}
2.12 + factss = [("", facts)]}
2.13 in
2.14 (case prover params (K (K (K ""))) problem of
2.15 {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
2.16 | _ => NONE)
2.17 - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
2.18 + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
2.19 end
2.20
2.21 fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100
3.3 @@ -88,7 +88,7 @@
3.4 val mash_weight : real
3.5 val relevant_facts :
3.6 Proof.context -> params -> string -> int -> fact_override -> term list
3.7 - -> term -> raw_fact list -> fact list * fact list * fact list
3.8 + -> term -> raw_fact list -> (string * fact list) list
3.9 val kill_learners : unit -> unit
3.10 val running_learners : unit -> unit
3.11 end;
3.12 @@ -536,7 +536,7 @@
3.13 let
3.14 val problem =
3.15 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
3.16 - fact_triple = (facts, facts, facts)}
3.17 + factss = [("", facts)]}
3.18 in
3.19 get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
3.20 problem
3.21 @@ -1106,10 +1106,10 @@
3.22 error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
3.23 else if only then
3.24 let val facts = facts |> map fact_of_raw_fact in
3.25 - (facts, facts, facts)
3.26 + [("", facts)]
3.27 end
3.28 else if max_facts <= 0 orelse null facts then
3.29 - ([], [], [])
3.30 + [("", [])]
3.31 else
3.32 let
3.33 fun maybe_learn () =
3.34 @@ -1164,8 +1164,9 @@
3.35 in
3.36 case mess of
3.37 [(_, (mepo, _)), (_, (mash, _))] =>
3.38 - (mesh, mepo |> map fst |> add_and_take, mash |> map fst |> add_and_take)
3.39 - | _ => (mesh, mesh, mesh)
3.40 + [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
3.41 + (mashN, mash |> map fst |> add_and_take)]
3.42 + | _ => [("", mesh)]
3.43 end
3.44
3.45 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 31 17:54:05 2013 +0100
4.3 @@ -81,7 +81,7 @@
4.4 preplay_timeout = preplay_timeout, expect = ""}
4.5 val problem =
4.6 {state = state, goal = goal, subgoal = i, subgoal_count = n,
4.7 - fact_triple = (facts, facts, facts)}
4.8 + factss = [("", facts)]}
4.9 val result as {outcome, used_facts, run_time, ...} =
4.10 prover params (K (K (K ""))) problem
4.11 in
4.12 @@ -267,8 +267,7 @@
4.13
4.14 fun maybe_minimize ctxt mode do_learn name
4.15 (params as {verbose, isar_proofs, minimize, ...})
4.16 - ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...}
4.17 - : prover_problem)
4.18 + ({state, subgoal, subgoal_count, ...} : prover_problem)
4.19 (result as {outcome, used_facts, used_from, run_time, preplay, message,
4.20 message_tail} : prover_result) =
4.21 if is_some outcome orelse null used_facts then
4.22 @@ -310,7 +309,7 @@
4.23 if minimize then
4.24 minimize_facts do_learn minimize_name params
4.25 (mode <> Normal orelse not verbose) subgoal subgoal_count state
4.26 - (filter_used_facts true used_facts (map (apsnd single) facts))
4.27 + (filter_used_facts true used_facts (map (apsnd single) used_from))
4.28 |>> Option.map (map fst)
4.29 else
4.30 (SOME used_facts, (preplay, message, ""))
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 31 17:54:05 2013 +0100
5.3 @@ -68,7 +68,7 @@
5.4 goal : thm,
5.5 subgoal : int,
5.6 subgoal_count : int,
5.7 - fact_triple : fact list * fact list * fact list}
5.8 + factss : (string * fact list) list}
5.9
5.10 type prover_result =
5.11 {outcome : failure option,
5.12 @@ -355,7 +355,7 @@
5.13 goal : thm,
5.14 subgoal : int,
5.15 subgoal_count : int,
5.16 - fact_triple : fact list * fact list * fact list}
5.17 + factss : (string * fact list) list}
5.18
5.19 type prover_result =
5.20 {outcome : failure option,
5.21 @@ -632,7 +632,7 @@
5.22 max_new_mono_instances, isar_proofs, isar_shrink,
5.23 slice, timeout, preplay_timeout, ...})
5.24 minimize_command
5.25 - ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *)
5.26 + ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *)
5.27 ...} : prover_problem) =
5.28 let
5.29 val thy = Proof.theory_of state
5.30 @@ -1064,7 +1064,7 @@
5.31
5.32 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
5.33 minimize_command
5.34 - ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *)
5.35 + ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *)
5.36 ...} : prover_problem) =
5.37 let
5.38 val ctxt = Proof.context_of state
5.39 @@ -1108,7 +1108,7 @@
5.40 fun run_reconstructor mode name
5.41 (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
5.42 minimize_command
5.43 - ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...}
5.44 + ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
5.45 : prover_problem) =
5.46 let
5.47 val reconstr =
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100
6.3 @@ -18,7 +18,7 @@
6.4 val noneN : string
6.5 val timeoutN : string
6.6 val unknownN : string
6.7 - val string_of_fact_triple : fact list * fact list * fact list -> string
6.8 + val string_of_factss : (string * fact list) list -> string
6.9 val run_sledgehammer :
6.10 params -> mode -> int -> fact_override
6.11 -> ((string * string list) list -> string -> minimize_command)
6.12 @@ -66,9 +66,8 @@
6.13
6.14 fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
6.15 timeout, expect, ...})
6.16 - mode minimize_command only learn
6.17 - {state, goal, subgoal, subgoal_count,
6.18 - fact_triple as (facts, _, _)} name =
6.19 + mode minimize_command only learn
6.20 + {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
6.21 let
6.22 val ctxt = Proof.context_of state
6.23 val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
6.24 @@ -82,12 +81,12 @@
6.25 val problem =
6.26 {state = state, goal = goal, subgoal = subgoal,
6.27 subgoal_count = subgoal_count,
6.28 - fact_triple =
6.29 - fact_triple
6.30 - |> triple_self ((not (is_ho_atp ctxt name)
6.31 - ? filter_out (fn ((_, (_, Induction)), _) => true
6.32 - | _ => false))
6.33 - #> take num_facts)}
6.34 + factss =
6.35 + factss
6.36 + |> map (apsnd ((not (is_ho_atp ctxt name)
6.37 + ? filter_out (fn ((_, (_, Induction)), _) => true
6.38 + | _ => false))
6.39 + #> take num_facts))}
6.40 fun print_used_facts used_facts used_from =
6.41 tag_list 1 used_from
6.42 |> map (fn (j, fact) => fact |> apsnd (K j))
6.43 @@ -167,21 +166,22 @@
6.44
6.45 val auto_try_max_facts_divisor = 2 (* FUDGE *)
6.46
6.47 +fun eq_facts p = eq_list (op = o pairself fst) p
6.48 +
6.49 fun string_of_facts facts =
6.50 "Including " ^ string_of_int (length facts) ^
6.51 " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
6.52 (facts |> map (fst o fst) |> space_implode " ") ^ "."
6.53
6.54 -fun eq_facts p = eq_list (op = o pairself fst) p
6.55 -
6.56 -fun string_of_fact_triple ([], [], []) = "Found no relevant facts."
6.57 - | string_of_fact_triple (mesh, mepo, mash) =
6.58 - if eq_facts (mesh, mepo) andalso eq_facts (mesh, mash) then
6.59 - string_of_facts mesh
6.60 - else
6.61 - MeShN ^ ": " ^ string_of_facts mesh ^ "\n\n" ^
6.62 - MePoN ^ ": " ^ string_of_facts mepo ^ "\n\n" ^
6.63 - MaShN ^ ": " ^ string_of_facts mash
6.64 +fun string_of_factss factss =
6.65 + if forall (null o snd) factss then
6.66 + "Found no relevant facts."
6.67 + else case factss of
6.68 + [(_, facts)] => string_of_facts facts
6.69 + | _ =>
6.70 + factss
6.71 + |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
6.72 + |> space_implode "\n\n"
6.73
6.74 fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
6.75 slice, ...})
6.76 @@ -213,7 +213,7 @@
6.77 val (smts, (ueq_atps, full_atps)) =
6.78 provers |> List.partition (is_smt_prover ctxt)
6.79 ||> List.partition (is_unit_equational_atp ctxt)
6.80 - fun get_fact_triple label is_appropriate_prop provers =
6.81 + fun get_factss label is_appropriate_prop provers =
6.82 let
6.83 val max_max_facts =
6.84 case max_facts of
6.85 @@ -229,20 +229,20 @@
6.86 | NONE => I)
6.87 |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
6.88 hyp_ts concl_t
6.89 - |> tap (fn fact_triple =>
6.90 + |> tap (fn factss =>
6.91 if verbose then
6.92 label ^ plural_s (length provers) ^ ": " ^
6.93 - string_of_fact_triple fact_triple
6.94 + string_of_factss factss
6.95 |> print
6.96 else
6.97 ())
6.98 end
6.99 fun launch_provers state label is_appropriate_prop provers =
6.100 let
6.101 - val fact_triple = get_fact_triple label is_appropriate_prop provers
6.102 + val factss = get_factss label is_appropriate_prop provers
6.103 val problem =
6.104 {state = state, goal = goal, subgoal = i, subgoal_count = n,
6.105 - fact_triple = fact_triple}
6.106 + factss = factss}
6.107 fun learn prover =
6.108 mash_learn_proof ctxt params prover (prop_of goal) all_facts
6.109 val launch = launch_prover params mode minimize_command only learn
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jan 31 17:54:05 2013 +0100
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Jan 31 17:54:05 2013 +0100
7.3 @@ -11,7 +11,6 @@
7.4 val plural_s : int -> string
7.5 val serial_commas : string -> string list -> string list
7.6 val simplify_spaces : string -> string
7.7 - val triple_self : ('a -> 'b) -> 'a * 'a * 'a -> 'b * 'b * 'b
7.8 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
7.9 val infinite_timeout : Time.time
7.10 val time_mult : real -> Time.time -> Time.time
7.11 @@ -44,8 +43,6 @@
7.12 val serial_commas = Try.serial_commas
7.13 val simplify_spaces = strip_spaces false (K true)
7.14
7.15 -fun triple_self f (x, y, z) = (f x, f y, f z)
7.16 -
7.17 fun with_cleanup clean_up f x =
7.18 Exn.capture f x
7.19 |> tap (fn _ => clean_up x)