1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 24 18:46:38 2014 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 24 18:53:14 2014 +0200
1.3 @@ -551,12 +551,15 @@
1.4 Graph.default_node (parent, (Isar_Proof, [], []))
1.5 #> Graph.add_edge (parent, name)
1.6
1.7 -fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) =
1.8 - ((Graph.new_node (name, (kind, feats, deps)) access_G
1.9 - handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
1.10 - |> fold (add_edge_to name) parents,
1.11 - (maybe_add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
1.12 - (name, feats, deps) :: learns)
1.13 +fun add_node kind name parents feats deps (accum as (access_G, (fact_xtab, feat_xtab), learns)) =
1.14 + let val fact_xtab' = add_to_xtab name fact_xtab in
1.15 + ((Graph.new_node (name, (kind, feats, deps)) access_G
1.16 + handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
1.17 + |> fold (add_edge_to name) parents,
1.18 + (fact_xtab', fold maybe_add_to_xtab feats feat_xtab),
1.19 + (name, feats, deps) :: learns)
1.20 + end
1.21 + handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *)
1.22
1.23 fun try_graph ctxt when def f =
1.24 f ()
1.25 @@ -1211,7 +1214,8 @@
1.26
1.27 fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
1.28
1.29 -fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (access_G, (fact_xtab, feat_xtab)) =
1.30 +fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
1.31 + (accum as (access_G, (fact_xtab, feat_xtab))) =
1.32 let
1.33 fun maybe_learn_from from (accum as (parents, access_G)) =
1.34 try_graph ctxt "updating graph" accum (fn () =>
1.35 @@ -1221,11 +1225,12 @@
1.36 val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
1.37 val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
1.38
1.39 - val fact_xtab = maybe_add_to_xtab name fact_xtab
1.40 + val fact_xtab = add_to_xtab name fact_xtab
1.41 val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
1.42 in
1.43 - ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
1.44 + (SOME (name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
1.45 end
1.46 + handle Symtab.DUP _ => (NONE, accum) (* facts sometimes have the same name, confusingly *)
1.47
1.48 fun relearn_wrt_access_graph ctxt (name, deps) access_G =
1.49 let
1.50 @@ -1333,6 +1338,7 @@
1.51
1.52 val (learns, (access_G', xtabs')) =
1.53 fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
1.54 + |>> map_filter I
1.55 val (relearns, access_G'') =
1.56 fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
1.57