name tuning
authorblanchet
Fri Dec 21 14:35:29 2012 +0100 (2012-12-21)
changeset 50610d9c4fbbb0c11
parent 50609 1d8dae3257f0
child 50611 99af6b652b3a
name tuning
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 21 13:33:54 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 21 14:35:29 2012 +0100
     1.3 @@ -260,7 +260,7 @@
     1.4    | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
     1.5  
     1.6  (* FIXME: Here a "Graph.update_node" function would be useful *)
     1.7 -fun update_fact_graph_node (name, kind) =
     1.8 +fun update_access_graph_node (name, kind) =
     1.9    Graph.default_node (name, Isar_Proof)
    1.10    #> kind <> Isar_Proof ? Graph.map_node name (K kind)
    1.11  
    1.12 @@ -290,9 +290,9 @@
    1.13    string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
    1.14    string_of_int (length (Graph.maximals G)) ^ " maximal"
    1.15  
    1.16 -type mash_state = {fact_G : unit Graph.T, dirty : string list option}
    1.17 +type mash_state = {access_G : unit Graph.T, dirty : string list option}
    1.18  
    1.19 -val empty_state = {fact_G = Graph.empty, dirty = SOME []}
    1.20 +val empty_state = {access_G = Graph.empty, dirty = SOME []}
    1.21  
    1.22  local
    1.23  
    1.24 @@ -324,9 +324,9 @@
    1.25               case extract_node line of
    1.26                 NONE => I (* shouldn't happen *)
    1.27               | SOME (name, parents, kind) =>
    1.28 -               update_fact_graph_node (name, kind)
    1.29 +               update_access_graph_node (name, kind)
    1.30                 #> fold (add_edge_to name) parents
    1.31 -           val fact_G =
    1.32 +           val access_G =
    1.33               case string_ord (version', version) of
    1.34                 EQUAL =>
    1.35                 try_graph ctxt "loading state" Graph.empty (fn () =>
    1.36 @@ -335,14 +335,14 @@
    1.37               | GREATER => raise Too_New ()
    1.38           in
    1.39             trace_msg ctxt (fn () =>
    1.40 -               "Loaded fact graph (" ^ graph_info fact_G ^ ")");
    1.41 -           {fact_G = fact_G, dirty = SOME []}
    1.42 +               "Loaded fact graph (" ^ graph_info access_G ^ ")");
    1.43 +           {access_G = access_G, dirty = SOME []}
    1.44           end
    1.45         | _ => empty_state)
    1.46      end
    1.47  
    1.48  fun save _ (state as {dirty = SOME [], ...}) = state
    1.49 -  | save ctxt {fact_G, dirty} =
    1.50 +  | save ctxt {access_G, dirty} =
    1.51      let
    1.52        fun str_of_entry (name, parents, kind) =
    1.53          str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^
    1.54 @@ -352,17 +352,17 @@
    1.55        val (banner, entries) =
    1.56          case dirty of
    1.57            SOME names =>
    1.58 -          (NONE, fold (append_entry o Graph.get_entry fact_G) names [])
    1.59 -        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G [])
    1.60 +          (NONE, fold (append_entry o Graph.get_entry access_G) names [])
    1.61 +        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])
    1.62      in
    1.63        write_file banner (entries, str_of_entry) (mash_state_file ());
    1.64        trace_msg ctxt (fn () =>
    1.65 -          "Saved fact graph (" ^ graph_info fact_G ^
    1.66 +          "Saved fact graph (" ^ graph_info access_G ^
    1.67            (case dirty of
    1.68               SOME dirty =>
    1.69               "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
    1.70             | _ => "") ^  ")");
    1.71 -      {fact_G = fact_G, dirty = SOME []}
    1.72 +      {access_G = access_G, dirty = SOME []}
    1.73      end
    1.74  
    1.75  val global_state =
    1.76 @@ -694,7 +694,7 @@
    1.77  
    1.78  fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
    1.79  
    1.80 -fun maximal_in_graph fact_G facts =
    1.81 +fun maximal_in_graph access_G facts =
    1.82    let
    1.83      val facts = [] |> fold (cons o nickname_of o snd) facts
    1.84      val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
    1.85 @@ -703,11 +703,11 @@
    1.86      fun find_maxes _ (maxs, []) = map snd maxs
    1.87        | find_maxes seen (maxs, new :: news) =
    1.88          find_maxes
    1.89 -            (seen |> num_keys (Graph.imm_succs fact_G new) > 1
    1.90 +            (seen |> num_keys (Graph.imm_succs access_G new) > 1
    1.91                       ? Symtab.default (new, ()))
    1.92              (if Symtab.defined tab new then
    1.93                 let
    1.94 -                 val newp = Graph.all_preds fact_G [new]
    1.95 +                 val newp = Graph.all_preds access_G [new]
    1.96                   fun is_ancestor x yp = member (op =) yp x
    1.97                   val maxs =
    1.98                     maxs |> filter (fn (_, max) => not (is_ancestor max newp))
    1.99 @@ -721,11 +721,11 @@
   1.100                 end
   1.101               else
   1.102                 (maxs, Graph.Keys.fold (insert_new seen)
   1.103 -                                      (Graph.imm_preds fact_G new) news))
   1.104 -  in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
   1.105 +                                      (Graph.imm_preds access_G new) news))
   1.106 +  in find_maxes Symtab.empty ([], Graph.maximals access_G) end
   1.107  
   1.108 -fun is_fact_in_graph fact_G (_, th) =
   1.109 -  can (Graph.get_node fact_G) (nickname_of th)
   1.110 +fun is_fact_in_graph access_G (_, th) =
   1.111 +  can (Graph.get_node access_G) (nickname_of th)
   1.112  
   1.113  val weight_raw_mash_facts = weight_mepo_facts
   1.114  val weight_mash_facts = weight_raw_mash_facts
   1.115 @@ -762,23 +762,23 @@
   1.116                           concl_t facts =
   1.117    let
   1.118      val thy = Proof_Context.theory_of ctxt
   1.119 -    val (fact_G, suggs) =
   1.120 -      peek_state ctxt (fn {fact_G, ...} =>
   1.121 -          if Graph.is_empty fact_G then
   1.122 -            (fact_G, [])
   1.123 +    val (access_G, suggs) =
   1.124 +      peek_state ctxt (fn {access_G, ...} =>
   1.125 +          if Graph.is_empty access_G then
   1.126 +            (access_G, [])
   1.127            else
   1.128              let
   1.129 -              val parents = maximal_in_graph fact_G facts
   1.130 +              val parents = maximal_in_graph access_G facts
   1.131                val feats =
   1.132                  features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
   1.133              in
   1.134 -              (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
   1.135 +              (access_G, mash_QUERY ctxt overlord max_facts (parents, feats))
   1.136              end)
   1.137      val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
   1.138 -    val unknown = facts |> filter_out (is_fact_in_graph fact_G)
   1.139 +    val unknown = facts |> filter_out (is_fact_in_graph access_G)
   1.140    in find_mash_suggestions max_facts suggs facts chained unknown end
   1.141  
   1.142 -fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   1.143 +fun add_wrt_access_graph ctxt (name, parents, feats, deps) (adds, graph) =
   1.144    let
   1.145      fun maybe_add_from from (accum as (parents, graph)) =
   1.146        try_graph ctxt "updating graph" accum (fn () =>
   1.147 @@ -788,17 +788,17 @@
   1.148      val (deps, _) = ([], graph) |> fold maybe_add_from deps
   1.149    in ((name, parents, feats, deps) :: adds, graph) end
   1.150  
   1.151 -fun reprove_wrt_fact_graph ctxt (name, deps) (reps, graph) =
   1.152 +fun reprove_wrt_access_graph ctxt (name, deps) (reps, graph) =
   1.153    let
   1.154      fun maybe_rep_from from (accum as (parents, graph)) =
   1.155        try_graph ctxt "updating graph" accum (fn () =>
   1.156            (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   1.157 -    val graph = graph |> update_fact_graph_node (name, Automatic_Proof)
   1.158 +    val graph = graph |> update_access_graph_node (name, Automatic_Proof)
   1.159      val (deps, _) = ([], graph) |> fold maybe_rep_from deps
   1.160    in ((name, deps) :: reps, graph) end
   1.161  
   1.162 -fun flop_wrt_fact_graph name =
   1.163 -  update_fact_graph_node (name, Isar_Proof_wegen_Prover_Flop)
   1.164 +fun flop_wrt_access_graph name =
   1.165 +  update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop)
   1.166  
   1.167  val learn_timeout_slack = 2.0
   1.168  
   1.169 @@ -826,8 +826,8 @@
   1.170            val feats = features_of ctxt prover thy (Local, General) [t]
   1.171            val deps = used_ths |> map nickname_of
   1.172          in
   1.173 -          peek_state ctxt (fn {fact_G, ...} =>
   1.174 -              let val parents = maximal_in_graph fact_G facts in
   1.175 +          peek_state ctxt (fn {access_G, ...} =>
   1.176 +              let val parents = maximal_in_graph access_G facts in
   1.177                  mash_ADD ctxt overlord [(name, parents, feats, deps)]
   1.178                end);
   1.179            (true, "")
   1.180 @@ -844,10 +844,10 @@
   1.181      val timer = Timer.startRealTimer ()
   1.182      fun next_commit_time () =
   1.183        Time.+ (Timer.checkRealTimer timer, commit_timeout)
   1.184 -    val {fact_G, ...} = peek_state ctxt I
   1.185 +    val {access_G, ...} = peek_state ctxt I
   1.186      val facts = facts |> sort (thm_ord o pairself snd)
   1.187      val (old_facts, new_facts) =
   1.188 -      facts |> List.partition (is_fact_in_graph fact_G)
   1.189 +      facts |> List.partition (is_fact_in_graph access_G)
   1.190    in
   1.191      if null new_facts andalso (not run_prover orelse null old_facts) then
   1.192        if auto_level < 2 then
   1.193 @@ -873,14 +873,14 @@
   1.194            else
   1.195              isar_dependencies_of all_names th
   1.196          fun do_commit [] [] [] state = state
   1.197 -          | do_commit adds reps flops {fact_G, dirty} =
   1.198 +          | do_commit adds reps flops {access_G, dirty} =
   1.199              let
   1.200 -              val was_empty = Graph.is_empty fact_G
   1.201 -              val (adds, fact_G) =
   1.202 -                ([], fact_G) |> fold (add_wrt_fact_graph ctxt) adds
   1.203 -              val (reps, fact_G) =
   1.204 -                ([], fact_G) |> fold (reprove_wrt_fact_graph ctxt) reps
   1.205 -              val fact_G = fact_G |> fold flop_wrt_fact_graph flops
   1.206 +              val was_empty = Graph.is_empty access_G
   1.207 +              val (adds, access_G) =
   1.208 +                ([], access_G) |> fold (add_wrt_access_graph ctxt) adds
   1.209 +              val (reps, access_G) =
   1.210 +                ([], access_G) |> fold (reprove_wrt_access_graph ctxt) reps
   1.211 +              val access_G = access_G |> fold flop_wrt_access_graph flops
   1.212                val dirty =
   1.213                  case (was_empty, dirty, reps) of
   1.214                    (false, SOME names, []) => SOME (map #1 adds @ names)
   1.215 @@ -888,7 +888,7 @@
   1.216              in
   1.217                mash_ADD ctxt overlord (rev adds);
   1.218                mash_REPROVE ctxt overlord reps;
   1.219 -              {fact_G = fact_G, dirty = dirty}
   1.220 +              {access_G = access_G, dirty = dirty}
   1.221              end
   1.222          fun commit last adds reps flops =
   1.223            (if debug andalso auto_level = 0 then
   1.224 @@ -936,7 +936,7 @@
   1.225                val ancestors =
   1.226                  old_facts
   1.227                  |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
   1.228 -              val parents = maximal_in_graph fact_G ancestors
   1.229 +              val parents = maximal_in_graph access_G ancestors
   1.230                val (adds, (_, n, _, _)) =
   1.231                  ([], (parents, 0, next_commit_time (), false))
   1.232                  |> fold learn_new_fact new_facts
   1.233 @@ -967,7 +967,7 @@
   1.234              let
   1.235                val max_isar = 1000 * max_dependencies
   1.236                fun kind_of_proof th =
   1.237 -                try (Graph.get_node fact_G) (nickname_of th)
   1.238 +                try (Graph.get_node access_G) (nickname_of th)
   1.239                  |> the_default Isar_Proof
   1.240                fun priority_of (_, th) =
   1.241                  random_range 0 max_isar
   1.242 @@ -1034,7 +1034,7 @@
   1.243  
   1.244  fun is_mash_enabled () = (getenv "MASH" = "yes")
   1.245  fun mash_can_suggest_facts ctxt =
   1.246 -  not (Graph.is_empty (#fact_G (peek_state ctxt I)))
   1.247 +  not (Graph.is_empty (#access_G (peek_state ctxt I)))
   1.248  
   1.249  (* Generate more suggestions than requested, because some might be thrown out
   1.250     later for various reasons. *)