src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 48439 67a6bcbd3587
parent 48438 3e45c98fe127
child 48440 159e320ef851
equal deleted inserted replaced
48438:3e45c98fe127 48439:67a6bcbd3587
   717         ""
   717         ""
   718     else
   718     else
   719       let
   719       let
   720         val all_names =
   720         val all_names =
   721           facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
   721           facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
   722         val deps_of =
   722         fun deps_of status th =
   723           if atp then
   723           if status = Non_Rec_Def orelse status = Rec_Def then
   724             atp_dependencies_of ctxt params prover auto_level facts all_names
   724             SOME []
       
   725           else if atp then
       
   726             atp_dependencies_of ctxt params prover auto_level facts all_names th
   725           else
   727           else
   726             isar_dependencies_of all_names
   728             isar_dependencies_of all_names th
   727         fun do_commit [] [] state = state
   729         fun do_commit [] [] state = state
   728           | do_commit adds reps {fact_G} =
   730           | do_commit adds reps {fact_G} =
   729             let
   731             let
   730               val (adds, fact_G) =
   732               val (adds, fact_G) =
   731                 ([], fact_G) |> fold (add_to_fact_graph ctxt) adds
   733                 ([], fact_G) |> fold (add_to_fact_graph ctxt) adds
   749                |> Output.urgent_message
   751                |> Output.urgent_message
   750              end
   752              end
   751            else
   753            else
   752              ())
   754              ())
   753         fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
   755         fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
   754           | learn_new_fact ((_, stature), th)
   756           | learn_new_fact ((_, stature as (_, status)), th)
   755                            (adds, (parents, n, next_commit, _)) =
   757                            (adds, (parents, n, next_commit, _)) =
   756             let
   758             let
   757               val name = nickname_of th
   759               val name = nickname_of th
   758               val feats =
   760               val feats =
   759                 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
   761                 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
   760               val deps = deps_of th |> these
   762               val deps = deps_of status th |> these
   761               val n = n |> not (null deps) ? Integer.add 1
   763               val n = n |> not (null deps) ? Integer.add 1
   762               val adds = (name, parents, feats, deps) :: adds
   764               val adds = (name, parents, feats, deps) :: adds
   763               val (adds, next_commit) =
   765               val (adds, next_commit) =
   764                 if Time.> (Timer.checkRealTimer timer, next_commit) then
   766                 if Time.> (Timer.checkRealTimer timer, next_commit) then
   765                   (commit false adds []; ([], next_commit_time ()))
   767                   (commit false adds []; ([], next_commit_time ()))
   781               val (adds, (_, n, _, _)) =
   783               val (adds, (_, n, _, _)) =
   782                 ([], (parents, 0, next_commit_time (), false))
   784                 ([], (parents, 0, next_commit_time (), false))
   783                 |> fold learn_new_fact new_facts
   785                 |> fold learn_new_fact new_facts
   784             in commit true adds []; n end
   786             in commit true adds []; n end
   785         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
   787         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
   786           | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
   788           | relearn_old_fact ((_, (_, status)), th)
       
   789                              (reps, (n, next_commit, _)) =
   787             let
   790             let
   788               val name = nickname_of th
   791               val name = nickname_of th
   789               val (n, reps) =
   792               val (n, reps) =
   790                 case deps_of th of
   793                 case deps_of status th of
   791                   SOME deps => (n + 1, (name, deps) :: reps)
   794                   SOME deps => (n + 1, (name, deps) :: reps)
   792                 | NONE => (n, reps)
   795                 | NONE => (n, reps)
   793               val (reps, next_commit) =
   796               val (reps, next_commit) =
   794                 if Time.> (Timer.checkRealTimer timer, next_commit) then
   797                 if Time.> (Timer.checkRealTimer timer, next_commit) then
   795                   (commit false [] reps; ([], next_commit_time ()))
   798                   (commit false [] reps; ([], next_commit_time ()))