1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -238,10 +238,12 @@
1.4 (Term.add_vars t [] |> sort_wrt (fst o fst))
1.5 |> fst
1.6
1.7 -fun backquote_thm th =
1.8 - th |> prop_of |> close_form
1.9 - |> hackish_string_for_term (theory_of_thm th)
1.10 - |> backquote
1.11 +fun backquote_term thy t =
1.12 + t |> close_form
1.13 + |> hackish_string_for_term thy
1.14 + |> backquote
1.15 +
1.16 +fun backquote_thm th = backquote_term (theory_of_thm th) (prop_of th)
1.17
1.18 fun clasimpset_rule_table_of ctxt =
1.19 let
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
2.3 @@ -167,9 +167,10 @@
2.4 ("lam_trans", [name])
2.5 else if member (op =) fact_filters name then
2.6 ("fact_filter", [name])
2.7 - else case Int.fromString name of
2.8 - SOME n => ("max_facts", [name])
2.9 - | NONE => error ("Unknown parameter: " ^ quote name ^ "."))
2.10 + else if can Int.fromString name then
2.11 + ("max_facts", [name])
2.12 + else
2.13 + error ("Unknown parameter: " ^ quote name ^ "."))
2.14
2.15
2.16 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
2.17 @@ -375,7 +376,7 @@
2.18 let
2.19 val ctxt = ctxt |> Config.put instantiate_inducts false
2.20 val i = the_default 1 opt_i
2.21 - val params as {provers, ...} =
2.22 + val params =
2.23 get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
2.24 override_params)
2.25 val goal = prop_of (#goal (Proof.goal state))
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
3.3 @@ -472,9 +472,9 @@
3.4 "Internal error when " ^ when ^ ":\n" ^
3.5 ML_Compiler.exn_message exn); def)
3.6
3.7 -type mash_state = {fact_graph : unit Graph.T}
3.8 +type mash_state = {fact_G : unit Graph.T}
3.9
3.10 -val empty_state = {fact_graph = Graph.empty}
3.11 +val empty_state = {fact_G = Graph.empty}
3.12
3.13 local
3.14
3.15 @@ -496,25 +496,25 @@
3.16 | (name, parents) =>
3.17 Graph.default_node (name, ())
3.18 #> fold (add_edge_to name) parents
3.19 - val fact_graph =
3.20 + val fact_G =
3.21 try_graph ctxt "loading state" Graph.empty (fn () =>
3.22 Graph.empty |> version' = version
3.23 ? fold add_fact_line fact_lines)
3.24 - in {fact_graph = fact_graph} end
3.25 + in {fact_G = fact_G} end
3.26 | _ => empty_state)
3.27 end
3.28
3.29 -fun save {fact_graph} =
3.30 +fun save {fact_G} =
3.31 let
3.32 val path = mash_state_path ()
3.33 fun fact_line_for name parents =
3.34 escape_meta name ^ ": " ^ escape_metas parents
3.35 val append_fact = File.append path o suffix "\n" oo fact_line_for
3.36 + fun append_entry (name, ((), (parents, _))) () =
3.37 + append_fact name (Graph.Keys.dest parents)
3.38 in
3.39 File.write path (version ^ "\n");
3.40 - Graph.fold (fn (name, ((), (parents, _))) => fn () =>
3.41 - append_fact name (Graph.Keys.dest parents))
3.42 - fact_graph ()
3.43 + Graph.fold append_entry fact_G ()
3.44 end
3.45
3.46 val global_state =
3.47 @@ -535,45 +535,52 @@
3.48 end
3.49
3.50 fun mash_could_suggest_facts () = mash_home () <> ""
3.51 -fun mash_can_suggest_facts ctxt =
3.52 - not (Graph.is_empty (#fact_graph (mash_get ctxt)))
3.53 +fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
3.54
3.55 -fun parents_wrt_facts facts fact_graph =
3.56 +fun queue_of xs = Queue.empty |> fold Queue.enqueue xs
3.57 +
3.58 +fun max_facts_in_graph fact_G facts =
3.59 let
3.60 val facts = [] |> fold (cons o nickname_of o snd) facts
3.61 val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
3.62 - fun insert_not_seen seen name =
3.63 - not (member (op =) seen name) ? insert (op =) name
3.64 - fun parents_of _ parents [] = parents
3.65 - | parents_of seen parents (name :: names) =
3.66 - if Symtab.defined tab name then
3.67 - parents_of (name :: seen) (name :: parents) names
3.68 - else
3.69 - parents_of (name :: seen) parents
3.70 - (Graph.Keys.fold (insert_not_seen seen)
3.71 - (Graph.imm_preds fact_graph name) names)
3.72 - in parents_of [] [] (Graph.maximals fact_graph) end
3.73 + fun enqueue_new seen name =
3.74 + not (member (op =) seen name) ? Queue.enqueue name
3.75 + fun find_maxes seen maxs names =
3.76 + case try Queue.dequeue names of
3.77 + NONE => maxs
3.78 + | SOME (name, names) =>
3.79 + if Symtab.defined tab name then
3.80 + let
3.81 + fun no_path x y = not (member (op =) (Graph.all_preds fact_G [y]) x)
3.82 + val maxs = maxs |> filter (fn max => no_path max name)
3.83 + val maxs = maxs |> forall (no_path name) maxs ? cons name
3.84 + in find_maxes (name :: seen) maxs names end
3.85 + else
3.86 + find_maxes (name :: seen) maxs
3.87 + (Graph.Keys.fold (enqueue_new seen)
3.88 + (Graph.imm_preds fact_G name) names)
3.89 + in find_maxes [] [] (queue_of (Graph.maximals fact_G)) end
3.90
3.91 (* Generate more suggestions than requested, because some might be thrown out
3.92 later for various reasons and "meshing" gives better results with some
3.93 slack. *)
3.94 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
3.95
3.96 -fun is_fact_in_graph fact_graph (_, th) =
3.97 - can (Graph.get_node fact_graph) (nickname_of th)
3.98 +fun is_fact_in_graph fact_G (_, th) =
3.99 + can (Graph.get_node fact_G) (nickname_of th)
3.100
3.101 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
3.102 concl_t facts =
3.103 let
3.104 val thy = Proof_Context.theory_of ctxt
3.105 - val fact_graph = #fact_graph (mash_get ctxt)
3.106 - val parents = parents_wrt_facts facts fact_graph
3.107 + val fact_G = #fact_G (mash_get ctxt)
3.108 + val parents = max_facts_in_graph fact_G facts
3.109 val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
3.110 val suggs =
3.111 - if Graph.is_empty fact_graph then []
3.112 + if Graph.is_empty fact_G then []
3.113 else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
3.114 val selected = facts |> suggested_facts suggs
3.115 - val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
3.116 + val unknown = facts |> filter_out (is_fact_in_graph fact_G)
3.117 in (selected, unknown) end
3.118
3.119 fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
3.120 @@ -596,6 +603,10 @@
3.121 val desc = ("machine learner for Sledgehammer", "")
3.122 in Async_Manager.launch MaShN birth_time death_time desc task end
3.123
3.124 +fun freshish_name () =
3.125 + Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^
3.126 + serial_string ()
3.127 +
3.128 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
3.129 used_ths =
3.130 if is_smt_prover ctxt prover then
3.131 @@ -605,18 +616,17 @@
3.132 (fn () =>
3.133 let
3.134 val thy = Proof_Context.theory_of ctxt
3.135 - val name = timestamp () ^ " " ^ serial_string () (* freshish *)
3.136 + val name = freshish_name ()
3.137 val feats = features_of ctxt prover thy (Local, General) [t]
3.138 val deps = used_ths |> map nickname_of
3.139 in
3.140 - mash_map ctxt (fn {fact_graph} =>
3.141 + mash_map ctxt (fn {fact_G} =>
3.142 let
3.143 - val parents = parents_wrt_facts facts fact_graph
3.144 + val parents = max_facts_in_graph fact_G facts
3.145 val upds = [(name, parents, feats, deps)]
3.146 - val (upds, fact_graph) =
3.147 - ([], fact_graph) |> fold (update_fact_graph ctxt) upds
3.148 - in
3.149 - mash_ADD ctxt overlord upds; {fact_graph = fact_graph}
3.150 + val (upds, fact_G) =
3.151 + ([], fact_G) |> fold (update_fact_graph ctxt) upds
3.152 + in mash_ADD ctxt overlord upds; {fact_G = fact_G}
3.153 end);
3.154 (true, "")
3.155 end)
3.156 @@ -636,10 +646,10 @@
3.157 val timer = Timer.startRealTimer ()
3.158 fun next_commit_time () =
3.159 Time.+ (Timer.checkRealTimer timer, commit_timeout)
3.160 - val {fact_graph} = mash_get ctxt
3.161 - val new_facts =
3.162 - facts |> filter_out (is_fact_in_graph fact_graph)
3.163 - |> sort (thm_ord o pairself snd)
3.164 + val {fact_G} = mash_get ctxt
3.165 + val (old_facts, new_facts) =
3.166 + facts |> List.partition (is_fact_in_graph fact_G)
3.167 + ||> sort (thm_ord o pairself snd)
3.168 val num_new_facts = length new_facts
3.169 in
3.170 (if not auto then
3.171 @@ -654,7 +664,7 @@
3.172 else
3.173 "")
3.174 |> Output.urgent_message;
3.175 - if null new_facts then
3.176 + if num_new_facts = 0 then
3.177 if not auto then
3.178 "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
3.179 sendback relearn_atpN ^ " to learn from scratch."
3.180 @@ -662,17 +672,21 @@
3.181 ""
3.182 else
3.183 let
3.184 - val ths = facts |> map snd
3.185 + val last_th = new_facts |> List.last |> snd
3.186 + (* crude approximation *)
3.187 + val ancestors =
3.188 + old_facts |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
3.189 val all_names =
3.190 - ths |> filter_out is_likely_tautology_or_too_meta
3.191 - |> map (rpair () o nickname_of)
3.192 - |> Symtab.make
3.193 + facts |> map snd
3.194 + |> filter_out is_likely_tautology_or_too_meta
3.195 + |> map (rpair () o nickname_of)
3.196 + |> Symtab.make
3.197 fun do_commit [] state = state
3.198 - | do_commit upds {fact_graph} =
3.199 + | do_commit upds {fact_G} =
3.200 let
3.201 - val (upds, fact_graph) =
3.202 - ([], fact_graph) |> fold (update_fact_graph ctxt) upds
3.203 - in mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph} end
3.204 + val (upds, fact_G) =
3.205 + ([], fact_G) |> fold (update_fact_graph ctxt) upds
3.206 + in mash_ADD ctxt overlord (rev upds); {fact_G = fact_G} end
3.207 fun trim_deps deps = if length deps > max_dependencies then [] else deps
3.208 fun commit last upds =
3.209 (if debug andalso not auto then Output.urgent_message "Committing..."
3.210 @@ -708,7 +722,7 @@
3.211 val timed_out =
3.212 Time.> (Timer.checkRealTimer timer, learn_timeout)
3.213 in (upds, ([name], n, next_commit, timed_out)) end
3.214 - val parents = parents_wrt_facts facts fact_graph
3.215 + val parents = max_facts_in_graph fact_G ancestors
3.216 val (upds, (_, n, _, _)) =
3.217 ([], (parents, 0, next_commit_time (), false))
3.218 |> fold do_fact new_facts