implemented learning of single proofs in SML MaSh
authorblanchet
Tue May 20 00:13:31 2014 +0200 (2014-05-20)
changeset 57011a4428f517f46
parent 57010 121b63d7bcdb
child 57012 43fd82a537a3
implemented learning of single proofs in SML MaSh
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 19 23:43:53 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 00:13:31 2014 +0200
     1.3 @@ -498,6 +498,15 @@
     1.4    | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
     1.5    | proof_kind_of_str _ (* "i" *) = Isar_Proof
     1.6  
     1.7 +fun add_edge_to name parent =
     1.8 +  Graph.default_node (parent, (Isar_Proof, [], []))
     1.9 +  #> Graph.add_edge (parent, name)
    1.10 +
    1.11 +fun add_node kind name parents feats deps =
    1.12 +  Graph.default_node (name, (kind, feats, deps))
    1.13 +  #> Graph.map_node name (K (kind, feats, deps))
    1.14 +  #> fold (add_edge_to name) parents;
    1.15 +
    1.16  fun try_graph ctxt when def f =
    1.17    f ()
    1.18    handle
    1.19 @@ -550,21 +559,16 @@
    1.20         (case try File.read_lines path of
    1.21           SOME (version' :: node_lines) =>
    1.22           let
    1.23 -           fun add_edge_to name parent =
    1.24 -             Graph.default_node (parent, (Isar_Proof, [], []))
    1.25 -             #> Graph.add_edge (parent, name)
    1.26 -           fun add_node line =
    1.27 +           fun extract_line_and_add_node line =
    1.28               (case extract_node line of
    1.29                 NONE => I (* should not happen *)
    1.30 -             | SOME (kind, name, parents, feats, deps) =>
    1.31 -               Graph.default_node (name, (kind, feats, deps))
    1.32 -               #> Graph.map_node name (K (kind, feats, deps))
    1.33 -               #> fold (add_edge_to name) parents)
    1.34 +             | SOME (kind, name, parents, feats, deps) => add_node kind name parents feats deps)
    1.35 +
    1.36             val (access_G, num_known_facts) =
    1.37               (case string_ord (version', version) of
    1.38                 EQUAL =>
    1.39                 (try_graph ctxt "loading state" Graph.empty (fn () =>
    1.40 -                  fold add_node node_lines Graph.empty),
    1.41 +                  fold extract_line_and_add_node node_lines Graph.empty),
    1.42                  length node_lines)
    1.43               | LESS =>
    1.44                 (if Config.get ctxt sml then wipe_out_mash_state_dir ()
    1.45 @@ -1260,6 +1264,9 @@
    1.46      Async_Manager.thread MaShN birth_time death_time desc task
    1.47    end
    1.48  
    1.49 +fun fresh_enough_name () =
    1.50 +  Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^ serial_string ()
    1.51 +
    1.52  fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths =
    1.53    if is_mash_enabled () then
    1.54      launch_thread timeout (fn () =>
    1.55 @@ -1267,15 +1274,20 @@
    1.56          val thy = Proof_Context.theory_of ctxt
    1.57          val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t]
    1.58        in
    1.59 -        peek_state ctxt overlord (fn {access_G, ...} =>
    1.60 +        map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty} =>
    1.61            let
    1.62 +            val name = fresh_enough_name ()
    1.63              val parents = maximal_wrt_access_graph access_G facts
    1.64 -            val deps =
    1.65 -              used_ths |> filter (is_fact_in_graph access_G)
    1.66 -                       |> map nickname_of_thm
    1.67 +            val deps = used_ths
    1.68 +              |> filter (is_fact_in_graph access_G)
    1.69 +              |> map nickname_of_thm
    1.70            in
    1.71 -            if Config.get ctxt sml then () (* TODO: implement *)
    1.72 -            else MaSh_Py.learn ctxt overlord true [("", parents, map fst feats, deps)]
    1.73 +            if Config.get ctxt sml then
    1.74 +              {access_G = add_node Automatic_Proof name parents feats deps access_G,
    1.75 +               num_known_facts = num_known_facts + 1,
    1.76 +               dirty = Option.map (cons name) dirty}
    1.77 +            else
    1.78 +              (MaSh_Py.learn ctxt overlord true [("", parents, map fst feats, deps)]; state)
    1.79            end);
    1.80          (true, "")
    1.81        end)
    1.82 @@ -1525,8 +1537,7 @@
    1.83              val {access_G, num_known_facts, ...} = peek_state ctxt overlord I
    1.84              val is_in_access_G = is_fact_in_graph access_G o snd
    1.85            in
    1.86 -            if length facts - num_known_facts
    1.87 -               <= max_facts_to_learn_before_query then
    1.88 +            if length facts - num_known_facts <= max_facts_to_learn_before_query then
    1.89                (case length (filter_out is_in_access_G facts) of
    1.90                  0 => false
    1.91                | num_facts_to_learn =>